Progression and verification of situation calculus agents with bounded beliefs.

*(English)*Zbl 1397.68191Summary: We investigate agents that have incomplete information and make decisions based on their beliefs expressed as situation calculus bounded action theories. Such theories have an infinite object domain, but the number of objects that belong to fluents at each time point is bounded by a given constant. Recently, it has been shown that verifying temporal properties over such theories is decidable. We take a first-person view and use the theory to capture what the agent believes about the domain of interest and the actions affecting it. In this paper, we study verification of temporal properties over online executions. These are executions resulting from agents performing only actions that are feasible according to their beliefs. To do so, we first examine progression, which captures belief state update resulting from actions in the situation calculus. We show that, for bounded action theories, progression, and hence belief states, can always be represented as a bounded first-order logic theory. Then, based on this result, we prove decidability of temporal verification over online executions for bounded action theories.

##### Keywords:

reasoning about actions; situation calculus; progression; online execution; verification of agent behaviors; mu-calculus
PDF
BibTeX
XML
Cite

\textit{G. De Giacomo} et al., Stud. Log. 104, No. 4, 705--739 (2016; Zbl 1397.68191)

Full Text:
DOI

##### References:

[1] | Bagheri Hariri, B., D. Calvanese, G. De Giacomo, R. De Masellis, and P. Felli, Foundations of relational artifacts verification, in Proceedings of BPM, 2011. · Zbl 1327.68272 |

[2] | Bagheri Hariri, B., D. Calvanese, G. De Giacomo, A. Deutsch, and M. Montali, Verification of relational data-centric dynamic systems with external services, in Proceedings of PODS, 2013. · Zbl 0226.68044 |

[3] | Baier C., Katoen J.-P., Guldstrand Larsen K.: Principles of Model Checking. MIT Press, Cambridge (2008) |

[4] | Belardinelli, F.; Lomuscio, A.; Patrizi, F., Verification of agent-based artifact systems, Journal of Artificial Intelligence Research, 51, 333-376, (2014) · Zbl 1367.68321 |

[5] | Bonet, B., Conformant plans and beyond: principles and complexity, Artificial Intelligence Research, 174, 245-269, (2010) · Zbl 1207.68344 |

[6] | Bordini, R. H., M. Fisher, C. Pardavila, and M. Wooldridge, Model checking agentspeak, in Proceedings of AAMAS, 2003. · Zbl 0880.68008 |

[7] | Burkart, O., D. Caucal, F. Moller, and B. Steffen, Verification of infinite structures, in Handbook of Process Algebra, Elsevier Science, Amsterdam, 2001. · Zbl 1035.68067 |

[8] | Classen, J., and G. Lakemeyer, A logic for non-terminating Golog programs, in Proceedings of KR, 2008. · Zbl 1211.68399 |

[9] | Classen, J., M. Liebenberg, G. Lakemeyer, and B. Zarriess, Exploring the boundaries of decidable verification of non-terminating Golog programs, in Proceedings of AAAI, 2014. · Zbl 1079.68625 |

[10] | De Giacomo, G., Y. Lespérance, H. J. Levesque, and S. Sardina, IndiGolog: A high-level programming language for embedded reasoning agents, in Multi-Agent Programming: Languages, Tools and Applications, Springer, Berlin, 2009. · Zbl 1017.68510 |

[11] | De Giacomo, G., Y. Lespérance, and F. Patrizi, Bounded situation calculus action theories and decidable verification, in Proceedings of KR, 2012. · Zbl 1065.68627 |

[12] | De Giacomo, G., Y. Lespérance, and F. Patrizi, Bounded epistemic situation calculus theories, in Proceedings of IJCAI, 2013. · Zbl 1207.68344 |

[13] | De Giacomo, G., Y. Lespérance, F. Patrizi, and S. Vassos, LTL verification of online executions with sensing in bounded situation calculus, in Proceedings of ECAI, 2014. · Zbl 1366.68340 |

[14] | De Giacomo, G., Y. Lespérance, F. Patrizi, and S. Vassos, Progression and verification of situation calculus agents with bounded beliefs, in Proceedings of AAMAS, 2014. · Zbl 1397.68191 |

[15] | De Giacomo, G., Y. Lespérance, and A. R. Pearce, Situation calculus based programs for representing and reasoning about game structures, in Proceedings of KR, 2010. · Zbl 1396.91011 |

[16] | De Giacomo G., and H. J. Levesque, An incremental interpreter for high-level programs with sensing, in Logical Foundations for Cognitive Agents: Contributions in Honor of Ray Reiter, Springer, Berlin, 1999. · Zbl 0944.68170 |

[17] | De Giacomo, G., and H. J. Levesque, Projection using regression and sensors, in Proceedings of IJCAI, 1999. |

[18] | Dennis, L. A.; Fisher, M.; Webster, M. P.; Bordini, R. H., Model checking agent programming languages., Automated Software Engineering, 19, 5-63, (2012) |

[19] | Deutsch, A., R. Hull, F. Patrizi, and V. Vianu, Automatic verification of data-centric business processes, in Proceedings of ICDT, 2009. |

[20] | Dumas, M., W. M. P. van der Aalst, and A. H. M. ter Hofstede, Process-Aware Information Systems: Bridging People and Software Through Process Technology. Wiley, Hoboken, 2005. |

[21] | Emerson, E. A., Model checking and the Mu-calculus, in Descriptive Complexity and Finite Models. Proceedings of a DIMACS Workshop, 1996. |

[22] | Gerede, C. E., and J. Su, Specification and verification of artifact behaviors in business process models, in Proceedings of ICSOC, 2007. |

[23] | Gu, Y., and M. Soutchanski, Decidable reasoning in a modified situation calculus, in Proceedings of IJCAI 2007. · Zbl 1205.68405 |

