| Abstract: | We examine a bidirectional Propositional Dynamic Logic (PDL) for
finite and infinite message sequence charts (MSCs) extending LTL and TLC^-.
By this kind of multi-modal logic we can express properties both in the
entire future and in the past of an event. Path expressions strengthen the
classical until operator of temporal logic. For every formula defining an MSC
language, we construct a communicating finite-state machine (CFM) accepting
the same language. The CFM obtained has size exponential in the size of the
formula. This synthesis problem is solved in full generality, i.e., also for
MSCs with unbounded channels. The model checking problem for CFMs and HMSCs
turns out to be in PSPACE for existentially bounded MSCs. Finally, we show
that, for PDL with intersection, the semantics of a formula cannot be
captured by a CFM anymore. |