Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking

Benedikt Bollig (1, 2) , Aiswarya Cyriac (2, 1) , Paul Gastin (2, 1) , Marc Zeitoun (3)

1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
2 LSV - Laboratoire Spécification et Vérification [Cachan]
3 LaBRI - Laboratoire Bordelais de Recherche en Informatique

We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and that, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satifiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.

Mots clés: Temporal logic; Concurrent recursive programs; Nested words; Mazurkiewicz traces; Satisfiability; Model checking

Domaines: Théorie et langage formel [cs.FL]; Logique en informatique [cs.LO]

Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, Marc Zeitoun. Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking. Journal of Applied Logic, 2014, 12 (4), pp.395-416. ⟨10.1016/j.jal.2014.05.001⟩. ⟨hal-01005353⟩