---
_id: '1477'
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.
arxiv: 1
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: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  ama: Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable
    Markov decision processes with ω-regular objectives. <i>Journal of Computer and
    System Sciences</i>. 2016;82(5):878-911. doi:<a href="https://doi.org/10.1016/j.jcss.2016.02.009">10.1016/j.jcss.2016.02.009</a>
  apa: Chatterjee, K., Chmelik, M., &#38; Tracol, M. (2016). What is decidable about
    partially observable Markov decision processes with ω-regular objectives. <i>Journal
    of Computer and System Sciences</i>. Elsevier. <a href="https://doi.org/10.1016/j.jcss.2016.02.009">https://doi.org/10.1016/j.jcss.2016.02.009</a>
  chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable
    about Partially Observable Markov Decision Processes with ω-Regular Objectives.”
    <i>Journal of Computer and System Sciences</i>. Elsevier, 2016. <a href="https://doi.org/10.1016/j.jcss.2016.02.009">https://doi.org/10.1016/j.jcss.2016.02.009</a>.
  ieee: K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially
    observable Markov decision processes with ω-regular objectives,” <i>Journal of
    Computer and System Sciences</i>, 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.
  mla: Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable
    Markov Decision Processes with ω-Regular Objectives.” <i>Journal of Computer and
    System Sciences</i>, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:<a href="https://doi.org/10.1016/j.jcss.2016.02.009">10.1016/j.jcss.2016.02.009</a>.
  short: K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences
    82 (2016) 878–911.
date_created: 2018-12-11T11:52:15Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-02-23T12:24:38Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2016.02.009
ec_funded: 1
external_id:
  arxiv:
  - '1309.2802'
intvolume: '        82'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1309.2802
month: '08'
oa: 1
oa_version: Preprint
page: 878 - 911
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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '5718'
quality_controlled: '1'
related_material:
  record:
  - id: '2295'
    relation: earlier_version
    status: public
  - id: '5400'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: What is decidable about partially observable Markov decision processes with
  ω-regular objectives
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 82
year: '2016'
...
---
_id: '5400'
abstract:
- lang: eng
  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.
alternative_title:
- IST Austria Technical Report
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: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  ama: Chatterjee K, Chmelik M, Tracol M. <i>What Is Decidable about Partially Observable
    Markov Decision Processes with ω-Regular Objectives</i>. IST Austria; 2013. doi:<a
    href="https://doi.org/10.15479/AT:IST-2013-109-v1-1">10.15479/AT:IST-2013-109-v1-1</a>
  apa: Chatterjee, K., Chmelik, M., &#38; Tracol, M. (2013). <i>What is decidable
    about partially observable Markov decision processes with ω-regular objectives</i>.
    IST Austria. <a href="https://doi.org/10.15479/AT:IST-2013-109-v1-1">https://doi.org/10.15479/AT:IST-2013-109-v1-1</a>
  chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. <i>What Is
    Decidable about Partially Observable Markov Decision Processes with ω-Regular
    Objectives</i>. IST Austria, 2013. <a href="https://doi.org/10.15479/AT:IST-2013-109-v1-1">https://doi.org/10.15479/AT:IST-2013-109-v1-1</a>.
  ieee: K. Chatterjee, M. Chmelik, and M. Tracol, <i>What is decidable about partially
    observable Markov decision processes with ω-regular objectives</i>. IST Austria,
    2013.
  ista: Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially
    observable Markov decision processes with ω-regular objectives, IST Austria, 41p.
  mla: Chatterjee, Krishnendu, et al. <i>What Is Decidable about Partially Observable
    Markov Decision Processes with ω-Regular Objectives</i>. IST Austria, 2013, doi:<a
    href="https://doi.org/10.15479/AT:IST-2013-109-v1-1">10.15479/AT:IST-2013-109-v1-1</a>.
  short: K. Chatterjee, M. Chmelik, M. Tracol, What Is Decidable about Partially Observable
    Markov Decision Processes with ω-Regular Objectives, IST Austria, 2013.
