Markov Chains and Unambiguous Büchi Automata

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelComputer Aided Verification
Redakteure/-innenSwarat Chaudhuri, Azadeh Farzan
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten23-42
Seitenumfang20
ISBN (Print)978-3-319-41527-7
PublikationsstatusVeröffentlicht - 2016
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 9779
ISSN0302-9743

Konferenz

Titel28th International Conference on Computer Aided Verification
KurztitelCAV 2016
Veranstaltungsnummer
Dauer17 - 23 Juli 2016
BekanntheitsgradInternationale Veranstaltung
Ort
StadtToronto
LandKanada

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

Bibliotheksschlagworte