Keynote: The first-order logic of signals

A. Bakhirkin, T. Ferrere, T.A. Henzinger, D. Nickovicl, in:, 2018 International Conference on Embedded Software (EMSOFT), IEEE, 2018, pp. 1–10.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English
Author
; ; ;
Department
Abstract
Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain.
Publishing Year
Date Published
2018-09-30
Proceedings Title
2018 International Conference on Embedded Software (EMSOFT)
Page
1-10
Conference
EMSOFT: International Conference on Embedded Software
Conference Location
Turin, Italy
Conference Date
2018-09-30 – 2018-10-05
IST-REx-ID

Cite this

Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. Keynote: The first-order logic of signals. In: 2018 International Conference on Embedded Software (EMSOFT). IEEE; 2018:1-10. doi:10.1109/emsoft.2018.8537203
Bakhirkin, A., Ferrere, T., Henzinger, T. A., & Nickovicl, D. (2018). Keynote: The first-order logic of signals. In 2018 International Conference on Embedded Software (EMSOFT) (pp. 1–10). Turin, Italy: IEEE. https://doi.org/10.1109/emsoft.2018.8537203
Bakhirkin, Alexey, Thomas Ferrere, Thomas A Henzinger, and Deian Nickovicl. “Keynote: The First-Order Logic of Signals.” In 2018 International Conference on Embedded Software (EMSOFT), 1–10. IEEE, 2018. https://doi.org/10.1109/emsoft.2018.8537203.
A. Bakhirkin, T. Ferrere, T. A. Henzinger, and D. Nickovicl, “Keynote: The first-order logic of signals,” in 2018 International Conference on Embedded Software (EMSOFT), Turin, Italy, 2018, pp. 1–10.
Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. 2018. Keynote: The first-order logic of signals. 2018 International Conference on Embedded Software (EMSOFT). EMSOFT: International Conference on Embedded Software 1–10.
Bakhirkin, Alexey, et al. “Keynote: The First-Order Logic of Signals.” 2018 International Conference on Embedded Software (EMSOFT), IEEE, 2018, pp. 1–10, doi:10.1109/emsoft.2018.8537203.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar
ISBN Search