date_created: 2018-12-12T11:39:07Z
date_published: 2013-02-20T00:00:00Z
date_updated: 2023-02-23T10:36:45Z
day: '20'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2013-109-v1-1
file:
- access_level: open_access
  checksum: cbba40210788a1b22c6cf06433b5ed6f
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:06Z
  date_updated: 2020-07-14T12:46:44Z
  file_id: '5467'
  file_name: IST-2013-109-v1+1_What_is_Decidable_about_Partially_Observable_Markov_Decision_Processes_with_ω-Regular_Objectives.pdf
  file_size: 483407
  relation: main_file
file_date_updated: 2020-07-14T12:46:44Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '41'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '109'
related_material:
  record:
  - id: '1477'
    relation: later_version
    status: public
  - id: '2295'
    relation: later_version
    status: public
status: public
title: What is decidable about partially observable Markov decision processes with
  ω-regular objectives
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2295'
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.
alternative_title:
- LIPIcs
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: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  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:<a
    href="https://doi.org/10.4230/LIPIcs.CSL.2013.165">10.4230/LIPIcs.CSL.2013.165</a>
  apa: 'Chatterjee, K., Chmelik, M., &#38; 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. <a href="https://doi.org/10.4230/LIPIcs.CSL.2013.165">https://doi.org/10.4230/LIPIcs.CSL.2013.165</a>'
  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. <a href="https://doi.org/10.4230/LIPIcs.CSL.2013.165">https://doi.org/10.4230/LIPIcs.CSL.2013.165</a>.
  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.
  ista: Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially
    observable Markov decision processes with omega-regular objectives. 23, 165–180.
  mla: Chatterjee, Krishnendu, et al. <i>What Is Decidable about Partially Observable
    Markov Decision Processes with Omega-Regular Objectives</i>. Vol. 23, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 165–80, doi:<a href="https://doi.org/10.4230/LIPIcs.CSL.2013.165">10.4230/LIPIcs.CSL.2013.165</a>.
  short: K. Chatterjee, M. Chmelik, M. Tracol, 23 (2013) 165–180.
conference:
  end_date: 2013-09-05
  location: Torino, Italy
  name: 'CSL: Computer Science Logic'
  start_date: 2013-09-02
date_created: 2018-12-11T11:56:50Z
date_published: 2013-08-27T00:00:00Z
date_updated: 2023-02-23T12:24:38Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CSL.2013.165
ec_funded: 1
file:
- access_level: open_access
  checksum: ba2828322955574d9283bea0e17a37a6
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:09:42Z
  date_updated: 2020-07-14T12:45:37Z
  file_id: '4766'
  file_name: IST-2017-756-v1+1_2.pdf
  file_size: 345171
  relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: '        23'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 165 - 180
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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4633'
pubrep_id: '756'
quality_controlled: '1'
related_material:
  record:
  - id: '1477'
    relation: later_version
    status: public
  - id: '5400'
    relation: earlier_version
    status: public
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: What is decidable about partially observable Markov decision processes with
  omega-regular objectives
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 23
year: '2013'
...
---
_id: '2957'
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
    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.'
article_number: '6280437'
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  ama: 'Chatterjee K, Tracol M. Decidable problems for probabilistic automata on infinite
    words. In: <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic
    in Computer Science</i>. IEEE; 2012. doi:<a href="https://doi.org/10.1109/LICS.2012.29">10.1109/LICS.2012.29</a>'
  apa: 'Chatterjee, K., &#38; Tracol, M. (2012). Decidable problems for probabilistic
    automata on infinite words. In <i>Proceedings of the 2012 27th Annual ACM/IEEE
    Symposium on Logic in Computer Science</i>. Dubrovnik, Croatia : IEEE. <a href="https://doi.org/10.1109/LICS.2012.29">https://doi.org/10.1109/LICS.2012.29</a>'
  chicago: Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic
    Automata on Infinite Words.” In <i>Proceedings of the 2012 27th Annual ACM/IEEE
    Symposium on Logic in Computer Science</i>. IEEE, 2012. <a href="https://doi.org/10.1109/LICS.2012.29">https://doi.org/10.1109/LICS.2012.29</a>.
  ieee: K. Chatterjee and M. Tracol, “Decidable problems for probabilistic automata
    on infinite words,” in <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium
    on Logic in Computer Science</i>, Dubrovnik, Croatia , 2012.
  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.'
  mla: Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic
    Automata on Infinite Words.” <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium
    on Logic in Computer Science</i>, 6280437, IEEE, 2012, doi:<a href="https://doi.org/10.1109/LICS.2012.29">10.1109/LICS.2012.29</a>.
  short: K. Chatterjee, M. Tracol, in:, Proceedings of the 2012 27th Annual ACM/IEEE
    Symposium on Logic in Computer Science, IEEE, 2012.
