Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs

Jens ClaßenJens Claßen, Martin LiebenbergMartin Liebenberg, Gerhard LakemeyerGerhard Lakemeyer, Benjamin ZarrießBenjamin Zarrieß

Download

Jens Claßen, Martin Liebenberg, Gerhard Lakemeyer, Benjamin Zarrieß
Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs
In Carla E. Brodley; Peter Stone, eds., Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence (AAAI'14), 1012--1019, July 2014. AAAI Press

Details
Bibtex

KurzfassungAbstract
The action programming language Golog has been found useful for the control of autonomous agents such as mobile robots. In scenarios like these, tasks are often open-ended so that the respective control programs are non-terminating. Before deploying such programs on a robot, it is often desirable to verify that they meet certain requirements. For this purpose, Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of Golog programs. However, given the expressiveness of Golog, their verification procedures are not guaranteed to terminate. In this paper, we show how decidability can be obtained by suitably restricting the underlying base logic, the effect axioms for primitive actions, and the use of actions within Golog programs. Moreover, we show that dropping any of these restrictions immediately leads to undecidability of the verification problem.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{CLLZ2014,
  author    = {Jens Cla{\ss}en and Martin Liebenberg and Gerhard Lakemeyer and
               Benjamin Zarrie{\ss}},
  title     = {Exploring the Boundaries of Decidable Verification of
               Non-Terminating Golog Programs},
  editor    = {Carla E. Brodley; Peter Stone},
  booktitle = {Proceedings of the Twenty-Eighth {AAAI} Conference on Artificial
               Intelligence (AAAI'14)},
  publisher = {AAAI Press},
  year      = {2014},
  month     = {July},
  pages     = {1012--1019}
}