---
_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'
...
---
_id: '13292'
abstract:
- lang: eng
  text: The operator precedence languages (OPLs) represent the largest known subclass
    of the context-free languages which enjoys all desirable closure and decidability
    properties. This includes the decidability of language inclusion, which is the
    ultimate verification problem. Operator precedence grammars, automata, and logics
    have been investigated and used, for example, to verify programs with arithmetic
    expressions and exceptions (both of which are deterministic pushdown but lie outside
    the scope of the visibly pushdown languages). In this paper, we complete the picture
    and give, for the first time, an algebraic characterization of the class of OPLs
    in the form of a syntactic congruence that has finitely many equivalence classes
    exactly for the operator precedence languages. This is a generalization of the
    celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of
    the consequences, we show that universality and language inclusion for nondeterministic
    operator precedence automata can be solved by an antichain algorithm. Antichain
    algorithms avoid determinization and complementation through an explicit subset
    construction, by leveraging a quasi-order on words, which allows the pruning of
    the search space for counterexample words without sacrificing completeness. Antichain
    algorithms can be implemented symbolically, and these implementations are today
    the best-performing algorithms in practice for the inclusion of finite automata.
    We give a generic construction of the quasi-order needed for antichain algorithms
    from a finite syntactic congruence. This yields the first antichain algorithm
    for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem
    for OPLs in exponential time.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe
  thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful
  comments.\r\n"
alternative_title:
- LIPIcs
article_processing_charge: Yes
arxiv: 1
author:
- 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: Pavol
  full_name: Kebis, Pavol
  last_name: Kebis
- 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: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator
    precedence languages. In: <i>50th International Colloquium on Automata, Languages,
    and Programming</i>. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
    2023:129:1--129:20. doi:<a href="https://doi.org/10.4230/LIPIcs.ICALP.2023.129">10.4230/LIPIcs.ICALP.2023.129</a>'
  apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., &#38; Sarac, N. E. (2023).
    Regular methods for operator precedence languages. In <i>50th International Colloquium
    on Automata, Languages, and Programming</i> (Vol. 261, p. 129:1--129:20). Paderborn,
    Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.ICALP.2023.129">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>'
  chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E
    Sarac. “Regular Methods for Operator Precedence Languages.” In <i>50th International
    Colloquium on Automata, Languages, and Programming</i>, 261:129:1--129:20. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href="https://doi.org/10.4230/LIPIcs.ICALP.2023.129">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>.
  ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods
    for operator precedence languages,” in <i>50th International Colloquium on Automata,
    Languages, and Programming</i>, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.
  ista: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for
    operator precedence languages. 50th International Colloquium on Automata, Languages,
    and Programming. ICALP: International Colloquium on Automata, Languages, and Programming,
    LIPIcs, vol. 261, 129:1--129:20.'
  mla: Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.”
    <i>50th International Colloquium on Automata, Languages, and Programming</i>,
    vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20,
    doi:<a href="https://doi.org/10.4230/LIPIcs.ICALP.2023.129">10.4230/LIPIcs.ICALP.2023.129</a>.
  short: T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International
    Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2023, p. 129:1--129:20.
conference:
  end_date: 2023-07-14
  location: Paderborn, Germany
  name: 'ICALP: International Colloquium on Automata, Languages, and Programming'
  start_date: 2023-07-10
date_created: 2023-07-24T15:11:41Z
date_published: 2023-07-05T00:00:00Z
date_updated: 2023-07-31T08:38:38Z
day: '05'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.4230/LIPIcs.ICALP.2023.129
ec_funded: 1
external_id:
  arxiv:
  - '2305.03447'
file:
- access_level: open_access
  checksum: 5d4c8932ef3450615a53b9bb15d92eb2
  content_type: application/pdf
  creator: esarac
  date_created: 2023-07-24T15:11:05Z
  date_updated: 2023-07-24T15:11:05Z
  file_id: '13293'
  file_name: icalp23.pdf
  file_size: 859379
  relation: main_file
  success: 1
file_date_updated: 2023-07-24T15:11:05Z
has_accepted_license: '1'
intvolume: '       261'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 129:1--129:20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 50th International Colloquium on Automata, Languages, and Programming
publication_identifier:
  eissn:
  - 1868-8969
  isbn:
  - '9783959772785'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
status: public
title: Regular methods for operator precedence languages
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: 261
year: '2023'
...
---
_id: '12467'
abstract:
- lang: eng
  text: Safety and liveness are elementary concepts of computation, and the foundation
    of many verification paradigms. The safety-liveness classification of boolean
    properties characterizes whether a given property can be falsified by observing
    a finite prefix of an infinite computation trace (always for safety, never for
    liveness). In quantitative specification and verification, properties assign not
    truth values, but quantitative values to infinite traces (e.g., a cost, or the
    distance to a boolean property). We introduce quantitative safety and liveness,
    and we prove that our definitions induce conservative quantitative generalizations
    of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness
    decomposition of boolean properties. In particular, we show that every quantitative
    property can be written as the pointwise minimum of a quantitative safety property
    and a quantitative liveness property. Consequently, like boolean properties, also
    quantitative properties can be min-decomposed into safety and liveness parts,
    or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover,
    quantitative properties can be approximated naturally. We prove that every quantitative
    property that has both safe and co-safe approximations can be monitored arbitrarily
    precisely by a monitor that uses only a finite number of states.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
  work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- 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: 'Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In:
    <i>26th International Conference Foundations of Software Science and Computation
    Structures</i>. Vol 13992. Springer Nature; 2023:349-370. doi:<a href="https://doi.org/10.1007/978-3-031-30829-1_17">10.1007/978-3-031-30829-1_17</a>'
  apa: 'Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Quantitative
    safety and liveness. In <i>26th International Conference Foundations of Software
    Science and Computation Structures</i> (Vol. 13992, pp. 349–370). Paris, France:
    Springer Nature. <a href="https://doi.org/10.1007/978-3-031-30829-1_17">https://doi.org/10.1007/978-3-031-30829-1_17</a>'
  chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative
    Safety and Liveness.” In <i>26th International Conference Foundations of Software
    Science and Computation Structures</i>, 13992:349–70. Springer Nature, 2023. <a
    href="https://doi.org/10.1007/978-3-031-30829-1_17">https://doi.org/10.1007/978-3-031-30829-1_17</a>.
  ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and
    liveness,” in <i>26th International Conference Foundations of Software Science
    and Computation Structures</i>, Paris, France, 2023, vol. 13992, pp. 349–370.
  ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness.
    26th International Conference Foundations of Software Science and Computation
    Structures. FOSSACS: Foundations of Software Science and Computation Structures,
    LNCS, vol. 13992, 349–370.'
  mla: Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” <i>26th International
    Conference Foundations of Software Science and Computation Structures</i>, vol.
    13992, Springer Nature, 2023, pp. 349–70, doi:<a href="https://doi.org/10.1007/978-3-031-30829-1_17">10.1007/978-3-031-30829-1_17</a>.
  short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference
    Foundations of Software Science and Computation Structures, Springer Nature, 2023,
    pp. 349–370.
conference:
  end_date: 2023-04-27
  location: Paris, France
  name: 'FOSSACS: Foundations of Software Science and Computation Structures'
  start_date: 2023-04-22
date_created: 2023-01-31T07:23:56Z
date_published: 2023-04-21T00:00:00Z
date_updated: 2023-07-14T11:20:27Z
day: '21'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-30829-1_17
ec_funded: 1
external_id:
  arxiv:
  - '2301.11175'
file:
- access_level: open_access
  checksum: 981025aed580b6b27c426cb8856cf63e
  content_type: application/pdf
  creator: esarac
  date_created: 2023-01-31T07:22:21Z
  date_updated: 2023-01-31T07:22:21Z
  file_id: '12468'
  file_name: qsl.pdf
  file_size: 449027
  relation: main_file
  success: 1
- access_level: open_access
  checksum: f16e2af1e0eb243158ab0f0fe74e7d5a
  content_type: application/pdf
  creator: dernst
  date_created: 2023-06-19T10:28:09Z
  date_updated: 2023-06-19T10:28:09Z
  file_id: '13153'
  file_name: 2023_LNCS_HenzingerT.pdf
  file_size: 1048171
  relation: main_file
  success: 1
