The Satisfiability Problem for Probabilistic CTL

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Problém splnitelnosti pro pravděpodobnostní CTL
Autoři

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

Rok publikování 2008
Druh Článek ve sborníku
Konference 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova Stochastic systems; branching-time temporal logics
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.