9 Search Results for "Bauer, Reinhard"

Document
DOI: 10.4230/LIPIcs.CSL.2026.17
A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials

Authors: Alexis Saurin and Esaïe Bauer

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proofs of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives. Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller’s subexponentials and from the first author and Laurent’s super exponentials. Our work is motivated, on the one hand, by Baillot’s work on light logics with recursive types and on the other hand by our recent work on the proof theory of the modal μ-calculus.
Cite as

Alexis Saurin and Esaïe Bauer. A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 17:1-17:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{saurin_et_al:LIPIcs.CSL.2026.17,
  author =	{Saurin, Alexis and Bauer, Esa\"{i}e},
  title =	{{A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{17:1--17:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.17},
  URN =		{urn:nbn:de:0030-drops-254418},
  doi =		{10.4230/LIPIcs.CSL.2026.17},
  annote =	{Keywords: cut elimination, exponential modalities, fixed-points, linear logic, light logics, mu-calculus, non-wellfounded proofs, proof theory, sequent calculus, subexponentials, super exponentials}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2025.12
Separator-Based Alternative Paths in Customizable Contraction Hierarchies

Authors: Scott Bacherle, Thomas Bläsius, and Michael Zündorf

Published in: OASIcs, Volume 137, 25th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2025)

Abstract
We propose an algorithm for computing alternatives to the shortest path in a road network, based on the speed-up technique CCH (customizable contraction hierarchy). Computing alternative paths is a well-studied problem, motivated by the fact that route-planning applications benefit from presenting different high-quality options the user can choose from. Another crucial feature of modern routing applications is the inclusion of live traffic, which requires speed-up techniques that allow efficient metric updates. Besides CCH, the other speed-up technique supporting metric updates is CRP (customizable route planning). Of the two, CCH is the more modern solution with the advantages of providing faster queries and being substantially simpler to implement efficiently. However, so far, CCH has been lacking a way of computing alternative paths. While for CRP, the commonly used plateau method for computing alternatives can be applied, this is not so straightforward for CCH. With this paper, we make CCH a viable option for alternative paths, by proposing a new separator-based approach to computing alternative paths that works hand-in-hand with the CCH data structure. With our experiments, we demonstrate that CCH can indeed be used to compute alternative paths efficiently. With this, we provide an alternative to CRP that is simpler and has lower query times.
Cite as

Scott Bacherle, Thomas Bläsius, and Michael Zündorf. Separator-Based Alternative Paths in Customizable Contraction Hierarchies. In 25th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2025). Open Access Series in Informatics (OASIcs), Volume 137, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bacherle_et_al:OASIcs.ATMOS.2025.12,
  author =	{Bacherle, Scott and Bl\"{a}sius, Thomas and Z\"{u}ndorf, Michael},
  title =	{{Separator-Based Alternative Paths in Customizable Contraction Hierarchies}},
  booktitle =	{25th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2025)},
  pages =	{12:1--12:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-404-8},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{137},
  editor =	{Sauer, Jonas and Schmidt, Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2025.12},
  URN =		{urn:nbn:de:0030-drops-247685},
  doi =		{10.4230/OASIcs.ATMOS.2025.12},
  annote =	{Keywords: Alternative routes, realistic road networks, customizable contraction hierarchies, route planning, shortest paths}
}
Document
Industrial Challenge Description
DOI: 10.4230/LIPIcs.ECRTS.2025.22
Embedded Reconfiguration of TSN (Industrial Challenge Description)

Authors: Marc Boyer and Rafik Henia

Published in: LIPIcs, Volume 335, 37th Euromicro Conference on Real-Time Systems (ECRTS 2025)

Abstract
The sets of Ethernet extensions known as "Time Sensitive Networking" (TSN) is a promising candidate as the next backbone of real-time distributed systems. The flexibility of TSN is also an opportunity to reconfigure the network in presence of faults. This white paper presents an avionic case study for a TSN reconfiguration.
Cite as

Marc Boyer and Rafik Henia. Embedded Reconfiguration of TSN (Industrial Challenge Description). In 37th Euromicro Conference on Real-Time Systems (ECRTS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 335, pp. 22:1-22:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{boyer_et_al:LIPIcs.ECRTS.2025.22,
  author =	{Boyer, Marc and Henia, Rafik},
  title =	{{Embedded Reconfiguration of TSN}},
  booktitle =	{37th Euromicro Conference on Real-Time Systems (ECRTS 2025)},
  pages =	{22:1--22:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-377-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{335},
  editor =	{Mancuso, Renato},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2025.22},
  URN =		{urn:nbn:de:0030-drops-237709},
  doi =		{10.4230/LIPIcs.ECRTS.2025.22},
  annote =	{Keywords: Real-time network, Time Sensitive Networks, TSN, Time Aware Shaper, TAS, Credit Based Shaper, CBS, Reconfiguration}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.32
Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation

Authors: Alexis Saurin

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

Abstract
Analyzing Maehara’s method for proving Craig’s interpolation theorem, we extract a "proof relevant" interpolation theorem for first-order LL in the sense that if π is a cut-free sequent proof of A⊢ B, we can find a formula C in the common vocabulary of A and B and proofs π₁,π₂ of A⊢ C and C⊢ B respectively such that π₁ composed with π₂ cut-reduces to π. As a direct corollary, we get similar proof relevant interpolation results for LJ and LK using linear translations. This refined interpolation is then rephrased in terms of a cut-introduction process synthetizing the interpolant. Finally, we analyze the computational content of interpolation by proving an interpolation result for Curien and Herbelin’s Duality of Computation.
Cite as

Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{saurin:LIPIcs.FSCD.2025.32,
  author =	{Saurin, Alexis},
  title =	{{Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{32:1--32:21},
  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.32},
  URN =		{urn:nbn:de:0030-drops-236478},
  doi =		{10.4230/LIPIcs.FSCD.2025.32},
  annote =	{Keywords: Classical Logic, Interpolation, Cut Elimination, Linear Logic, Sequent calculus, System L}
}
Document
DOI: 10.4230/LITES-v003-i001-a001
Programming Language Constructs Supporting Fault Tolerance

Authors: Christina Houben and Sebastian Houben

Published in: LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1

Abstract
In order to render software viable for highly safety-critical applications, we describe how to incorporate fault tolerance mechanisms into the real-time programming language PEARL. Therefore, we present, classify, evaluate and illustrate known fault tolerance methods for software. We link them together with the requirements of the international standard IEC 61508-3 for functional safety. We contribute PEARL-2020 programming language constructs for fault tolerance methods that need to be implemented by operating systems, and code-snippets as well as libraries for those independent from runtime systems.
Cite as

Christina Houben and Sebastian Houben. Programming Language Constructs Supporting Fault Tolerance. In LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1, pp. 01:1-01:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{houben_et_al:LITES-v003-i001-a001,
  author =	{Houben, Christina and Houben, Sebastian},
  title =	{{Programming Language Constructs Supporting Fault Tolerance}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:20},
  ISSN =	{2199-2002},
  year =	{2016},
  volume =	{3},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v003-i001-a001},
  URN =		{urn:nbn:de:0030-drops-192560},
  doi =		{10.4230/LITES-v003-i001-a001},
  annote =	{Keywords: Fault tolerance, Functional safety, PEARL, Embedded systems, Software engineering}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2012.71
On the Complexity of Partitioning Graphs for Arc-Flags

Authors: Reinhard Bauer, Moritz Baum, Ignaz Rutter, and Dorothea Wagner

Published in: OASIcs, Volume 25, 12th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (2012)

Abstract
Precomputation of auxiliary data in an additional off-line step is a common approach towards improving the performance of shortest-path queries in large-scale networks. One such technique is the arc-flags algorithm, where the preprocessing involves computing a partition of the input graph. The quality of this partition significantly affects the speed-up observed in the query phase. It is evaluated by considering the search-space size of subsequent shortest-path queries, in particular its maximum or its average over all queries. In this paper, we substantially strengthen existing hardness results of Bauer et al. and show that optimally filling this degree of freedom is NP-hard for trees with unit-length edges, even if we bound the height or the degree. On the other hand, we show that optimal partitions for paths can be computed efficiently and give approximation algorithms for cycles and trees.
Cite as

Reinhard Bauer, Moritz Baum, Ignaz Rutter, and Dorothea Wagner. On the Complexity of Partitioning Graphs for Arc-Flags. In 12th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems. Open Access Series in Informatics (OASIcs), Volume 25, pp. 71-82, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:OASIcs.ATMOS.2012.71,
  author =	{Bauer, Reinhard and Baum, Moritz and Rutter, Ignaz and Wagner, Dorothea},
  title =	{{On the Complexity of Partitioning Graphs for Arc-Flags}},
  booktitle =	{12th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems},
  pages =	{71--82},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-45-3},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{25},
  editor =	{Delling, Daniel and Liberti, Leo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2012.71},
  URN =		{urn:nbn:de:0030-drops-37048},
  doi =		{10.4230/OASIcs.ATMOS.2012.71},
  annote =	{Keywords: shortest paths, arc-flags, search space, preprocessing, complexity}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2007.1169
14. Experimental Study on Speed-Up Techniques for Timetable Information Systems

Authors: Reinhard Bauer, Daniel Delling, and Dorothea Wagner

Published in: OASIcs, Volume 7, 7th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'07) (2007)

Abstract
During the last years, impressive speed-up techniques for Dijkstra's algorithm have been developed. Unfortunately, recent research mainly focused on road networks. However, fast algorithms are also needed for other applications like timetable information systems. Even worse, the adaption of recently developed techniques to timetable information is often more complicated than expected. In this work, we check whether results from road networks are transferable to timetable information. To this end, we present an extensive experimental study of the most prominent speed-up techniques on different types of inputs. It turns out that recently developed techniques are much slower on graphs derived from timetable information than on road networks. In addition, we gain amazing insights into the behavior of speed-up techniques in general.
Cite as

Reinhard Bauer, Daniel Delling, and Dorothea Wagner. 14. Experimental Study on Speed-Up Techniques for Timetable Information Systems. In 7th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'07). Open Access Series in Informatics (OASIcs), Volume 7, pp. 209-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:OASIcs.ATMOS.2007.1169,
  author =	{Bauer, Reinhard and Delling, Daniel and Wagner, Dorothea},
  title =	{{14. Experimental Study on Speed-Up Techniques for Timetable Information Systems}},
  booktitle =	{7th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'07)},
  pages =	{209--225},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-04-0},
  ISSN =	{2190-6807},
  year =	{2007},
  volume =	{7},
  editor =	{Ahuja, Ravindra K. and Liebchen, Christian and Mesa, Juan A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2007.1169},
  URN =		{urn:nbn:de:0030-drops-11695},
  doi =		{10.4230/OASIcs.ATMOS.2007.1169},
  annote =	{Keywords: Speed-up techniques, timetable information, shortest path}
}
Document
DOI: 10.4230/DagSemProc.06081.3
Analysis of Dynamic Communicating Systems by Hierarchical Abstraction

Authors: Jörg Bauer and Reinhard Wilhelm

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

Abstract
We propose a new abstraction technique for verifying topology properties of dynamic communicating systems (DCS), a special class of infinite-state systems. DCS are characterized by unbounded creation and destruction of objects along with an evolving communication connectivity or topology. We employ a lightweight graph transformation system to specify DCS. Hierarchical Abstraction (HA) computes a bounded over-approximation of all topologies that can occur in a DCS directly from its transformation rules. HA works in two steps. First, for each connected component, called cluster, of a topology, objects sharing a common property are summarized to one abstract object. Then isomorphic abstract connected components are summarized to one abstract component, called abstract cluster. This yields a conservative approximation of all graphs that may occur during any DCS run. The technique is implemented.
Cite as

Jörg Bauer and Reinhard Wilhelm. Analysis of Dynamic Communicating Systems by Hierarchical Abstraction. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:DagSemProc.06081.3,
  author =	{Bauer, J\"{o}rg and Wilhelm, Reinhard},
  title =	{{Analysis of Dynamic Communicating Systems by Hierarchical Abstraction}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--25},
  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.3},
  URN =		{urn:nbn:de:0030-drops-7271},
  doi =		{10.4230/DagSemProc.06081.3},
  annote =	{Keywords: Graph transformation, Abstract Interpretation, Shape Analysis}
}
Document
DOI: 10.4230/DagSemProc.06161.5
Abstract Interpretation of Graph Transformation

Authors: Jörg Bauer and Reinhard Wilhelm

Published in: Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006)

