Paper Info
Title
Backtracking temporal logic synthesis for uncertain environments
Abstract
This paper considers the problem of synthesizing correct-by-construction robotic controllers in environments with uncertain but fixed structure. “Environment” has two notions in this work: a map or “world” in which some controlled agent must operate and navigate (i.e., evolve in a configuration space with obstacles); and an adversarial player that selects continuous and discrete variables to try to make the agent fail (as in a game). Both the robot and the environment are subjected to behavioral specifications expressed as an assume-guarantee linear temporal logic (LTL) formula. We then consider how to efficiently modify the synthesized controller when the robot encounters unexpected changes in its environment. The crucial insight is that a portion of this problem takes place in a metric space, which provides a notion of nearness. Thus if a nominal plan fails, we need not resynthesize it entirely, but instead can “patch” it locally. We present an algorithm for doing this, prove soundness (correctness of output), and demonstrate it on an example gridworld.
Year
DOI
Venue
2012
10.1109/ICRA.2012.6225208
Robotics and Automation
Keywords
Field
DocType
control system synthesis,robots,temporal logic,adversarial player,assume-guarantee linear temporal logic formula,behavioral specifications,correct-by-construction robotic controllers,example gridworld,robot,synthesized controller,temporal logic synthesis,uncertain environments
Control theory,Automaton,Correctness,Linear temporal logic,Control engineering,Artificial intelligence,Soundness,Temporal logic,Engineering,Metric space,Robot,Backtracking
Conference
Volume
Issue
ISSN
2012
1
1050-4729 E-ISBN : 978-1-4673-1404-6
ISBN
Citations 
PageRank 
978-1-4673-1404-6
22
0.95
References 
Authors
9
3
Name
Order
Citations
PageRank
Scott C. Livingston1220.95
Richard M. Murray2123221223.70
Burdick, J.W.32988516.87