BRÁZDIL, Tomáš, Vojtěch FOREJT, Jan KŘETÍNSKÝ a 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. s. 391-402, 10 s. ISBN 978-0-7695-3183-0.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název The Satisfiability Problem for Probabilistic CTL
Název česky Problém splnitelnosti pro pravděpodobnostní CTL
Autoři BRÁZDIL, Tomáš (203 Česká republika), Vojtěch FOREJT (203 Česká republika), Jan KŘETÍNSKÝ (203 Česká republika) a Antonín KUČERA (203 Česká republika, garant).
Vydání Los Alamitos, California, 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings, od s. 391-402, 10 s. 2008.
Nakladatel IEEE Computer Society
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy americké
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/08:00026224
Organizační jednotka Fakulta informatiky
ISBN 978-0-7695-3183-0
UT WoS 000258728700033
Klíčová slova anglicky Stochastic systems; branching-time temporal logics
Štítky best, branching-time temporal logics, stochastic systems
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 22. 5. 2009 15:16.
Anotace
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.
Anotace česky
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.
Návaznosti
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 23. 10. 2019 07:17