Abstract
The semantics of many dynamic systems can be described by evolving graphs. Graph transformation systems (GTS) are a natural, intuitive, and formally defined method to specify systems of evolving graphs, whereas verification techniques for GTS are scarce. We present an abstract interpretation based approach for GTS verification. Single graphs are abstracted in two steps. First similar nodes within a connected component, then similar abstracted connected components are summarized. Transformation rules are applied directly to abstract graphs yielding a bounded set of abstract graphs of bounded size that over-approximates the concrete GTS and can be used for further verification. Since our abstraction is homomorphic, existential positive properties are preserved under abstraction. Furthermore, we identify automatically checkable completeness criteria for the abstraction. The technique is implemented and successfully tested on the platoon case study.
Cite as

Jörg Bauer and Reinhard Wilhelm. Abstract Interpretation of Graph Transformation. In Simulation and Verification of Dynamic Systems. Dagstuhl Seminar Proceedings, Volume 6161, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:DagSemProc.06161.5,
  author =	{Bauer, J\"{o}rg and Wilhelm, Reinhard},
  title =	{{Abstract Interpretation of Graph Transformation}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.5},
  URN =		{urn:nbn:de:0030-drops-7039},
  doi =		{10.4230/DagSemProc.06161.5},
  annote =	{Keywords: Abstract Interpretation, Graph Transformation}
}
  • Refine by Type
  • 9 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 3 2025
  • 1 2016
  • 1 2012
  • 1 2007
  • Show More...

  • Refine by Author
  • 2 Bauer, Jörg
  • 2 Bauer, Reinhard
  • 2 Saurin, Alexis
  • 2 Wagner, Dorothea
  • 2 Wilhelm, Reinhard
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 3 OASIcs
  • 1 LITES
  • 2 DagSemProc

  • Refine by Classification
  • 2 Theory of computation → Linear logic
  • 2 Theory of computation → Proof theory
  • 1 Applied computing → Transportation
  • 1 Mathematics of computing → Graph algorithms
  • 1 Networks → Cyber-physical networks
  • Show More...

  • Refine by Keyword
  • 2 Abstract Interpretation
  • 2 shortest paths
  • 1 Alternative routes
  • 1 CBS
  • 1 Classical Logic
  • 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