×

zbMATH — the first resource for mathematics

Non-terminating processes in the situation calculus. (English) Zbl 1444.68179
Summary: By their very design, many robot control programs are non-terminating. This paper describes a situation calculus approach to expressing and proving properties of non-terminating programs expressed in Golog, a high level logic programming language for modeling and implementing dynamical systems. Because in this approach actions and programs are represented in classical (second-order) logic, it is natural to express and prove properties of Golog programs, including non-terminating ones, in the very same logic. This approach to program proofs has the advantage of logical uniformity and the availability of classical proof theory.
MSC:
68T27 Logic in artificial intelligence
68N17 Logic programming
68Q60 Specification and verification (program logics, model checking, etc.)
68T30 Knowledge representation
Software:
ConGolog; GOLOG
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp 739-782. Elsevier (1977)
[2] Baader, F., Liu, H., ul Mehdi, A.: Verifying properties of infinite sequences of description logic actions. In: ECAI, pp. 53-58 (2010) · Zbl 1211.68394
[3] Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., Montali, M.: Verification of relational data-centric dynamic systems with external services. In: PODS, pp. 163-174 (2013)
[4] Bagheri Hariri, B.; Calvanese, D.; Montali, M.; De Giacomo, G.; Masellis, RD; Felli, P., Description logic knowledge and action bases, J. Artif. Intell. Res. (JAIR), 46, 651-686 (2013) · Zbl 1280.68249
[5] Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008) · Zbl 1179.68076
[6] Baier, J.A., Fritz, C., McIlraith, S.A.: Exploiting procedural domain control knowledge in state-of-the-art planners. In: ICAPS, pp. 26-33 (2007)
[7] Belardinelli, F.; Lomuscio, A.; Patrizi, F., Verification of agent-based artifact systems, J. Artif. Intell. Res. (JAIR), 51, 333-376 (2014) · Zbl 1367.68321
[8] Calvanese, D.; De Giacomo, G.; Montali, M.; Patrizi, F., First-order μ-calculus over generic transition systems and applications to the situation calculus, Inf. Comput., 259, 3, 328-347 (2018) · Zbl 1390.68462
[9] Claßen, J., Lakemeyer, G.: A logic for non-terminating Golog programs. In: KR, pp. 589-599 (2008)
[10] Claßen, J., Liebenberg, M., Lakemeyer, G., Zarrieß, B.: Exploring the boundaries of decidable verification of non-terminating Golog programs. In: AAAI, pp. 1012-1019 (2014)
[11] Cousot, P.: Methods and logics for proving programs. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 841-994 (1990) · Zbl 0900.68307
[12] Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretation. In: POPL, pp. 83-94 (1992) · Zbl 0776.68024
[13] De Giacomo, G., Lespérance, Y., Levesque, H.J.: Reasoning about concurrent execution prioritized interrupts, and exogenous actions in the situation calculus. In: IJCAI, pp. 1221-1226 (1997)
[14] De Giacomo, G.; Lespérance, Y.; Levesque, HJ, ConGolog, a concurrent programming language based on the situation calculus, Artif. Intell., 121, 1-2, 109-169 (2000) · Zbl 0948.68175
[15] De Giacomo, G., Lespérance, Y., Patrizi, F.: Bounded situation calculus action theories and decidable verification. In: KR (2012) · Zbl 1357.68227
[16] De Giacomo, G., Lespérance, Y., Patrizi, F.: Bounded epistemic situation calculus theories. In: IJCAI (2013) · Zbl 1357.68227
[17] De Giacomo, G.; Lespérance, Y.; Patrizi, F., Bounded situation calculus action theories, Artif. Intell., 237, 172-203 (2016) · Zbl 1357.68227
[18] De Giacomo, G., Lespérance, Y., Patrizi, F., Sardiña, S.: Verifying ConGolog programs on bounded situation calculus theories. In: AAAI, pp. 950-956 (2016)
[19] De Giacomo, G., Lespérance, Y., Patrizi, F., Vassos, S.: LTL verification of online executions with sensing in bounded situation calculus. In: ECAI, pp. 369-374 (2014) · Zbl 1366.68340
[20] De Giacomo, G., Lespérance, Y., Patrizi, F., Vassos, S.: Progression and verification of situation calculus agents with bounded beliefs. In: AAMAS, pp. 141-148 (2014) · Zbl 1397.68191
[21] De Giacomo, G., Lespérance, Y., Pearce, A.R.: Situation calculus based programs for representing and reasoning about game structures. In: KR (2010)
[22] De Giacomo, G., Levesque, H.J.: An incremental interpreter for high-level programs with sensing. In: Levesque, H.J., Pirri, F. (eds.) Logical Foundation for Cognitive Agents: Contributions in Honor of Ray Reiter, pp 86-102. Springer (1999) · Zbl 0944.68170
[23] De Giacomo, G., Reiter, R., Soutchanski, M.: Execution monitoring of high-level robot programs. In: KR, pp. 453-465 (1998)
[24] De Giacomo, G., Ternovskaia, E., Reiter, R.: Non-terminating processes in the situation calculus. In: Proc.of the AAAI’97 Workshop on Robots, Softbots, Immobots: Theories of Action, Planning and Control (1997)
[25] Emerson, E.A.: Automated temporal reasoning about reactive systems. In: Logics for Concurrency: Structure versus Automata, no. 1043 in Lecture Notes in Computer Science, pp. 41-101. Springer (1996)
[26] Fritz, C., Baier, J.A., McIlraith, S.A.: ConGolog, Sin Trans: Compiling ConGolog into basic action theories for planning and beyond. In: KR, pp. 600-610 (2008)
[27] Gu, Y., Kiringa, I.: Model checking meets theorem proving: A situation calculus based approach. In: 11th International Workshop on Nonmonotonic Reasoning, Action, and Change (2006)
[28] Hehner, E.C.R.: A Practical Theory of Programming. Texts and Monographs in Computer Science Springer (1993)
[29] Hennessy, M., The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics (1990), New York: Wiley, New York · Zbl 0723.68067
[30] Kelly, RF; Pearce, AR, Property persistence in the situation calculus, Artif. Intell., 174, 12-13, 865-888 (2010) · Zbl 1205.68398
[31] Knaster, B., Un thèoréme sur les fonctions d’ensembles, Ann. Soc. Polon. Math., 6, 133-134 (1928) · JFM 54.0091.04
[32] Kozen, D., Tiuryn, J.: Logics of programs. In: van Leeuwen, J (ed.) Handbook of Theoretical Computer Science, pp 790-840. Elsevier (1990) · Zbl 0900.68306
[33] Leivant, D.: Higher order logic. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2. Clarendon Press, pp. 229-321 (1994)
[34] Lespérance, Y.: On the epistemic feasibility of plans in multiagent systems specifications. In: 8th International Workshop on Intelligent Agents VIII, ATAL 2001 Seattle, WA, USA, August 1-3, 2001, Revised Papers, pp. 69-85 (2001) · Zbl 1050.68141
[35] Lespérance, Y.; Levesque, HJ; Lin, F.; Scherl, RB, Ability and knowing how in the situation calculus, Stud. Logica., 66, 1, 165-186 (2000) · Zbl 0968.68151
[36] Levesque, HJ; Reiter, R.; Lespérance, Y.; Lin, F.; Scherl, RB, Golog: A logic programming language for dynamic domains, J. Log. Program., 31, 1-3, 59-83 (1997) · Zbl 0880.68008
[37] Lin, F.: A first-order semantics for Golog and ConGolog under a second-order induction axiom for situations. In: KR (2014)
[38] Loeckx, J.; Sieber, K., Foundation of Program Verification (1987), New York: Teubner-Wiley, New York
[39] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, vol.1-2. Springer (1992) · Zbl 0753.68003
[40] Moschovakis, Y.: Elementary Induction on Abstract Structures. Amsterdam (1974) · Zbl 0307.02003
[41] Park, D.: Fixpoint induction and proofs of program properties. In: Machine Intelligence, vol. 5, pp. 59-78. Edinburgh University Press (1970) · Zbl 0219.68007
[42] Plotkin, G.: A structural approach to operational semantics. Tech. Rep. DAIMI-FN-19, Computer Science Dept. Aarhus Univ Denmark (1981)
[43] Reiter, R.: The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp 359-380. Academic Press, San Diego (1991) · Zbl 0755.68124
[44] Reiter, R.: Knowledge in Action. Logical Foundations for Specifying and Implementing Dynamical Systems. The MIT Press (2001) · Zbl 1018.03022
[45] Sardiña, S., De Giacomo, G.: Composition of ConGolog programs. In: IJCAI, pp. 904-910 (2009)
[46] Sardiña, S.; De Giacomo, G.; Lespérance, Y.; Levesque, HJ, On the semantics of deliberation in IndiGolog- from theory to implementation, Ann. Math. Artif. Intell., 41, 2-4, 259-299 (2004) · Zbl 1048.68100
[47] Shapiro, S., Lespérance, Y., Levesque, H.J.: The cognitive agents specification language and verification environment for multiagent systems. In: AAMAS, pp. 19-26 (2002)
[48] Sohrabi, S., Prokoshyna, N., McIlraith, S.A.: Web service composition via the customization of Golog programs with user preferences. In: Conceptual Modeling: Foundations and Applications - Essays in Honor of John Mylopoulos, pp. 319-334 (2009)
[49] Stirling, C.: Modal and temporal logics for processes. In: Logics for Concurrency: Structure versus Automata, no. 1043 in Lecture Notes in Computer Science, pp. 149-237. Springer (1996)
[50] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pac. J. Math., 5, 2, 285-309 (1955) · Zbl 0064.26004
[51] Ternovskaia, E.: Inductive definability and the situation calculus. In: Transactions and Change in Logic Databases, International Seminar on Logic Databases and the Meaning of Change, Schloss Dagstuhl, Germany, September 23-27, 1996 and ILPS ’97 Post-Conference Workshop on (Trans)Actions and Change in Logic Programming and Deductive Databases, (DYNAMICS’97) Port Jefferson, NY, USA, October 17, 1997, Invited Surveys and Selected Papers, pp. 227-248 (1998) · Zbl 0927.03059
[52] Ternovskaia, E.: Automata theory for reasoning about actions. In: IJCAI, pp. 153-159 (1999)
[53] Wang, Y., Chang, L., Li, F., Gu, T.: Verification of branch-time property based on dynamic description logic. In: Intelligent Information Processing VII - 8th IFIP TC 12 International Conference, IIP 2014, Hangzhou, China, October 17-20, 2014, Proceedings, pp. 161-170 (2014)
[54] Zarrieß, B., Claßen, J.: Verifying CTL* properties of Golog programs over local-effect actions. In: ECAI, pp. 939-944 (2014) · Zbl 1366.68028
[55] Zarrieß, B., Claßen, J.: Decidable verification of Golog programs over non-local effect actions. In: AAAI, pp. 1109-1115 (2016)
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.