Verification of Golog Programs over Description Logic Actions

Franz BaaderFranz Baader, Benjamin ZarrießBenjamin Zarrieß

Download

Franz Baader, Benjamin Zarrieß
Verification of Golog Programs over Description Logic Actions
In Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt, eds., Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), volume 8152 of Lecture Notes in Computer Science, 181-196, September 2013. Springer

Details
Bibtex

KurzfassungAbstract
High-level action programming languages such as Golog have successfully been used to model the behavior of autonomous agents. In addition to a logic-based action formalism for describing the environment and the effects of basic actions, they enable the construction of complex actions using typical programming language constructs. To ensure that the execution of such complex actions leads to the desired behavior of the agent, one needs to specify the required properties in a formal way, and then verify that these requirements are met by any execution of the program. Due to the expressiveness of the action formalism underlying Golog (Situation Calculus), the verification problem for Golog programs is in general undecidable. Action formalisms based on Description Logic (DL) try to achieve decidability of inference problems such as the projection problem by restricting the expressiveness of the underlying base logic. However, until now these formalisms have not been used within Golog programs. In the present paper, we introduce a variant of Golog where basic actions are defined using such a DL-based formalism, and show that the verification problem for such programs is decidable. This improves on our previous work on verifying properties of infinite sequences of DL actions in that it considers (finite and infinite) sequences of DL actions that correspond to (terminating and non-terminating) runs of a Golog program rather than just infinite sequences accepted by a Büchi automaton abstracting the program.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaZa-FroCoS13,
  address = {Nancy, France},
  author = {Franz {Baader} and Benjamin {Zarrie{\ss}}},
  booktitle = {Proceedings of the 9th International Symposium on Frontiers of Combining Systems ({FroCoS 2013})},
  editor = {Pascal {Fontaine} and Christophe {Ringeissen} and Renate A. {Schmidt}},
  month = {September},
  pages = {181--196},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Verification of Golog Programs over Description Logic Actions},
  volume = {8152},
  year = {2013},
}