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.
BaierCKatoenJP (2008) Principles of Model Checking. Cambridge, MA: MIT Press.
3.
BerwangerDChatterjeeKWulfMD. (2010) Strategy construction for parity games with imperfect information. Information Computing208: 1206–1220.
4.
BhatiaAKavrakiLEVardiMY (2010) Motion planning with hybrid dynamics and temporal goals. In: Proceedings of IEEE conference on decision and control (CDC 2010), Atlanta, GA, 15–17 December 2010, pp. 1108–1115.
5.
BiancoADe AlfaroL (1995) Model checking of probabilistic and nondeterministic systems. In: Foundations of Software Technology and Theoretical Computer Science (Lecture Notes in Computer Science). Berlin; Heidelberg: Springer, pp.499–513.
6.
ChenYDingXCBeltaC (2011) Synthesis of distributed control and communication schemes from global LTL specifications. In: Proceedings of IEEE conference on decision and control (CDC 2011). Orlando, FL, 12–15 December 2011, pp. 2718–2723.
7.
ClarkeEMPeledDGrumbergO (1999) Model Checking. Cambridge, MA: MIT Press.
8.
DingXCSmithSLBeltaC. (2011) MDP optimal control under temporal logic constraints. In: Proceedings of IEEE conference on decision and control (CDC 2011), Orlando, FL, 12–15 December 2011, pp. 532–538.
9.
EmersonEA (1990) Temporal and Modal Logic. In: Van LeeuwenJ (ed) Handbook of Theoretical Computer Science: Formal Models and Semantics. Amsterdam; New York; MIT Press: North-Holland Publishing Co./MIT Press, Vol. B, pp. 995–1072.
10.
GulwaniSJhaSTiwariA. (2011) Synthesis of loop-free programs. In: Proceedings of 32nd ACM SIGPLAN conference on programming language design and implementation (PLDI 2011), San Jose, CA, 4–8 June 2011, pp. 62–73.
11.
HagbergAASchultDASwartPJ (2008) Exploring network structure, dynamics, and function using NetworkX. In: Proceedings of the 7th Python in science conference (SciPy 2008), Pasadena, CA, 19–24 August 2008, pp. 11–15.
12.
HopcroftJEMotwaniRUllmanJD (2007) Introduction to Automata Theory, Languages, and Computation. Reading, MA: Addison Wesley.
13.
JhaSGulwaniSSeshiaS. (2010) Synthesizing switching logic for safety and dwell-time requirements. In: Proceedings of international conference on cyber-physical systems, Stockholm, Sweden, 12–14 April 2010, pp. 22–31.
14.
JohnsonBKress-GazitH (2012) Probabilistic guarantees for high-level robot behavior in the presence of sensor error. Autonomous Robots33(3): 309–321.
15.
KloetzerMBeltaC (2008) Dealing with non-determinism in symbolic control. In: EgerstedtMMishraB (eds) Hybrid Systems: Computation and Control: 11th International Workshop (Lecture Notes in Computer Science). Berlin; Heidelberg: Springer, pp. 287–300.
16.
KloetzerMBeltaC (2010) Automatic deployment of distributed teams of robots from temporal logic specifications. IEEE Transactions on Robotics26(1): 48–61.
17.
Kress-GazitHFainekosGEPappasGJ (2007) Where’s Waldo? sensor-based temporal logic motion planning. In: Proceedings of IEEE International conference on robotics and automation (ICRA 2007), Rome, 10–14 April 2007, pp. 3116–3121.
18.
KupfermanOVardiMY (2001) Model checking of safety properties. Formal Methods in System Design19: 291–314.
19.
KwiatkowskaMNormanGParkerD (2002) Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Proceedings of 8th International conference TACAS 2002 held as part of the joint European conferences on theory and practice of software (ETAPS 2002), Grenoble, France, 8–12 April 2002, pp. 52–66.
20.
LahijanianMAnderssonSBBeltaC (2012) Temporal logic motion planning and control with probabilistic satisfaction guarantees. IEEE Transactions on Robotics28(2): 396–409.
21.
LatvalaT (2003) Efficient model checking of safety properties. In: Proceedings of 10th International SPIN workshop on model checking software, Portland, OR, 9–10 May 2002, pp. 74–88.
22.
OzayNTopcuUWongpiromsarnTMurrayRM (2011) Distributed synthesis of control protocols for smart camera networks. In: Proceedings of IEEE/ACM International conference on cyber-physical systems (ICCPS 2011), Chicago, IL, 12–14 April 2011, pp. 45–54.
23.
TabuadaPPappasGJ (2006) Linear time logic control of discrete-time linear systems. IEEE Transactions on Automatic Control51(12): 1862–1877.
24.
ThomasW (2002) Infinite games and verification. In: Proceedings of conference on computer-aided verification (CAV), Copenhagen, Denmark, 27–31 July 2002, pp. 58–64.
25.
TůmováJYordanovBBeltaC. (2010) A symbolic approach to controlling piecewise affine systems. In: Proceedings of IEEE conference on decision and control (CDC 2010), Atlanta, GA, 15–17 December 2010, pp. 4230–4235.
26.
UlusoyAWongpiromsarnTBeltaC (2012) Incremental control synthesis in probabilistic environments with temporal logic constraints. In: Proceedings of IEEE conference on decision and control (CDC 2012), Maui, HI, 10–13 December 2012, pp. 7658–7663.
27.
WongpiromsarnTTopcuUMurrayRM (2010) Receding horizon control for temporal logic specifications. In: Proceedings of Hybrid systems: Computation and control, Stockholm, Sweden, 12–16 April 2010, pp. 101–110.
28.
WongpiromsarnTUlusoyABeltaC. (2012) Incremental temporal logic synthesis of control policies for robots interacting with dynamic agents. In: Proceedings of IEEE/RSJ International conference on intelligent robots and systems (IROS 2012), Vilamoura, Portugal, 7–12 October 2012, pp. 229–236.
29.
WongpiromsarnTUlusoyABeltaC. (2013) Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications. In: Proceedings of IEEE International conference on robotics and automation, Karlsruhe, Germany, 6–10 May 2013, pp. 5011–5018.
Supplementary Material
Please find the following supplemental material available below.
For Open Access articles published under a Creative Commons License, all supplemental material carries the same license as the article it is associated with.
For non-Open Access articles published, all supplemental material carries a non-exclusive license, and permission requests for re-use of supplemental material or any part of supplemental material shall be sent directly to the copyright owner as specified in the copyright notice associated with the article.
