Markov Chains and Unambiguous Büchi Automata

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-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 languageEnglish
Title of host publicationComputer Aided Verification
EditorsSwarat Chaudhuri, Azadeh Farzan
PublisherSpringer, Berlin [u. a.]
Pages23-42
Number of pages20
ISBN (print)978-3-319-41527-7
Publication statusPublished - 2016
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 9779
ISSN0302-9743

Conference

Title28th International Conference on Computer Aided Verification
Abbreviated titleCAV 2016
Conference number
Duration17 - 23 July 2016
Degree of recognitionInternational event
Location
CityToronto
CountryCanada

External IDs

ORCID /0000-0002-5321-9343/work/142236727
Scopus 84978818963

Keywords

Keywords

  • Markov Chains and Unambiguous Büchi Automata

Library keywords