The Satisfiability Problem for Probabilistic CTL
| Název česky | Problém splnitelnosti pro pravděpodobnostní CTL |
|---|---|
| Autoři | |
| 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 | |
| Citace | 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. |
| 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: |