A probabilistic dynamic logic (Q792757): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0022-0000(84)90065-5 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1984960155 / rank | |||
Normal rank |
Revision as of 22:43, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A probabilistic dynamic logic |
scientific article |
Statements
A probabilistic dynamic logic (English)
0 references
1984
0 references
This paper defines a formal logic PrDL whose syntax derives from Pratt's first-order dynamic logic and whose semantics is an extension of Kozen's for probabilistic programs. An axiom system for PrDL is given and shown to be complete relative to an extension of first-order analysis. For discrete probabilities it is shown that first-order analysis actually suffices. Some precursors of this paper are \textit{J. H. Reif's} propositional version [12th ACM Symp. Theory of Computing, 8-13 (1980)] and \textit{L. Ramshaw's} semiformal system based on the Floyd-Hoare inductive assertion method [Ph. D. thesis (1981), Stanford University].
0 references
completeness
0 references
dynamic logic
0 references
semantics
0 references
probabilistic programs
0 references