Model Checking Markov Chains Against Unambiguous Buchi Automata
Logic in Computer Science
2016-03-29 v2 Formal Languages and Automata Theory
Abstract
We give a polynomial-time algorithm for model checking finite Markov chains against omega-regular specifications given as unambiguous Buchi automata.
Cite
@article{arxiv.1405.4560,
title = {Model Checking Markov Chains Against Unambiguous Buchi Automata},
author = {Michael Benedikt and Rastislav Lenhardt and James Worrell},
journal= {arXiv preprint arXiv:1405.4560},
year = {2016}
}
Related papers
View all related →
Logic in Computer Science · Computer Science
Markov Chains and Unambiguous Automata
Christel Baier, Stefan Kiefer, Joachim Klein, David Müller +1
2023-04-10
Formal Languages and Automata Theory · Computer Science
Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques
Stefan Kiefer, Cas Widdershoven
2024-09-17
Logic in Computer Science · Computer Science
Fast detection of cycles in timed automata
Aakash Deshpande, Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran +1
2014-10-17
Computational Complexity · Computer Science
General Algorithms for Testing the Ambiguity of Finite Automata
Cyril Allauzen, Mehryar Mohri, Ashish Rastogi
2008-02-25
Logic in Computer Science · Computer Science
Certificates and Witnesses for Multi-objective {\omega}-regular Queries in Markov Decision Processes
Christel Baier, Calvin Chau, Volodymyr Drobitko, Simon Jantsch +1
2025-08-26
Logic in Computer Science · Computer Science
Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata
T. Lin
2023-07-19
Logic in Computer Science · Computer Science
Faster Statistical Model Checking for Unbounded Temporal Properties
Przemysław Daca, Thomas A. Henzinger, Jan Křetínský, Tatjana Petrov
2016-03-04
Logic in Computer Science · Computer Science
Liveness of Parameterized Timed Networks
Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger
2016-09-15
Quantum Physics · Physics
Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
Lvzhou Li, Yuan Feng
2015-07-01
Logic in Computer Science · Computer Science
Antichains for the Automata-Based Approach to Model-Checking
Laurent Doyen, Jean-Francois Raskin
2015-07-01
Logic in Computer Science · Computer Science
Lazy Probabilistic Model Checking without Determinisation
Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini +1
2015-04-27
Logic in Computer Science · Computer Science
Model Checking Probabilistic Timed Automata with One or Two Clocks
Marcin Jurdzinski, Francois Laroussinie, Jeremy Sproston
2019-03-14
Logic in Computer Science · Computer Science
Are Parametric Markov Chains Monotonic?
Jip Spel, Sebastian Junges, Joost-Pieter Katoen
2019-07-22
Computation · Statistics
Unbiased Markov chain Monte Carlo for intractable target distributions
Lawrence Middleton, George Deligiannidis, Arnaud Doucet, Pierre E. Jacob
2020-06-17
Signal Processing · Electrical Eng. & Systems
Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems
Maxence Dutreix, Samuel Coogan
2020-01-31
Logic in Computer Science · Computer Science
Compositional Verification and Optimization of Interactive Markov Chains
Holger Hermanns, Jan Krčál, Jan Křetínský
2013-12-05
Logic in Computer Science · Computer Science
Probabilistic Model Checking and Autonomy
Marta Kwiatkowska, Gethin Norman, David Parker
2021-11-23
Formal Languages and Automata Theory · Computer Science
Layered automata: A canonical model for automata over infinite words
Antonio Casares, Christof Löding, Igor Walukiewicz
2026-01-23
Formal Languages and Automata Theory · Computer Science
Constructing Concise Characteristic Samples for Acceptors of Omega Regular Languages
Dana Angluin, Dana Fisman
2024-11-13
Machine Learning · Computer Science
Formal Verification of Markov Processes with Learned Parameters
Muhammad Maaz, Timothy C. Y. Chan
2025-05-13
Machine Learning · Computer Science
Learning Markov Decision Processes for Model Checking
Hua Mao, Yingke Chen, Manfred Jaeger, Thomas D. Nielsen +2
2012-12-18
Theoretical Economics · Economics
On the Computational Properties of Obviously Strategy-Proof Mechanisms
Louis Golowich, Shengwu Li
2022-10-25
Formal Languages and Automata Theory · Computer Science
Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
Hongfei Fu, Yi Li, Jianlin Li, Lijun Zhang
2018-06-14
Logic in Computer Science · Computer Science
Probabilistic Model Checking for Continuous Time Markov Chains via Sequential Bayesian Inference
Dimitrios Milios, Guido Sanguinetti, David Schnoerr
2018-06-12
Logic in Computer Science · Computer Science
Multi-Objective Model Checking of Markov Decision Processes
Kousha Etessami, Marta Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis
2015-07-01