Verification of Probabilistic Recursive Sequential Programs
This work studies algorithmic verification of infinite-state probabilistic systems generated by probabilistic pushdown automata (pPDA). Probabilistic pushdown automata are obtained as a probabilistic variant of pushdown automata that proved to be a successful abstract model of recursive sequential p...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2007.
|
| Témata: | |
| On-line přístup: | Elektronická verze přístupná pouze pro studenty a pracovníky MU |
| Shrnutí: | This work studies algorithmic verification of infinite-state probabilistic systems generated by probabilistic pushdown automata (pPDA). Probabilistic pushdown automata are obtained as a probabilistic variant of pushdown automata that proved to be a successful abstract model of recursive sequential programs. The main aim of this work is to study decidability and complexity of the problem whether a given probabilistic system generated by a pPDA satisfies a given property expressed in a suitable formalism. There are plenty of formalisms available for specifying properties of probabilistic systems. In this work we consider various temporal properties expressed by finite-state automata on infinite words and formulae of temporal logics, long-run average properties, and properties connected with expected behavior. Concerning temporal logics, we consider both linear and branching time ones. Among others we consider linear temporal logic (LTL) and probabilistic computation tree l. |
|---|---|
| Popis jednotky: | Vedoucí práce: Antonín Kučera. |
| Fyzický popis: | viii, 128 s. |