International Center for Computational Logic - Benutzerbeiträge [de]

Inproceedings3062/en

2015-12-14T16:05:15Z

Benjamin Zarrieß: Page created automatically by parser function on page Inproceedings3062

#REDIRECT [[Inproceedings3062]]

Inproceedings3062

2015-12-14T16:05:14Z

Benjamin Zarrieß: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Benjamin |ErsterAutorNachname=Zarrieß |FurtherAuthors=Jens Claßen }} {{Inproceedings |Referiert=1 |Title=Decid…“

{{Publikation Erster Autor
|ErsterAutorVorname=Benjamin
|ErsterAutorNachname=Zarrieß
|FurtherAuthors=Jens Claßen
}}
{{Inproceedings
|Referiert=1
|Title=Decidable Verification of Golog Programs over Non-Local Effect Actions
|To appear=1
|Year=2016
|Month=Februar
|Booktitle=Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16)
|Publisher=AAAI Press
|Editor=Dale Schuurmans, Michael Wellman
}}
{{Publikation Details
|Abstract=The Golog action programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. In particular for physical systems, verifying that the program satisfies certain desired temporal properties is often crucial, but undecidable in general, the latter being due to the language's high expressiveness in terms of first-order quantification and program constructs. So far, approaches to achieve decidability involved restrictions where action effects either had to be context-free (i.e. not depend on the current state), local (i.e. only affect objects mentioned in the action's parameters), or at least bounded (i.e. only affect a finite number of objects). In this paper, we present a new, more general class of action theories (called acyclic) that allows for context-sensitive, non-local, unbounded effects, i.e. actions that may affect an unbounded number of possibly unnamed objects in a state-dependent fashion. We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for acyclic theories in the two-variable fragment of first-order logic, verification of CTL* properties of programs over ground actions is decidable.
|Download=ZarriessClassenAAAI16.pdf
|Forschungsgruppe=Automatentheorie
}}

Datei:ZarriessClassenAAAI16.pdf

2015-12-14T16:01:18Z

Benjamin Zarrieß:

Inproceedings3028

2015-08-07T10:48:55Z

Benjamin Zarrieß:

{{Publikation Erster Autor
|ErsterAutorVorname=Benjamin
|ErsterAutorNachname=Zarrieß
|FurtherAuthors=Jens Claßen
}}
{{Inproceedings
|Referiert=1
|Title=Verification of Knowledge-Based Programs over Description Logic Actions
|To appear=0
|Year=2015
|Booktitle=Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI'15)
|Pages=3278-3284
|Publisher=AAAI Press
|Editor=Qiang Yang, Michael Wooldridge
}}
{{Publikation Details
|Abstract=A knowledge-based program defines the behavior of an agent by combining primitive actions, programming constructs and test conditions that make explicit reference to the agent's knowledge. In this paper we consider a setting where an agent is equipped with a Description Logic (DL) knowledge base providing general domain knowledge and an incomplete description of the initial situation. We introduce a corresponding new DL-based action language that allows for representing both physical and sensing actions, that we then use to build knowledge-based programs with test conditions expressed in an epistemic DL. After proving undecidability for the general case, we then discuss a restricted fragment where verification becomes decidable. The provided proof is constructive and comes with an upper bound on the procedure's complexity.
|Link=http://ijcai.org/papers15/Abstracts/IJCAI15-462.html
|Forschungsgruppe=Automatentheorie
}}

Inproceedings3028

2015-08-07T10:47:24Z

Benjamin Zarrieß:

{{Publikation Erster Autor
|ErsterAutorVorname=Benjamin
|ErsterAutorNachname=Zarrieß
|FurtherAuthors=Jens Claßen
}}
{{Inproceedings
|Referiert=1
|Title=Verification of Knowledge-Based Programs over Description Logic Actions
|To appear=0
|Year=2015
|Booktitle=Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI'15)
25-31, 2015
|Pages=3278-3284
|Publisher=AAAI Press
|Editor=Qiang Yang, Michael Wooldridge
}}
{{Publikation Details
|Abstract=A knowledge-based program defines the behavior of an agent by combining primitive actions, programming constructs and test conditions that make explicit reference to the agent's knowledge. In this paper we consider a setting where an agent is equipped with a Description Logic (DL) knowledge base providing general domain knowledge and an incomplete description of the initial situation. We introduce a corresponding new DL-based action language that allows for representing both physical and sensing actions, that we then use to build knowledge-based programs with test conditions expressed in an epistemic DL. After proving undecidability for the general case, we then discuss a restricted fragment where verification becomes decidable. The provided proof is constructive and comes with an upper bound on the procedure's complexity.
|Link=http://ijcai.org/papers15/Abstracts/IJCAI15-462.html
|Forschungsgruppe=Automatentheorie
}}

