Please use this identifier to cite or link to this item:
Files in This Item:
File Description SizeFormat 
Botta et al 2017, SEQUENTIAL DECISION PROBLEMS.pdf304,74 kBAdobe PDFView/Open
Title: Sequential decision problems, dependent types and generic solutions
Authors: Botta, N.Jansson, P.Ionescu, C.Christiansen, D.R.Brady, E.
Publishers Version:
Issue Date: 2017
Published in: Logical Methods in Computer Science Vol. 13 (2017), No. 1
Publisher: Braunschweig : Department of Theoretical Computer Science, Technical University of Braunschweig
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.
Keywords: Dynamical systems; Stochastic systems; Central component; Climate impact researches; Dependent types; Generic implementation; Generic solutions; Induction algorithms; Principle of optimality; Sequential decisions; Problem oriented languages
DDC: 510
License: CC BY 4.0 Unported
Link to License:
Appears in Collections:Mathematik

This item is licensed under a Creative Commons License Creative Commons