What’s decidable about weighted automata

S. Almagor, U. Boker, O. Kupferman, in:, T. Bultan, P.-A. Hsiung (Eds.), Springer, 2011, pp. 482–491.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English
Author
; ;
Editor
;
Department
Series Title
LNCS
Abstract
Weighted automata map input words to numerical values. Ap- plications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. A weighted au- tomaton is defined with respect to a semiring. For the tropical semiring, the weight of a run is the sum of the weights of the transitions taken along the run, and the value of a word is the minimal weight of an accepting run on it. In the 90’s, Krob studied the decidability of problems on rational series defined with respect to the tropical semiring. Rational series are strongly related to weighted automata, and Krob’s results apply to them. In par- ticular, 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 defined with respect to the tropical semir- ing with domain ∪ {∞}, and that the equality problem is undecidable when the domain is ∪ {∞}. 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, make the un- decidability result accessible to the automata-theoretic community, and strengthen it 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 on the transitions are from the set {−1, 0, 1}. The fact we work directly with the automata enables us to tighten also the decidability re- sults and to show that the universality problem for weighted automata defined with respect to the tropical semiring with domain ∪ {∞}, and in fact even with domain ≥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 containment vs. universality and the front of the ∪ {∞} vs. the ∪ {∞} domains.
Publishing Year
Date Published
2011-10-14
Volume
6996
Page
482 - 491
Conference
ATVA: Automated Technology for Verification and Analysis
Conference Location
Taipei, Taiwan
Conference Date
2011-10-11 – 2011-10-14
IST-REx-ID

Cite this

Almagor S, Boker U, Kupferman O. What’s decidable about weighted automata . In: Bultan T, Hsiung P-A, eds. Vol 6996. Springer; 2011:482-491. doi:10.1007/978-3-642-24372-1_37
Almagor, S., Boker, U., & Kupferman, O. (2011). What’s decidable about weighted automata . In T. Bultan & P.-A. Hsiung (Eds.) (Vol. 6996, pp. 482–491). Presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan: Springer. https://doi.org/10.1007/978-3-642-24372-1_37
Almagor, Shaull, Udi Boker, and Orna Kupferman. “What’s Decidable about Weighted Automata .” edited by Tevfik Bultan and Pao-Ann Hsiung, 6996:482–91. Springer, 2011. https://doi.org/10.1007/978-3-642-24372-1_37.
S. Almagor, U. Boker, and O. Kupferman, “What’s decidable about weighted automata ,” presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan, 2011, vol. 6996, pp. 482–491.
Almagor S, Boker U, Kupferman O. 2011. What’s decidable about weighted automata . ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 6996. 482–491.
Almagor, Shaull, et al. What’s Decidable about Weighted Automata . Edited by Tevfik Bultan and Pao-Ann Hsiung, vol. 6996, Springer, 2011, pp. 482–91, doi:10.1007/978-3-642-24372-1_37.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar