--- res: bibo_abstract: - We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) for POMDPs with all parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Krishnendu foaf_name: Chatterjee, Krishnendu foaf_surname: Chatterjee foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-4561-241X - foaf_Person: foaf_givenName: Martin foaf_name: Chmelik, Martin foaf_surname: Chmelik foaf_workInfoHomepage: http://www.librecat.org/personId=3624234E-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Mathieu foaf_name: Tracol, Mathieu foaf_surname: Tracol foaf_workInfoHomepage: http://www.librecat.org/personId=3F54FA38-F248-11E8-B48F-1D18A9856A87 bibo_doi: 10.1016/j.jcss.2016.02.009 bibo_issue: '5' bibo_volume: 82 dct_date: 2016^xs_gYear dct_language: eng dct_publisher: Elsevier@ dct_title: What is decidable about partially observable Markov decision processes with ω-regular objectives@ ...