[{"department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:24:38Z","type":"journal_article","status":"public","_id":"1477","related_material":{"record":[{"status":"public","id":"2295","relation":"earlier_version"},{"id":"5400","status":"public","relation":"earlier_version"}]},"volume":82,"issue":"5","ec_funded":1,"publication_status":"published","language":[{"iso":"eng"}],"scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1309.2802","open_access":"1"}],"month":"08","intvolume":" 82","abstract":[{"lang":"eng","text":"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."}],"oa_version":"Preprint","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin"},{"full_name":"Tracol, Mathieu","last_name":"Tracol","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","first_name":"Mathieu"}],"publist_id":"5718","external_id":{"arxiv":["1309.2802"]},"title":"What is decidable about partially observable Markov decision processes with ω-regular objectives","citation":{"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.","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.","ama":"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","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.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"page":"878 - 911","doi":"10.1016/j.jcss.2016.02.009","date_published":"2016-08-01T00:00:00Z","date_created":"2018-12-11T11:52:15Z","year":"2016","day":"01","publication":"Journal of Computer and System Sciences","quality_controlled":"1","publisher":"Elsevier","oa":1},{"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:37Z","date_updated":"2023-02-23T12:24:38Z","ddc":["000"],"type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2013-09-02","end_date":"2013-09-05","location":"Torino, Italy","name":"CSL: Computer Science Logic"},"status":"public","pubrep_id":"756","_id":"2295","series_title":"Leibniz International Proceedings in Informatics","volume":23,"related_material":{"record":[{"id":"1477","status":"public","relation":"later_version"},{"status":"public","id":"5400","relation":"earlier_version"}]},"license":"https://creativecommons.org/licenses/by/4.0/","ec_funded":1,"publication_status":"published","file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"ba2828322955574d9283bea0e17a37a6","file_id":"4766","creator":"system","date_updated":"2020-07-14T12:45:37Z","file_size":345171,"date_created":"2018-12-12T10:09:42Z","file_name":"IST-2017-756-v1+1_2.pdf"}],"language":[{"iso":"eng"}],"scopus_import":1,"alternative_title":["LIPIcs"],"month":"08","intvolume":" 23","abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. 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 known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal EXPTIME-complete complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite-memory strategies. We also establish asymptotically optimal (exponential) memory bounds."}],"oa_version":"Published Version","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"first_name":"Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","full_name":"Tracol, Mathieu","last_name":"Tracol"}],"publist_id":"4633","title":"What is decidable about partially observable Markov decision processes with omega-regular objectives","citation":{"ista":"Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially observable Markov decision processes with omega-regular objectives. 23, 165–180.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable about Partially Observable Markov Decision Processes with Omega-Regular Objectives.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.165.","ama":"Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable Markov decision processes with omega-regular objectives. 2013;23:165-180. doi:10.4230/LIPIcs.CSL.2013.165","apa":"Chatterjee, K., Chmelik, M., & Tracol, M. (2013). What is decidable about partially observable Markov decision processes with omega-regular objectives. Presented at the CSL: Computer Science Logic, Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.165","short":"K. Chatterjee, M. Chmelik, M. Tracol, 23 (2013) 165–180.","ieee":"K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially observable Markov decision processes with omega-regular objectives,” vol. 23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 165–180, 2013.","mla":"Chatterjee, Krishnendu, et al. What Is Decidable about Partially Observable Markov Decision Processes with Omega-Regular Objectives. Vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 165–80, doi:10.4230/LIPIcs.CSL.2013.165."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"page":"165 - 180","doi":"10.4230/LIPIcs.CSL.2013.165","date_published":"2013-08-27T00:00:00Z","date_created":"2018-12-11T11:56:50Z","has_accepted_license":"1","year":"2013","day":"27","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","oa":1},{"type":"technical_report","status":"public","pubrep_id":"109","_id":"5400","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin"},{"full_name":"Tracol, Mathieu","last_name":"Tracol","first_name":"Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"file_date_updated":"2020-07-14T12:46:44Z","department":[{"_id":"KrCh"}],"title":"What is decidable about partially observable Markov decision processes with ω-regular objectives","citation":{"ista":"Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially observable Markov decision processes with ω-regular objectives, IST Austria, 41p.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-109-v1-1.","ama":"Chatterjee K, Chmelik M, Tracol M. What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives. IST Austria; 2013. doi:10.15479/AT:IST-2013-109-v1-1","apa":"Chatterjee, K., Chmelik, M., & Tracol, M. (2013). What is decidable about partially observable Markov decision processes with ω-regular objectives. IST Austria. https://doi.org/10.15479/AT:IST-2013-109-v1-1","short":"K. Chatterjee, M. Chmelik, M. Tracol, What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives, IST Austria, 2013.","ieee":"K. Chatterjee, M. Chmelik, and M. Tracol, What is decidable about partially observable Markov decision processes with ω-regular objectives. IST Austria, 2013.","mla":"Chatterjee, Krishnendu, et al. What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives. IST Austria, 2013, doi:10.15479/AT:IST-2013-109-v1-1."},"date_updated":"2023-02-23T10:36:45Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"02","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages extends regular languages to infinite strings and provides a robust specification language to express all properties used in verification, and parity objectives are canonical forms to express ω-regular conditions. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satis- fied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite- memory strategies. We establish asymptotically optimal (exponential) memory bounds and EXPTIME- completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives.","lang":"eng"}],"oa_version":"Published Version","page":"41","related_material":{"record":[{"relation":"later_version","id":"1477","status":"public"},{"status":"public","id":"2295","relation":"later_version"}]},"doi":"10.15479/AT:IST-2013-109-v1-1","date_published":"2013-02-20T00:00:00Z","date_created":"2018-12-12T11:39:07Z","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","year":"2013","publication_status":"published","file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"5467","checksum":"cbba40210788a1b22c6cf06433b5ed6f","creator":"system","date_updated":"2020-07-14T12:46:44Z","file_size":483407,"date_created":"2018-12-12T11:53:06Z","file_name":"IST-2013-109-v1+1_What_is_Decidable_about_Partially_Observable_Markov_Decision_Processes_with_ω-Regular_Objectives.pdf"}],"day":"20","language":[{"iso":"eng"}]},{"conference":{"name":"LICS: Logic in Computer Science","start_date":"2012-06-25","location":"Dubrovnik, Croatia ","end_date":"2012-06-28"},"type":"conference","status":"public","_id":"2957","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:23:51Z","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1107.2091"}],"scopus_import":1,"month":"08","abstract":[{"text":"We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether words are accepted with probability arbitrarily close to 1. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape (regular) words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. For most decidable problems we show an optimal PSPACE-complete complexity bound.","lang":"eng"}],"oa_version":"Preprint","ec_funded":1,"related_material":{"record":[{"id":"5384","status":"public","relation":"earlier_version"}]},"publication_status":"published","language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"article_number":"6280437","external_id":{"arxiv":["1107.2091"]},"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","first_name":"Mathieu","last_name":"Tracol","full_name":"Tracol, Mathieu"}],"publist_id":"3769","title":"Decidable problems for probabilistic automata on infinite words","citation":{"ieee":"K. Chatterjee and M. Tracol, “Decidable problems for probabilistic automata on infinite words,” in Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia , 2012.","short":"K. Chatterjee, M. Tracol, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.","ama":"Chatterjee K, Tracol M. Decidable problems for probabilistic automata on infinite words. In: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2012. doi:10.1109/LICS.2012.29","apa":"Chatterjee, K., & Tracol, M. (2012). Decidable problems for probabilistic automata on infinite words. In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. Dubrovnik, Croatia : IEEE. https://doi.org/10.1109/LICS.2012.29","mla":"Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, 6280437, IEEE, 2012, doi:10.1109/LICS.2012.29.","ista":"Chatterjee K, Tracol M. 2012. Decidable problems for probabilistic automata on infinite words. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280437.","chicago":"Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 2012. https://doi.org/10.1109/LICS.2012.29."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"quality_controlled":"1","publisher":"IEEE","date_created":"2018-12-11T12:00:33Z","doi":"10.1109/LICS.2012.29","date_published":"2012-08-23T00:00:00Z","year":"2012","publication":"Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science","day":"23"},{"month":"04","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1104.0127","open_access":"1"}],"publisher":"ArXiv","oa_version":"Preprint","abstract":[{"text":"We consider probabilistic automata on infinite words with acceptance defined by safety, reachability, Büchi, coBüchi, and limit-average conditions. We consider quantitative and qualitative decision problems. We present extensions and adaptations of proofs for probabilistic finite automata and present a complete characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems for probabilistic automata on infinite words.","lang":"eng"}],"date_created":"2018-12-11T12:02:54Z","ec_funded":1,"date_published":"2011-04-01T00:00:00Z","page":"19","language":[{"iso":"eng"}],"day":"01","publication_status":"submitted","year":"2011","status":"public","project":[{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"grant_number":"214373","name":"Design for Embedded Systems","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"type":"preprint","_id":"3363","title":"The decidability frontier for probabilistic automata on infinite words","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"external_id":{"arxiv":["1104.0127"]},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Tracol","full_name":"Tracol, Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","first_name":"Mathieu"}],"publist_id":"3251","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2020-01-21T13:20:24Z","citation":{"apa":"Chatterjee, K., Henzinger, T. A., & Tracol, M. (n.d.). The decidability frontier for probabilistic automata on infinite words. ArXiv.","ama":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words.","ieee":"K. Chatterjee, T. A. Henzinger, and M. Tracol, “The decidability frontier for probabilistic automata on infinite words.” ArXiv.","short":"K. Chatterjee, T.A. Henzinger, M. Tracol, (n.d.).","mla":"Chatterjee, Krishnendu, et al. The Decidability Frontier for Probabilistic Automata on Infinite Words. ArXiv.","ista":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Mathieu Tracol. “The Decidability Frontier for Probabilistic Automata on Infinite Words.” ArXiv, n.d."}},{"pubrep_id":"20","status":"public","type":"technical_report","_id":"5384","title":"Decidable problems for probabilistic automata on infinite words","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:40Z","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","last_name":"Tracol","full_name":"Tracol, Mathieu"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"citation":{"apa":"Chatterjee, K., & Tracol, M. (2011). Decidable problems for probabilistic automata on infinite words. IST Austria. https://doi.org/10.15479/AT:IST-2011-0004","ama":"Chatterjee K, Tracol M. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria; 2011. doi:10.15479/AT:IST-2011-0004","short":"K. Chatterjee, M. Tracol, Decidable Problems for Probabilistic Automata on Infinite Words, IST Austria, 2011.","ieee":"K. Chatterjee and M. Tracol, Decidable problems for probabilistic automata on infinite words. IST Austria, 2011.","mla":"Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria, 2011, doi:10.15479/AT:IST-2011-0004.","ista":"Chatterjee K, Tracol M. 2011. Decidable problems for probabilistic automata on infinite words, IST Austria, 30p.","chicago":"Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0004."},"date_updated":"2023-02-23T11:05:53Z","month":"04","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa_version":"Published Version","abstract":[{"lang":"eng","text":"We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether for every ε > 0 there is a word that is accepted with probability at least 1 − ε. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions."}],"date_created":"2018-12-12T11:39:01Z","related_material":{"record":[{"status":"public","id":"2957","relation":"later_version"}]},"date_published":"2011-04-11T00:00:00Z","doi":"10.15479/AT:IST-2011-0004","page":"30","language":[{"iso":"eng"}],"file":[{"file_name":"IST-2011-004_IST-2011-0004.pdf","date_created":"2018-12-12T11:54:23Z","creator":"system","file_size":570827,"date_updated":"2020-07-14T12:46:40Z","checksum":"f5a0f664fadc335990f5fcf138df19f1","file_id":"5545","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"day":"11","publication_status":"published","year":"2011","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1"}]