A probabilistic PDL (Q1063584)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A probabilistic PDL |
scientific article; zbMATH DE number 3918337
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A probabilistic PDL |
scientific article; zbMATH DE number 3918337 |
Statements
A probabilistic PDL (English)
0 references
1985
0 references
The paper gives a probabilistic analog of propositional dynamic logic (PDL), so called PPDL, in order to analyze the properties of probabilistic programs (in the same sense in which PDL intends for the analysis of standard ones). The main result is a ''small model property'' of PPDL stating roughly that if a PPDL formula F has a model, it has small finite ones. Then a polynomial-space algorithm is proposed deciding upon validity of formulas involving ''well-structured'' probabilistic programs. The last part illustrates the usage of some proposed deductive calculus (for PPDL) in an example of simple random walk.
0 references
analysis of probabilistic algorithms
0 references
probabilistic analog of propositional dynamic logic
0 references
probabilistic programs
0 references
small model property
0 references
deductive calculus
0 references
