Li, Yong 
ORCID: 0000-0002-7301-9234, Paul, Soumyajit ORCID: 0000-0002-7233-2018, Schewe, Sven ORCID: 0000-0002-9093-9518 and Tang, Qiyi ORCID: 0000-0002-9265-3011
(2025)
Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata.
In: Computer Aided Verification (CAV), 2025-7-21 - ?.
|
Text
UBA_Reduction-Liverpool-elements.pdf - Author Accepted Manuscript Available under License Creative Commons Attribution. Download (514kB) | Preview |
Abstract
<jats:title>Abstract</jats:title> <jats:p>Good-for-Games (GfG) automata require that their nondeterminism can be resolved on-the-fly, while unambiguous automata guarantee that no word has more than one accepting run. These two mutually exclusive ways of restricted nondeterminism play their roles independently in Markov chain model checking (MCMC) for almost a decade but synthesising them seems hopeless: an automaton that is both GfG and unambiguous is essentially deterministic. This work breaks this perception by combining the strengths of unambiguity with the GfG co-Büchi minimisation recently proposed by Abu Radi and Kupferman. More precisely, this combination allows us to turn unambiguous automata to certain types of probabilistic automata that can be used for MCMC. The resulting automata can be exponentially smaller, and we have provided a family of automata exemplifying this state space reduction, which translates into a significant acceleration of MCMC. </jats:p>
| Item Type: | Conference Item (Unspecified) |
|---|---|
| Uncontrolled Keywords: | 4613 Theory Of Computation, 46 Information and Computing Sciences |
| Divisions: | Faculty of Science and Engineering Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 02 May 2025 07:10 |
| Last Modified: | 22 Aug 2025 03:07 |
| DOI: | 10.1007/978-3-031-98679-6_13 |
| Related Websites: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3192169 |
Altmetric
Altmetric