7 Search Results for "Müller, Julian-Steffen"

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-dev.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/OASIcs.ATMOS.2022.13
Passenger-Aware Real-Time Planning of Short Turns to Reduce Delays in Public Transport

Authors: Julian Patzner, Ralf Rückert, and Matthias Müller-Hannemann

Published in: OASIcs, Volume 106, 22nd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2022)

Abstract
Delays and disruptions are commonplace in public transportation. An important tool to limit the impact of severely delayed vehicles is the use of short turns, where a planned trip is shortened in order to be able to resume the following trip in the opposite direction as close to the schedule as possible. Short turns have different effects on passengers: some suffer additional delays and have to reschedule their route, while others can benefit from them. Dispatchers therefore need decision support in order to use short turns only if the overall delay of all affected passengers is positively influenced. In this paper, we study the planning of short turns based on passenger flows. We propose a simulation framework which can be used to decide upon single short turns in real time. An experimental study with a scientific model (LinTim) of an entire public transport system for the German city of Stuttgart including busses, trams, and local trains shows that we can solve these problems on average within few milliseconds. Based on features of the current delay scenario and the passenger flow we use machine learning to classify cases where short turns are beneficial. Depending on how many features are used, we reach a correct classification rate of more than 93% (full feature set) and 90% (partial feature set) using random forests. Since precise passenger flows are often not available in urban public transportation, our machine learning approach has the great advantage of working with significantly less detailed passenger information.
Cite as

Julian Patzner, Ralf Rückert, and Matthias Müller-Hannemann. Passenger-Aware Real-Time Planning of Short Turns to Reduce Delays in Public Transport. In 22nd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2022). Open Access Series in Informatics (OASIcs), Volume 106, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{patzner_et_al:OASIcs.ATMOS.2022.13,
  author =	{Patzner, Julian and R\"{u}ckert, Ralf and M\"{u}ller-Hannemann, Matthias},
  title =	{{Passenger-Aware Real-Time Planning of Short Turns to Reduce Delays in Public Transport}},
  booktitle =	{22nd Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2022)},
  pages =	{13:1--13:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-259-4},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{106},
  editor =	{D'Emidio, Mattia and Lindner, Niels},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2022.13},
  URN =		{urn:nbn:de:0030-drops-171171},
  doi =		{10.4230/OASIcs.ATMOS.2022.13},
  annote =	{Keywords: Public Transportation, Delays, Real-time Dispatching, Passenger Flows}
}
Document
DOI: 10.4230/OASIcs.ASD.2020.1
Towards a Reliable and Context-Based System Architecture for Autonomous Vehicles

Authors: Tobias Kain, Philipp Mundhenk, Julian-Steffen Müller, Hans Tompits, Maximilian Wesche, and Hendrik Decke

Published in: OASIcs, Volume 79, 2nd International Workshop on Autonomous Systems Design (ASD 2020)

Abstract
Full vehicle autonomy excludes a takeover by passengers in case a safety-critical application fails. Therefore, the system responsible for operating the autonomous vehicle has to detect and handle failures autonomously. Moreover, this system has to ensure the safety of the passengers, as well as the safety of other road users at any given time. Especially in the initial phase of autonomous vehicles, building up consumer confidence is essential. Therefore, in this regard, handling all failures by simply performing an emergency stop is not desirable. In this paper, we introduce an approach enabling a dynamic and safe reconfiguration of the autonomous driving system to handle occurring hardware and software failures. Since the requirements concerning safe reconfiguration actions are significantly affected by the current context the car is experiencing, the developed reconfiguration approach is sensitive to context changes. Our approach defines three interconnected layers, which are distinguished by their level of awareness. The top layer, referred to as the context layer, is responsible for observing the context. These context observations, in turn, imply a set of requirements, which constitute the input for the reconfiguration layer. The latter layer is required to determine reconfiguration actions, which are then executed by the architecture layer.
Cite as

Tobias Kain, Philipp Mundhenk, Julian-Steffen Müller, Hans Tompits, Maximilian Wesche, and Hendrik Decke. Towards a Reliable and Context-Based System Architecture for Autonomous Vehicles. In 2nd International Workshop on Autonomous Systems Design (ASD 2020). Open Access Series in Informatics (OASIcs), Volume 79, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kain_et_al:OASIcs.ASD.2020.1,
  author =	{Kain, Tobias and Mundhenk, Philipp and M\"{u}ller, Julian-Steffen and Tompits, Hans and Wesche, Maximilian and Decke, Hendrik},
  title =	{{Towards a Reliable and Context-Based System Architecture for Autonomous Vehicles}},
  booktitle =	{2nd International Workshop on Autonomous Systems Design (ASD 2020)},
  pages =	{1:1--1:7},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-141-2},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{79},
  editor =	{Steinhorst, Sebastian and Deshmukh, Jyotirmoy V.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ASD.2020.1},
  URN =		{urn:nbn:de:0030-drops-125956},
  doi =		{10.4230/OASIcs.ASD.2020.1},
  annote =	{Keywords: autonomous driving, fail-operational systems, context-based architecture, application placement, optimization, monitoring}
}
Document
DOI: 10.4230/DagRep.6.5.56
Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201)

