First-order mu-calculus over Generic Transition Systems and Applications to the Situation Calculus
De Giacomo G
MetadataShow full item record
We consider muL, muLa, and muLp, three variants of the first-order mu-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.
Showing items related by title, author, creator and subject.
Calvanese D; De Giacomo G; Montali M; Patrizi F (AAAI Press, 2016)In this paper we study verification of situation calculus action theories against first-order mu-calculus with quantification across situations. Specifically, we consider muLa and muLp, the two variants of mu-calculus ...
Chesani F; Mello P; Montali M; Torroni P (2012)Multiagent social commitments provide a principled basis for agent interactions, and serve as a natural tool to resolve design ambiguities. Indeed, they have been the subject of considerable research for more than a decade. ...