Publication
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 , 2023
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 (2023) , p. 264-288
Full text (Publisher's DOI)
Full text (open access)
The author-created version that incorporates referee comments and is the accepted for publication version Available from 30.06.2024
UAntwerpen
Faculty/Department
Research group
Publication type
Subject
Affiliation
Publications with a UAntwerp address
External links
Record
Identifier
Creation 08.02.2024
Last edited 09.02.2024
To cite this reference