---
res:
  bibo_abstract:
  - The safety-liveness dichotomy is a fundamental concept in formal languages which
    plays a key role in verification. Recently, this dichotomy has been lifted to
    quantitative properties, which are arbitrary functions from infinite words to
    partially-ordered domains. We look into harnessing the dichotomy for the specific
    classes of quantitative properties expressed by quantitative automata. These automata
    contain finitely many states and rational-valued transition weights, and their
    common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum
    map infinite words into the totallyordered domain of real numbers. In this automata-theoretic
    setting, we establish a connection between quantitative safety and topological
    continuity and provide an alternative characterization of quantitative safety
    and liveness in terms of their boolean counterparts. For all common value functions,
    we show how the safety closure of a quantitative automaton can be constructed
    in PTime, and we provide PSpace-complete checks of whether a given quantitative
    automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata,
    for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf,
    and LimSup automata, we give PTime decompositions into safe and live automata.
    These decompositions enable the separation of techniques for safety and liveness
    verification for quantitative specifications.@eng
  bibo_authorlist:
  - 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: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-2985-7724
  - foaf_Person:
      foaf_givenName: Nicolas Adrien
      foaf_name: Mazzocchi, Nicolas Adrien
      foaf_surname: Mazzocchi
      foaf_workInfoHomepage: http://www.librecat.org/personId=b26baa86-3308-11ec-87b0-8990f34baa85
  - foaf_Person:
      foaf_givenName: Naci E
      foaf_name: Sarac, Naci E
      foaf_surname: Sarac
      foaf_workInfoHomepage: http://www.librecat.org/personId=8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  bibo_doi: 10.4230/LIPIcs.CONCUR.2023.17
  bibo_volume: 279
  dct_date: 2023^xs_gYear
  dct_identifier:
  - UT:001570542500017
  dct_isPartOf:
  - http://id.crossref.org/issn/1868-8969
  - http://id.crossref.org/issn/9783959772990
  dct_language: eng
  dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
  dct_title: Safety and liveness of quantitative automata@
...