---
_id: '81'
abstract:
- lang: eng
  text: We solve the offline monitoring problem for timed propositional temporal logic
    (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider
    extends linear temporal logic (LTL) with clock variables and reset quantifiers,
    providing a mechanism to specify real-time constraints. We first describe a general
    monitoring algorithm based on an exhaustive computation of the set of satisfying
    clock assignments as a finite union of zones. We then propose a specialized monitoring
    algorithm for the one-variable case using a partition of the time domain based
    on the notion of region equivalence, whose complexity is linear in the length
    of the signal, thereby generalizing a known result regarding the monitoring of
    metric temporal logic (MTL). The region and zone representations of time constraints
    are known from timed automata verification and can also be used in the discrete-time
    case. Our prototype implementation appears to outperform previous discrete-time
    implementations of TPTL monitoring,
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Adrian
  full_name: Elgyütt, Adrian
  id: 4A2E9DBA-F248-11E8-B48F-1D18A9856A87
  last_name: Elgyütt
- 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
citation:
  ama: 'Elgyütt A, Ferrere T, Henzinger TA. Monitoring temporal logic with clock variables.
    In: Vol 11022. Springer; 2018:53-70. doi:<a href="https://doi.org/10.1007/978-3-030-00151-3_4">10.1007/978-3-030-00151-3_4</a>'
  apa: 'Elgyütt, A., Ferrere, T., &#38; Henzinger, T. A. (2018). Monitoring temporal
    logic with clock variables (Vol. 11022, pp. 53–70). Presented at the FORMATS:
    Formal Modeling and Analysis of Timed Systems, Beijing, China: Springer. <a href="https://doi.org/10.1007/978-3-030-00151-3_4">https://doi.org/10.1007/978-3-030-00151-3_4</a>'
  chicago: Elgyütt, Adrian, Thomas Ferrere, and Thomas A Henzinger. “Monitoring Temporal
    Logic with Clock Variables,” 11022:53–70. Springer, 2018. <a href="https://doi.org/10.1007/978-3-030-00151-3_4">https://doi.org/10.1007/978-3-030-00151-3_4</a>.
  ieee: 'A. Elgyütt, T. Ferrere, and T. A. Henzinger, “Monitoring temporal logic with
    clock variables,” presented at the FORMATS: Formal Modeling and Analysis of Timed
    Systems, Beijing, China, 2018, vol. 11022, pp. 53–70.'
  ista: 'Elgyütt A, Ferrere T, Henzinger TA. 2018. Monitoring temporal logic with
    clock variables. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS,
    vol. 11022, 53–70.'
  mla: Elgyütt, Adrian, et al. <i>Monitoring Temporal Logic with Clock Variables</i>.
    Vol. 11022, Springer, 2018, pp. 53–70, doi:<a href="https://doi.org/10.1007/978-3-030-00151-3_4">10.1007/978-3-030-00151-3_4</a>.
  short: A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70.
conference:
  end_date: 2018-09-06
  location: Beijing, China
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
  start_date: 2018-09-04
date_created: 2018-12-11T11:44:31Z
date_published: 2018-08-26T00:00:00Z
date_updated: 2025-04-15T06:26:03Z
day: '26'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-00151-3_4
external_id:
  isi:
  - '000884993200004'
file:
- access_level: open_access
  checksum: e5d81c9b50a6bd9d8a2c16953aad7e23
  content_type: application/pdf
  creator: dernst
  date_created: 2020-10-09T06:24:21Z
  date_updated: 2020-10-09T06:24:21Z
  file_id: '8638'
  file_name: 2018_LNCS_Elgyuett.pdf
  file_size: 537219
  relation: main_file
  success: 1
file_date_updated: 2020-10-09T06:24:21Z
has_accepted_license: '1'
intvolume: '     11022'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 53 - 70
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
publication_status: published
publisher: Springer
publist_id: '7973'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring temporal logic with clock variables
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11022
year: '2018'
...