A Propositional Dynamic Logic for Concurrent Programs Based on the π-Calculus

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.