On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
| Název česky | O rozhodnutelnosti temporálních vlastností zásobníkových automatů |
|---|---|
| Autoři | |
| 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 | |
| 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: |