Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata

2015/02/26 by Lin, T.
#F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Languages and Automata Theory (cs.FL) #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1502.07549

Abstract

This paper studies the problem of model-checking of probabilistic automaton and probabilistic one-counter automata against probabilistic branching-time temporal logics (PCTL and PCTL^*). We show that it is undecidable for these problems. We first show, by reducing to emptiness problem of probabilistic automata, that the model-checking of probabilistic finite automata against branching-time temporal logics are undecidable. And then, for each probabilistic automata, by constructing a probabilistic one-counter automaton with the same behavior as questioned probabilistic automata the undecidability of model-checking problems against branching-time temporal logics are derived, herein.

Related

• An automata-theoretic approach to branching-time model checking
• Model Checking Probabilistic Operator Precedence Automata
• Linear-Time Model Checking Branching Processes
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
• Model Checking Algorithms for Markov Automata