Semantisches Browsen
Aus International Center for Computational Logic
The high-level action programming language … 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.he verification problem undecidable again. +
@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},
}
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},
}
Proceedings of the AAAI 2014 Spring Symposium: Knowledge Representation and Reasoning in Robotics (KRR'14) +
Zarrieß +
Benjamin +
Benjamin Zarrieß, Jens Claßen<br/> ' … Benjamin Zarrieß, Jens Claßen<br/> '''[[LATPub550|<b>On the Decidability of Verifying LTL Properties of Golog Programs</b>]]''' <br/>__NOTOC__<i>Proceedings of the AAAI 2014 Spring Symposium: Knowledge Representation and Reasoning in Robotics (KRR'14)</i>, to appear. AAAI Press<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[LATPub550|Details]] <span class="fas fa-chevron-right" style="font-size: 85%; margin-left: 2ex; "></span> [[Media:ZaCla-KRR14.pdf|Download]]ia:ZaCla-KRR14.pdf|Download]] +
Benjamin Zarrieß, Jens Claßen<br/> ' … Benjamin Zarrieß, Jens Claßen<br/> '''[[LATPub550/en|<b>On the Decidability of Verifying LTL Properties of Golog Programs</b>]]''' <br/>__NOTOC__<i>Proceedings of the AAAI 2014 Spring Symposium: Knowledge Representation and Reasoning in Robotics (KRR'14)</i>, to appear. AAAI Press<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[LATPub550|Details]] <span class="fas fa-chevron-right" style="font-size: 85%; margin-left: 2ex;" ></span> [[Media:ZaCla-KRR14.pdf|Download]]ia:ZaCla-KRR14.pdf|Download]] +
Anzeigetitel„Anzeigetitel <span style="font-size:small;">(Display title of)</span>“ ist ein softwareseitig fest definiertes Attribut, das einen eindeutigen Anzeigetitel zu einem Objekt speichert und ihm zuweist. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
On the Decidability of Verifying LTL Properties of Golog Programs +
Zuletzt geändert„Zuletzt geändert <span style="font-size:small;">(Modification date)</span>“ ist ein softwareseitig fest definiertes Attribut, das das Datum der letzten Änderung einer Seite speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
25. März 2015, 14:34:08 +
Hat Abfrage„Hat Abfrage <span style="font-size:small;">(Has query)</span>“ ist ein softwareseitig fest definiertes Attribut, das die Metainformationen einer Abfrage als <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">Subobjekt</a> speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
On the Decidability of Verifying LTL Properties of Golog Programs +, On the Decidability of Verifying LTL Properties of Golog Programs +, On the Decidability of Verifying LTL Properties of Golog Programs +, On the Decidability of Verifying LTL Properties of Golog Programs +, On the Decidability of Verifying LTL Properties of Golog Programs + und On the Decidability of Verifying LTL Properties of Golog Programs +
