[{"creator":{"id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","login":"kschuh"},"ec_funded":1,"publist_id":"5718","dini_type":"doc-type:article","date_updated":"2023-02-23T12:24:38Z","date_created":"2018-12-11T11:52:15Z","volume":82,"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Tracol","first_name":"Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"2295"},{"id":"5400","relation":"earlier_version","status":"public"}]},"publication_status":"published","department":[{"_id":"KrCh","tree":[{"_id":"ResearchGroups"},{"_id":"IST"}]}],"month":"08","language":[{}],"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1309.2802","open_access":"1"}],"external_id":{"arxiv":[]},"abstract":[{"lang":"eng"}],"issue":"5","type":"journal_article","oa_version":"Preprint","status":"public","intvolume":" 82","_id":"1477","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","uri_base":"https://research-explorer.ista.ac.at","dc":{"creator":["Chatterjee, Krishnendu","Chmelik, Martin","Tracol, Mathieu"],"identifier":["https://research-explorer.ista.ac.at/record/1477"],"type":["info:eu-repo/semantics/article","doc-type:article","text","http://purl.org/coar/resource_type/c_6501"],"description":["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."],"date":["2016"],"language":["eng"],"rights":["info:eu-repo/semantics/openAccess"],"source":["Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 2016;82(5):878-911. doi:10.1016/j.jcss.2016.02.009"],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.1016/j.jcss.2016.02.009","info:eu-repo/semantics/altIdentifier/arxiv/1309.2802","info:eu-repo/grantAgreement/FWF//P 23499-N23","info:eu-repo/grantAgreement/FWF//S11407","info:eu-repo/grantAgreement/EC/FP7/279307"],"publisher":["Elsevier"],"title":["What is decidable about partially observable Markov decision processes with ω-regular objectives"]},"scopus_import":1,"date_published":"2016-08-01T00:00:00Z","page":"878 - 911","publication":"Journal of Computer and System Sciences","citation":{"apa":"Chatterjee, K., Chmelik, M., & Tracol, M. (2016). What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.02.009","ieee":"K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially observable Markov decision processes with ω-regular objectives,” Journal of Computer and System Sciences, vol. 82, no. 5. Elsevier, pp. 878–911, 2016.","ista":"Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 82(5), 878–911.","short":"K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences 82 (2016) 878–911.","mla":"Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and System Sciences, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:10.1016/j.jcss.2016.02.009.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and System Sciences. Elsevier, 2016. https://doi.org/10.1016/j.jcss.2016.02.009."}}]