2009/04/01 by Mário Benevides, Benevides, Mario R. F., L. Menasché Schechter +1
Computer Science · #F.1.2 #F.3.1 #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.0904.0034
openalex publication_date 2009/04/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This work presents three increasingly expressive Dynamic Logics in which the programs are CCS processes (sCCS-PDL, CCS-PDL and XCCS-PDL). Their goal is to reason about properties of concurrent programs and systems described using CCS. In order to accomplish that, CCS's operators and constructions are added to a basic modal logic in order to create dynamic logics that are suitable for the description and verification of properties of communicating, concurrent and non-deterministic programs and systems, in a similar way as PDL is used for the sequential case. We provide complete axiomatizations for the three logics. Unlike Peleg's Concurrent PDL with Channels, our logics have a simple Kripke semantics, complete axiomatizations and the finite model property.