Model Checking Markov Chains Against Unambiguous Buchi Automata
Michael Benedikt, Rastislav Lenhardt, James Worrell
TL;DR
This paper presents a polynomial-time algorithm for verifying finite Markov chains against omega-regular properties expressed through unambiguous Buchi automata, improving efficiency in probabilistic model checking.
Contribution
The paper introduces a novel polynomial-time algorithm for model checking Markov chains with unambiguous Buchi automata, enhancing existing verification techniques.
Findings
Algorithm operates in polynomial time
Efficient verification of omega-regular properties
Applicable to finite Markov chains
Abstract
We give a polynomial-time algorithm for model checking finite Markov chains against omega-regular specifications given as unambiguous Buchi automata.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · DNA and Biological Computing