Markov Chains and Unambiguous Büchi Automata
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
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
| Originalsprache | Englisch |
|---|---|
| Titel | Computer Aided Verification |
| Redakteure/-innen | Swarat Chaudhuri, Azadeh Farzan |
| Herausgeber (Verlag) | Springer, Berlin [u. a.] |
| Seiten | 23-42 |
| Seitenumfang | 20 |
| ISBN (Print) | 978-3-319-41527-7 |
| Publikationsstatus | Veröffentlicht - 2016 |
| Peer-Review-Status | Ja |
Publikationsreihe
| Reihe | Lecture Notes in Computer Science, Volume 9779 |
|---|---|
| ISSN | 0302-9743 |
Konferenz
| Titel | 28th International Conference on Computer Aided Verification |
|---|---|
| Kurztitel | CAV 2016 |
| Veranstaltungsnummer | |
| Dauer | 17 - 23 Juli 2016 |
| Bekanntheitsgrad | Internationale Veranstaltung |
| Ort | |
| Stadt | Toronto |
| Land | Kanada |
Externe IDs
| ORCID | /0000-0002-5321-9343/work/142236727 |
|---|---|
| Scopus | 84978818963 |
| ORCID | /0000-0003-1724-2586/work/165453595 |
Schlagworte
Schlagwörter
- Markov Chains and Unambiguous Büchi Automata