---
OA_place: publisher
OA_type: hybrid
_id: '22006'
abstract:
- lang: eng
  text: Runtime monitoring checks, during execution, whether a partial signal produced
    by a hybrid system satisfies its specification. Signal First-Order Logic (SFO)
    offers expressive real-time specifications over such signals, but currently comes
    only with Boolean semantics and has no tool support. We provide the first robustness-based
    quantitative semantics for SFO, enabling the expression and evaluation of rich
    real-time properties beyond the scope of existing formalisms such as Signal Temporal
    Logic. To enable online monitoring, we identify a past-time fragment of SFO and
    give a pastification procedure that transforms bounded-response SFO formulas into
    equisatisfiable formulas in this fragment. We then develop an efficient runtime
    monitoring algorithm for this past-time fragment and evaluate its performance
    on a set of benchmarks, demonstrating the practicality and effectiveness of our
    approach. To the best of our knowledge, this is the first publicly available prototype
    for online quantitative monitoring of full SFO.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
  work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093)
  and HYPER (No. 101055412), and by the Advanced Research and Invention Agency under
  the Safeguarded AI programme (MSAI-PR01-P047).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
  full_name: Chalupa, Marek
  id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
  last_name: Chalupa
- 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: Naci E
  full_name: Sarac, Naci E
  id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  last_name: Sarac
- first_name: Zhengqi
  full_name: Yu, Zhengqi
  id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
  last_name: Yu
  orcid: 0000-0002-4993-773X
citation:
  ama: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal
    First-Order logic. In: <i>27th International Symposium on Formal Methods</i>.
    Vol 16557. Springer Nature; 2026:214-233. doi:<a href="https://doi.org/10.1007/978-3-032-26220-2_11">10.1007/978-3-032-26220-2_11</a>'
  apa: 'Chalupa, M., Henzinger, T. A., Sarac, N. E., &#38; Yu, E. (2026). Quantitative
    monitoring of Signal First-Order logic. In <i>27th International Symposium on
    Formal Methods</i> (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. <a
    href="https://doi.org/10.1007/978-3-032-26220-2_11">https://doi.org/10.1007/978-3-032-26220-2_11</a>'
  chicago: Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative
    Monitoring of Signal First-Order Logic.” In <i>27th International Symposium on
    Formal Methods</i>, 16557:214–33. Springer Nature, 2026. <a href="https://doi.org/10.1007/978-3-032-26220-2_11">https://doi.org/10.1007/978-3-032-26220-2_11</a>.
  ieee: M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring
    of Signal First-Order logic,” in <i>27th International Symposium on Formal Methods</i>,
    Tokyo, Japan, 2026, vol. 16557, pp. 214–233.
  ista: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal
    First-Order logic. 27th International Symposium on Formal Methods. FM: Formal
    Methods, LNCS, vol. 16557, 214–233.'
  mla: Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.”
    <i>27th International Symposium on Formal Methods</i>, vol. 16557, Springer Nature,
    2026, pp. 214–33, doi:<a href="https://doi.org/10.1007/978-3-032-26220-2_11">10.1007/978-3-032-26220-2_11</a>.
  short: M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium
    on Formal Methods, Springer Nature, 2026, pp. 214–233.
conference:
  end_date: 2026-05-22
  location: Tokyo, Japan
  name: 'FM: Formal Methods'
  start_date: 2026-05-18
das_tickbox: '0'
date_created: 2026-06-14T22:01:44Z
date_published: 2026-05-18T00:00:00Z
date_updated: 2026-06-22T08:21:09Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-032-26220-2_11
ec_funded: 1
external_id:
  arxiv:
  - '2603.00728'
file:
- access_level: open_access
  checksum: 7055199ecb985e9e2e272f4988827067
  content_type: application/pdf
  creator: dernst
  date_created: 2026-06-22T08:18:41Z
  date_updated: 2026-06-22T08:18:41Z
  file_id: '22113'
  file_name: 2026_LNCS_Chalupa.pdf
  file_size: 849237
  relation: main_file
  success: 1
file_date_updated: 2026-06-22T08:18:41Z
has_accepted_license: '1'
intvolume: '     16557'
keyword:
- Signal first-order logic
- Robustness-based quantitative semantics
- Online runtime monitoring
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 214-233
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 27th International Symposium on Formal Methods
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783032262196'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative monitoring of Signal First-Order logic
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: 16557
year: '2026'
...