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 (AAAI Press, 2009)Runtime commitment verification is an important, open issue in multiagent research. To address it, we build on Yolum and Singh's formalization of commitment operations, on Chittaro and Montanari's cached event calculus, ...
Chesani, F; Mello, P; Montali, M; Torroni, P (Springer, 2009)This article presents a run-time verification method of web service behaviour with respect to choreographies. We start from DecSerFlow as a graphical choreography description language. We select a core set of DecSerFlow ...