## First-order mu-calculus over Generic Transition Systems and
Applications to the Situation Calculus

**Diego Calvanese, Giuseppe De Giacomo, Marco Montali, and Fabio
Patrizi**
*Information and Computation. 259(3):328--347* 2018.

We consider #L, #La, and #Lp, 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,
#L, #La, and #Lp 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 #L
(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 #L.

@article{IC-2018,
title = "First-order mu-calculus over Generic Transition Systems and
Applications to the Situation Calculus",
year = "2018",
author = "Diego Calvanese and De Giacomo, Giuseppe and Marco Montali
and Fabio Patrizi",
journal = "Information and Computation",
pages = "328--347",
number = "3",
volume = "259",
doi = "10.1016/j.ic.2017.08.007",
}

pdf
url