CCS-Based Dynamic Logics for Communicating Concurrent Programs
| dc.creator | Benevides, Mario R. F. | |
| dc.creator | Schechter, L. Menasché | |
| dc.date | 2009-04-01 | |
| dc.date.accessioned | 2026-07-07T12:58:58Z | |
| dc.date.available | 2026-07-07T12:58:58Z | |
| dc.description | 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. | |
| dc.description | 28 pages | |
| dc.identifier | https://arxiv.org/abs/0904.0034 | |
| dc.identifier | http://arxiv.org/abs/0904.0034 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/225424 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.4.1; F.3.1; F.1.2 | |
| dc.title | CCS-Based Dynamic Logics for Communicating Concurrent Programs | |
| dc.type | text |