AAAI Publications, Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning

Font Size: 
Bounded Situation Calculus Action Theories and Decidable Verification
Giuseppe De Giacomo, Yves Lespérance, Fabio Patrizi

Last modified: 2012-05-17


We define a notion of bounded action theory in the situation calculus, where the theory entails that in all situations, the number of ground fluent atoms is bounded by a constant. Such theories can still have an infinite domain and an infinite set of states. We argue that such theories are fairly common in applications, either because facts do not persist indefinitely or because one eventually forgets some facts, as one learns new ones. We discuss various ways of obtaining bounded action theories. The main result of the paper is that verification of an expressive class of first-order mu-calculus temporal properties in such theories is in fact decidable.


Action Theories; Decidable Verification; Infinite-State Model Checking; Temporal First-Order mu-Calculus

Full Text: PDF