CCS-Based Dynamic Logics for Communicating Concurrent Programs

TL;DR

This paper introduces three expressive dynamic logics based on CCS processes to reason about properties of concurrent, communicating, and non-deterministic systems, with complete axiomatizations and simple semantics.

Contribution

It extends modal logic with CCS operators to create dynamic logics for concurrent systems, providing complete axiomatizations and finite model properties.

Findings

Complete axiomatizations for all three logics

Simple Kripke semantics for the logics

Finite model property established

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 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.