A probabilistic dynamic logic
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].
- A decidable propositional dynamic logic with explicit probabilities
- A propositional dynamic logic with qualitative probabilities
- A First-Order Dynamic Probability Logic
- Probabilistic dynamic epistemic logic
- scientific article; zbMATH DE number 4016864
- Probabilistic logic
- scientific article; zbMATH DE number 2227378
- Decidability of finite probabilistic propositional dynamic logics
- A stochastic interpretation of propositional dynamic logic: expressivity
- A stochastic interpretation of propositional dynamic logic: expressivity
- A probabilistic PDL
- Concerning measures in first order calculi
- Descriptive set theory
- First-order dynamic logic
- scientific article; zbMATH DE number 3982506 (Why is no real title available?)
- scientific article; zbMATH DE number 140573 (Why is no real title available?)
- scientific article; zbMATH DE number 3562575 (Why is no real title available?)
- scientific article; zbMATH DE number 3597592 (Why is no real title available?)
- scientific article; zbMATH DE number 3248792 (Why is no real title available?)
- scientific article; zbMATH DE number 3291134 (Why is no real title available?)
- scientific article; zbMATH DE number 3321248 (Why is no real title available?)
- scientific article; zbMATH DE number 3190627 (Why is no real title available?)
- Probabilistic parallel prefix computation
- Propositional dynamic logic of regular programs
- Semantics of probabilistic programs
- Soundness and Completeness of an Axiom System for Program Verification
- Termination of Probabilistic Concurrent Program
- A probabilistic PDL
- Modeling a dynamic and uncertain world. I: Symbolic and probabilistic reasoning about change
- Reasoning about probabilistic sequential programs in a probabilistic logic
- A propositional dynamic logic with qualitative probabilities
- A dynamic hybrid logic for followership
- Reasoning about probabilistic sequential programs
- scientific article; zbMATH DE number 1696513 (Why is no real title available?)
- Extending propositional dynamic logic for Petri nets
- Reasoning About States of Probabilistic Sequential Programs
- A decidable propositional dynamic logic with explicit probabilities
- scientific article; zbMATH DE number 1556014 (Why is no real title available?)
- Stochastic differential dynamic logic for stochastic hybrid programs
- Probabilistic logic over paths
- Partial correctness for probabilistic demonic programs
- VPHL: a verified partial-correctness logic for probabilistic programs
- A dynamic logic with branching modalities
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
- On lexicographic proof rules for probabilistic termination
- An analysis of first-order logics of probability
- Decidability of finite probabilistic propositional dynamic logics
This page was built for publication: A probabilistic dynamic logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q792757)
