Polytime model checking for times probabilistic computation tree logic

DOI10.1007/S002360050136MaRDI QIDQ1127817zbMATH OpenOpenAlexFDO

Authors Danièle Beauquier, Anatol Slissenko

Publication date 29 March 1999

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s002360050136

zbMATH Keywords

model checkingpolytime algorithmprobabilistic transition systemstimed probabilistic computation tree logic

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Logic in artificial intelligence (68T27) Parallel algorithms in computer science (68W10)

Review text

We consider the model checking problem for timed probabilistic computation tree logic (TPCTL) introduced by H. A. Hansson and D. Jonsson, and studied in a recent book by \textit{H. A. Hansson} ``Time and probability in formal design of distributed systems (Elsevier, 1994). The semantics of TPCTL is defined in terms of probabilistic transition systems. It is shown in this book that model checking for TPCTL has exponential time complexity, the latter being measured in terms of the size of formula, the size of transition system and the value of explicit time that appears in the formula. Besides that, some polytime decidable classes are described in the cited book, the proofs being rather voluminous. We show, by a short proof, that this model checking problem is polytime decidable in the general case. The proof is essentially based on results on the complexity of Markov decision processes.

Recommendations

• A decidable probability logic for timed probabilistic systems
• On probabilistic timed automata.
• Model checking of probabilistic and nondeterministic systems
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Model Checking Probabilistic Timed Automata with One or Two Clocks

Cited in

(4)

• A survey on temporal logics for specifying and verifying real-time systems
• scientific article; zbMATH DE number 7280017 (Why is no real title available?)
• Model checking for a class of weighted automata
• Probabilistic and prioritized models of timed CSP

This page was built for publication: Polytime model checking for times probabilistic computation tree logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1127817)