Metric First-Order Temporal Logic with Complex Data Types
OPEN ACCESS
Loading...
Author / Producer
Date
2023
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Temporal logics are widely used in runtime verification as they enable the creation of declarative and compositional specifications. However, their ability to model complex data is limited. One must resort to complicated encoding schemes to express properties involving basic structures such as lists or trees. To avoid this drawback, we extend metric first-order temporal logic with a minimalistic, yet expressive, functional programming language. The extension features an expressive collection of types including function, record, variant, and inductive types, as well as support for type inference and monitoring.
Our monitor implementation directly parses traces in the JSON format, based on the user’s type specification, which avoids a separate pre-processing step. We compare our approach to existing shallow embeddings of temporal properties in general-purpose host languages and to encodings into simple temporal logics. Specifically, our language benefits from a precise semantics and a good support for monitoring-specific static analysis.
Permanent link
Publication status
published
External links
Book title
Runtime Verification
Journal / series
Volume
14245
Pages / Article No.
126 - 147
Publisher
Springer
Event
23th International Conference on Runtime Verification (RV 2023)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Monitoring; Temporal logic; Data types
Organisational unit
03634 - Basin, David / Basin, David
02150 - Dep. Informatik / Dep. of Computer Science