Abstract
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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Bollig, B., Kuske, D., & Meinecke, I. (2007). Propositional dynamic logic for message-passing systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4855 LNCS, pp. 303–315). Springer Verlag. https://doi.org/10.1007/978-3-540-77050-3_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
