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. pages ??--?? 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",
   pages = "??--??",
   doi = "10.1016/j.ic.2017.08.007",
   note = "To appear.  Available online.",
}
pdf