@INPROCEEDINGS{ZarriessClassen2017,
  author      = {Jens Cla{\ss}en and Benjamin Zarrie{\ss}},
  title       = {Decidable Verification of Decision-Theoretic {G}olog},
  booktitle   = {Proceedings of the Eleventh International Symposium
                  on Frontiers of Combining Systems (FroCoS 2017)},
  pages       = {227--243},
  year        = {2017},
  publisher   = {Springer},
  doi         = {10.1007/978-3-319-66167-4_13},
  abstract    = {The Golog agent programming language is a powerful
                  means to express high-level behaviours in terms of
                  programs over actions defined in a Situation
                  Calculus theory. Its variant DTGolog includes
                  decision-theoretic aspects in the form of stochastic
                  (probabilistic) actions and reward functions. In
                  particular for physical systems such as robots,
                  verifying that a 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, range of action effects,
                  and program constructs. Recent results for classical
                  Golog show that by suitably restricting these
                  aspects, the verification problem becomes decidable
                  for a non-trivial fragment that retains a large
                  degree of expressiveness. In this paper, we lift
                  these results to the decision-theoretic case by
                  providing an abstraction mechanism for reducing the
                  infinite-state Markov Decision Process induced by
                  the DTGolog program to a finite-state
                  representation, which then can be fed into a
                  state-of-the-art probabilistic model checker.},
  url         = {https://link.springer.com/chapter/10.1007/978-3-319-66167-4_13}
}

{"_id":"dZu9APoLe5CRqaxWz","bibbaseid":"claen-zarrie-decidableverificationofdecisiontheoreticgolog-2017","author_short":["Claßen, J.","Zarrieß, B."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Jens"],"propositions":[],"lastnames":["Claßen"],"suffixes":[]},{"firstnames":["Benjamin"],"propositions":[],"lastnames":["Zarrieß"],"suffixes":[]}],"title":"Decidable Verification of Decision-Theoretic Golog","booktitle":"Proceedings of the Eleventh International Symposium on Frontiers of Combining Systems (FroCoS 2017)","pages":"227–243","year":"2017","publisher":"Springer","doi":"10.1007/978-3-319-66167-4_13","abstract":"The Golog agent programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. Its variant DTGolog includes decision-theoretic aspects in the form of stochastic (probabilistic) actions and reward functions. In particular for physical systems such as robots, verifying that a 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, range of action effects, and program constructs. Recent results for classical Golog show that by suitably restricting these aspects, the verification problem becomes decidable for a non-trivial fragment that retains a large degree of expressiveness. In this paper, we lift these results to the decision-theoretic case by providing an abstraction mechanism for reducing the infinite-state Markov Decision Process induced by the DTGolog program to a finite-state representation, which then can be fed into a state-of-the-art probabilistic model checker.","url":"https://link.springer.com/chapter/10.1007/978-3-319-66167-4_13","bibtex":"@INPROCEEDINGS{ZarriessClassen2017,\n author = {Jens Cla{\\ss}en and Benjamin Zarrie{\\ss}},\n title = {Decidable Verification of Decision-Theoretic {G}olog},\n booktitle = {Proceedings of the Eleventh International Symposium\n on Frontiers of Combining Systems (FroCoS 2017)},\n pages = {227--243},\n year = {2017},\n publisher = {Springer},\n doi = {10.1007/978-3-319-66167-4_13},\n abstract = {The Golog agent programming language is a powerful\n means to express high-level behaviours in terms of\n programs over actions defined in a Situation\n Calculus theory. Its variant DTGolog includes\n decision-theoretic aspects in the form of stochastic\n (probabilistic) actions and reward functions. In\n particular for physical systems such as robots,\n verifying that a program satisfies certain desired\n temporal properties is often crucial, but\n undecidable in general, the latter being due to the\n language's high expressiveness in terms of\n first-order quantification, range of action effects,\n and program constructs. Recent results for classical\n Golog show that by suitably restricting these\n aspects, the verification problem becomes decidable\n for a non-trivial fragment that retains a large\n degree of expressiveness. In this paper, we lift\n these results to the decision-theoretic case by\n providing an abstraction mechanism for reducing the\n infinite-state Markov Decision Process induced by\n the DTGolog program to a finite-state\n representation, which then can be fed into a\n state-of-the-art probabilistic model checker.},\n url = {https://link.springer.com/chapter/10.1007/978-3-319-66167-4_13}\n}\n\n\n","author_short":["Claßen, J.","Zarrieß, B."],"key":"ZarriessClassen2017","id":"ZarriessClassen2017","bibbaseid":"claen-zarrie-decidableverificationofdecisiontheoreticgolog-2017","role":"author","urls":{"Paper":"https://link.springer.com/chapter/10.1007/978-3-319-66167-4_13"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["decidable","verification","decision","theoretic","golog","claßen","zarrieß"],"title":"Decidable Verification of Decision-Theoretic Golog","year":2017}