file_date_updated: 2023-06-19T10:28:09Z
has_accepted_license: '1'
intvolume: '     13992'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 349-370
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 26th International Conference Foundations of Software Science and Computation
  Structures
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031308284'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative safety and liveness
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: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 13992
year: '2023'
...
---
_id: '11775'
abstract:
- lang: eng
  text: 'Quantitative monitoring can be universal and approximate: For every finite
    sequence of observations, the specification provides a value and the monitor outputs
    a best-effort approximation of it. The quality of the approximation may depend
    on the resources that are available to the monitor. By taking to the limit the
    sequences of specification values and monitor outputs, we obtain precision-resource
    trade-offs also for limit monitoring. This paper provides a formal framework for
    studying such trade-offs using an abstract interpretation for monitors: For each
    natural number n, the aggregate semantics of a monitor at time n is an equivalence
    relation over all sequences of at most n observations so that two equivalent sequences
    are indistinguishable to the monitor and thus mapped to the same output. This
    abstract interpretation of quantitative monitors allows us to measure the number
    of equivalence classes (or “resource use”) that is necessary for a certain precision
    up to a certain time, or at any time. Our framework offers several insights. For
    example, we identify a family of specifications for which any resource-optimal
    exact limit monitor is independent of any error permitted over finite traces.
    Moreover, we present a specification for which any resource-optimal approximate
    limit monitor does not minimize its resource use at any time. '
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
  work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: Yes
