Polytime model checking for times probabilistic computation tree logic
type: Item
instance of: scholarly article
title: Polytime model checking for times probabilistic computation tree logic
zbMATH Open document ID: 0910.68201
author: Danièle Beauquier
author: Anatol Slissenko
published in: Acta Informatica
publication date: 1999-03-29T00:00:00Z
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.
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 68W10
zbMATH DE Number: 1186249
zbMATH Keywords: polytime algorithm
zbMATH Keywords: timed probabilistic computation tree logic
zbMATH Keywords: probabilistic transition systems
zbMATH Keywords: model checking
MaRDI profile type: Publication
full work available at URL: s002360050136
OpenAlex ID: W1999733611
DOI: 10.1007/S002360050136
description: scientific article; zbMATH DE number 1186249