The Satisfiability Problem for Probabilistic CTL

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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:	Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy