---
_id: '14405'
abstract:
- lang: eng
  text: We introduce hypernode automata as a new specification formalism for hyperproperties
    of concurrent systems. They are finite automata with nodes labeled with hypernode
    logic formulas and transitions labeled with actions. A hypernode logic formula
    specifies relations between sequences of variable values in different system executions.
    Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces
    by constraining the values and the order of value changes of each variable without
    correlating the timing of the changes. Different execution traces are synchronized
    solely through the transitions of hypernode automata. Hypernode automata naturally
    combine asynchronicity at the node level with synchronicity at the transition
    level. We show that the model-checking problem for hypernode automata is decidable
    over action-labeled Kripke structures, whose actions induce transitions of the
    specification automata. For this reason, hypernode automaton is a suitable formalism
    for specifying and verifying asynchronous hyperproperties, such as declassifying
    observational determinism in multi-threaded programs.
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)
  SFB project\r\nSpyCoDe F8502, by the FWF projects ZK-35 and W1255-N23, and by the
  ERC Advanced Grant\r\nVAMOS 101020093."
alternative_title:
- LIPIcs
article_number: '21'
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Ezio
  full_name: Bartocci, Ezio
  last_name: Bartocci
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Dejan
  full_name: Nickovic, Dejan
  id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
  last_name: Nickovic
- first_name: Ana
  full_name: Oliveira da Costa, Ana
  id: f347ec37-6676-11ee-b395-a888cb7b4fb4
  last_name: Oliveira da Costa
  orcid: 0000-0002-8741-5799
citation:
  ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata.
    In: <i>34th International Conference on Concurrency Theory</i>. Vol 279. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.21">10.4230/LIPIcs.CONCUR.2023.21</a>'
  apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A.
    (2023). Hypernode automata. In <i>34th International Conference on Concurrency
    Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.21">https://doi.org/10.4230/LIPIcs.CONCUR.2023.21</a>'
  chicago: Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
    Costa. “Hypernode Automata.” In <i>34th International Conference on Concurrency
    Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
    <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.21">https://doi.org/10.4230/LIPIcs.CONCUR.2023.21</a>.
  ieee: E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode
    automata,” in <i>34th International Conference on Concurrency Theory</i>, Antwerp,
    Belgium, 2023, vol. 279.
  ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2023. Hypernode
    automata. 34th International Conference on Concurrency Theory. CONCUR: Conference
    on Concurrency Theory, LIPIcs, vol. 279, 21.'
  mla: Bartocci, Ezio, et al. “Hypernode Automata.” <i>34th International Conference
    on Concurrency Theory</i>, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik, 2023, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.21">10.4230/LIPIcs.CONCUR.2023.21</a>.
  short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, 34th
    International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2023.
conference:
  end_date: 2023-09-22
  location: Antwerp, Belgium
  name: 'CONCUR: Conference on Concurrency Theory'
  start_date: 2023-09-19
date_created: 2023-10-08T22:01:16Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2023-10-09T07:43:44Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.21
ec_funded: 1
external_id:
  arxiv:
  - '2305.02836'
file:
- access_level: open_access
  checksum: 215765e40454d806174ac0a223e8d6fa
  content_type: application/pdf
  creator: dernst
  date_created: 2023-10-09T07:42:45Z
  date_updated: 2023-10-09T07:42:45Z
  file_id: '14413'
  file_name: 2023_LIPcs_Bartocci.pdf
  file_size: 795790
  relation: main_file
  success: 1
file_date_updated: 2023-10-09T07:42:45Z
has_accepted_license: '1'
intvolume: '       279'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 34th International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - '9783959772990'
  issn:
  - '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Hypernode automata
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 279
year: '2023'
...
---
_id: '13221'
abstract:
- lang: eng
  text: 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.
acknowledgement: We thank Christof Löding for pointing us to some results on PSpace-hardess
  of universality problems and the anonymous reviewers for their helpful comments.
  This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science
  Foundation grant 2410/22.
alternative_title:
- LIPIcs
article_number: '17'
article_processing_charge: No
arxiv: 1
author:
- first_name: Udi
  full_name: Boker, Udi
  id: 31E297B6-F248-11E8-B48F-1D18A9856A87
  last_name: Boker
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
  full_name: Mazzocchi, Nicolas Adrien
  id: b26baa86-3308-11ec-87b0-8990f34baa85
  last_name: Mazzocchi
- first_name: Naci E
  full_name: Sarac, Naci E
  id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  last_name: Sarac
citation:
  ama: 'Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative
    automata. In: <i>34th International Conference on Concurrency Theory</i>. Vol
    279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.17">10.4230/LIPIcs.CONCUR.2023.17</a>'
  apa: 'Boker, U., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023).
    Safety and liveness of quantitative automata. In <i>34th International Conference
    on Concurrency Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.17">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>'
  chicago: Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac.
    “Safety and Liveness of Quantitative Automata.” In <i>34th International Conference
    on Concurrency Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2023. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.17">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>.
  ieee: U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness
    of quantitative automata,” in <i>34th International Conference on Concurrency
    Theory</i>, Antwerp, Belgium, 2023, vol. 279.
  ista: 'Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness
    of quantitative automata. 34th International Conference on Concurrency Theory.
    CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17.'
  mla: Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” <i>34th
    International Conference on Concurrency Theory</i>, vol. 279, 17, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2023, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2023.17">10.4230/LIPIcs.CONCUR.2023.17</a>.
  short: U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 34th International
    Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2023.
conference:
  end_date: 2023-09-23
  location: Antwerp, Belgium
  name: 'CONCUR: Conference on Concurrency Theory'
  start_date: 2023-09-18
date_created: 2023-07-14T10:00:15Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2023-10-09T07:14:03Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.17
ec_funded: 1
external_id:
  arxiv:
  - '2307.06016'
file:
- access_level: open_access
  checksum: d40e57a04448ea5c77d7e1cfb9590a81
  content_type: application/pdf
  creator: esarac
  date_created: 2023-07-14T12:03:48Z
  date_updated: 2023-07-14T12:03:48Z
  file_id: '13224'
  file_name: CONCUR23.pdf
  file_size: 755529
  relation: main_file
  success: 1
file_date_updated: 2023-07-14T12:03:48Z
has_accepted_license: '1'
intvolume: '       279'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 34th International Conference on Concurrency Theory
publication_identifier:
  eissn:
  - 1868-8969
  isbn:
  - '9783959772990'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
status: public
title: Safety and liveness of quantitative automata
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 279
year: '2023'
...