Abstract
Regular dynamic logic is extended by the program constructα∩β, meaning “α andβ executed in parallel”. In a semantics due to Peleg, each commandα is interpreted as a set of pairs (s,T), withT being the set of states “reachable” froms by a single execution ofα, possibly involving several processes acting in parallel. The modalities <α< and [α] are given the interpretations
<α>A is true ats iff there existsT withsRβT andA true throughoutT, and
[α]A is true ats iff for allT, ifsRβT thenA is true throughoutT, which make <α> and [α] no longer interdefinable via negation, as they are in the regular case.
We prove that the logic defined by this modelling is finitely axiomatisable and has the finite model property, hence is decidable. This requires the development a new theory of canonical models and filtrations for “reachability” relations.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Robert Goldblatt,Logics of Time and Computation, Lecture Notes No. 7, CSLI, Stanford, 1987. (Revised edition in preparation.)
A. Nerode andD. Wijesekera,Constructive concurrent dynamic logic I,technical report '90-43, Mathematical Sciences Institute, Cornell University, 1990.
David Peleg,Concurrent dynamic logic,JACM 34 (1987), pp. 450–479.
David Peleg,Communication in concurrent dynamic logic,J. Comp. Syst. Sci. 35 (1987), pp. 23–58.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Goldblatt, R. Parallel action: Concurrent dynamic logic with independent modalities. Stud Logica 51, 551–578 (1992). https://doi.org/10.1007/BF01028975
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01028975