On first-order μ-calculus over situation calculus action theories
De Giacomo G
MetadataShow full item record
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 introduced in the literature for verification of data-aware processes. The former requires that quantification ranges over objects in the current active domain, while the latter additionally requires that objects assigned to variables persist across situations. Each of these two logics has a distinct corresponding notion of bisimulation. In spite of the differences we show that the two notions of bisimulation collapse for dynamic systems that are generic, which include all those systems specified through a situation calculus action theory. Then, by exploiting this result, we show that for bounded situation calculus action theories, muLa and muLp have exactly the same expressive power. Finally, we prove decidability of verification of muLa properties over bounded action theories, using finite faithful abstractions. Differently from the muLp case, these abstractions must depend on the number of quantified variables in the muLa formula.
Showing items related by title, author, creator and subject.
First-order mu-calculus over Generic Transition Systems and Applications to the Situation Calculus Calvanese D; De Giacomo G; Montali M; Patrizi F (2018)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 ...
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 ...