We address the problem of controlling a noisy differential drive mobile robot such that the probability of satisfying a specification given as a bounded linear temporal logic formula over a set of properties at the regions in the environment is maximized. We assume that the vehicle can determine its precise initial position in a known map of the environment. However, motivated by practical limitations, we assume that the vehicle is equipped with noisy actuators and, during its motion in the environment, it can only measure the angular velocity of its wheels using limited accuracy incremental encoders. Assuming the duration of the motion is finite, we map the measurements to a Markov decision process (MDP). We use recent results in statistical model checking to obtain an MDP control policy that maximizes the probability of satisfaction. We translate this policy to a vehicle feedback control strategy and show that the probability that the vehicle satisfies the specification in the environment is bounded from below by the probability of satisfying the specification on the MDP. We illustrate our method with simulations and experimental results.
AbateAD’InnocenzoADi BenedettoM (2011) Approximate abstractions of stochastic hybrid systems. IEEE Transactions on Automatic Control56(11): 2688–2694.
2.
AlterovitzRSimeonTGoldbergK (2007) The stochastic motion roadmap: a sampling framework for planning with Markov motion uncertainty. In: Proceedings of robotics: science and systems III (RSS 2007), Atlanta, GA, USA, 27–30 June 2007, pp. 233–241.
3.
AlthoffMDolanJ (2011) Set-based computation of vehicle behaviors for the online verification of autonomous vehicles. In: Proceedings of 14th International IEEE conference on intelligent transportation systems (ITSC), Washington DC, USA, 5–7 October 2011, pp. 1162–1167.
4.
BaiHHsuDLeeWS (2013) Planning how to learn. In: Proceedings of International conference on robotics and automation (ICRA), Karlsruhe, Germany, 6–10 May 2013, pp. 2853–2859.
5.
BaierCKatoenJP (2008) Principles of Model Checking. Cambridge, MA: MIT Press.
6.
BalkcomDMasonMT (2000) Time optimal trajectories for bounded velocity differential drive robots. In: Proceedings of IEEE International conference on robotics and automation (ICRA), Volume 3, San Francisco, CA, USA, 24–28 April 2000, pp. 2499–2504.
7.
BhatiaAKavrakiLVardiM (2010) Motion planning with hybrid dynamics and temporal goals. In: Proceedings of 49th IEEE conference on decision and control (CDC), Atlanta, GA, USA, 15–17 December 2010, pp. 1108–1115.
CizeljIBeltaC (2012) Probabilistically safe control of noisy dubins vehicles. In: Proceedings of IEEE intelligent robots and systems (IROS) conference, Algarve, Portugal, 7–12 October 2012, pp. 2857–2862.
10.
CizeljIBeltaC (2013) Control of noisy differential-drive vehicles from time-bounded temporal logic specifications. In: Proceedings of IEEE International conference on robotics and automation (ICRA), Karlsruhe, Germany, 6–10 May 2013, pp. 2021–2026.
11.
ClarkeEGrumbergOPeledDA (1999) Model Checking. Cambridge, MA: MIT Press.
12.
DingXCLazarMBeltaC (2012) Receding horizon temporal logic control for finite deterministic systems. In: Proceedings of IEEE American control conference (ACC), Montreal, QC, Canada, 27–29 June 2012, pp. 715–720.
13.
D’InnocenzoAAbateABenedettoMDD. (2008) Approximate abstractions of discrete-time controlled stochastic hybrid systems. In: Proceedings of IEEE conference on decision and control (CDC), Cancun, Mexico, 9–11 December 2008, pp. 221–226.
14.
EkekweNEtienne-CummingsRKazanzidesP (2007) Incremental encoder based position and velocity measurements VLSI chip with serial peripheral interface. In: Proceedings of IEEE International symposium on circuits and systems (ISCAS) 2007, New Orleans, LA, USA, 27–30 May 2007, pp. 3558–3561.
FraichardTMermondR (1998) Path planning with uncertainty for car-like robots. In: Proceedings of IEEE International conference on robotics and automation (ICRA), Leuven, Belgium, 16–20 May 1998, pp. 27–32.
17.
GirardA (2007) Approximately bisimilar finite abstractions of stable linear systems. In: Proceedings of International conference on hybrid systems: Computation and control (HSCC), Pisa, Italy, 3–5 April 2007, pp. 231–244.
18.
GradyDKMollMKavrakiLE (2013) Combining a POMDP abstraction with replanning to solve complex, position-dependent sensing tasks. Arlington, VA: AAAI Press.
19.
HenriquesDMartinsJZulianiP. (2012) Statistical model checking for Markov decision processes. In: Proceedings of 9th International conference on quantitative evaluation of systems (QEST), London, UK, 17–20 September 2012, pp. 84–93.
20.
JhaSKClarkeEMLangmeadCJ. (2009) A Bayesian approach to model checking biological systems. In: Proceedings of International conference on computational methods in systems biology (CMSB), Bologna, Italy, 31 August–1 September 2009, pp. 218–234.
21.
JuliusAAPappasGJ (2009) Approximations of stochastic hybrid systems. IEEE Transactions on Automatic Control54(6): 1193–1203.
22.
KaramanSFrazzoliE (2008) Vehicle routing problem with metric temporal logic specifications. In: Proceedings of IEEE conference on decision and control (CDC), Cancun, Mexico, 9–11 December 2008, pp. 3953–3958.
23.
KloetzerMBeltaC (2008a) Dealing with non-determinism in symbolic control. In: Hybrid Systems: Computation and Control: 11th International Workshop (Lecture Notes in Computer Science). Berlin; Heidelberg, Germany: Springer, pp. 287–300.
24.
KloetzerMBeltaC (2008b) A fully automated framework for control of linear systems from temporal logic specifications. IEEE Transactions on Automatic Control53(1): 287–297.
Kress-GazitHFainekosGEPappasGJ (2007) Where’s Waldo? Sensor-based temporal logic motion planning. In: Proceedings of IEEE International conference on robotics and automation (ICRA) 2007, Shanghai, 9–13 May 2011, pp. 3116–3121.
27.
LahijanianMAnderssonSBBeltaC (2012) Temporal logic motion planning and control with probabilistic satisfaction guarantees. IEEE Transactions on Robotics28(2): 396–409.
28.
LaValleSM (2006) Planning Algorithms. Cambridge: Cambridge University Press.
29.
LoizouSGKyriakopoulosKJ (2004) Automatic Synthesis of multi-agent motion tasks based on LTL specifications. In: Proceedings of 43rd IEEE conference on decision and control (CDC), Volume 1, Atlantis, Bahamas, 14–17 December 2004, pp. 153–158.
30.
MelchiorNRSimmons (2007) Particle RRT for path planning with uncertainty. In: Proceedings of IEEE International conference on robotics and automation (ICRA), Roma, Italy, 10–14 April 2007, pp. 1617–1624.
31.
PetrellaRTursiniMPerettiL. (2007) Speed measurement algorithms for low-resolution incremental encoder equipped drives: A comparative analysis. In: Proceedings of International Aegean conference on electrical machines and power electronics (ACEMP), Bodrum, Turkey, 10–12 September 2007, pp. 780–787.
32.
ShkolnikAWalterMTedrakeR (2009) Reachability-guided sampling for planning under differential constraints. In: Proceedings of IEEE International conference on robotics and automation (ICRA), Kobe, Japan, 12–17 May 2009, pp. 4387–4393.
33.
TabuadaPPappasGJ (2006) Linear time logic control of discrete-time linear systems. IEEE Transactions on Automatic Control51(12): 1862–1877.
34.
WongpiromsarnTTopcuUMurrayRM (2009) Receding horizon temporal logic planning for dynamical systems. In: 48th IEEE conference on decision and control (CDC), Shanghai, 16–18 December 2009, pp. 5997–6004.
35.
YordanovBTumovaJCernaI. (2012) Temporal Logic Control of discrete-time piecewise affine systems. IEEE Transactions on Automatic Control57(6): 1491–1504.
36.
ZulianiPPlatzerAClarkeEM (2010) Bayesian statistical model checking with application to simulink/stateflow verification. In: Proceedings of International conference on hybrid systems: computation and control (HSCC), Stockholm, Sweden, 12–16 April 2010, pp. 243–252.
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.
