Article

Free access

A probabilistic PDL

Author:

Dexter KozenAuthors Info & Claims

STOC '83: Proceedings of the fifteenth annual ACM symposium on Theory of computing

Pages 291 - 297

https://doi.org/10.1145/800061.808758

Published: 01 December 1983 Publication History

PDF eReader

Abstract

In this paper we give a probabilistic analog PPDL of Propositional Dynamic Logic. We prove a small model property and give a polynomial space decision procedure for formulas involving well-structured programs. We also give a deductive calculus and illustrate its use by calculating the expected running time of a simple random walk program.

References

[1]

Feldman, Y.A., "A Decidable Propositional Probabilistic Dynamic Logic," this proceedings.

Google Scholar

[2]

Feldman, Y.A, and D. Harel, "A Probabilistic Dynamic Logic," 14th Symp. on Theory of Computing, 1982, p. 181.

Digital Library

Google Scholar

[3]

Fischer, M.J. and R.E.Ladner, "Propositional Dynamic Logic of Regular Programs," J. Comput. Syst. Sci. 18:2 (1979).

Crossref

Google Scholar

[4]

Halpern and Reif, "Propositional Dynamic Logic of Deterministic, Well-structured Programs," 22nd Symp. on Foundations of Computer Science, 1981, p. 322.

Google Scholar

[5]

Kozen, D., "Semantics of Probabilistic Programs," JCSS 22 (1981), p. 328.

Crossref

Google Scholar

[6]

Lehmann, D., and S. Shelah, "Reasoning with Time and Chance," manuscript, Oct. 1982.

Google Scholar

[7]

Makowsky, J.A. and M.L. Tiomkin, "Probabilistic Propositional Dynamic Logic," manuscript.

Google Scholar

[8]

Parikh, R. and A. Mahoney, "A Theory of Probabilistic Programs," manuscript.

Google Scholar

[9]

Pnueli, A., "On the Extremely Fair Treatment of Probabilistic Algorithms," manuscript, Nov. 1982.

Google Scholar

[10]

Ramshaw, L., Formalizing the Analysis of Algorithms, Ph.D thesis, Stanford, 1980.

Digital Library

Google Scholar

[11]

Reif, J., "Logics for Probabilistic Programming," 12th Symp. on Theory of Computing, 1980.

Digital Library

Google Scholar

[12]

Revuz, D., Markov chains, North-Holland, 1975.

Google Scholar

[13]

Schaefer, H.H., Topological Vector Spaces, Springer-Verlag Graduate Texts in Mathematics 3, 1971.

Google Scholar

[14]

Sharir, Pnueli, and Hart, "Probabilistic Verification of Programs: I. Correctness Analysis of Sequential Programs," manuscript, Dec. 1981.

Google Scholar

Cited By

View all

Batz KBiskup TKatoen JWinkler T(2024)Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36329358:POPL(2792-2820)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632935
Müllner JMoosbrugger MKovács L(2024)Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) ProgramsProceedings of the ACM on Programming Languages10.1145/36328728:POPL(882-910)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632872
Gladyshev MAlechina NDastani MDoder D(2024)Reasoning About Group Responsibility for Exceeding Risk Threshold in One-Shot GamesInformation and Computation10.1016/j.ic.2024.105257(105257)Online publication date: Nov-2024
https://doi.org/10.1016/j.ic.2024.105257
Show More Cited By

Index Terms

A probabilistic PDL
1. Theory of computation

Recommendations

Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Bisimilar and Logically Equivalent Programs in PDL

In standard Propositional Dynamic Logic (PDL) literature [D. Harel and D. Kozen and J. Tiuryn. Dynamic Logics. MIT Press, 2000; R. Goldblatt. Logics of Time and Computation. CSLI Lecture Notes 7. Stanford, 1992; P. Blackburn, M. de Rijke, and Y. Venema. ...
A Reduction from DLP to PDL

We present a reduction from a new logic extending van der Meyden's dynamic logic of permission (DLP) into propositional dynamic logic (PDL), providing a 2 EXPTIME decision procedure and showing that all the machinery for PDL can be reused for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

STOC '83: Proceedings of the fifteenth annual ACM symposium on Theory of computing

December 1983

487 pages

ISBN:0897910990

DOI:10.1145/800061

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 December 1983

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 1,469 of 4,586 submissions, 32%

Upcoming Conference

STOC '25

Sponsor:
sigact

57th Annual ACM Symposium on Theory of Computing (STOC 2025)

June 23 - 27, 2025

Prague , Czech Republic

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

75
Total Citations
View Citations
186
Total Downloads

Downloads (Last 12 months)70
Downloads (Last 6 weeks)9

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Batz KBiskup TKatoen JWinkler T(2024)Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36329358:POPL(2792-2820)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632935
Müllner JMoosbrugger MKovács L(2024)Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) ProgramsProceedings of the ACM on Programming Languages10.1145/36328728:POPL(882-910)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632872
Gladyshev MAlechina NDastani MDoder D(2024)Reasoning About Group Responsibility for Exceeding Risk Threshold in One-Shot GamesInformation and Computation10.1016/j.ic.2024.105257(105257)Online publication date: Nov-2024
https://doi.org/10.1016/j.ic.2024.105257
Wu HCui ADeng Y(2024)An Assertion-Based Logic for Local Reasoning about Probabilistic ProgramsDependable Software Engineering. Theories, Tools, and Applications10.1007/978-981-96-0602-3_2(25-45)Online publication date: 25-Nov-2024
https://doi.org/10.1007/978-981-96-0602-3_2
Chen CMcIver AMorgan C(2024)Source-Level Reasoning for Quantifying Information LeaksPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_5(98-127)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_5
Batz KKaminski BMatheja CWinkler T(2024)J-P: MDP. FP. PPPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_11(255-302)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_11
Schröer PBatz KKaminski BKatoen JMatheja C(2023)A Deductive Verification Infrastructure for Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36228707:OOPSLA2(2052-2082)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622870
Li JAhmed AHoltzen S(2023)Lilac: A Modal Separation Logic for Conditional ProbabilityProceedings of the ACM on Programming Languages10.1145/35912267:PLDI(148-171)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591226
Feng SChen MSu HKaminski BKatoen JZhan N(2023)Lower Bounds for Possibly Divergent Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/35860517:OOPSLA1(696-726)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586051
Zilberstein NDreyer DSilva A(2023)Outcome Logic: A Unifying Foundation for Correctness and Incorrectness ReasoningProceedings of the ACM on Programming Languages10.1145/35860457:OOPSLA1(522-550)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586045
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Completeness and decidability of converse PDL in the constructive type theory of Coq

Bisimilar and Logically Equivalent Programs in PDL

A Reduction from DLP to PDL

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations