conference paper published Mária Svoreňová author Martin Chmelik author 3624234E-F248-11E8-B48F-1D18A9856A87 Kevin Leahy author Hasan Eniser author Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Ivana Cěrná author Cǎlin Belta author KrCh department HSCC: Hybrid Systems - Computation and Control Modern Graph Algorithmic Techniques in Formal Verification project Rigorous Systems Engineering project Quantitative Graph Games: Theory and Applications project We consider a case study of the problem of deploying an autonomous air vehicle in a partially observable, dynamic, indoor environment from a specification given as a linear temporal logic (LTL) formula over regions of interest. We model the motion and sensing capabilities of the vehicle as a partially observable Markov decision process (POMDP). We adapt recent results for solving POMDPs with parity objectives to generate a control policy. We also extend the existing framework with a policy minimization technique to obtain a better implementable policy, while preserving its correctness. The proposed techniques are illustrated in an experimental setup involving an autonomous quadrotor performing surveillance in a dynamic environment. ACM2015Seattle, WA, United States eng 10.1145/2728606.2728617 233 - 238 Svoreňová M, Chmelik M, Leahy K, Eniser H, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 233–238. Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 233–38, doi:<a href="https://doi.org/10.1145/2728606.2728617">10.1145/2728606.2728617</a>. M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–238. Svoreňová, Mária, Martin Chmelik, Kevin Leahy, Hasan Eniser, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 233–38. ACM, 2015. <a href="https://doi.org/10.1145/2728606.2728617">https://doi.org/10.1145/2728606.2728617</a>. Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In: <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2015:233-238. doi:<a href="https://doi.org/10.1145/2728606.2728617">10.1145/2728606.2728617</a> M. Svoreňová <i>et al.</i>, “Temporal logic motion planning using POMDPs with parity objectives: Case study paper,” in <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, Seattle, WA, United States, 2015, pp. 233–238. Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2015). Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i> (pp. 233–238). Seattle, WA, United States: ACM. <a href="https://doi.org/10.1145/2728606.2728617">https://doi.org/10.1145/2728606.2728617</a> 16912018-12-11T11:53:29Z2021-01-12T06:52:33Z