article

Free access

Concurrent dynamic logic

Author:

David PelegAuthors Info & Claims

Journal of the ACM (JACM), Volume 34, Issue 2

Pages 450 - 479

https://doi.org/10.1145/23005.23008

Published: 01 April 1987 Publication History

PDF eReader

Abstract

In this paper concurrent dynamic logic (CDL) is introduced as an extension of dynamic logic tailored toward handling concurrent programs. Properties of CDL are discussed, both on the propositional and first-order level, and the extension is shown to possess most of the desirable properties of DL. Its relationships with the μ-calculus, game logic, DL with recursive procedures, and PTIME are further explored, revealing natural connections between concurrency, recursion, and alternation.

References

[1]

CHANDRA, A.K. The power of parallelism anO nonaetermlnlsm m programming, in rroceeamgs oflFIP '74. North-Holland, Amsterdam, Holland, 1974, pp. 461-465.

Google Scholar

[2]

CHANDRA, A. K., KOZEN, D. C., AND STOCKMEYER, L.J. Alternation. J. ACM 28, 1 (Jan. 1981), 114-133.

Crossref

Google Scholar

[3]

CLOCt:SlN, W. F., AND MELLISrt, C.S. Programming in Prolog, Springer-Vedag, New York, 1981.

Crossref

Google Scholar

[4]

Coot:, S.A. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, I (1978), 70-90.

Google Scholar

[5]

FISCHEI~, M. J., AND LADNER, R.E. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18 (1979), 194-211.

Google Scholar

[6]

HAREL, D. First Order Dynamic Logic. In Lecture Notes in Computer Science, vol. 68. Spdnger- Verlag, New York, 1979.

Crossref

Google Scholar

[7]

HAREL, D. And/Or programs: A new approach to structured programming. ACM Trans. Prog. Lang. and Syst. 2, 1 (Jan. 1980), 1-17.

Crossref

Google Scholar

[8]

HAREL, D. Dynamic Logic. In Handbook of Philosophical Logic, vol. lI. Reidel Publishing, Holland, 1984, pp. 497-604.

Google Scholar

[9]

HAREL, D., AND KOZEN, D.C. A programming language for the inductive sets, and applications. Inf. Control 63 (1985), 118-139.

Crossref

Google Scholar

[10]

HAREL, D., AND PELEG, D. On static logics, dynamic logics and complexity classes. Inf. Control 60 (1984), 86-102.

Google Scholar

[11]

HAREL, D., AND PELEG, D. Process logic with regular formulas. Theoret. Comput. Sci. 38 (1985), 307-322.

Google Scholar

[12]

HAREL, D., AND PFL~G, D. More on looping vs. repeating in dynamic logic. Inf. Proc. Lett. 20 (1985), 87-90.

Crossref

Google Scholar

[13]

HAREL, D., KOZEN, D. C., AND PARIKH, R. PrOCeSS logic: Expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25 (1982), 144-170.

Google Scholar

[14]

HAREL, D., MEYER, A. R., AND PRATT, V. R. Computability and completeness in logics of programs. In Proceedings of the 9th A CM Symposium on Theory of Computing (Boulder, Colo., May 2-4). ACM, New York, 1977, pp. 261-268.

Crossref

Google Scholar

[15]

HITCHCOCK, P., AND PARK, D. M. R. Induction rules and termination proofs. In Automata, Languages and Programming, M. Nivat, Ed. North-Holland, Amsterdam, 1973, pp. 253-263.

Google Scholar

[16]

IMMERMAN, N. Relational queries computable in polynomial time. In Proceedings of the 14th ACM Symposium on Theory of Computing (San Francisco, Calif., May 5-7). ACM, New York, 1982, pp. 147-152.

Crossref

Google Scholar

[17]

I~ISLER, J. Model Theory for lnfinitary Logic. North-Holland, Amsterdam, 197 I.

Google Scholar

[18]

KOWALSKI, R. Logic for Problem Solving. The Computer Science Library, Artificial Intelligence Series, North-Holland, Amsterdam, 1983.

Crossref

Google Scholar

[19]

KOZEN, D.C. Results on the propositional t~-calculus. In Proceedings "of the 9th ICALP. Lecture Notes in Computer Science, vol. 140. Springer-Vedag, New York, 1982, pp. 348-359.

Crossref

Google Scholar

[20]

MANNA, Z. The correctness of nondeterministic programs. Artif. Intell. 1 (I 970), 1-26.

Google Scholar

[21]

MIRKOWSKA, G. On formalized systems of algorithmic logic. Bull. Acad. Polon. Sci., Set. Sci. Math. Astron. Phys. 19 (1971), 421-428.

Google Scholar

[22]

MEYER, A. R., AND HALPERN, J.Y. Axiomatic definitions of programming languages: A theoretical assessment. J. ACM 29, 2 (Apr. 1982), 555-576.

Crossref

Google Scholar

[23]

MWYER, A. R., ANt) PARIKH, R. Definability in dynamic logic. J. Comput. Syst. Sci., 23 (1981), 279-298.

Google Scholar

[24]

NISHIMURA, H. Descriptively complete process logic. Acta Inf. 14 (1980), 359-369.

Google Scholar

[25]

NlSmMURA, H. Arithmetical completeness in first-order dynamic logic for concurrent programs. Publ. RIMS, Kyoto Univ. 17 ( 1981), 297-309.

Google Scholar

[26]

PARmH, R. A decidability result for second order process logic. In Proceedings of the 19th IEEE Symposium on Foundations of Computing Science. IEEE, New York, 1978, pp. 178-183.

Google Scholar

[27]

PARIKH, R. Propositional logics of programs: New directions. In Proceedings of the Conference on Foundations of Computer Theory (Borgholm, Sweden). Lecture Notes in Computer Sciences, vol. 158. Springer-Verlag, New York, 1983, pp. 347-359.

Crossref

Google Scholar

[28]

PARIKH, R. The logic of games and its applications. Ann. Disc. Math. 24 (1985), 111-140.

Google Scholar

[29]

PARK, D. M.R. Finiteness is mu-ineffable. Theor. Comput. Sci. 3 (1976), 173-181.

Google Scholar

[30]

PELEG, D. Communication in concurrent dynamic logic. J. Comput. Syst. Sci. (1987), in press.

Crossref

Google Scholar

[31]

