%0 Conference Paper %1 CDMP-P-16 %A Calvanese, Diego %A Giacomo, Giuseppe De %A Montali, Marco %A Patrizi, Fabio %B Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016. %D 2016 %K optique-project %P 411--420 %T On First-Order mu-Calculus over Situation Calculus Action Theories %X In this paper we study verification of situation calculus action theories against first-order mu-calculus with quantification across situations. Specifically, we consider mu-La and mu-Lp, 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, mu-La and mu-Lp have exactly the same expressive power. Finally, we prove decidability of verification of mu-La properties over bounded action theories, using finite faithful abstractions. Differently from the mu-Lp case, these abstractions must depend on the number of quantified variables in the mu-La formula.

@inproceedings{CDMP-P-16, abstract = {In this paper we study verification of situation calculus action theories against first-order mu-calculus with quantification across situations. Specifically, we consider mu-La and mu-Lp, 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, mu-La and mu-Lp have exactly the same expressive power. Finally, we prove decidability of verification of mu-La properties over bounded action theories, using finite faithful abstractions. Differently from the mu-Lp case, these abstractions must depend on the number of quantified variables in the mu-La formula.}, added-at = {2016-10-24T11:58:14.000+0200}, audience = {academic}, author = {Calvanese, Diego and Giacomo, Giuseppe De and Montali, Marco and Patrizi, Fabio}, biburl = {https://www.bibsonomy.org/bibtex/26dfb34e06f75e874f3f423722f74cef6/savo.fabio}, booktitle = {Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, {KR} 2016, Cape Town, South Africa, April 25-29, 2016.}, interhash = {8494e3da170930fcd6bba5fe6d5c7181}, intrahash = {6dfb34e06f75e874f3f423722f74cef6}, keywords = {optique-project}, openaccess = {Yes}, pages = {411--420}, partneroptique = {UNIROMA1}, timestamp = {2016-12-01T18:47:59.000+0100}, title = {On First-Order mu-Calculus over Situation Calculus Action Theories}, wpoptique = {WP4}, year = 2016, yearoptique = {Y4} }