Search Results

Documents authored by Wille, Robert

Document
Short Paper
DOI: 10.4230/OASIcs.ATMOS.2024.12
Towards an Optimization Pipeline for the Design of Train Control Systems with Hybrid Train Detection (Short Paper)

Authors: Stefan Engels and Robert Wille

Published in: OASIcs, Volume 123, 24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024)

Abstract
Increasing the capacity of our railway infrastructure will become more and more essential in coping with the need for sustainable transportation. This can be achieved by intelligently implementing train control systems on specific railway networks. Methods that automate and optimize parts of this planning process are of great interest. For control systems based on hybrid train detection, such optimization tasks simultaneously involve routing and block layout generation. These tasks are already complex on their own; hence, a joint consideration often becomes infeasible. This work-in-progress paper proposes an idea to tackle the corresponding complexity. To this end, we present a pipeline that allows to sequentially handle corresponding optimization tasks in a less complex fashion while generating results that remain (close to) optimal. Results from an initial case study showcase that this approach is, indeed, promising. A prototypical implementation is included in the open-source Munich Train Control Toolkit available at https://github.com/cda-tum/mtct.
Cite as

Stefan Engels and Robert Wille. Towards an Optimization Pipeline for the Design of Train Control Systems with Hybrid Train Detection (Short Paper). In 24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024). Open Access Series in Informatics (OASIcs), Volume 123, pp. 12:1-12:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{engels_et_al:OASIcs.ATMOS.2024.12,
  author =	{Engels, Stefan and Wille, Robert},
  title =	{{Towards an Optimization Pipeline for the Design of Train Control Systems with Hybrid Train Detection}},
  booktitle =	{24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024)},
  pages =	{12:1--12:6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-350-8},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{123},
  editor =	{Bouman, Paul C. and Kontogiannis, Spyros C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2024.12},
  URN =		{urn:nbn:de:0030-drops-212002},
  doi =		{10.4230/OASIcs.ATMOS.2024.12},
  annote =	{Keywords: ETCS, MILP, Design Automation, Hybrid Train Detection}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2023.6
A Symbolic Design Method for ETCS Hybrid Level 3 at Different Degrees of Accuracy

Authors: Stefan Engels, Tom Peham, and Robert Wille

Published in: OASIcs, Volume 115, 23rd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2023)

Abstract
The European Train Control System (Hybrid) Level 3 (ETCS Hybrid Level 3) allows for introducing Virtual Subsections (VSS) into existing railway infrastructures. These VSS work similarly to blocks in conventional block signaling but do not require installation or maintenance of trackside train detection. This added flexibility can be used to adapt a given railway network’s (virtual) layout to the changing demands of new schedules. Automated methods are needed to properly use this flexibility and design such layouts on demand and avoid time-intensive manual labor. Recently, approaches inspired by design automation of electronic hardware have been proposed to address this need. But those methods - which are particularly well suited for inherently discrete problems in electronic design automation - have struggled with modeling continuous properties like train positions, time, and acceleration. This work proposes a Mixed Integer Linear Programming (MILP) formulation that, for the first time, can accurately model design problems for ETCS Hybrid Level 3 by including essential, continuous constraints, e.g., for train dynamics or braking curves. The formulation is designed to be flexible and extendable, allowing the user to include/exclude certain constraints or simplify the model as needed. By this, the user can decide whether he/she wants to quickly generate a less accurate solution or a more accurate one at the expense of higher runtimes - basically allowing him/her to trade-off accuracy and efficiency. A case study showcases the potential of the proposed approach and sketches examples to analyze which trade-offs are worthwhile and which simplifications can be safely made. The resulting tool and the benchmarks considered in this work are publicly available at https://github.com/cda-tum/mtct (as part of the Munich Train Control Toolkit, MTCT).
Cite as

Stefan Engels, Tom Peham, and Robert Wille. A Symbolic Design Method for ETCS Hybrid Level 3 at Different Degrees of Accuracy. In 23rd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2023). Open Access Series in Informatics (OASIcs), Volume 115, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{engels_et_al:OASIcs.ATMOS.2023.6,
  author =	{Engels, Stefan and Peham, Tom and Wille, Robert},
  title =	{{A Symbolic Design Method for ETCS Hybrid Level 3 at Different Degrees of Accuracy}},
  booktitle =	{23rd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2023)},
  pages =	{6:1--6:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-302-7},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{115},
  editor =	{Frigioni, Daniele and Schiewe, Philine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2023.6},
  URN =		{urn:nbn:de:0030-drops-187676},
  doi =		{10.4230/OASIcs.ATMOS.2023.6},
  annote =	{Keywords: ETCS, MILP, design automation, block signaling, virtual subsection}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.18
Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond

Authors: Lucas Berent, Lukas Burgholzer, and Robert Wille

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
Boolean Satisfiability (SAT) techniques are well-established in classical computing where they are used to solve a broad variety of problems, e.g., in the design of classical circuits and systems. Analogous to the classical realm, quantum algorithms are usually modelled as circuits and similar design tasks need to be tackled. Thus, it is natural to pose the question whether these design tasks in the quantum realm can also be approached using SAT techniques. To the best of our knowledge, no SAT formulation for arbitrary quantum circuits exists and it is unknown whether such an approach is feasible at all. In this work, we define a propositional SAT encoding that, in principle, can be applied to arbitrary quantum circuits. However, we show that, due to the inherent complexity of representing quantum states, constructing such an encoding is not feasible in general. Therefore, we establish general criteria for determining the feasibility of the proposed encoding and identify classes of quantum circuits fulfilling these criteria. We explicitly demonstrate how the proposed encoding can be applied to the class of Clifford circuits as a representative. Finally, we empirically demonstrate the applicability and efficiency of the proposed encoding for Clifford circuits. With these results, we lay the foundation for continuing the ongoing success of SAT in classical circuit and systems design for quantum circuits.
Cite as

