Showing 1–1 of 1 results for author: Schechter, L M

CCS-Based Dynamic Logics for Communicating Concurrent Programs

Authors: Mario R. F. Benevides, L. Menasché Schechter

Abstract: 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 descrip… ▽ More 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. △ Less

Submitted 31 March, 2009; originally announced April 2009.

Comments: 28 pages

ACM Class: F.4.1; F.3.1; F.1.2