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.

• Type: Conference
• Year: 2007
• Where: FSTTCS
• Authors: Benedikt Bollig, Dietrich Kuske, Ingmar Meinecke
• Keywords: Communicating finite-state Machine, FSTTCS 2007, Message Sequence Charts, Propositional Dynamic Logic