A near-linear-time algorithm for weak bisimilarity on Markov chains

Autor:	Jansen, David, Groote, Jan Friso, Timmers, Ferry, Yang, Pengfei, Konnov, Igor, Kovacs, Laura
Přispěvatelé:	Formal System Analysis, EAISI High Tech Systems, EAISI Foundational
Jazyk:	angličtina
Rok vydání:	2020
Předmět:	Theory of computation → Probabilistic computation Behavioural Equivalence Theory of computation → Formal languages and automata theory Software and its engineering → Formal software verification Weak Bisimulation Theory of computation → Random walks and Markov chains Markov Chain
Zdroj:	31st International Conference on Concurrency Theory (CONCUR2020), 8:1-8:20 STARTPAGE=8:1;ENDPAGE=8:20;TITLE=31st International Conference on Concurrency Theory (CONCUR2020)
Popis:	This article improves the time bound for calculating the weak/branching bisimulation minimisation quotient on state-labelled discrete-time Markov chains from O(m n) to an expected-time O(m log4 n), where n is the number of states and m the number of transitions. The algorithm in this article also can determine branching bisimulation for action-labelled fully probabilistic systems in the same time complexity. It follows the ideas of Groote et al. (ACM ToCL 2017) in combination with an efficient algorithm to handle decremental strongly connected components (Bernstein et al., STOC 2019).
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::de5d452cbdde17c3b095b7c41418d57f https://research.tue.nl/nl/publications/b61095dc-c86e-497d-9fef-8ffc97a4188f Zobrazit plný text záznamu