Benedikt Bollig ; Dietrich Kuske ; Ingmar Meinecke - Propositional Dynamic Logic for Message-Passing Systems

lmcs:1057 - Logical Methods in Computer Science, September 4, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:16)2010
Propositional Dynamic Logic for Message-Passing SystemsArticle

Authors: Benedikt Bollig ; Dietrich Kuske ; Ingmar Meinecke

    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.


    Volume: Volume 6, Issue 3
    Published on: September 4, 2010
    Imported on: June 5, 2009
    Keywords: Computer Science - Logic in Computer Science,F.3.1

    3 Documents citing this article

    Consultation statistics

    This page has been seen 972 times.
    This article's PDF has been downloaded 345 times.