We define the class of e-bounded theories in the epistemic situation calculus, where the number of fluent atoms that the agent thinks may be true is bounded by a constant. Such theories can still have an infinite domain and an infinite set of states. We show that for them verification of an expressive class of first-order μ-calculus temporal epistemic properties is decidable. We also show that if the agent's knowledge in the initial situation is e-bounded and the objective part of an action theory maintains boundedness, then the entire epistemic theory is e-bounded.
Bounded epistemic situation calculus theories / DE GIACOMO, Giuseppe; Yves, Lesperance; Patrizi, Fabio. - STAMPA. - (2013), pp. 846-853. (Intervento presentato al convegno 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013 tenutosi a Beijing nel 3 August 2013 through 9 August 2013).
Bounded epistemic situation calculus theories
DE GIACOMO, Giuseppe;PATRIZI, FABIO
2013
Abstract
We define the class of e-bounded theories in the epistemic situation calculus, where the number of fluent atoms that the agent thinks may be true is bounded by a constant. Such theories can still have an infinite domain and an infinite set of states. We show that for them verification of an expressive class of first-order μ-calculus temporal epistemic properties is decidable. We also show that if the agent's knowledge in the initial situation is e-bounded and the objective part of an action theory maintains boundedness, then the entire epistemic theory is e-bounded.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
