Sciweavers

Share
FSTTCS
2007
Springer

Propositional Dynamic Logic for Message-Passing Systems

11 years 7 months ago
Propositional Dynamic Logic for Message-Passing Systems
We examine a bidirectional Propositional Dynamic Logic (PDL) for message sequence charts (MSCs) extending LTL and TLC− . Every formula is translated into an equivalent communicating finite-state machine (CFM) of exponential size. This synthesis problem is solved in full generality, i.e., also for MSCs with unbounded channels. The model checking problems for CFMs and for HMSCs against PDL formulas are shown to be in PSPACE for existentially bounded MSCs. It is shown that CFMs are to weak to capture the semantics of PDL with intersection.
Benedikt Bollig, Dietrich Kuske, Ingmar Meinecke
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FSTTCS
Authors Benedikt Bollig, Dietrich Kuske, Ingmar Meinecke
Comments (0)
books