Home » Publication » 14303

Dettaglio pubblicazione

2018, INFORMATION AND COMPUTATION, Pages 328-347 (volume: 259)

First-order μ-calculus over generic transition systems and applications to the situation calculus (01a Articolo in rivista)

Calvanese Diego, DE GIACOMO Giuseppe, Montali Marco, Patrizi Fabio

We consider meL, meLa, and meLp, three variants of the first-order μ-calculus studied in verification of data-aware processes, that differ in the form of quantification on objects across states. Each of these three logics has a distinct notion of bisimulation. We show that the three notions collapse for generic dynamic systems, which include all state-based systems specified using a logical formalism, e.g., the situation calculus. Hence, for such systems, muL, muLa, and muLp have the same expressive power. We also show that, when the dynamic system stores only a bounded number of objects in each state (e.g., for bounded situation calculus action theories), a finite abstraction can be constructed that is faithful for muL (the most general variant), yielding decidability of verification. This contrasts with the undecidability for first-order LTL, and notably implies that first-order ltl cannot be captured by muL.
© Università degli Studi di Roma "La Sapienza" - Piazzale Aldo Moro 5, 00185 Roma