License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.17
URN: urn:nbn:de:0030-drops-190118
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19011/
Go to the corresponding LIPIcs Volume Portal

Boker, Udi ; Henzinger, Thomas A. ; Mazzocchi, Nicolas ; Saraç, N. Ege

Safety and Liveness of Quantitative Automata

pdf-format:
LIPIcs-CONCUR-2023-17.pdf (0.8 MB)

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 totally-ordered 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.

BibTeX - Entry

@InProceedings{boker_et_al:LIPIcs.CONCUR.2023.17,
  author =	{Boker, Udi and Henzinger, Thomas A. and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Safety and Liveness of Quantitative Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19011},
  URN =		{urn:nbn:de:0030-drops-190118},
  doi =		{10.4230/LIPIcs.CONCUR.2023.17},
  annote =	{Keywords: quantitative safety, quantitative liveness, quantitative automata}
}

Keywords: quantitative safety, quantitative liveness, quantitative automata
Collection: 34th International Conference on Concurrency Theory (CONCUR 2023)
Issue Date: 2023
Date of publication: 07.09.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI