Conference item
Markov chains and unambiguous Büchi automata
- 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 Buchi automata specifications and report on our implementation and experiments.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 515.1KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-319-41528-4_2
Authors
+ Engineering and Physical Sciences Research Council
More from this funder
- Funding agency for:
- Worrell, J
- Grant:
- EP/M012298/1
- Publisher:
- Springer, Cham
- Host title:
- CAV 2016: Computer Aided Verification
- Journal:
- Lecture Notes in Computer Science More from this journal
- Volume:
- 9779
- Pages:
- 23-42
- Series:
- Lecture Notes in Computer Science
- Publication date:
- 2016-07-13
- Acceptance date:
- 2016-04-25
- DOI:
- ISSN:
-
0302-9743
- ISBN:
- 9783319415277
- Keywords:
- Pubs id:
-
pubs:623539
- UUID:
-
uuid:77f47690-52a3-4b1b-8a45-3cb69e3cbe75
- Local pid:
-
pubs:623539
- Source identifiers:
-
623539
- Deposit date:
-
2016-08-11
- ARK identifier:
Terms of use
- Copyright holder:
- Springer International Publishing Switzerland
- Copyright date:
- 2016
- Notes:
- Copyright © Springer International Publishing Switzerland 2016. This is the accepted manuscript version of the paper. The final version is available online from Springer at: https://doi.org/10.1007/978-3-319-41528-4_2
If you are the owner of this record, you can report an update to it here: Report update to this record