2 Search Results for "Thoma, Daniel"

Document
DOI: 10.4230/OASIcs.DX.2024.2
A Model-Based Approach for Monitoring and Diagnosing Digital Twin Discrepancies

Authors: Elaheh Hosseinkhani, Martin Leucker, Martin Sachenbacher, Hendrik Streichhahn, and Lars B. Vosteen

Published in: OASIcs, Volume 125, 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024)

Abstract
Recent decades have seen the increasing use of Digital Twins (DTs) - that is, digital models used over the lifetime of a physical product or system for tasks such as predictive maintenance or optimization - in a number of domains such as buildings, manufacturing, or design. DTs face a challenge known as the DT synchronization problem; a DT, often based on machine-learned, or complex simulation models, needs to adequately mirror the physical product or system at all times, as any deviations might affect the quality of predictions or control actions. In this paper, we present a model-based approach that aims to add a level of awareness to DT models by supervising if they are in sync with the physical counterpart. The approach is agnostic to the type of models used in the DT, as long as they are compositional, and based on monitoring critical properties (behavioral or functional aspects) of the system at run-time. In the case violations are detected, it reasons on the DT’s structure to localize and identify parts of the model that cause deviations and need to be adapted. We give a formal description and an implementation of this approach, and illustrate it with an example from building climatisation.
Cite as

Elaheh Hosseinkhani, Martin Leucker, Martin Sachenbacher, Hendrik Streichhahn, and Lars B. Vosteen. A Model-Based Approach for Monitoring and Diagnosing Digital Twin Discrepancies. In 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024). Open Access Series in Informatics (OASIcs), Volume 125, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hosseinkhani_et_al:OASIcs.DX.2024.2,
  author =	{Hosseinkhani, Elaheh and Leucker, Martin and Sachenbacher, Martin and Streichhahn, Hendrik and Vosteen, Lars B.},
  title =	{{A Model-Based Approach for Monitoring and Diagnosing Digital Twin Discrepancies}},
  booktitle =	{35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024)},
  pages =	{2:1--2:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-356-0},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{125},
  editor =	{Pill, Ingo and Natan, Avraham and Wotawa, Franz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.DX.2024.2},
  URN =		{urn:nbn:de:0030-drops-220944},
  doi =		{10.4230/OASIcs.DX.2024.2},
  annote =	{Keywords: Digital Twins, Runtime Verification, Diagnosis, FDIR, TeSSLa}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.29
Model-Checking Counting Temporal Logics on Flat Structures

Authors: Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.
Cite as

Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Model-Checking Counting Temporal Logics on Flat Structures. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{decker_et_al:LIPIcs.CONCUR.2017.29,
  author =	{Decker, Normann and Habermehl, Peter and Leucker, Martin and Sangnier, Arnaud and Thoma, Daniel},
  title =	{{Model-Checking Counting Temporal Logics on Flat Structures}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.29},
  URN =		{urn:nbn:de:0030-drops-77709},
  doi =		{10.4230/LIPIcs.CONCUR.2017.29},
  annote =	{Keywords: Counting Temporal Logic, Model checking, Flat Kripke Structure}
}
  • Refine by Author
  • 2 Leucker, Martin
  • 1 Decker, Normann
  • 1 Habermehl, Peter
  • 1 Hosseinkhani, Elaheh
  • 1 Sachenbacher, Martin
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Counting Temporal Logic
  • 1 Diagnosis
  • 1 Digital Twins
  • 1 FDIR
  • 1 Flat Kripke Structure
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2017
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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