## On First-Order mu-Calculus over Situation Calculus Action
Theories

**Diego Calvanese, Giuseppe De Giacomo, Marco Montali, and Fabio
Patrizi**
*Proc. of the 15th Int. Conf. on the Principles of Knowledge
Representation and Reasoning (KR 2016).* 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 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.

@inproceedings{KR-2016-mulap,
title = "On First-Order mu-Calculus over Situation Calculus Action
Theories",
year = "2016",
author = "Diego Calvanese and De Giacomo, Giuseppe and Marco Montali
and Fabio Patrizi",
booktitle = "Proc. of the 15th Int. Conf. on the Principles of Knowledge
Representation and Reasoning (KR 2016)",
pages = "411--420",
publisher = "AAAI Press",
}

pdf
url