conference:
  end_date: 2012-06-28
  location: 'Dubrovnik, Croatia '
  name: 'LICS: Logic in Computer Science'
  start_date: 2012-06-25
date_created: 2018-12-11T12:00:33Z
date_published: 2012-08-23T00:00:00Z
date_updated: 2023-02-23T12:23:51Z
day: '23'
department:
- _id: KrCh
doi: 10.1109/LICS.2012.29
ec_funded: 1
external_id:
  arxiv:
  - '1107.2091'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1107.2091
month: '08'
oa: 1
oa_version: Preprint
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer
  Science
publication_status: published
publisher: IEEE
publist_id: '3769'
quality_controlled: '1'
related_material:
  record:
  - id: '5384'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Decidable problems for probabilistic automata on infinite words
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '3363'
abstract:
- lang: eng
  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.
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  ama: Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic
    automata on infinite words.
  apa: Chatterjee, K., Henzinger, T. A., &#38; Tracol, M. (n.d.). The decidability
    frontier for probabilistic automata on infinite words. ArXiv.
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Mathieu Tracol. “The Decidability
    Frontier for Probabilistic Automata on Infinite Words.” ArXiv, n.d.
  ieee: K. Chatterjee, T. A. Henzinger, and M. Tracol, “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.
  mla: Chatterjee, Krishnendu, et al. <i>The Decidability Frontier for Probabilistic
    Automata on Infinite Words</i>. ArXiv.
  short: K. Chatterjee, T.A. Henzinger, M. Tracol, (n.d.).
date_created: 2018-12-11T12:02:54Z
date_published: 2011-04-01T00:00:00Z
date_updated: 2020-01-21T13:20:24Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
ec_funded: 1
external_id:
  arxiv:
  - '1104.0127'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1104.0127
month: '04'
oa: 1
oa_version: Preprint
page: '19'
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
publication_status: submitted
publisher: ArXiv
publist_id: '3251'
status: public
title: The decidability frontier for probabilistic automata on infinite words
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5384'
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.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  ama: Chatterjee K, Tracol M. <i>Decidable Problems for Probabilistic Automata on
    Infinite Words</i>. IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0004">10.15479/AT:IST-2011-0004</a>
  apa: Chatterjee, K., &#38; Tracol, M. (2011). <i>Decidable problems for probabilistic
    automata on infinite words</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0004">https://doi.org/10.15479/AT:IST-2011-0004</a>
  chicago: Chatterjee, Krishnendu, and Mathieu Tracol. <i>Decidable Problems for Probabilistic
    Automata on Infinite Words</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0004">https://doi.org/10.15479/AT:IST-2011-0004</a>.
  ieee: K. Chatterjee and M. Tracol, <i>Decidable problems for probabilistic automata
    on infinite words</i>. IST Austria, 2011.
  ista: Chatterjee K, Tracol M. 2011. Decidable problems for probabilistic automata
    on infinite words, IST Austria, 30p.
  mla: Chatterjee, Krishnendu, and Mathieu Tracol. <i>Decidable Problems for Probabilistic
    Automata on Infinite Words</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0004">10.15479/AT:IST-2011-0004</a>.
  short: K. Chatterjee, M. Tracol, Decidable Problems for Probabilistic Automata on
    Infinite Words, IST Austria, 2011.
date_created: 2018-12-12T11:39:01Z
date_published: 2011-04-11T00:00:00Z
date_updated: 2023-02-23T11:05:53Z
day: '11'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0004
file:
- access_level: open_access
  checksum: f5a0f664fadc335990f5fcf138df19f1
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:54:23Z
  date_updated: 2020-07-14T12:46:40Z
  file_id: '5545'
  file_name: IST-2011-004_IST-2011-0004.pdf
  file_size: 570827
  relation: main_file
file_date_updated: 2020-07-14T12:46:40Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '30'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '20'
related_material:
  record:
  - id: '2957'
    relation: later_version
    status: public
status: public
title: Decidable problems for probabilistic automata on infinite words
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...