Abstract
Weighted automata map input words to numerical values. Applications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing.
In the 90’s, Krob studied the decidability of problems on rational series, which strongly relate to weighted automata. In particular, it follows from Krob’s results that the universality problem (that is, deciding whether the values of all words are below some threshold) is decidable for weighted automata with weights in ℕ ∪ { ∞ }, and that the equality problem is undecidable when the weights are in ℤ ∪ { ∞ }.
In this paper we continue the study of the borders of decidability in weighted automata, describe alternative and direct proofs of the above results, and tighten them further. Unlike the proofs of Krob, which are algebraic in their nature, our proofs stay in the terrain of state machines, and the reduction is from the halting problem of a two-counter machine. This enables us to significantly simplify Krob’s reasoning and strengthen the results to apply already to a very simple class of automata: all the states are accepting, there are no initial nor final weights, and all the weights are from the set { − 1,0,1}. The fact we work directly with automata enables us to tighten also the decidability results and to show that the universality problem for weighted automata with weights in ℕ ∪ { ∞ }, and in fact even with weights in ℚ ≥ 0 ∪ { ∞ }, is PSPACE-complete. Our results thus draw a sharper picture about the decidability of decision problems for weighted automata, in both the front of equality vs. universality and the front of the ℕ ∪ { ∞ } vs. the ℤ ∪ { ∞ } domains.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Boker, U., Henzinger, T.A.: Determinizing discounted-sum automata. In: Proc. 20th Annual Conf. for Computer Science Logic (2011)
Chatterjee, K., Doyen, L., Henzinger, T.: Quantative languages. In: Proc. 17th Annual Conf. for Computer Science Logic, pp. 385–400 (2008)
Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. Logical Methods in Computer Science 6(3) (2010)
Degorre, A., Doyen, L., Gentilini, R., Raskin, J., Torunczyk, S.: Energy and mean-payoff games with imperfect information. In: Proc. 19th Annual Conf. for Computer Science Logic, pp. 260–274 (2010)
Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer, Heidelberg (2009)
Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. of Algebra and Computation 4(3), 405–425 (1994)
Krob, D.: Some consequences of a fatou property of the tropical semiring. Journal of Pure and Appllied Algebra 93(3), 231–249 (1994)
Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential time. In: Proc. 13th IEEE Symp. on Switching and Automata Theory, pp. 125–129 (1972)
Minsky, M.L.: Computation: Finite and Infinite Machines, 1st edn. (1967)
Simon, I.: Recognizable sets with multiplicitives in the tropical semiring. In: Koubek, V., Janiga, L., Chytil, M.P. (eds.) MFCS 1988. LNCS, vol. 324, pp. 107–120. Springer, Heidelberg (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Almagor, S., Boker, U., Kupferman, O. (2011). What’s Decidable about Weighted Automata?. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_37
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)