Verifying ConGolog Programs on Bounded Situation Calculus Theories

Authors

  • Giuseppe De Giacomo Sapienza University of Rome
  • Yves Lespérance York University
  • Fabio Patrizi Free University of Bozen-Bolzano
  • Sebastian Sardina RMIT University

DOI:

https://doi.org/10.1609/aaai.v30i1.10117

Keywords:

Situation Calculus, Congolog Programs, Verification, Bounded Action Theories

Abstract

We address verification of high-level programs over situation calculus action theories that have an infinite object domain, but bounded fluent extensions in each situation. We show that verification of mu-calculus temporal properties against ConGolog programs over such bounded theories is decidable in general. To do this, we reformulate the transition semantics of ConGolog to keep the bindings of “pick variables” into a separate variable environment whose size is naturally bounded by the number of variables. We also show that for situation-determined ConGolog programs, we can compile away the program into the action theory itself without loss of generality. This can also be done for arbitrary programs, but only to check certain properties, such as if a situation is the result of a program execution, not for mu-calculus verification.

AAAI 2016 Proceedings Cover

Downloads

Published

2016-02-21

How to Cite

De Giacomo, G., Lespérance, Y., Patrizi, F., & Sardina, S. (2016). Verifying ConGolog Programs on Bounded Situation Calculus Theories. Proceedings of the AAAI Conference on Artificial Intelligence, 30(1). https://doi.org/10.1609/aaai.v30i1.10117

Issue

Vol. 30 No. 1 (2016): Thirtieth AAAI Conference on Artificial Intelligence

Section

Technical Papers: Knowledge Representation and Reasoning