Verifying ConGolog programs on bounded situation calculus theories

De Giacomo, G, Lesperance, Y, Patrizi, F and Sardina, S 2016, 'Verifying ConGolog programs on bounded situation calculus theories', in Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI-2016), Phoenix, United States, 12-17 February 2016, pp. 950-956.


Document type: Conference Paper
Collection: Conference Papers

Title Verifying ConGolog programs on bounded situation calculus theories
Author(s) De Giacomo, G
Lesperance, Y
Patrizi, F
Sardina, S
Year 2016
Conference name AAAI-2016
Conference location Phoenix, United States
Conference dates 12-17 February 2016
Proceedings title Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI-2016)
Publisher AAAI
Place of publication United States
Start page 950
End page 956
Total pages 7
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 μ-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 m-calculus verification.
Subjects Adaptive Agents and Intelligent Robotics
Keyword(s) AI
verification
programs
golog
Copyright notice © 2016 Association for the Advancement of Artificial Intelligence. All Rights Reserved.
Versions
Version Filter Type
Access Statistics: 49 Abstract Views  -  Detailed Statistics
Created: Wed, 11 Jan 2017, 12:29:00 EST by Catalyst Administrator
© 2014 RMIT Research Repository • Powered by Fez SoftwareContact us