PELEG, D. Concurrent program schemes and their logics, Tech. Rep. CS84-25. The Weizmann{ Institute of Science, Rehovot, Israel, Nov. 1984.

Google Scholar

[32]

PNUELI, A. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1977, pp. 46-57.

Google Scholar

[33]

PRATT, V. R. Models of program logics. In Proceedings of the 20th IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1979, pp. 115-122.

Google Scholar

[34]

PRATt, V. R. A Decidable #-calculus (Preliminary Report). In Proceedings of the 22th IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1981, pp. 421-427.

Google Scholar

[35]

SHAPIRO, E. Y. Alternation and the computational complexity of logic programs. Tech. Rep. CS84-06. The Weizmann Institute of Science, Rehovot, Israel.

Google Scholar

[36]

SHERMAN, R., AND HAREL, D. A combined proofofone-exponential decidability and completeness for PDL, manuscript. The Weizmann Institute of Science, Rehovot, Israel.

Google Scholar

[37]

TARSKI, A. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. S (1955), 285-309.

Google Scholar

[38]

TIURYN, J. Unbounded program memory adds to the expressive power of first-order dynamic logic. In Proceedings of the 22nd IEEE Symposium on Foundation of Computer Science. IEEE, New York, 1981, pp. 335-339.

Google Scholar

[39]

URZYCZYN, P. "During" cannot be expressed by "after." J. Comput. Syst. Sci., 32 (1986), 97-104.

Crossref

Google Scholar

[40]

VARDI, M.Y. The complexity of relational query languagesl in Proceedings of the 14th ACM Symposium on Theory of Computing (San Francisco, Calif., May 5-7). ACM, New York, 1982, pp. 137-146.

Crossref

Google Scholar

[41]

VARDI, M. Y., AND WOLPER, P. Yet another process logic. In Proceedings of the Workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 164. Springcr-Verlag, New York, 1983, pp. 501-512.

Crossref

Google Scholar

[42]

VARDI, M., AND WOLPER, P. Automata theoretic techniques for modal logics of programs. In Proceedings of the 16th A CM Symposium on Theory of Computing (Washington, DC, Apr. 30- May 2). ACM, New York, 1984, pp. 446-456.

Crossref

Google Scholar

[43]

WOLPER, P., VARDI, M. Y., AND SlSTLA, A.P. Reasoning about Infinite Computation Paths. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1983, pp. 185-194.

Google Scholar

Cited By

View all

Furusawa HGuttmann WStruth G(2024)Modal algebra of multirelationsJournal of Logic and Computation10.1093/logcom/exae023Online publication date: 28-May-2024
https://doi.org/10.1093/logcom/exae023
Furusawa HGuttmann WStruth G(2024)Determinism of multirelationsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100976139(100976)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100976
Jacobs JWißmann T(2023)Fast Coalgebraic Bisimilarity MinimizationProceedings of the ACM on Programming Languages10.1145/35712457:POPL(1514-1541)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571245
Show More Cited By

Index Terms

Concurrent dynamic logic
1. Theory of computation

Recommendations

Concurrent dynamic logic
STOC '85: Proceedings of the seventeenth annual ACM symposium on Theory of computing

In this paper we investigate extensions of dynamic logic tailored towards handling concurrent programs, with or without communication. The basic version of concurrent dynamic logic, CDL, is a natural extension of regular DL, and is shown to possess most ...
Sequential Dynamic Logic

We introduce a substructural propositional calculus of Sequential Dynamic Logic that subsumes a propositional part of dynamic predicate logic, and is shown to be expressively equivalent to propositional dynamic logic. Completeness of the calculus with ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...

Reviews

Reviewer: Christopher Martin Holt

In classical logic the truth of an assertion depends on the values of its variables in a given state. Dynamic logic extends this by defining an assertion of the form::3W(rogram:3W)postcondition, which is true if and only if the postcondition is true after applying the program to the given state. This paper extends the programs allowed to include a concurrency operation :3Wd the result of applying a program may be any of a set of states, and an assertion of the above form is true if and only if the postcondition is true in each of the possible results. Communication as in CCS or TCSP is not considered, so the rule :3W(9T a :3WdCb :3W)9T P = :3W(9T a :3W)9T P :3W-5775 p :3W(Cb :3W)9T P holds. The most interesting results (for me) involve the interaction of concurrency with recursion and fixed points. Various strengths are considered. These include propositional, quantified (first-order) with random assignment, and quantified with a Herbrand version of multiple random assignment. These are compared with a good variety of other approaches. The bulk of the paper is involved with the comparisons, so the primary interest is in logical hierarchies. Concurrent logicians will be interested in the initial description of the logic and some examples in the proofs that illustrate that CPDL (concurrent propositional dynamic logic) is stronger than PDL (propositional dynamic logic) (non-concurrent), and that simulate procedures via concurrency and vice versa. An understanding of the basics (monotonicity, continuity, fixed points) is useful.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Journal of the ACM Volume 34, Issue 2

April 1987

286 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/23005

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1987

Published in JACM Volume 34, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

131
Total Citations
View Citations
924
Total Downloads

Downloads (Last 12 months)56
Downloads (Last 6 weeks)2

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Furusawa HGuttmann WStruth G(2024)Modal algebra of multirelationsJournal of Logic and Computation10.1093/logcom/exae023Online publication date: 28-May-2024
https://doi.org/10.1093/logcom/exae023
Furusawa HGuttmann WStruth G(2024)Determinism of multirelationsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100976139(100976)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100976
Jacobs JWißmann T(2023)Fast Coalgebraic Bisimilarity MinimizationProceedings of the ACM on Programming Languages10.1145/35712457:POPL(1514-1541)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571245
Görlitz OHausmann DHumml MPattinson DPrucker SSchröder L(2023)COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)Automated Deduction – CADE 2910.1007/978-3-031-38499-8_14(234-247)Online publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38499-8_14
Sedlár I(2022)Propositional Dynamic Logic with Quantification over Regular Computation SequencesLogical Foundations of Computer Science10.1007/978-3-030-93100-1_19(301-315)Online publication date: 10-Jan-2022
https://dl.acm.org/doi/10.1007/978-3-030-93100-1_19
Ditmarsch HGoubault ÉLedent JRajsbaum S(2022)Knowledge and Simplicial ComplexesPhilosophy of Computing10.1007/978-3-030-75267-5_1(1-50)Online publication date: 5-May-2022
https://doi.org/10.1007/978-3-030-75267-5_1
Boudou JHerzig ATroquard N(2021)Resource separation in dynamic logic of propositional assignmentsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2021.100683121(100683)Online publication date: Jun-2021
https://doi.org/10.1016/j.jlamp.2021.100683
Gomes LMadeira ABarbosa L(2021)A semantics and a logic for Fuzzy Arden SyntaxSoft Computing - A Fusion of Foundations, Methodologies and Applications10.1007/s00500-021-05593-925:9(6789-6805)Online publication date: 13-Feb-2021
https://dl.acm.org/doi/10.1007/s00500-021-05593-9
Hausmann DSchröder L(2021)Quasipolynomial Computation of Nested FixpointsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72016-2_3(38-56)Online publication date: 20-Mar-2021
https://doi.org/10.1007/978-3-030-72016-2_3
Hausmann DSchröder L(2020)NP Reasoning in the Monotone -CalculusAutomated Reasoning10.1007/978-3-030-51074-9_28(482-499)Online publication date: 1-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-51074-9_28
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