Markov Chains and Unambiguous Büchi Automata
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
Unambiguous automata, i.e., nondeterministic automata with the restriction of having at most one accepting run over a word, have the potential to be used instead of deterministic automata in settings where nondeterministic automata can not be applied in general. In this paper, we provide a polynomially time-bounded algorithm for probabilistic model checking of discrete-time Markov chains against unambiguous Büchi automata specifications and report on our implementation and experiments.
Details
Original language | English |
---|---|
Title of host publication | Computer Aided Verification |
Editors | Swarat Chaudhuri, Azadeh Farzan |
Publisher | Springer, Berlin [u. a.] |
Pages | 23-42 |
Number of pages | 20 |
ISBN (print) | 978-3-319-41527-7 |
Publication status | Published - 2016 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 9779 |
---|---|
ISSN | 0302-9743 |
Conference
Title | 28th International Conference on Computer Aided Verification |
---|---|
Abbreviated title | CAV 2016 |
Conference number | |
Duration | 17 - 23 July 2016 |
Degree of recognition | International event |
Location | |
City | Toronto |
Country | Canada |
External IDs
ORCID | /0000-0002-5321-9343/work/142236727 |
---|---|
Scopus | 84978818963 |
ORCID | /0000-0003-1724-2586/work/165453595 |
Keywords
Keywords
- Markov Chains and Unambiguous Büchi Automata