---
res:
  bibo_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.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Shaull
      foaf_name: Almagor, Shaull
      foaf_surname: Almagor
  - foaf_Person:
      foaf_givenName: Udi
      foaf_name: Boker, Udi
      foaf_surname: Boker
      foaf_workInfoHomepage: http://www.librecat.org/personId=31E297B6-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Orna
      foaf_name: Kupferman, Orna
      foaf_surname: Kupferman
  bibo_doi: 10.1007/978-3-642-24372-1_37
  bibo_volume: 6996
  dct_date: 2011^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: What’s decidable about weighted automata@
...