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. 2017. To appear. Available online.

We consider #L, #Laa, 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-2017,
   title = "First-order mu-calculus over Generic Transition Systems and
Applications to the Situation Calculus",
   year = "2017",
   author = "Diego Calvanese and De Giacomo, Giuseppe and Marco Montali
and Fabio Patrizi",
   journal = "Information and Computation",
   doi = "10.1016/j.ic.2017.08.007",
   note = "To appear.  Available online",
}
pdf