Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM
| Authors |
N. Botta Patrik Jansson Cesar Ionescu D. R. Christiansen E. Brady |
|---|---|
| Published in | Logical Methods in Computer Science |
| Volume | 13 |
| Issue | 1 |
| ISSN | 1860-5974 |
| Publication year | 2017 |
| Published at |
Department of Computer Science and Engineering (GU) Department of Computer Science and Engineering, Computing Science (GU) |
| Language | en |
| Links |
doi.org/10.23638/LMCS-13(1:7)2017 |
| Keywords | Computer Science, Science & Technology - Other Topics |
| Subject categories | Computer and Information Science |
We present a computer-checked generic implementation for solving finite horizon sequential decision problems. This is a wide class of problems, including inter temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman's principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research.
© UNIVERSITY OF GOTHENBURG • Sweden • Box 100 • SE-405 30 Gothenburg
Phone: +46 31 786 0000 • Contact • Organisation number: 202100-3153
About the website
Facebook
Twitter
Instagram
Youtube
Weibo