[24] | Hull, R., Artifact-centric business process models: Brief survey of research results and challenges, in Proceedings of OTM 2008 Confederated International Conferences, 2008. |

[25] | Lakemeyer, G., and H. J. Levesque, Situations, si! situation terms, no!, in Proceedings of KR, 2004. |

[26] | Lakemeyer, G., and H. J. Levesque, Semantics for a useful fragment of the situation calculus, in Proceedings of IJCAI, 2005. · Zbl 1216.68269 |

[27] | Levesque, H. J.; Reiter, R.; Lespérance, Y.; Lin, F.; Scherl, R. B., GOLOG: A logic programming language for dynamic domains, Journal of Logic Programming, 31, 59-84, (1997) · Zbl 0880.68008 |

[28] | Libkin, L., Embedded finite models and constraint databases, in Finite Model Theory and Its Applications, Springer, Heidelberg, 2007. |

[29] | Lin, F.; Reiter, R., How to progress a database., Artificial Intelligence, 92, 131-167, (1997) · Zbl 1017.68510 |

[30] | Liu, Y., and G. Lakemeyer, On first-order definability and computability of progression for local-effect actions and beyond, in Proceedings of IJCAI, 2009. · Zbl 1341.68216 |

[31] | Liu, Y., and H. J. Levesque, Tractable reasoning with incomplete first-order knowledge in dynamic systems with context-dependent actions, in Proceedings of IJCAI, 2005. |

[32] | Lomuscio, A., H. Qu, and F. Raimondi, MCMAS: A model checker for the verification of multi-agent systems, in Proceedings of CAV, 2009. · Zbl 1207.68344 |

[33] | McCarthy, J.; Hayes, P. J., Some philosophical problems from the standpoint of artificial intelligence, Machine Intelligence, 4, 463-502, (1969) · Zbl 0226.68044 |

[34] | Moore, R. C., A formal theory of knowledge and action, in J. R. Hobbs and R. C. Moore (eds.), Formal Theories of the Common Sense World, Ablex Publishing, Norwood, NJ, 1985, pp. 319-358. |

[35] | Pirri, F.; Reiter, R., Some contributions to the metatheory of the situation calculus, Journal of ACM, 46, 261-325, (1999) · Zbl 1065.68627 |

[36] | Reiter, R., Knowledge in Action. Logical Foundations for Specifying and Implementing Dynamical Systems, MIT Press, Cambridge, 2001. · Zbl 1018.03022 |

[37] | Sardina, S., and G. De Giacomo, Composition of ConGolog programs, in Proceedings of IJCAI, 2009. |

[38] | Sardina, S., G. De Giacomo, Y. Lespérance, and H. J. Levesque, On the semantics of deliberation in IndiGolog—from theory to implementation. Annals of Mathematics and Artificial Intelligence 41(2-4):259-299, 2004. · Zbl 1048.68100 |

[39] | Sardina, S., G. D. Giacomo, Y. Lespérance, and H. J. Levesque, On ability to autonomously execute agent programs with sensing, in Proceedings of AAMAS, 2004. |

[40] | Sardina, S., G. D. Giacomo, Y. Lespérance, and H. J. Levesque, On the limits of planning over belief states under strict uncertainty, in Proceedings of KR, 2006. |

[41] | Scherl, R. B., and H. J. Levesque, The frame problem and knowledge-producing actions, in Proceedings of AAAI, 1993. |

[42] | Scherl, R. B.; Levesque, H. J., Knowledge, action, and the frame problem, Artificial Intelligence, 144, 1-39, (2003) · Zbl 1079.68625 |

[43] | Shapiro, S., Y. Lespérance, and H. J. Levesque, The cognitive agents specification language and verification environment for multiagent systems, in Proceedings of AAMAS, 2002. · Zbl 1201.68127 |

[44] | Shapiro, S., Y. Lespérance, and H. J. Levesque, The cognitive agent specification language and verification environment, in M. Dastani, K. Hindriks, and J.-J. C. Meyer (eds.), Specification and Verification of Multi-agent Systems/Programs, Springer, Berlin, 2010, pp. 289-316. · Zbl 1201.68127 |

[45] | Stirling, C., Modal and Temporal Properties of Processes, Springer, Heidelberg, 2001. · Zbl 0981.68114 |

[46] | Ternovskaia, E., Automata theory for reasoning about actions, In Proceedings of IJCAI, 1999. |

[47] | van Riemsdijk, M., L. Atefnoaei, and F. de Boer, Using the Maude term rewriting language for agent development with formal foundations, in M. Dastani, K. V. Hindriks, and J.-J. C. Meyer (eds.), Specification and Verification of Multi-agent Systems. Springer, Berlin, 2010, pp. 255-287. · Zbl 1201.68130 |

[48] | Vardi, M. Y., An automata-theoretic approach to linear temporal logic, in Proceedings of Banff Higher Order Workshop, 1995. |

[49] | Vassos, S., G. Lakemeyer, and H. J. Levesque, First-order strong progression for local-effect basic action theories, in Proceedings of KR, 2008. |

[50] | Vassos, S., and H. J. Levesque, How to progress a database III, Artificial Intelligence 195:203-221, 2013. · Zbl 1270.68291 |

[51] | Vassos, S., and F. Patrizi, A classification of first-order progressable action theories in situation calculus, in In Proceedings of IJCAI, 2013. |

[52] | Wooldridge, M., Lomuscio A.:A computationally grounded logic of visibility, perception, and knowledge. Logic Journal of the IGPL 9(2):257-272 (2001) · Zbl 0974.68203 |

[53] | Yadav, N., and S. Sardina, Reasoning about BDI agent programs using ATL-like logics, in Proceedings of JELIA, 2012. · Zbl 1361.68247 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.