On Decidable Verification of Non-terminating Golog Programs. Claßen, J., Liebenberg, M., & Lakemeyer, G. In Ji, J., Strass, H., & Wang, X., editors, Proceedings of the 10th International Workshop on Nonmonotonic Reasoning, Action and Change (NRAC 2013), pages 13–20, Beijing, China, 2013. Paper abstract bibtex The high-level action programming language Golog has proven to be a useful means for the control of autonomous agents such as mobile robots. Usually, such agents perform open-ended tasks, and their control programs are hence non-terminating. Before deploying such a program to the robot, it is often desirable if not crucial to verify that it meets certain requirements, preferably by means of an automated method. For this purpose, Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of non-terminating Golog programs, based on the first-order modal Situation Calculus variant \ES, and regression-based reasoning. However, while Golog\textquoterights high expressiveness is a desirable feature, it also means that their verification procedures cannot be guaranteed to terminate in general. In this paper, we address this problem by showing that, for a relevant subset, the verification of non-terminating Golog programs is indeed decidable, which is achieved by means of three restrictions. First, we use the ES variant of a decidable two-variable fragment of the Situation Calculus that was introduced by Gu and Soutchanski. Second, we have to restrict the Golog program to contain ground action only. Finally, we consider special classes of successor state axioms, namely the context-free ones and those that only admit local effects.
@INPROCEEDINGS{LiebenbergNRAC13,
title = {On Decidable Verification of Non-terminating {G}olog
Programs},
author = {Jens Cla{\ss}en and Martin Liebenberg and Gerhard
Lakemeyer},
booktitle = {Proceedings of the 10th International Workshop on
Nonmonotonic Reasoning, Action and Change (NRAC
2013)},
year = {2013},
address = {Beijing, China},
editor = {Jianmin Ji and Hannes Strass and Xun Wang},
pages = {13--20},
abstract = {The high-level action programming language Golog has
proven to be a useful means for the control of
autonomous agents such as mobile robots. Usually,
such agents perform open-ended tasks, and their
control programs are hence non-terminating. Before
deploying such a program to the robot, it is often
desirable if not crucial to verify that it meets
certain requirements, preferably by means of an
automated method. For this purpose, Cla{\ss}en and
Lakemeyer recently introduced algorithms for the
verification of temporal properties of
non-terminating Golog programs, based on the
first-order modal Situation Calculus variant \ES,
and regression-based reasoning. However, while
Golog{\textquoteright}s high expressiveness is a
desirable feature, it also means that their
verification procedures cannot be guaranteed to
terminate in general. In this paper, we address this
problem by showing that, for a relevant subset, the
verification of non-terminating Golog programs is
indeed decidable, which is achieved by means of
three restrictions. First, we use the ES variant of
a decidable two-variable fragment of the Situation
Calculus that was introduced by Gu and
Soutchanski. Second, we have to restrict the Golog
program to contain ground action only. Finally, we
consider special classes of successor state axioms,
namely the context-free ones and those that only
admit local effects.},
url = {https://kbsg.rwth-aachen.de/~classen/pub/ClassenLiebenbergLakemeyer2013.pdf}
}
Downloads: 0
{"_id":"mHwArikhE94Ppqi6Q","bibbaseid":"claen-liebenberg-lakemeyer-ondecidableverificationofnonterminatinggologprograms-2013","author_short":["Claßen, J.","Liebenberg, M.","Lakemeyer, G."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"On Decidable Verification of Non-terminating Golog Programs","author":[{"firstnames":["Jens"],"propositions":[],"lastnames":["Claßen"],"suffixes":[]},{"firstnames":["Martin"],"propositions":[],"lastnames":["Liebenberg"],"suffixes":[]},{"firstnames":["Gerhard"],"propositions":[],"lastnames":["Lakemeyer"],"suffixes":[]}],"booktitle":"Proceedings of the 10th International Workshop on Nonmonotonic Reasoning, Action and Change (NRAC 2013)","year":"2013","address":"Beijing, China","editor":[{"firstnames":["Jianmin"],"propositions":[],"lastnames":["Ji"],"suffixes":[]},{"firstnames":["Hannes"],"propositions":[],"lastnames":["Strass"],"suffixes":[]},{"firstnames":["Xun"],"propositions":[],"lastnames":["Wang"],"suffixes":[]}],"pages":"13–20","abstract":"The high-level action programming language Golog has proven to be a useful means for the control of autonomous agents such as mobile robots. Usually, such agents perform open-ended tasks, and their control programs are hence non-terminating. Before deploying such a program to the robot, it is often desirable if not crucial to verify that it meets certain requirements, preferably by means of an automated method. For this purpose, Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of non-terminating Golog programs, based on the first-order modal Situation Calculus variant \\ES, and regression-based reasoning. However, while Golog\\textquoterights high expressiveness is a desirable feature, it also means that their verification procedures cannot be guaranteed to terminate in general. In this paper, we address this problem by showing that, for a relevant subset, the verification of non-terminating Golog programs is indeed decidable, which is achieved by means of three restrictions. First, we use the ES variant of a decidable two-variable fragment of the Situation Calculus that was introduced by Gu and Soutchanski. Second, we have to restrict the Golog program to contain ground action only. Finally, we consider special classes of successor state axioms, namely the context-free ones and those that only admit local effects.","url":"https://kbsg.rwth-aachen.de/~classen/pub/ClassenLiebenbergLakemeyer2013.pdf","bibtex":"@INPROCEEDINGS{LiebenbergNRAC13,\n title = {On Decidable Verification of Non-terminating {G}olog\n Programs},\n author = {Jens Cla{\\ss}en and Martin Liebenberg and Gerhard\n Lakemeyer},\n booktitle = {Proceedings of the 10th International Workshop on\n Nonmonotonic Reasoning, Action and Change (NRAC\n 2013)},\n year = {2013},\n address = {Beijing, China},\n editor = {Jianmin Ji and Hannes Strass and Xun Wang},\n pages = {13--20},\n abstract = {The high-level action programming language Golog has\n proven to be a useful means for the control of\n autonomous agents such as mobile robots. Usually,\n such agents perform open-ended tasks, and their\n control programs are hence non-terminating. Before\n deploying such a program to the robot, it is often\n desirable if not crucial to verify that it meets\n certain requirements, preferably by means of an\n automated method. For this purpose, Cla{\\ss}en and\n Lakemeyer recently introduced algorithms for the\n verification of temporal properties of\n non-terminating Golog programs, based on the\n first-order modal Situation Calculus variant \\ES,\n and regression-based reasoning. However, while\n Golog{\\textquoteright}s high expressiveness is a\n desirable feature, it also means that their\n verification procedures cannot be guaranteed to\n terminate in general. In this paper, we address this\n problem by showing that, for a relevant subset, the\n verification of non-terminating Golog programs is\n indeed decidable, which is achieved by means of\n three restrictions. First, we use the ES variant of\n a decidable two-variable fragment of the Situation\n Calculus that was introduced by Gu and\n Soutchanski. Second, we have to restrict the Golog\n program to contain ground action only. Finally, we\n consider special classes of successor state axioms,\n namely the context-free ones and those that only\n admit local effects.},\n url = {https://kbsg.rwth-aachen.de/~classen/pub/ClassenLiebenbergLakemeyer2013.pdf}\n}\n\n","author_short":["Claßen, J.","Liebenberg, M.","Lakemeyer, G."],"editor_short":["Ji, J.","Strass, H.","Wang, X."],"key":"LiebenbergNRAC13","id":"LiebenbergNRAC13","bibbaseid":"claen-liebenberg-lakemeyer-ondecidableverificationofnonterminatinggologprograms-2013","role":"author","urls":{"Paper":"https://kbsg.rwth-aachen.de/~classen/pub/ClassenLiebenbergLakemeyer2013.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["decidable","verification","non","terminating","golog","programs","claßen","liebenberg","lakemeyer"],"title":"On Decidable Verification of Non-terminating Golog Programs","year":2013}