Quantitative Monitoring of Signal First-Order Logic
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911480990924800 |
|---|---|
| author | Chalupa, Marek Henzinger, Thomas A. Saraç, N. Ege Yu, Emily |
| author_facet | Chalupa, Marek Henzinger, Thomas A. Saraç, N. Ege Yu, Emily |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_00728 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Quantitative Monitoring of Signal First-Order Logic Chalupa, Marek Henzinger, Thomas A. Saraç, N. Ege Yu, Emily Logic in Computer Science Software Engineering Systems and Control 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. |
| title | Quantitative Monitoring of Signal First-Order Logic |
| topic | Logic in Computer Science Software Engineering Systems and Control |
| url | https://arxiv.org/abs/2603.00728 |