---
_id: '14076'
abstract:
- lang: eng
  text: Hyperproperties are properties that relate multiple execution traces. Previous
    work on monitoring hyperproperties focused on synchronous hyperproperties, usually
    specified in HyperLTL. When monitoring synchronous hyperproperties, all traces
    are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers
    and show how to use them for monitoring synchronous as well as, for the first
    time, asynchronous hyperproperties. Prefix transducers map multiple input traces
    into one or more output traces by incrementally matching prefixes of the input
    traces against expressions similar to regular expressions. The prefixes of different
    traces which are consumed by a single matching step of the monitor may have different
    lengths. The deterministic and executable nature of prefix transducers makes them
    more suitable as an intermediate formalism for runtime verification than logical
    specifications, which tend to be highly non-deterministic, especially in the case
    of asynchronous hyperproperties. We report on a set of experiments about monitoring
    asynchronous version of observational determinism.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
  authors would like to thank Ana Oliveira da Costa for commenting on a draft of the
  paper.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Marek
  full_name: Chalupa, Marek
  id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
  last_name: Chalupa
- 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: 'Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers.
    In: <i>23nd International Conference on Runtime Verification</i>. Vol 14245. Springer
    Nature; 2023:168-190. doi:<a href="https://doi.org/10.1007/978-3-031-44267-4_9">10.1007/978-3-031-44267-4_9</a>'
  apa: 'Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with
    prefix transducers. In <i>23nd International Conference on Runtime Verification</i>
    (Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-44267-4_9">https://doi.org/10.1007/978-3-031-44267-4_9</a>'
  chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with
    Prefix Transducers.” In <i>23nd International Conference on Runtime Verification</i>,
    14245:168–90. Springer Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-44267-4_9">https://doi.org/10.1007/978-3-031-44267-4_9</a>.
  ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,”
    in <i>23nd International Conference on Runtime Verification</i>, Thessaloniki,
    Greek, 2023, vol. 14245, pp. 168–190.
  ista: 'Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers.
    23nd International Conference on Runtime Verification. RV: Conference on Runtime
    Verification, LNCS, vol. 14245, 168–190.'
  mla: Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix
    Transducers.” <i>23nd International Conference on Runtime Verification</i>, vol.
    14245, Springer Nature, 2023, pp. 168–90, doi:<a href="https://doi.org/10.1007/978-3-031-44267-4_9">10.1007/978-3-031-44267-4_9</a>.
  short: M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime
    Verification, Springer Nature, 2023, pp. 168–190.
conference:
  end_date: 2023-10-07
  location: Thessaloniki, Greek
  name: 'RV: Conference on Runtime Verification'
  start_date: 2023-10-04
date_created: 2023-08-16T20:46:08Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2024-02-28T12:33:08Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_9
ec_funded: 1
file:
- access_level: open_access
  checksum: ee33bd6f1a26f4dae7a8192584869fd8
  content_type: application/pdf
  creator: dernst
  date_created: 2023-10-16T07:15:11Z
  date_updated: 2023-10-16T07:15:11Z
  file_id: '14430'
  file_name: 2023_LNCS_RV_Chalupa.pdf
  file_size: 867256
  relation: main_file
  success: 1
file_date_updated: 2023-10-16T07:15:11Z
has_accepted_license: '1'
intvolume: '     14245'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '10'
oa: 1
oa_version: Published Version
page: 168-190
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 23nd International Conference on Runtime Verification
publication_identifier:
  eisbn:
  - 978-3-031-44267-4
  isbn:
  - 978-3-031-44266-7
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '15035'
    relation: research_data
    status: public
status: public
title: Monitoring hyperproperties with prefix transducers
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14245
year: '2023'
...