LATPub577

2015-06-17T16:19:40Z

Benjamin Zarrieß:

{{Publikation Erster Autor
|ErsterAutorVorname=Jens
|ErsterAutorNachname=Claßen
|FurtherAuthors=Martin Liebenberg; Gerhard Lakemeyer; Benjamin Zarrieß
}}
{{Inproceedings
|Referiert=1
|Title=Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs
|To appear=0
|Year=2014
|Month=Juli
|Booktitle=Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence (AAAI'14)
|Pages=1012--1019
|Publisher=AAAI Press
|Editor=Carla E. Brodley; Peter Stone
|Organization=
}}
{{Publikation Details
|Abstract=The action programming language Golog has been found useful for the control of autonomous agents such as mobile robots. In scenarios like these, tasks are often open-ended so that the respective control programs are non-terminating. Before deploying such programs on a robot, it is often desirable to verify that they meet certain requirements. For this purpose, Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of Golog programs. However, given the expressiveness of Golog, their verification procedures are not guaranteed to terminate. In this paper, we show how decidability can be obtained by suitably restricting the underlying base logic, the effect axioms for primitive actions, and the use of actions within Golog programs. Moreover, we show that dropping any of these restrictions immediately leads to undecidability of the verification problem.
|Download=ClaLLZ-AAAI14.pdf
|Forschungsgruppe=Automatentheorie
}}

Inproceedings3028/en

2015-06-17T16:11:23Z

Benjamin Zarrieß: Page created automatically by parser function on page Inproceedings3028

#REDIRECT [[Inproceedings3028]]

Inproceedings3028

2015-06-17T16:11:22Z

{{Publikation Erster Autor
|ErsterAutorVorname=Benjamin
|ErsterAutorNachname=Zarrieß
|FurtherAuthors=Jens Claßen
}}
{{Inproceedings
|Referiert=1
|Title=Verification of Knowledge-Based Programs over Description Logic Actions
|To appear=1
|Year=2015
|Booktitle=Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI-15)
|Publisher=AAAI Press
}}
{{Publikation Details
|Abstract=A knowledge-based program defines the behavior of an agent by combining primitive actions, programming constructs and test conditions that make explicit reference to the agent's knowledge. In this paper we consider a setting where an agent is equipped with a Description Logic (DL) knowledge base providing general domain knowledge and an incomplete description of the initial situation. We introduce a corresponding new DL-based action language that allows for representing both physical and sensing actions, and that we then use to build knowledge-based programs with test conditions expressed in the epistemic DL. After proving undecidability for the general case, we then discuss a restricted fragment where verification becomes decidable. The provided proof is constructive and comes with an upper bound on the procedure's complexity.
|Download=ZarriessClassenIJCAI15.pdf
|Forschungsgruppe=Automatentheorie
}}

Datei:ZarriessClassenIJCAI15.pdf

2015-06-17T16:07:15Z

Benjamin Zarrieß:

Benjamin Zarrieß

2014-11-10T16:25:46Z

Benjamin Zarrieß:

{{Mitarbeiter
|Vorname=Benjamin
|Nachname=Zarrieß
|Forschungsgruppe=Automatentheorie
|Stellung=Wissenschaftlicher Mitarbeiter
|Ehemaliger=0
|Telefon=+49 351 463 43501
|Email=zarriess@tcs.inf.tu-dresden.de
|Raum=APB 3029
|DBLP=http://www.informatik.uni-trier.de/~ley/pers/hd/z/Zarrie=szlig=:Benjamin.html
|Publikationen anzeigen=1
|Abschlussarbeiten anzeigen=0
}}