Lucas Berent, Lukas Burgholzer, and Robert Wille. Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{berent_et_al:LIPIcs.SAT.2022.18,
  author =	{Berent, Lucas and Burgholzer, Lukas and Wille, Robert},
  title =	{{Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.18},
  URN =		{urn:nbn:de:0030-drops-166927},
  doi =		{10.4230/LIPIcs.SAT.2022.18},
  annote =	{Keywords: Satisfiability, Quantum Computing, Design Automation, Clifford Circuits}
}
Document
DOI: 10.4230/DagRep.5.8.34
Design of Microfluidic Biochips (Dagstuhl Seminar 15352)

Authors: Krishnendu Chakrabarty, Tsung-Yi Ho, and Robert Wille

Published in: Dagstuhl Reports, Volume 5, Issue 8 (2016)

Abstract
Advances in microfluidic technologies have led to the emergence of biochip devices for automating laboratory procedures in biochemistry and molecular biology. Corresponding systems are revolutionizing a diverse range of applications, e.g.~air quality studies, point-of-care clinical diagnostics, drug discovery, and DNA sequencing -- with an increasing market. However, this continued growth depends on advances in chip integration and design-automation tools. Thus, there is a need to deliver the same level of Computer-Aided Design (CAD) support to the biochip designer that the semiconductor industry now takes for granted. The goal of the seminar was to bring together experts in order to present and to develop new ideas and concepts for design automation algorithms and tools for microfluidic biochips. This report documents the program and the outcomes of this endeavor.
Cite as

Krishnendu Chakrabarty, Tsung-Yi Ho, and Robert Wille. Design of Microfluidic Biochips (Dagstuhl Seminar 15352). In Dagstuhl Reports, Volume 5, Issue 8, pp. 34-53, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{chakrabarty_et_al:DagRep.5.8.34,
  author =	{Chakrabarty, Krishnendu and Ho, Tsung-Yi and Wille, Robert},
  title =	{{Design of Microfluidic Biochips (Dagstuhl Seminar 15352)}},
  pages =	{34--53},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{8},
  editor =	{Chakrabarty, Krishnendu and Ho, Tsung-Yi and Wille, Robert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.8.34},
  URN =		{urn:nbn:de:0030-drops-56776},
  doi =		{10.4230/DagRep.5.8.34},
  annote =	{Keywords: cyber-physical integration, microfluidic biochip, computer aided design, hardware and software co-design, test, verification}
}
Document
DOI: 10.4230/DagRep.1.12.47
Design of Reversible and Quantum Circuits (Dagstuhl Seminar 11502)

Authors: Kenichi Morita and Robert Wille

Published in: Dagstuhl Reports, Volume 1, Issue 12 (2012)

Abstract
It is a widely supported prediction that conventional computer hardware technologies are going to reach their limits in the near future. Consequently, researchers are working on alternatives. Reversible circuits and quantum circuits are one promising direction which allows to overcome fundamental barriers. However, no real design flow for this new kind of circuits exists so far. Physical implementations are in its infancy. Within this seminar, recent research questions of this emerging technology have been discussed.
Cite as

Kenichi Morita and Robert Wille. Design of Reversible and Quantum Circuits (Dagstuhl Seminar 11502). In Dagstuhl Reports, Volume 1, Issue 12, pp. 47-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Article{morita_et_al:DagRep.1.12.47,
  author =	{Morita, Kenichi and Wille, Robert},
  title =	{{Design of Reversible and Quantum Circuits (Dagstuhl Seminar 11502)}},
  pages =	{47--61},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{1},
  number =	{12},
  editor =	{Morita, Kenichi and Wille, Robert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.12.47},
  URN =		{urn:nbn:de:0030-drops-34503},
  doi =		{10.4230/DagRep.1.12.47},
  annote =	{Keywords: reversible computation, quantum computation, computer aided design, hardware and software design, physical implementation, applications}
}
Document
DOI: 10.4230/DagSemProc.09461.5
SWORD – Module-based SAT Solving

Authors: Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
In the paper, SWORD is described – a decision procedure for bit-vector logic that uses SAT techniques and exploits word level information. The main idea of SWORD is based on the following observation: While current SAT solvers perform very well on instances with a large number of logic operations, their performance on arithmetic operations degrades with increasing data-path width. In contrast, pure word-level approaches are able to handle arithmetic operations very fast, but suffer from irregularities in the word-level structure (e.g. bit slicing). SWORD tries to combine the best of both worlds: On the one hand, it includes fast propagation, sophisticated data structures, as well as advanced techniques like non-chronological backtracking and learning from modern SAT solvers. On the other hand word-level information is exploited in the decision heuristic and during propagation.
Cite as

Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler. SWORD – Module-based SAT Solving. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{wille_et_al:DagSemProc.09461.5,
  author =	{Wille, Robert and Jung, Jean Christoph and S\"{u}lflow, Andre and Drechsler, Rolf},
  title =	{{SWORD – Module-based SAT Solving}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.5},
  URN =		{urn:nbn:de:0030-drops-25069},
  doi =		{10.4230/DagSemProc.09461.5},
  annote =	{Keywords: SAT Solver, Word Level, SAT Modulo Theories}
}
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 Imprint Privacy Contact