Title
Incremental controller synthesis in probabilistic environments with temporal logic constraints
Abstract
In this paper, we consider automatic computation of optimal control strategies for a robot interacting with a set of independent uncontrollable agents in a graph-like environment. The mission specification is given as a syntactically co-safe Linear Temporal Logic formula over some properties that hold at the vertices of the environment. The robot is assumed to be a deterministic transition system, while the agents are probabilistic Markov models. The goal is to control the robot such that the probability of satisfying the mission specification is maximized. We propose a computationally efficient incremental algorithm based on the fact that temporal logic verification is computationally cheaper than synthesis. We present several case studies where we compare our approach to the classical non-incremental approach in terms of computation time and memory usage.
Year
DOI
Venue
2012
10.1177/0278364913519000
Decision and Control
Keywords
DocType
Volume
Control policy synthesis,incremental synthesis,probabilistic verification,temporal logic,formal methods
Conference
33
Issue
ISSN
ISBN
8
0743-1546 E-ISBN : 978-1-4673-2064-1
978-1-4673-2064-1
Citations 
PageRank 
References 
18
0.84
24
Authors
3
Name
Order
Citations
PageRank
Alphan Ulusoy11327.65
Tichakorn Wongpiromsarn244825.42
Calin Belta32197153.54