|
Title
|
|
|
|
Synthesizing efficiently monitorable formulas in metric temporal logic
| |
|
Author
|
|
|
|
| |
|
Abstract
|
|
|
|
| In runtime verification, manually formalizing a specification for monitoring system executions is a tedious and error-prone process. To address this issue, we consider the problem of automatically synthesizing formal specifications from system executions. To demonstrate our approach, we consider the popular specification language Metric Temporal Logic (MTL), which is particularly tailored towards specifying temporal properties for cyber-physical systems (CPS). Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. However, for efficiency in monitoring, along with the size, the amount of “lookahead” required for the specification becomes relevant, especially for safety-critical applications. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead. Our learning algorithm reduces the synthesis task to a series of satisfiability problems in Linear Real Arithmetic (LRA) and generates MTL formulas from their satisfying assignments. The reduction uses a novel encoding of a popular monitoring MTL procedure using LRA. Finally, we implement our algorithm in a tool called TEAL and demonstrate its ability to synthesize efficiently monitorable MTL formulas in CPS applications. |
| |
|
Language
|
|
|
|
English
| |
|
Source (journal)
|
|
|
|
Lecture notes in computer science. - Berlin, 1973, currens
| |
|
Source (book)
|
|
|
|
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II
| |
|
Publication
|
|
|
|
Berlin
:
Springer
,
2024
| |
|
ISSN
|
|
|
|
0302-9743
1611-3349
| |
|
ISBN
|
|
|
|
978-3-031-50520-1
978-3-031-50521-8
| |
|
DOI
|
|
|
|
10.1007/978-3-031-50521-8_13
| |
|
Volume/pages
|
|
|
|
14500
(2024)
, p. 264-288
| |
|
ISI
|
|
|
|
001166807400013
| |
|
Full text (Publisher's DOI)
|
|
|
|
| |
|
Full text (open access)
|
|
|
|
| |
|