×

zbMATH — the first resource for mathematics

A decidable propositional dynamic logic with explicit probabilities. (English) Zbl 0592.68031
Summary: A propositional version of Y. A. Feldman and D. Harel’s PrDL [J. Comput. Syst. Sci. 28, 193-215 (1984; Zbl 0537.68036)] is defined, and shown to be decidable in double-exponential space. The logic allows propositional-level formulas involving probabilistic programs, and contains the full (quantified) real-number theory for dealing with probabilities. The decidability proof introduces a succession of abstractions of the notion of a model, from the full generality of measure theoretical models, down to the finite schematic models, which seem to be the most basic structures relating programs and probabilities.

MSC:
68Q65 Abstract data types; algebraic specification
03B25 Decidability of theories and sets of sentences
68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)
PDF BibTeX XML Cite
Full Text: DOI