8 Search Results for "Müller-Olm, Markus"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.19
Time for Timed Monitorability

Authors: Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann

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

Abstract
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time. Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
Cite as

Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grosen_et_al:LIPIcs.CONCUR.2025.19,
  author =	{Grosen, Thomas M. and Kauffman, Sean and Larsen, Kim G. and Zimmermann, Martin},
  title =	{{Time for Timed Monitorability}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{19:1--19:20},
  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.19},
  URN =		{urn:nbn:de:0030-drops-239690},
  doi =		{10.4230/LIPIcs.CONCUR.2025.19},
  annote =	{Keywords: Monitorability, Monitoring, Timed Automata, MITL}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.21
An Expressive Trace Logic for Recursive Programs

Authors: Dilian Gurov and Reiner Hähnle

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed points, for precise specification of programs with recursive procedures. Both programs and trace formulas are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.
Cite as

Dilian Gurov and Reiner Hähnle. An Expressive Trace Logic for Recursive Programs. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gurov_et_al:LIPIcs.FSCD.2025.21,
  author =	{Gurov, Dilian and H\"{a}hnle, Reiner},
  title =	{{An Expressive Trace Logic for Recursive Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{21:1--21:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.21},
  URN =		{urn:nbn:de:0030-drops-236360},
  doi =		{10.4230/LIPIcs.FSCD.2025.21},
  annote =	{Keywords: Denotational semantics, compositional semantics, program specification, compositional verification, fixed point logic, trace logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.10
The Complexity of Second-Order HyperLTL

Authors: Hadar Frenkel and Martin Zimmermann

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is Σ₁¹-complete, i.e., only as hard as for (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in Σ₂² and are Σ₁¹-hard, and thus also less complex than for full second-order HyperLTL.
Cite as

Hadar Frenkel and Martin Zimmermann. The Complexity of Second-Order HyperLTL. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{frenkel_et_al:LIPIcs.CSL.2025.10,
  author =	{Frenkel, Hadar and Zimmermann, Martin},
  title =	{{The Complexity of Second-Order HyperLTL}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.10},
  URN =		{urn:nbn:de:0030-drops-227679},
  doi =		{10.4230/LIPIcs.CSL.2025.10},
  annote =	{Keywords: HyperLTL, Satisfiability, Model-checking}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.50
Propositional Dynamic Logic for Hyperproperties

Authors: Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Information security properties of reactive systems like non-interference often require relating different executions of the system to each other and following them simultaneously. Such hyperproperties can also be useful in other contexts, e.g., when analysing properties of distributed systems like linearizability. Since common logics like LTL, CTL, or the modal μ-calculus cannot express hyperproperties, the hyperlogics HyperLTL and HyperCTL^* were developed to cure this defect. However, these logics are not able to express arbitrary ω-regular properties. In this paper, we introduce HyperPDL-Δ, an adaptation of the Propositional Dynamic Logic of Fischer and Ladner for hyperproperties, in order to remove this limitation. Using an elegant automata-theoretic framework, we show that HyperPDL-Δ model checking is asymptotically not more expensive than HyperCTL^* model checking, despite its vastly increased expressive power. We further investigate fragments of HyperPDL-Δ with regard to satisfiability checking.
Cite as

Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Propositional Dynamic Logic for Hyperproperties. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 50:1-50:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gutsfeld_et_al:LIPIcs.CONCUR.2020.50,
  author =	{Gutsfeld, Jens Oliver and M\"{u}ller-Olm, Markus and Ohrem, Christoph},
  title =	{{Propositional Dynamic Logic for Hyperproperties}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{50:1--50:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.50},
  URN =		{urn:nbn:de:0030-drops-128628},
  doi =		{10.4230/LIPIcs.CONCUR.2020.50},
  annote =	{Keywords: Hyperlogics, Hyperproperties, Model Checking, Automata}
}
Document
DOI: 10.4230/DagSemProc.06081.1
06081 Abstracts Collection – Software Verification: Infinite-State Model Checking and Static Program Analysis

Authors: Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract
From 19.02.06 to 24.02.06, the Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm. 06081 Abstracts Collection – Software Verification: Infinite-State Model Checking and Static Program Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:DagSemProc.06081.1,
  author =	{Abdulla, Parosh Aziz and Bouajjani, Ahmed and M\"{u}ller-Olm, Markus},
  title =	{{06081 Abstracts Collection – Software Verification: Infinite-State Model Checking and Static Program Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.1},
  URN =		{urn:nbn:de:0030-drops-7997},
  doi =		{10.4230/DagSemProc.06081.1},
  annote =	{Keywords: Software verification, infinite-state systems, static program analysis, automatic analysis}
}
Document
DOI: 10.4230/DagSemProc.06081.2
06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis

Authors: Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract
{\em Software systems} are present at the very heart of many daily-life applications, such as in communication (telephony and mobile Internet), transportation, energy, health, etc. Such systems are very often {\em critical}\/ in the sense that their failure can have considerable human/economical consequences. In order to ensure reliability, development methods must include {\em algorithmic analysis and verification techniques} which allow (1) to detect automatically defective behaviors of the system and to analyze their source, and (2) to check that every component of a system conforms to its specification. Two important and quite active research communities are particularly concerned with this challenge: the community of computer-aided verification, especially the community of (infinite-state) model checking, and the community of static program analysis. From 19.02.06 to 24.02.06, 51 researchers from these two communities met at the Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis'' in order to improve and deepen the mutual understanding of the developed technologies and to trigger collaborations. During the seminar which was held at the International Conference and Research Center (IBFI), Schloss Dagstuhl, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper.
Cite as

Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm. 06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:DagSemProc.06081.2,
  author =	{Abdulla, Parosh Aziz and Bouajjani, Ahmed and M\"{u}ller-Olm, Markus},
  title =	{{06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.2},
  URN =		{urn:nbn:de:0030-drops-7973},
  doi =		{10.4230/DagSemProc.06081.2},
  annote =	{Keywords: Infinite-state systems, model checking, program analysis, software verification}
}
Document
DOI: 10.4230/DagSemRep.369
Reasoning about Shape (Dagstuhl Seminar 03101)

Authors: Markus Müller-Olm, Hanne Riis Nielson, and David Schmidt

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Markus Müller-Olm, Hanne Riis Nielson, and David Schmidt. Reasoning about Shape (Dagstuhl Seminar 03101). Dagstuhl Seminar Report 369, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{mullerolm_et_al:DagSemRep.369,
  author =	{M\"{u}ller-Olm, Markus and Riis Nielson, Hanne and Schmidt, David},
  title =	{{Reasoning about Shape (Dagstuhl Seminar 03101)}},
  pages =	{1--7},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{369},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.369},
  URN =		{urn:nbn:de:0030-drops-152496},
  doi =		{10.4230/DagSemRep.369},
}
  • Refine by Type
  • 8 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2023
  • 1 2020
  • 2 2006
  • 1 2003

  • Refine by Author
  • 4 Müller-Olm, Markus
  • 2 Abdulla, Parosh Aziz
  • 2 Bouajjani, Ahmed
  • 2 Zimmermann, Martin
  • 1 Frenkel, Hadar
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs
  • 1 DagSemRep
  • 2 DagSemProc

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 3 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Program verification
  • 2 Theory of computation → Verification by model checking
  • 1 Theory of computation → Algebraic semantics
  • Show More...

  • Refine by Keyword
  • 1 Automata
  • 1 Denotational semantics
  • 1 Formal Methods
  • 1 HyperLTL
  • 1 Hyperlogics
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact