2 Search Results for "Christensen, Rasmus Emil"

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/LIPIcs.SoCG.2023.13
Multilevel Skeletonization Using Local Separators

Authors: J. Andreas Bærentzen, Rasmus Emil Christensen, Emil Toftegaard Gæde, and Eva Rotenberg

Published in: LIPIcs, Volume 258, 39th International Symposium on Computational Geometry (SoCG 2023)

Abstract
In this paper we give a new, efficient algorithm for computing curve skeletons, based on local separators. Our efficiency stems from a multilevel approach, where we solve small problems across levels of detail and combine these in order to quickly obtain a skeleton. We do this in a highly modular fashion, ensuring complete flexibility in adapting the algorithm for specific types of input or for otherwise targeting specific applications. Separator based skeletonization was first proposed by Bærentzen and Rotenberg in [ACM Tran. Graphics'21], showing high quality output at the cost of running times which become prohibitive for large inputs. Our new approach retains the high quality output, and applicability to any spatially embedded graph, while being orders of magnitude faster for all practical purposes. We test our skeletonization algorithm for efficiency and quality in practice, comparing it to local separator skeletonization on the University of Groningen Skeletonization Benchmark [Telea'16].
Cite as

J. Andreas Bærentzen, Rasmus Emil Christensen, Emil Toftegaard Gæde, and Eva Rotenberg. Multilevel Skeletonization Using Local Separators. In 39th International Symposium on Computational Geometry (SoCG 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 258, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brentzen_et_al:LIPIcs.SoCG.2023.13,
  author =	{B{\ae}rentzen, J. Andreas and Christensen, Rasmus Emil and G{\ae}de, Emil Toftegaard and Rotenberg, Eva},
  title =	{{Multilevel Skeletonization Using Local Separators}},
  booktitle =	{39th International Symposium on Computational Geometry (SoCG 2023)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-273-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{258},
  editor =	{Chambers, Erin W. and Gudmundsson, Joachim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2023.13},
  URN =		{urn:nbn:de:0030-drops-178637},
  doi =		{10.4230/LIPIcs.SoCG.2023.13},
  annote =	{Keywords: Algorithm engineering, experimentation and implementation, shape skeletonization, curve skeletons, multilevel algorithm}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2023

  • Refine by Author
  • 1 Aceto, Luca
  • 1 Achilleos, Antonis
  • 1 Attard, Duncan Paul
  • 1 Bærentzen, J. Andreas
  • 1 Christensen, Rasmus Emil
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Computing methodologies → Computer graphics
  • 1 Software and its engineering → Software design engineering
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Computational geometry
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 1 Algorithm engineering
  • 1 Runtime verification
  • 1 curve skeletons
  • 1 experimentation and implementation
  • 1 monitorability
  • 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