Optimal control of MDPs with temporal logic constraints
| Autor: | Ivana Černá, Calin Belta, Maria Svorenova |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
FOS: Computer and information sciences
Model checking Computer Science - Logic in Computer Science 0209 industrial biotechnology Correctness Theoretical computer science 0102 computer and information sciences 02 engineering and technology Optimal control 01 natural sciences Logic in Computer Science (cs.LO) 020901 industrial engineering & automation Linear temporal logic 010201 computation theory & mathematics Automata theory Temporal logic Markov decision process Formal verification Mathematics |
| Zdroj: | CDC |
| Popis: | In this paper, we focus on formal synthesis of control policies for finite Markov decision processes with non-negative real-valued costs. We develop an algorithm to automatically generate a policy that guarantees the satisfaction of a correctness specification expressed as a formula of Linear Temporal Logic, while at the same time minimizing the expected average cost between two consecutive satisfactions of a desired property. The existing solutions to this problem are sub-optimal. By leveraging ideas from automata-based model checking and game theory, we provide an optimal solution. We demonstrate the approach on an illustrative example. Technical report accompanying the CDC 2013 paper |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|