On the Decidability of Temporal Properties of Probabilistic Pushdown Automata

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky O rozhodnutelnosti temporálních vlastností zásobníkových automatů
Autoři

BRÁZDIL Tomáš KUČERA Antonín STRAŽOVSKÝ Oldřich

Rok publikování 2005
Druh Článek ve sborníku
Konference Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova probabilistic pushdown automata; probabilistic temporal logics
Popis V článku se zkoumá rozhodnutelnost a složitost problému ověření platnosti formulí kvantitativních a kvalitativních temporálních logik pro pravděpodobnostní zásobníkové automaty. Je dokázáno, že problém ověření formulí kvalitativního resp. kvantitavního fragmentu omega-regulárních vlastností patří do třídy 2-EXPSPACE resp. 3-EXPTIME. Dále je dokázáno, že problém ověření formulí kvalitativního fragmentu logiky PECTL* resp. PCTL pro pravděpodobnostní zásobníkové automaty patří do třídy 2-EXPSPACE resp. EXPSPACE. Přitom pro kvalitativní fragment PCTL je podán rovněž EXPTIME dolní složitostní odhad, který platí také pro pravděpodobnostní zásobníkové automaty s jediným kontrolním stavem. Konečně je prokázána nerozhodnutelnost problému ověření platnosti obecných formulí logiky PCTL pro pravděpodobnostní zásobníkové automaty.
Související projekty:

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