Authors: Julian Dolby, Orna Grumberg, Peter Müller, and Omer Tripp

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

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16201 "Synergies among Testing, Verification, and Repair for Concurrent Programs". This seminar builds upon, and is inspired by, several past seminars on program testing, verification, repair and combinations thereof. These include Dagstuhl Seminar 13021 "Symbolic Methods in Testing"; Dagstuhl Seminar 13061 "Fault Prediction, Localization and Repair"; Dagstuhl Seminar 14171 "Evaluating Software Verification Systems: Benchmarks and Competitions"; Dagstuhl Seminar 14352 "Next Generation Static Software Analysis Tools"; Dagstuhl Seminar 14442 "Symbolic Execution and Constraint Solving"; and Dagstuhl Seminar 15191 "Compositional Verification Methods for Next-Generation Concurrency". These were held in January 2013; February 2013; April 2014; August 2014; October 2014; and May 2015, respectively. Two notable contributions of Dagstuhl Seminar 16201, which distinguish it from these past seminars, are (i) the focus on concurrent programming, which introduces significant challenges to testing, verification and repair tools, as well as (ii) the goal of identifying and exploiting synergies between the testing, verification and repair research communities in light of common needs and goals.
Cite as

Julian Dolby, Orna Grumberg, Peter Müller, and Omer Tripp. Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). In Dagstuhl Reports, Volume 6, Issue 5, pp. 56-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{dolby_et_al:DagRep.6.5.56,
  author =	{Dolby, Julian and Grumberg, Orna and M\"{u}ller, Peter and Tripp, Omer},
  title =	{{Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201)}},
  pages =	{56--71},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{5},
  editor =	{Dolby, Julian and Grumberg, Orna and M\"{u}ller, Peter and Tripp, Omer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.5.56},
  URN =		{urn:nbn:de:0030-drops-67203},
  doi =		{10.4230/DagRep.6.5.56},
  annote =	{Keywords: (automatic) bug repair, concurrency bugs, concurrent programming, deductive verification, interactive verification, linearizability, synchronization testing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.277
A Van Benthem Theorem for Modal Team Semantics

Authors: Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
The famous van Benthem theorem states that modal logic corresponds exactly to the fragment of first-order logic that is invariant under bisimulation. In this article we prove an exact analogue of this theorem in the framework of modal dependence logic (MDL) and team semantics. We show that Modal Team Logic (MTL) extending MDL by classical negation captures exactly the FO-definable bisimulation invariant properties of Kripke structures and teams. We also compare the expressive power of MTL to most of the variants and extensions of MDL recently studied in the area.
Cite as

Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. A Van Benthem Theorem for Modal Team Semantics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 277-291, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kontinen_et_al:LIPIcs.CSL.2015.277,
  author =	{Kontinen, Juha and M\"{u}ller, Julian-Steffen and Schnoor, Henning and Vollmer, Heribert},
  title =	{{A Van Benthem Theorem for Modal Team Semantics}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{277--291},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.277},
  URN =		{urn:nbn:de:0030-drops-54206},
  doi =		{10.4230/LIPIcs.CSL.2015.277},
  annote =	{Keywords: modal logic, dependence logic, team semantics, expressivity, bisimulation, independence, inclusion, generalized dependence atom}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2014.122
Timing of Train Disposition: Towards Early Passenger Rerouting in Case of Delays

Authors: Martin Lemnian, Ralf Rückert, Steffen Rechner, Christoph Blendinger, and Matthias Müller-Hannemann

Published in: OASIcs, Volume 42, 14th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (2014)

Abstract
Passenger-friendly train disposition is a challenging, highly complex online optimization problem with uncertain and incomplete information about future delays. In this paper we focus on the timing within the disposition process. We introduce three different classification schemes to predict as early as possible the status of a transfer: whether it will almost surely break, is so critically delayed that it requires manual disposition, or can be regarded as only slightly uncertain or as being safe. The three approaches use lower bounds on travel times, historical distributions of delay data, and fuzzy logic, respectively. In experiments with real delay data we achieve an excellent classification rate. Furthermore, using realistic passenger flows we observe that there is a significant potential to reduce the passenger delay if an early rerouting strategy is applied.
Cite as

Martin Lemnian, Ralf Rückert, Steffen Rechner, Christoph Blendinger, and Matthias Müller-Hannemann. Timing of Train Disposition: Towards Early Passenger Rerouting in Case of Delays. In 14th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems. Open Access Series in Informatics (OASIcs), Volume 42, pp. 122-137, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{lemnian_et_al:OASIcs.ATMOS.2014.122,
  author =	{Lemnian, Martin and R\"{u}ckert, Ralf and Rechner, Steffen and Blendinger, Christoph and M\"{u}ller-Hannemann, Matthias},
  title =	{{Timing of Train Disposition: Towards Early Passenger Rerouting in Case of Delays}},
  booktitle =	{14th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems},
  pages =	{122--137},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-75-0},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{42},
  editor =	{Funke, Stefan and Mihal\'{a}k, Mat\'{u}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2014.122},
  URN =		{urn:nbn:de:0030-drops-47576},
  doi =		{10.4230/OASIcs.ATMOS.2014.122},
  annote =	{Keywords: train delays, event-activity model, timing of decisions, passenger flows, passenger rerouting}
}
Document
DOI: 10.4230/DagSemProc.08391.5
08391 Group Summary – The Evolution and Dynamics of Research Networks

Authors: Vladimir Batagelj, Bettina Hoser, Claudia Müller, Steffen Staab, and Gerd Stumme

Published in: Dagstuhl Seminar Proceedings, Volume 8391, Social Web Communities (2008)

Abstract
Existing collaboration and innovation in scientific communities can be enhanced by understanding the underlying patterns und hidden relations. Social network analysis is an appropriate method to reveal such patterns. Nevertheless, research in this area is mainly focused on social networks. One promising approach is to use homophily networks as well. Furthermore, extending the static to a dynamic network model enables to understand existing interdependencies in these networks. A mathematical description of possible analyses is given. Finally, resulting research questions are illustrated and the necessity of an interdisciplinary research approach is pointed out.
Cite as

Vladimir Batagelj, Bettina Hoser, Claudia Müller, Steffen Staab, and Gerd Stumme. 08391 Group Summary – The Evolution and Dynamics of Research Networks. In Social Web Communities. Dagstuhl Seminar Proceedings, Volume 8391, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{batagelj_et_al:DagSemProc.08391.5,
  author =	{Batagelj, Vladimir and Hoser, Bettina and M\"{u}ller, Claudia and Staab, Steffen and Stumme, Gerd},
  title =	{{08391 Group Summary – The Evolution and Dynamics of Research  Networks}},
  booktitle =	{Social Web Communities},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8391},
  editor =	{Harith Alani and Steffen Staab and Gerd Stumme},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08391.5},
  URN =		{urn:nbn:de:0030-drops-17906},
  doi =		{10.4230/DagSemProc.08391.5},
  annote =	{Keywords: Homophily networks, social networks, evolution, scientific community}
}
  • Refine by Author
  • 2 Müller, Julian-Steffen
  • 2 Müller-Hannemann, Matthias
  • 2 Rückert, Ralf
  • 1 Batagelj, Vladimir
  • 1 Blendinger, Christoph
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Transportation
  • 1 Computer systems organization → Reconfigurable computing
  • 1 Theory of computation → Algebraic semantics
  • 1 Theory of computation → Invariants
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 (automatic) bug repair
  • 1 Delays
  • 1 Formal Methods
  • 1 Homophily networks
  • 1 Loop Analysis
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 1 2008
  • 1 2014
  • 1 2015
  • 1 2016
  • 1 2020
  • Show More...

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