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 -
Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems

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
    Accepted on: June 25, 2015
    Submitted on: December 21, 2012
    Keywords: Computer Science - Logic in Computer Science

    Linked data

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.concur.2022.28
    • 10.4230/lipics.concur.2022.28
    Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages
    Adsul, Bharat ; Gastin, Paul ; Sarkar, Saptarshi ; Weil, Pascal ;


    Consultation statistics

    This page has been seen 437 times.
    This article's PDF has been downloaded 271 times.