--- _id: '1732' abstract: - lang: eng text: We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty. author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Raghav full_name: Gupta, Raghav last_name: Gupta - first_name: Ayush full_name: Kanodia, Ayush last_name: Kanodia citation: ama: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. In: IEEE; 2015:325-330. doi:10.1109/ICRA.2015.7139019' apa: 'Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2015). Qualitative analysis of POMDPs with temporal logic specifications for robotics applications (pp. 325–330). Presented at the ICRA: International Conference on Robotics and Automation, Seattle, WA, United States: IEEE. https://doi.org/10.1109/ICRA.2015.7139019' chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications,” 325–30. IEEE, 2015. https://doi.org/10.1109/ICRA.2015.7139019. ieee: 'K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Qualitative analysis of POMDPs with temporal logic specifications for robotics applications,” presented at the ICRA: International Conference on Robotics and Automation, Seattle, WA, United States, 2015, pp. 325–330.' ista: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. ICRA: International Conference on Robotics and Automation, 325–330.' mla: Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IEEE, 2015, pp. 325–30, doi:10.1109/ICRA.2015.7139019. short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, IEEE, 2015, pp. 325–330. conference: end_date: 2015-05-30 location: Seattle, WA, United States name: 'ICRA: International Conference on Robotics and Automation' start_date: 2015-05-26 date_created: 2018-12-11T11:53:43Z date_published: 2015-01-01T00:00:00Z date_updated: 2023-02-23T12:25:52Z day: '01' department: - _id: KrCh doi: 10.1109/ICRA.2015.7139019 ec_funded: 1 external_id: arxiv: - '1409.3360' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1409.3360 month: '01' oa: 1 oa_version: Preprint page: 325 - 330 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_status: published publisher: IEEE publist_id: '5394' quality_controlled: '1' related_material: record: - id: '5424' relation: earlier_version status: public - id: '5426' relation: earlier_version status: public scopus_import: 1 status: public title: Qualitative analysis of POMDPs with temporal logic specifications for robotics applications type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ...