2 Search Results for "Hofman, Mads"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2006.687
Robustness and Recovery in Train Scheduling - a Case Study from DSB S-tog a/s

Authors: Mads Hofman, Line Madsen, Julie Jespersen Groth, Jens Clausen, and Jesper Larsen

Published in: OASIcs, Volume 5, 6th Workshop on Algorithmic Methods and Models for Optimization of Railways (ATMOS'06) (2006)

Abstract
This paper presents a simulation model to study the robustness of timetables of DSB S-tog a/s, the city rail of Copenhagen. Dealing with rush hour scenarios only, the simulation model investigates the effects of disturbances on the S-tog network. Several timetables are analyzed with respect to robustness. Some of these are used in operation and some are generated for the purpose of investigating timetables with specific alternative characteristics.
Cite as

Mads Hofman, Line Madsen, Julie Jespersen Groth, Jens Clausen, and Jesper Larsen. Robustness and Recovery in Train Scheduling - a Case Study from DSB S-tog a/s. In 6th Workshop on Algorithmic Methods and Models for Optimization of Railways (ATMOS'06). Open Access Series in Informatics (OASIcs), Volume 5, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{hofman_et_al:OASIcs.ATMOS.2006.687,
  author =	{Hofman, Mads and Madsen, Line and Jespersen Groth, Julie and Clausen, Jens and Larsen, Jesper},
  title =	{{Robustness and Recovery in Train Scheduling - a Case Study from DSB S-tog a/s}},
  booktitle =	{6th Workshop on Algorithmic Methods and Models for Optimization of Railways (ATMOS'06)},
  pages =	{1--22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-01-9},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{5},
  editor =	{Jacob, Riko and M\"{u}ller-Hannemann, Matthias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2006.687},
  URN =		{urn:nbn:de:0030-drops-6878},
  doi =		{10.4230/OASIcs.ATMOS.2006.687},
  annote =	{Keywords: Train scheduling, simulation model, robustness, recovery}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2006

  • Refine by Author
  • 1 Aceto, Luca
  • 1 Achilleos, Antonis
  • 1 Attard, Duncan Paul
  • 1 Clausen, Jens
  • 1 Exibard, Léo
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 1 Runtime verification
  • 1 Train scheduling
  • 1 monitorability
  • 1 recovery
  • 1 register automata
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact