Non-deterministic weighted automata evaluated over Markov chains. (English) Zbl 1436.68182
Summary: We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We consider the probabilistic questions of computing the expected value and the cumulative distribution for such random variables.
The exact answers to the probabilistic questions for non-deterministic automata can be irrational and are uncomputable in general. To overcome this limitation, we propose approximation algorithms for the probabilistic questions, which work in exponential time in the size of the automaton and polynomial time in the size of the Markov chain and the given precision. We apply this result to show that non-deterministic automata can be effectively determinised with respect to the standard deviation metric.
The exact answers to the probabilistic questions for non-deterministic automata can be irrational and are uncomputable in general. To overcome this limitation, we propose approximation algorithms for the probabilistic questions, which work in exponential time in the size of the automaton and polynomial time in the size of the Markov chain and the given precision. We apply this result to show that non-deterministic automata can be effectively determinised with respect to the standard deviation metric.
MSC:
| 68Q45 | Formal languages and automata |
| 60J20 | Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 68W25 | Approximation algorithms |
| 68W40 | Analysis of algorithms |
Software:
PRISMReferences:
| [1] | Almagor, S.; Boker, U.; Kupferman, O., What’s decidable about weighted automata?, (ATVA. LNCS, vol. 6996 (2011), Springer), 482-491 · Zbl 1348.68089 |
| [2] | Aminof, B.; Kupferman, O.; Lampert, R., Reasoning about online algorithms with weighted automata, ACM Trans. Algorithms, 6, 2, 28 (2010) · Zbl 1300.68071 |
| [3] | Astrom, K. J., Optimal control of Markov processes with incomplete state information, J. Math. Anal. Appl., 10, 1, 174-205 (1965) · Zbl 0137.35803 |
| [4] | Baier, C.; Katoen, J., Principles of Model Checking (2008), MIT Press · Zbl 1179.68076 |
| [5] | Baier, C.; Kiefer, S.; Klein, J.; Klüppelholz, S.; Müller, D.; Worrell, J., Markov chains and unambiguous büchi automata, (CAV 2016 (2016), Springer), 23-42 · Zbl 1411.68051 |
| [6] | Benedikt, M.; Puppis, G.; Riveros, C., Regular repair of specifications, (LICS 2011 (2011)), 335-344 |
| [7] | Bertoni, A.; Mauri, G.; Torelli, M., Some recursively unsolvable problems relating to isolated cutpoints in probabilistic automata, (ICALP (1977), Springer), 87-94 · Zbl 0366.94064 |
| [8] | Billingsley, P., Convergence of Probability Measures (2013), John Wiley & Sons · Zbl 0172.21201 |
| [9] | Boker, U.; Henzinger, T. A., Approximate determinization of quantitative automata, (FSTTCS 2012 (2012), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 362-373 · Zbl 1354.68147 |
| [10] | Chatterjee, K.; Doyen, L.; Henzinger, T. A., A survey of stochastic games with limsup and liminf objectives, (ICALP 2009 (2009)), 1-15 · Zbl 1248.91015 |
| [11] | Chatterjee, K.; Doyen, L.; Henzinger, T. A., Quantitative languages, ACM Trans. Comput. Log., 11, 23 (2010) · Zbl 1351.68155 |
| [12] | Chatterjee, K.; Henzinger, T. A.; Otop, J., Quantitative automata under probabilistic semantics, (LICS 2016 (2016), ACM), 76-85 · Zbl 1401.68155 |
| [13] | Chatterjee, K.; Randour, M.; Raskin, J., Strategy synthesis for multi-dimensional quantitative objectives, (CONCUR 2012 (2012)), 115-131 · Zbl 1364.68278 |
| [14] | Clarke, E.; Henzinger, T.; Veith, H., Handbook of Model Checking (2016), Springer International Publishing |
| [15] | Courcoubetis, C.; Yannakakis, M., The complexity of probabilistic verification, J. ACM, 42, 4, 857-907 (1995) · Zbl 0885.68109 |
| [16] | Droste, M.; Kuich, W.; Vogler, H., Handbook of Weighted Automata (2009), Springer · Zbl 1200.68001 |
| [17] | Feller, W., An Introduction to Probability Theory and Its Applications (1971), Wiley · Zbl 0219.60003 |
| [18] | Filar, J.; Vrieze, K., Competitive Markov Decision Processes (1996), Springer |
| [19] | Grinstead, C. M.; Snell, J. L., Introduction to Probability (2012), Amer. Math. Soc. |
| [20] | Gupta, A.; Popeea, C.; Rybalchenko, A., Predicate abstraction and refinement for verifying multi-threaded programs, (POPL 2011 (2011)), 331-344 · Zbl 1284.68427 |
| [21] | Henzinger, T. A.; Otop, J., Model measuring for discrete and hybrid systems, Nonlinear Anal. Hybrid Syst., 23, 166-190 (2017) · Zbl 1401.68198 |
| [22] | Hinton, A.; Kwiatkowska, M. Z.; Norman, G.; Parker, D., PRISM: a tool for automatic verification of probabilistic systems, (TACAS 2006 (2006)), 441-444 |
| [23] | Hopcroft, J. E.; Ullman, J. D., Introduction to Automata Theory, Languages, and Computation (1979), Adison-Wesley Publishing Company: Adison-Wesley Publishing Company Reading, Massachusets, USA · Zbl 0426.68001 |
| [24] | Kechris, A., Classical Descriptive Set Theory, vol. 156 (2012), Springer Science & Business Media |
| [25] | Krob, D., The equality problem for rational series with multiplicities in the tropical semiring is undecidable, Int. J. Algebra Comput., 4, 3, 405-426 (1994) · Zbl 0834.68058 |
| [26] | Kwiatkowska, M. Z.; Norman, G.; Parker, D., Quantitative analysis with the probabilistic model checker PRISM, Electron. Notes Theor. Comput. Sci., 153, 2, 5-31 (2006) |
| [27] | Michaliszyn, J.; Otop, J., Non-deterministic weighted automata on random words, (CONCUR 2018 (2018)), Article 10 pp. · Zbl 1520.68064 |
| [28] | Papadimitriou, C. H., Computational Complexity (2003), Wiley · Zbl 0557.68033 |
| [29] | Randour, M.; Raskin, J.; Sankur, O., Percentile queries in multi-dimensional Markov decision processes, (CAV 2015 (2015)), 123-139 · Zbl 1381.68219 |
| [30] | Roth, K. F., Rational approximations to algebraic numbers, Mathematika, 2, 1, 1-20 (1955) · Zbl 0064.28501 |
| [31] | Valiant, L. G., The complexity of computing the permanent, Theor. Comput. Sci., 8, 2, 189-201 (1979) · Zbl 0415.68008 |
| [32] | van Heerdt, G.; Hsu, J.; Ouaknine, J.; Silva, A., Convex language semantics for nondeterministic probabilistic automata, (ICTAC 2018 (2018)), 472-492 · Zbl 1518.68192 |
| [33] | Vardi, M. Y., Automatic verification of probabilistic concurrent finite-state programs, (FOCS 1985 (1985), IEEE Computer Society), 327-338 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
