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.

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)
Full Text: DOI