Roy Mennicke - Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems

lmcs:855 - Logical Methods in Computer Science, June 28, 2013, Volume 9, Issue 2 - https://doi.org/10.2168/LMCS-9(2:12)2013
Propositional Dynamic Logic with Converse and Repeat for Message-Passing SystemsArticle

Authors: Roy Mennicke

    The model checking problem for propositional dynamic logic (PDL) over message sequence charts (MSCs) and communicating finite state machines (CFMs) asks, given a channel bound $B$, a PDL formula $\varphi$ and a CFM $\mathcal{C}$, whether every existentially $B$-bounded MSC $M$ accepted by $\mathcal{C}$ satisfies $\varphi$. Recently, it was shown that this problem is PSPACE-complete. In the present work, we consider CRPDL over MSCs which is PDL equipped with the operators converse and repeat. The former enables one to walk back and forth within an MSC using a single path expression whereas the latter allows to express that a path expression can be repeated infinitely often. To solve the model checking problem for this logic, we define message sequence chart automata (MSCAs) which are multi-way alternating parity automata walking on MSCs. By exploiting a new concept called concatenation states, we are able to inductively construct, for every CRPDL formula $\varphi$, an MSCA precisely accepting the set of models of $\varphi$. As a result, we obtain that the model checking problem for CRPDL and CFMs is still in PSPACE.


    Volume: Volume 9, Issue 2
    Published on: June 28, 2013
    Imported on: December 21, 2012
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1124 times.
    This article's PDF has been downloaded 318 times.