To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Sequential decision probl… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

Sequential decision problems, dependent types and generic solutions

Journal article
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

Abstract

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.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?