Decidable and expressive classes of probabilistic automata.

*(English)*Zbl 1439.68011The contribution discusses the expressive power of certain
probabilistic automata. A probabilistic automaton is essentially a
(potentially nondeterministic) finite-state automaton whose
transitions carry a probability such that the probabilities of all
transitions that leave a state by a given symbol sum to \(1\). The
probability of a sequence of transitions is simply the product of the
individual transition probabilities, and the probability of an input
word is the sum of the probabilities of transition sequences for the
input word. An input word is accepted by the automaton if its
probability exceeds a given threshold (mostly 0.5 in the paper).
Probabilistic automata are still very expressive and most problems
remain undecidable for them. To this end, the contribution considers
\(k\)-hierarchical probabilistic automata, in which the states are
partitioned into \(k+1\) classes such that for each state \(q\) in class
\(i\), all transitions leaving the state go to states of class \(i\) or
higher. In addition, for each input symbol only a single transition
for that symbol leaving \(q\) can lead to a state of the same class \(i\).

It is demonstrated that \(1\)-hierarchical probabilistic automata can still recognize non-regular languages, but their non-emptiness as well as non-universality problems are decidable and shown to be in EXPTIME as well as PSPACE-hard. Already for \(2\)-hierarchical probabilistic automata, the emptiness problem becomes undecidable, which is also shown in the contribution. Finally, a new sufficient condition is presented that, provided that a \(1\)-hierarchical probabilistic automaton fulfills it, then its accepted language is guaranteed to be regular.

The paper is excellently written and contains examples and illustrations. Proof details are provided for all major claims and those proofs are easily understandable and well presented. Overall, anyone with some background knowledge in automata theory as well as a primer in complexity theory can appreciate the contribution fully.

It is demonstrated that \(1\)-hierarchical probabilistic automata can still recognize non-regular languages, but their non-emptiness as well as non-universality problems are decidable and shown to be in EXPTIME as well as PSPACE-hard. Already for \(2\)-hierarchical probabilistic automata, the emptiness problem becomes undecidable, which is also shown in the contribution. Finally, a new sufficient condition is presented that, provided that a \(1\)-hierarchical probabilistic automaton fulfills it, then its accepted language is guaranteed to be regular.

The paper is excellently written and contains examples and illustrations. Proof details are provided for all major claims and those proofs are easily understandable and well presented. Overall, anyone with some background knowledge in automata theory as well as a primer in complexity theory can appreciate the contribution fully.

Reviewer: Andreas Maletti (Leipzig)

##### MSC:

68Q45 | Formal languages and automata |

68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |

##### Keywords:

hierarchical probabilistic automata; regular languages; decidability; emptiness problem; universality problem
PDF
BibTeX
XML
Cite

\textit{Y. Ben} et al., J. Comput. Syst. Sci. 100, 70--95 (2019; Zbl 1439.68011)

Full Text:
DOI

##### References:

[1] | Rabin, M. O., Probabilistic automata, Inf. Control, 6, 3, 230-245, (1963) · Zbl 0182.33602 |

[2] | Paz, A., Introduction to Probabilistic Automata, (1971), Academic Press · Zbl 0234.94055 |

[3] | Baier, C.; Größer, M., Recognizing ω-regular languages with probabilistic automata, (20th IEEE Symp. on Logic in Computer Science, (2005)), 137-146 |

[4] | Größer, M., Reduction Methods for Probabilistic Model Checking, (2008), TU Dresden, Ph.D. thesis |

[5] | Chatterjee, K.; Henzinger, T. A., Probabilistic automata on infinite words: decidability and undecidability results, (Intl. Symp. on Automated Technology for Verification and Analysis, (2010)), 1-16 · Zbl 1305.68112 |

[6] | Chadha, R.; Sistla, A. P.; Viswanathan, M., Power of randomization in automata on infinite strings, Log. Methods Comput. Sci., 7, 3, 1-22, (2011) · Zbl 1237.68111 |

[7] | Fijalkow, N.; Gimbert, H.; Oualhadj, Y., Deciding the value 1 problem for probabilistic leaktight automata, (IEEE Symp. on Logic in Computer Science, (2012)), 295-304 · Zbl 1360.68553 |

[8] | Fijalkow, N.; Gimbert, H.; Kelmendi, E.; Oualhadj, Y., Deciding the value 1 problem for probabilistic leaktight automata, Log. Methods Comput. Sci., 11, 2, (2015) · Zbl 1391.68081 |

[9] | Gimbert, H.; Oualhadj, Y., Probabilistic automata on finite words: decidable and undecidable problems, (Intl. Colloquium on Automata, Languages and Programming, (2010)), 527-538 · Zbl 1288.68156 |

[10] | Chadha, R.; Sistla, A. P.; Viswanathan, M., Probabilistic Büchi automata with non-extremal acceptance thresholds, (Intl. Conference on Verification, Model checking and Abstract Interpretation, (2010)), 103-117 · Zbl 1317.68091 |

[11] | Baier, C.; Größer, M.; Bertrand, N., Probabilistic ω-automata, J. ACM, 59, 1, 1-52, (2012) · Zbl 1281.68152 |

[12] | Condon, A.; Lipton, R. J., On the complexity of space bounded interactive proofs (extended abstract), (Symp. on Foundations of Computer Science, (1989)), 462-467 |

[13] | Chadha, R.; Sistla, A. P.; Viswanathan, M.; Ben, Y., Decidable and expressive classes of probabilistic automata, (16th International Conference on Foundations of Software Science and Computation Structures, Lect. Notes Comput. Sci., vol. 9034, (2015), Springer), 200-214 · Zbl 06487993 |

[14] | Ben, Y.; Sistla, A. P., Model checking failure-prone open systems using probabilistic automata, (13th International Symposium on Automated Technology for Verification and Analysis, Lect. Notes Comput. Sci., vol. 9364, (2015), Springer), 148-165 · Zbl 06527547 |

[15] | Vardi, M., Automatic verification of probabilistic concurrent finite-state programs, (Symp. on Foundations of Computer Science, (1985)), 327-338 |

[16] | Kemeny, J.; Snell, J., Denumerable Markov Chains, (1976), Springer-Verlag · Zbl 0348.60090 |

[17] | Chadha, R.; Sistla, A. P.; Viswanathan, M., On the expressiveness and complexity of randomization in finite state monitors, J. ACM, 56, 5, (2009) · Zbl 1325.68128 |

[18] | Kozen, D., Lower bounds for natural proof systems, (18th Annual Symposium on Foundations of Computer Science, 31 October - 1 November 1977, Providence, Rhode Island, USA, (1977), IEEE Computer Society), 254-266 |

[19] | Wagner, K. W., Some observations on the connection between counting and recursion, Theor. Comput. Sci., 47, 3, 131-147, (1986) · Zbl 0637.03034 |

[20] | Chadha, R.; Kini, D.; Viswanathan, M., Decidable problems for unary pfas, (11th International Conference on Quantitative Evaluation of Systems, Lect. Notes Comput. Sci., vol. 8657, (2014), Springer), 329-344 |

[21] | Courcoubetis, C.; Yannakakis, M., The complexity of probabilistic verification, J. ACM, 42, 4, 857-907, (1995) · Zbl 0885.68109 |

[22] | Chadha, R.; Sistla, A.; Viswanathan, M., Power of randomization in automata on infinite strings, Log. Methods Comput. Sci., 7, 3, (2011) · Zbl 1237.68111 |

[23] | Baier, C.; Bertrand, N.; Größer, M., On Decision Problems for Probabilistic Büchi Automata, 287-301, (2008), FoSSaCS · Zbl 1139.68030 |

[24] | Chatterjee, K.; Tracol, M., Decidable problems for probabilistic automata on infinite words, (2012 27th Annual IEEE Symposium on Logic in Computer Science, (2012)), 185-194 · Zbl 1360.68546 |

[25] | Fijalkow, N.; Riveros, C.; Worrell, J., Probabilistic automata of bounded ambiguity, (28th International Conference on Concurrency Theory, CONCUR 2017, LIPIcs, vol. 85, (2017), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 19:1-19:14 |

[26] | Bertoni, A., The solution of problems relative to probabilistic automata in the frame of the formal languages theory, (GI Jahrestagung, (1974)), 107-112 |

[27] | Chadha, R.; Sistla, A.; Viswanathan, M., Probabilistic automata with isolated cut-points, (Proceedings of the International Symposium on Mathematical Foundation of Computer Science, (2013)), 254-265 · Zbl 1398.68304 |

[28] | Chadha, R.; Sistla, A. P.; Viswanathan, M., Emptiness under isolation and the value problem for hierarchical probabilistic automata, (Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Lect. Notes Comput. Sci., vol. 10203, (2017)), 231-247 · Zbl 06720993 |

[29] | Biscaia, M.; Henriques, D.; Mateus, P., Decidability of approximate skolem problem and applications to logical verification of dynamical properties of markov chains, ACM Trans. Comput. Log., 16, 1, 4:1-4:17, (2014) · Zbl 1354.68168 |

[30] | Akshay, S.; Antonopoulos, T.; Ouaknine, J.; Worrell, J., Reachability problems for Markov chains, Inf. Process. Lett., 115, 2, 155-158, (2015) · Zbl 1302.68204 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.