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
Technical Report, Chair of Automata Theory, TU Dresden, volume 13-10, 2013. LTCS-Report

Details
Bibtex

KurzfassungAbstract
Golog is a high-level action programming language for controlling autonomous agents such as mobile robots. It is defined on top of a logic-based action theory expressed in the Situation Calculus. Before a program is deployed onto an actual robot and executed in the physical world, it is desirable, if not crucial, to verify that it meets certain requirements (typically expressed through temporal formulas) and thus indeed exhibits the desired behaviour. However, due to the high (first-order) expressiveness of the language, the corresponding verification problem is in general undecidable. In this paper, we extend earlier results to identify a large, non-trivial fragment of the formalism where verification is decidable. In particular, we consider properties expressed in a first-order variant of the branching-time temporal logic CTL^*. Decidability is obtained by (1) resorting to the decidable first-order fragment C^2 as underlying base logic, (2) using a fragment of Golog with ground actions only, and (3) requiring the action theory to only admit local effects.
Bemerkung: Note: Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ ZaCla-LTCS-13-10,
  address = {Dresden, Germany},
  author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}},
  institution = {Chair of Automata Theory, TU Dresden},
  note = {Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {13-10},
  title = {On the Decidability of Verifying LTL Properties of Golog Programs},
  type = {LTCS-Report},
  year = {2013},
}