On the Decidability of Verifying LTL Properties of Golog Programs

Benjamin ZarrießBenjamin Zarrieß, Jens ClaßenJens Claßen

Download

Benjamin Zarrieß, Jens Claßen
On the Decidability of Verifying LTL Properties of Golog Programs
Proceedings of the AAAI 2014 Spring Symposium: Knowledge Representation and Reasoning in Robotics (KRR'14), to appear. AAAI Press

Details
Bibtex

KurzfassungAbstract
The high-level action programming language Golog is a useful means for modeling the behavior of autonomous agents such as mobile robots. It relies on a representation given in terms of a logic-based action theory in the Situation Calculus (SC). To guarantee that the possibly non-terminating execution of a Golog program leads to the desired behavior of the agent, it is desirable to (automatically) verify that it satisfies certain requirements given in terms of temporal formulas. However, due to the high (first-order) expressiveness of the Golog language, the verification problem is in general undecidable. In this paper we show that for a fragment of the Golog language defined on top of the decidable logic C^2, the verification problem for linear time temporal properties becomes decidable, which extends earlier results to a more expressive fragment of the input formalism. Moreover, we justify the involved restrictions on program constructs and action theory by showing that relaxing any of these restrictions instantly renders the verification problem undecidable again.
Bemerkung: Note: To appear.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ ZaCla-KRR14,
  address = {Palo Alto, California, USA},
  author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}},
  booktitle = {Proceedings of the AAAI 2014 Spring Symposium: Knowledge Representation and Reasoning in Robotics (KRR'14)},
  note = {To appear.},
  publisher = {AAAI Press},
  title = {On the Decidability of Verifying LTL Properties of Golog Programs},
  year = {2014},
}