Paper Info
Title
A Propositional Dynamic Logic for Concurrent Programs Based on the pi-Calculus
Abstract
This work presents a Propositional Dynamic Logic (πDL) in which the programs are described in a language based on the π-Calculus without replication. Our goal is to build a dynamic logic that is suitable for the description and verification of properties of communicating concurrent systems, in a similar way as PDL is used for the sequential case. We build a simple Kripke semantics for this logic, provide a complete axiomatization for it and show that it has the finite model property.
Year
DOI
Venue
2010
10.1016/j.entcs.2010.04.005
Electronic Notes in Theoretical Computer Science
Keywords
DocType
Volume
Dynamic Logic,Concurrency,Kripke Semantics,Axiomatization,Completeness
Journal
262
ISSN
Citations 
PageRank 
1571-0661
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Mario R. F. Benevides114323.75
L. Menasché Schechter2234.84