Verification of Golog Programs over Description Logic Actions
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
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.
Details
Original language | English |
---|---|
Title of host publication | Frontiers of Combining Systems |
Publisher | Springer, Berlin [u. a.] |
Pages | 181-196 |
Number of pages | 16 |
ISBN (electronic) | 978-3-642-40885-4 |
Publication status | Published - 2013 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 8152 |
---|---|
ISSN | 0302-9743 |
Conference
Title | International Symposium on Frontiers of Combining Systems 2013 |
---|---|
Abbreviated title | FroCoS 2013 |
Conference number | 9 |
Duration | 18 - 20 September 2013 |
Degree of recognition | International event |
City | Nancy |
Country | France |
External IDs
Scopus | 84886778129 |
---|---|
ORCID | /0000-0002-4049-221X/work/142247966 |