---
_id: '5959'
abstract:
- lang: eng
  text: 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.
article_processing_charge: No
author:
- first_name: Alexey
  full_name: Bakhirkin, Alexey
  last_name: Bakhirkin
- first_name: Thomas
  full_name: Ferrere, Thomas
  id: 40960E6E-F248-11E8-B48F-1D18A9856A87
  last_name: Ferrere
  orcid: 0000-0001-5199-3143
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Deian
  full_name: Nickovicl, Deian
  last_name: Nickovicl
citation:
  ama: 'Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. Keynote: The first-order
    logic of signals. In: <i>2018 International Conference on Embedded Software</i>.
    IEEE; 2018:1-10. doi:<a href="https://doi.org/10.1109/emsoft.2018.8537203">10.1109/emsoft.2018.8537203</a>'
  apa: 'Bakhirkin, A., Ferrere, T., Henzinger, T. A., &#38; Nickovicl, D. (2018).
    Keynote: The first-order logic of signals. In <i>2018 International Conference
    on Embedded Software</i> (pp. 1–10). Turin, Italy: IEEE. <a href="https://doi.org/10.1109/emsoft.2018.8537203">https://doi.org/10.1109/emsoft.2018.8537203</a>'
  chicago: 'Bakhirkin, Alexey, Thomas Ferrere, Thomas A Henzinger, and Deian Nickovicl.
    “Keynote: The First-Order Logic of Signals.” In <i>2018 International Conference
    on Embedded Software</i>, 1–10. IEEE, 2018. <a href="https://doi.org/10.1109/emsoft.2018.8537203">https://doi.org/10.1109/emsoft.2018.8537203</a>.'
  ieee: 'A. Bakhirkin, T. Ferrere, T. A. Henzinger, and D. Nickovicl, “Keynote: The
    first-order logic of signals,” in <i>2018 International Conference on Embedded
    Software</i>, Turin, Italy, 2018, pp. 1–10.'
  ista: 'Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. 2018. Keynote: The first-order
    logic of signals. 2018 International Conference on Embedded Software. EMSOFT:
    International Conference on Embedded Software, 1–10.'
  mla: 'Bakhirkin, Alexey, et al. “Keynote: The First-Order Logic of Signals.” <i>2018
    International Conference on Embedded Software</i>, IEEE, 2018, pp. 1–10, doi:<a
    href="https://doi.org/10.1109/emsoft.2018.8537203">10.1109/emsoft.2018.8537203</a>.'
  short: A. Bakhirkin, T. Ferrere, T.A. Henzinger, D. Nickovicl, in:, 2018 International
    Conference on Embedded Software, IEEE, 2018, pp. 1–10.
conference:
  end_date: 2018-10-05
  location: Turin, Italy
  name: 'EMSOFT: International Conference on Embedded Software'
  start_date: 2018-09-30
date_created: 2019-02-13T09:19:28Z
date_published: 2018-09-30T00:00:00Z
date_updated: 2023-09-19T10:41:29Z
day: '30'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/emsoft.2018.8537203
external_id:
  isi:
  - '000492828500005'
file:
- access_level: open_access
  checksum: 234a33ad9055b3458fcdda6af251b33a
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-14T16:01:29Z
  date_updated: 2020-07-14T12:47:13Z
  file_id: '7839'
  file_name: 2018_EMSOFT_Bakhirkin.pdf
  file_size: 338006
  relation: main_file
file_date_updated: 2020-07-14T12:47:13Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 1-10
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: 2018 International Conference on Embedded Software
publication_identifier:
  isbn:
  - '9781538655603'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Keynote: The first-order logic of signals'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2018'
...