The Satisfiability Problem for Probabilistic CTL

D 2008

The Satisfiability Problem for Probabilistic CTL

BRÁZDIL, Tomáš, Vojtěch FOREJT, Jan KŘETÍNSKÝ and Antonín KUČERA

Basic information

Original name

The Satisfiability Problem for Probabilistic CTL

Name in Czech

Problém splnitelnosti pro pravděpodobnostní CTL

Authors

BRÁZDIL, Tomáš (203 Czech Republic), Vojtěch FOREJT (203 Czech Republic), Jan KŘETÍNSKÝ (203 Czech Republic) and Antonín KUČERA (203 Czech Republic, guarantor)

Edition

Los Alamitos, California, 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings, p. 391-402, 10 pp. 2008

Publisher

IEEE Computer Society

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/08:00026224

Organization unit

Faculty of Informatics

ISBN

978-0-7695-3183-0

UT WoS

000258728700033

Keywords in English

Stochastic systems; branching-time temporal logics

Abstract

ORIG CZ

V originále

We study the satisfiability problem for qualitative PCTL (Probabilistic Computation Tree Logic), which is obtained from "ordinary" CTL by replacing the EX, AX, EU, and AU operators with their qualitative counterparts X>0, X=1, U>0, and U=1, respectively. As opposed to CTL, qualitative PCTL does not have a small model property, and there are even qualitative PCTL formulae which have only infinite-state models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is EXPTIME-complete and we give an exponential-time algorithm which for a given formula computes a finite description of a model (if it exists), or answers "not satisfiable" (otherwise). We also consider the finite satisfiability problem and provide analogous results. That is, we show that the finite satisfiability problem for qualitative PCTL is EXPTIME-complete, and every finite satisfiable formula has a model of an exponential size which can effectively be constructed in exponential time. Finally, we give some results about the quantitative PCTL, where the numerical bounds in probability constraints can be arbitrary rationals between 0 and 1. We prove that the problem whether a given quantitative PCTL formula has a model of the branching degree at most k, where k > 1 is an arbitrary but fixed constant, is highly undecidable. We also show that every satisfiable formula F has a model with branching degree at most |F| + 2. However, this does not yet imply the undecidability of the satisfiability problem for quantitative PCTL, and we in fact conjecture the opposite.

In Czech

V článku je studován problém splnitelnosti pro kvalitativní fragment logiky PCTL. Oproti nepravděpodobnostnímu CTL nemá kvalitativní fragment PCTL vlastnost malého modelu a existují dokonce formule, které mají pouze nekonečné modely. V článku je ukázáno, že problém splnitelnosti pro kvalitativní fragment PCTL je EXPTIME-úplný a je podán exponenciální algoritmus, který pro danou formuli sestrojí konečný popis modelu je-li daná formule splnitelná. Je také uvažován problém konečné splnitelnosti a jsou prezentovány analogické výsledky jako v případě splnitelnosti.

Links

MSM0021622419, plan (intention)

Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

1M0545, research and development project

Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science

Citovat

BRÁZDIL, Tomáš, Vojtěch FOREJT, Jan KŘETÍNSKÝ and Antonín KUČERA. The Satisfiability Problem for Probabilistic CTL. In 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings. Los Alamitos, California: IEEE Computer Society, 2008, p. 391-402, 10 pp. ISBN 978-0-7695-3183-0.

@inproceedings{771768,
   author = {Brázdil, Tomáš and Forejt, Vojtěch and Křetínský, Jan and Kučera, Antonín},
   address = {Los Alamitos, California},
   booktitle = {23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings},
   keywords = {Stochastic systems; branching-time temporal logics},
   language = {eng},
   location = {Los Alamitos, California},
   isbn = {978-0-7695-3183-0},
   pages = {391-402},
   publisher = {IEEE Computer Society},
   title = {The Satisfiability Problem for Probabilistic CTL},
   year = {2008}
}

TY  - JOUR
ID  - 771768
AU  - Brázdil, Tomáš - Forejt, Vojtěch - Křetínský, Jan - Kučera, Antonín
PY  - 2008
TI  - The Satisfiability Problem for Probabilistic CTL
PB  - IEEE Computer Society
CY  - Los Alamitos, California
SN  - 9780769531830
KW  - Stochastic systems
KW  - branching-time temporal logics
N2  - We study the satisfiability problem for qualitative PCTL (Probabilistic Computation Tree Logic), which is obtained from "ordinary" CTL by replacing the EX, AX, EU, and AU operators with their qualitative counterparts X>0, X=1, U>0, and U=1, respectively. As opposed to CTL, qualitative PCTL does not have a small model property, and there are even qualitative PCTL formulae which have only infinite-state models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is EXPTIME-complete and we give an exponential-time algorithm which for a given formula computes a finite description of a model (if it exists), or answers "not satisfiable" (otherwise). We also consider the finite satisfiability problem and provide analogous results. That is, we show that the finite satisfiability problem for qualitative PCTL is EXPTIME-complete, and every finite satisfiable formula has a model of an exponential size which can effectively be constructed in exponential time. Finally, we give some results about the quantitative PCTL, where the numerical bounds in probability constraints can be arbitrary rationals between 0 and 1. We prove that the problem whether a given quantitative PCTL formula has a model of the branching degree at most k, where k > 1 is an arbitrary but fixed constant, is highly undecidable. We also show that every satisfiable formula F has a model with branching degree at most |F| + 2. However, this does not yet imply the undecidability of the satisfiability problem for quantitative PCTL, and we in fact conjecture the opposite.
ER  -

BRÁZDIL, Tomáš, Vojtěch FOREJT, Jan KŘETÍNSKÝ and Antonín KUČERA. The Satisfiability Problem for Probabilistic CTL. In \textit{23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings}. Los Alamitos, California: IEEE Computer Society, 2008, p.~391-402, 10 pp. ISBN~978-0-7695-3183-0.

Detailed Information on Publication Record