Decidability of finite probabilistic propositional dynamic logics
In finite Probabilistic Propositional Dynamic Logic (PPDL) language, the basic dynamic construct is \(<\alpha >\lambda \phi\), interpreted as follows: the probability that the program \(\alpha\) will terminate in a state satisfying the formula \(\phi\) is \(\lambda\). The present paper considers three basic versions of PPDL: (1) Deterministic PPDL (DPPDL), where programs \(\alpha\) are only deterministic regular expressions, Boolean combinations of propositional variables \(\phi\) are allowed, and for estimating \(\lambda\), first-order formulas of real closed fields can be used; (2) Rational PPDL \((PPDL>r)\), where \(\lambda\) is greater than a rational constant r; (3) Positive PPDL \((PPDL>0)\), like \(PPDL>r\), for \(r=0\). Clearly, probabilistic estimations of (3) are a special case of (2), and those of (2) are a special case of (1). The present paper considers some natural variation and extension properties for them. Section 2 gives the basic formal definitions and the results concerning the (un)decidability of different PPDLs. In Section 3 there is proved that \(PPDL>0\) is reducible to standard Propositional Dynamic Logic (PDL), reminding a similar result for the extension \(PDL+GA\) (programs with global assignments). Section 4 proves that all PPDLs without nesting of probability estimations have the finite model property. The proof idea is to use the fact that a regular program is a limit of finite programs. Section 5 considers some DPPDL extensions and decidability results for them. In Section 6 undecidability results for \(PPDL>r\) are analysed, while the Appendix contains the undecidability proof for D. Kozen's PPDL that allows Boolean combinations of inequalities.
- A decidable propositional dynamic logic with explicit probabilities
- Probabilization of logics: completeness and decidability
- Discrete Linear-time Probabilistic Logics: Completeness, Decidability and Complexity
- A probabilistic dynamic logic
- Decidability and expressiveness for first-order logics of probability
- Decision complexity of variants of propositional dynamic logic
- A Logic of Probability with Decidable Model Checking
- A propositional dynamic logic with qualitative probabilities
- scientific article; zbMATH DE number 1948170
- A stochastic interpretation of propositional dynamic logic: expressivity
- A decidable propositional dynamic logic with explicit probabilities
- A practical decision method for propositional dynamic logic (preliminary report)
- A probabilistic dynamic logic
- A probabilistic PDL
- Decidability of finite probabilistic propositional dynamic logics
- Expressing program looping in regular dynamic logic
- First-order dynamic logic
- scientific article; zbMATH DE number 3145626 (Why is no real title available?)
- scientific article; zbMATH DE number 3890702 (Why is no real title available?)
- scientific article; zbMATH DE number 3371972 (Why is no real title available?)
- scientific article; zbMATH DE number 3194838 (Why is no real title available?)
- Propositional dynamic logic of regular programs
- Propositional dynamic logic with local assignments
- Semantics of probabilistic programs
- Verification of Probabilistic Programs
- A probabilistic PDL
- Concurrent program schemes and their logics
- Reasoning about probabilistic sequential programs
- Extending propositional dynamic logic for Petri nets
- A stochastic interpretation of propositional dynamic logic: expressivity
- A decidable propositional dynamic logic with explicit probabilities
- scientific article; zbMATH DE number 465528 (Why is no real title available?)
- Complexity Results for Probabilistic Datalog
- scientific article; zbMATH DE number 7713505 (Why is no real title available?)
- My writing
- A probabilistic dynamic logic
- Decidability of finite probabilistic propositional dynamic logics
This page was built for publication: Decidability of finite probabilistic propositional dynamic logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q809069)
