| Identifikační kód |
RIV/00216224:14330/05:00012349 |
| Název v anglickém jazyce |
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata |
| Druh |
D - Stať ve sborníku |
| Jazyk |
eng - angličtina |
| Obor - skupina |
I - Informatika |
| Obor |
IN - Informatika |
| Rok uplatnění |
2005 |
| Kód důvěrnosti údajů |
S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku |
6 |
| Počet tvůrců celkem |
3 |
| Počet domácích tvůrců |
3 |
| Výčet všech uvedených jednotlivých tvůrců |
Tomáš Brázdil (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1762834)
Antonín Kučera (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9872655)
Oldřich Stražovský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9797092) |
| Popis výsledku v anglickém jazyce |
We consider qualitative and quantitative model-checking problems for probabilistic pushdown automata (pPDA) and various temporal logics. We prove that the qualitative and quantitative model-checking problem for omega-regular properties and pPDA is in 2-EXPSPACE and 3-EXPTIME, respectively. We also prove that model-checking the qualitative fragment of the logic PECTL* for pPDA is in 2-EXPSPACE, and model-checking the qualitative fragment of PCTL for pPDA is in EXPSPACE. Furthermore, model-checking the qualitative fragment of PCTL is shown to be EXPTIME-hard even for stateless pPDA. Finally, we show that PCTL model-checking is undecidable for pPDA, and PCTL+ model-checking is undecidable even for stateless pPDA. |
| Klíčová slova oddělená středníkem |
probabilistic pushdown automata; probabilistic temporal logics |
| Stránka www, na které se nachází výsledek |
- |
| Odkaz na údaje z výzkumu |
- |