author:
- 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: 'Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications.
    In: <i>22nd International Conference on Runtime Verification</i>. Vol 13498. Springer
    Nature; 2022:200-220. doi:<a href="https://doi.org/10.1007/978-3-031-17196-3_11">10.1007/978-3-031-17196-3_11</a>'
  apa: 'Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2022). Abstract monitors
    for quantitative specifications. In <i>22nd International Conference on Runtime
    Verification</i> (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature.
    <a href="https://doi.org/10.1007/978-3-031-17196-3_11">https://doi.org/10.1007/978-3-031-17196-3_11</a>'
  chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract
    Monitors for Quantitative Specifications.” In <i>22nd International Conference
    on Runtime Verification</i>, 13498:200–220. Springer Nature, 2022. <a href="https://doi.org/10.1007/978-3-031-17196-3_11">https://doi.org/10.1007/978-3-031-17196-3_11</a>.
  ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for
    quantitative specifications,” in <i>22nd International Conference on Runtime Verification</i>,
    Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220.
  ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative
    specifications. 22nd International Conference on Runtime Verification. RV: Runtime
    Verification, LNCS, vol. 13498, 200–220.'
  mla: Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.”
    <i>22nd International Conference on Runtime Verification</i>, vol. 13498, Springer
    Nature, 2022, pp. 200–20, doi:<a href="https://doi.org/10.1007/978-3-031-17196-3_11">10.1007/978-3-031-17196-3_11</a>.
  short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference
    on Runtime Verification, Springer Nature, 2022, pp. 200–220.
conference:
  end_date: 2022-09-30
  location: Tbilisi, Georgia
  name: 'RV: Runtime Verification'
  start_date: 2022-09-28
date_created: 2022-08-08T17:09:09Z
date_published: 2022-09-23T00:00:00Z
date_updated: 2023-08-03T13:38:46Z
day: '23'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-17196-3_11
ec_funded: 1
external_id:
  isi:
  - '000866539700011'
file:
- access_level: open_access
  checksum: 05c7dcfbb9053a98f46441fb2eccb213
  content_type: application/pdf
  creator: dernst
  date_created: 2023-01-20T07:34:50Z
  date_updated: 2023-01-20T07:34:50Z
  file_id: '12317'
  file_name: 2022_LNCS_RV_Henzinger.pdf
  file_size: 477110
  relation: main_file
  success: 1
file_date_updated: 2023-01-20T07:34:50Z
has_accepted_license: '1'
intvolume: '     13498'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 200-220
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 22nd International Conference on Runtime Verification
publication_identifier:
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstract monitors for quantitative specifications
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13498
year: '2022'
...
---
_id: '12302'
abstract:
- lang: eng
  text: 'We propose a novel algorithm to decide the language inclusion between (nondeterministic)
    Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage
    a notion of quasiorder to prune the search for a counterexample by discarding
    candidates which are subsumed by others for the quasiorder. Discarded candidates
    are guaranteed to not compromise the completeness of the algorithm. The novelty
    of our work lies in the quasiorder used to discard candidates. We introduce FORQs
    (family of right quasiorders) that we obtain by adapting the notion of family
    of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based
    inclusion algorithm which we prove correct and instantiate it for a specific FORQ,
    called the structural FORQ, induced by the Büchi automaton to the right of the
    inclusion sign. The resulting implementation, called FORKLIFT, scales up better
    than the state-of-the-art on a variety of benchmarks including benchmarks from
    program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870'
acknowledgement: This work was partially funded by the ESF Investing in your future,
  the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00
  BOSCO, the Ramón y Cajal fellowship RYC-2016-20281, and the ERC grant PR1001ERC02.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Kyveli
  full_name: Doveri, Kyveli
  last_name: Doveri
- first_name: Pierre
  full_name: Ganty, Pierre
  last_name: Ganty
- first_name: Nicolas Adrien
  full_name: Mazzocchi, Nicolas Adrien
  id: b26baa86-3308-11ec-87b0-8990f34baa85
  last_name: Mazzocchi
citation:
  ama: 'Doveri K, Ganty P, Mazzocchi NA. FORQ-based language inclusion formal testing.
    In: <i>Computer Aided Verification</i>. Vol 13372. Springer Nature; 2022:109-129.
    doi:<a href="https://doi.org/10.1007/978-3-031-13188-2_6">10.1007/978-3-031-13188-2_6</a>'
  apa: 'Doveri, K., Ganty, P., &#38; Mazzocchi, N. A. (2022). FORQ-based language
    inclusion formal testing. In <i>Computer Aided Verification</i> (Vol. 13372, pp.
    109–129). Haifa, Israel: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-13188-2_6">https://doi.org/10.1007/978-3-031-13188-2_6</a>'
  chicago: Doveri, Kyveli, Pierre Ganty, and Nicolas Adrien Mazzocchi. “FORQ-Based
    Language Inclusion Formal Testing.” In <i>Computer Aided Verification</i>, 13372:109–29.
    Springer Nature, 2022. <a href="https://doi.org/10.1007/978-3-031-13188-2_6">https://doi.org/10.1007/978-3-031-13188-2_6</a>.
  ieee: K. Doveri, P. Ganty, and N. A. Mazzocchi, “FORQ-based language inclusion formal
    testing,” in <i>Computer Aided Verification</i>, Haifa, Israel, 2022, vol. 13372,
    pp. 109–129.
  ista: 'Doveri K, Ganty P, Mazzocchi NA. 2022. FORQ-based language inclusion formal
    testing. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
    vol. 13372, 109–129.'
  mla: Doveri, Kyveli, et al. “FORQ-Based Language Inclusion Formal Testing.” <i>Computer
    Aided Verification</i>, vol. 13372, Springer Nature, 2022, pp. 109–29, doi:<a
    href="https://doi.org/10.1007/978-3-031-13188-2_6">10.1007/978-3-031-13188-2_6</a>.
  short: K. Doveri, P. Ganty, N.A. Mazzocchi, in:, Computer Aided Verification, Springer
    Nature, 2022, pp. 109–129.
conference:
  end_date: 2022-08-10
  location: Haifa, Israel
  name: 'CAV: Computer Aided Verification'
  start_date: 2022-08-07
date_created: 2023-01-16T10:06:31Z
date_published: 2022-08-06T00:00:00Z
date_updated: 2023-09-05T15:13:36Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-13188-2_6
ec_funded: 1
external_id:
  arxiv:
  - '2207.13549'
  isi:
  - '000870310500006'
file:
- access_level: open_access
  checksum: edc363b1be5447a09063e115c247918a
  content_type: application/pdf
  creator: dernst
  date_created: 2023-01-30T12:51:02Z
  date_updated: 2023-01-30T12:51:02Z
  file_id: '12465'
  file_name: 2022_LNCS_Doveri.pdf
  file_size: 497682
  relation: main_file
  success: 1
file_date_updated: 2023-01-30T12:51:02Z
has_accepted_license: '1'
intvolume: '     13372'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 109-129
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: Computer Aided Verification
publication_identifier:
  eisbn:
  - '9783031131882'
  eissn:
  - 1611-3349
  isbn:
  - '9783031131875'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: FORQ-based language inclusion formal testing
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13372
year: '2022'
...