4 Search Results for "Lange, Alexander"

Document
DOI: 10.4230/LIPIcs.TIME.2023.10
The Calculus of Temporal Influence

Authors: Florian Bruse, Marit Kastaun, Martin Lange, and Sören Möller

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
We present the Calculus of Temporal Influence, a simple logical calculus that allows reasoning about the behaviour of real-valued functions over time by making assertions that bound their values or the values of their derivatives. The motivation for the design of such a proof system comes from the need to provide the background computational machinery for tools that support learning in experimental subjects in secondary-education classrooms. The end goal is a tool that allows school pupils to formalise hypotheses about phenomena in natural sciences, such that their validity with respect to some formal experiment model can be checked automatically. The Calculus of Temporal Influence provides a language for formal statements and the mechanisms for reasoning about valid logical consequences. It extends (and deviates in parts from) previous work introducing the Calculus of (Non-Temporal) Influence by integrating the ability to model temporal effects in such experiments. We show that reasoning in the calculus is sound with respect to a natural formal semantics, that logical consequence is at least semi-decidable, and that one obtains polynomial-time decidability for a natural stratification of the problem.
Cite as

Florian Bruse, Marit Kastaun, Martin Lange, and Sören Möller. The Calculus of Temporal Influence. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.TIME.2023.10,
  author =	{Bruse, Florian and Kastaun, Marit and Lange, Martin and M\"{o}ller, S\"{o}ren},
  title =	{{The Calculus of Temporal Influence}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.10},
  URN =		{urn:nbn:de:0030-drops-191009},
  doi =		{10.4230/LIPIcs.TIME.2023.10},
  annote =	{Keywords: temporal reasoning, formal models, continuous functions, polynomial decidability}
}
Document
DOI: 10.4230/LIPIcs.TIME.2022.5
The Tail-Recursive Fragment of Timed Recursive CTL

Authors: Florian Bruse, Martin Lange, and Etienne Lozes

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

Abstract
Timed Recursive CTL (TRCTL) was recently proposed as a merger of two extensions of the well-known branching-time logic CTL: Timed CTL on one hand is interpreted over real-time systems like timed automata, and Recursive CTL (RecCTL) on the other hand obtains high expressiveness through the introduction of a recursion operator. Model checking for the resulting logic is known to be 2-EXPTIME-complete. The aim of this paper is to investigate the possibility to obtain a fragment of lower complexity without losing too much expressive power. It is obtained by a syntactic property called "tail-recursiveness" that restricts the way that recursive formulas can be built. This restriction is known to decrease the complexity of model checking by half an exponential in the untimed setting. We show that this also works in the real-time world: model checking for the tail-recursive fragment of TRCTL is EXPSPACE-complete. The upper bound is obtained by a standard untiming construction via region graphs, and rests on the known complexity of tail-recursive fragments of higher-order modal logics. The lower bound is established by a reduction from a suitable tiling problem.
Cite as

Florian Bruse, Martin Lange, and Etienne Lozes. The Tail-Recursive Fragment of Timed Recursive CTL. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.TIME.2022.5,
  author =	{Bruse, Florian and Lange, Martin and Lozes, Etienne},
  title =	{{The Tail-Recursive Fragment of Timed Recursive CTL}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.5},
  URN =		{urn:nbn:de:0030-drops-172527},
  doi =		{10.4230/LIPIcs.TIME.2022.5},
  annote =	{Keywords: formal specification, temporal logic, real-time systems}
}
Document
DOI: 10.4230/LIPIcs.TQC.2018.5
Subset Sum Quantumly in 1.17^n

Authors: Alexander Helm and Alexander May

Published in: LIPIcs, Volume 111, 13th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2018)

Abstract
We study the quantum complexity of solving the subset sum problem, where the elements a_1, ..., a_n are randomly chosen from Z_{2^{l(n)}} and t = sum_i a_i in Z_{2^{l(n)}} is a sum of n/2 elements. In 2013, Bernstein, Jeffery, Lange and Meurer constructed a quantum subset sum algorithm with heuristic time complexity 2^{0.241n}, by enhancing the classical subset sum algorithm of Howgrave-Graham and Joux with a quantum random walk technique. We improve on this by defining a quantum random walk for the classical subset sum algorithm of Becker, Coron and Joux. The new algorithm only needs heuristic running time and memory 2^{0.226n}, for almost all random subset sum instances.
Cite as

Alexander Helm and Alexander May. Subset Sum Quantumly in 1.17^n. In 13th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 111, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{helm_et_al:LIPIcs.TQC.2018.5,
  author =	{Helm, Alexander and May, Alexander},
  title =	{{Subset Sum Quantumly in 1.17^n}},
  booktitle =	{13th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2018)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-080-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{111},
  editor =	{Jeffery, Stacey},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2018.5},
  URN =		{urn:nbn:de:0030-drops-92527},
  doi =		{10.4230/LIPIcs.TQC.2018.5},
  annote =	{Keywords: Subset sum, Quantum walk, Representation technique}
}
Document
DOI: 10.4230/OASIcs.WCET.2016.4
Continuous Non-Intrusive Hybrid WCET Estimation Using Waypoint Graphs

Authors: Boris Dreyer, Christian Hochberger, Alexander Lange, Simon Wegener, and Alexander Weiss

Published in: OASIcs, Volume 55, 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)

Abstract
Traditionally, the Worst-Case Execution Time (WCET) of Embedded Software has been estimated using analytical approaches. This is effective, if good models of the processor/System-on-Chip (SoC) architecture exist. Unfortunately, modern high performance SoCs often contain unpredictable and/or undocumented components that influence the timing behaviour. Thus, analytical results for such processors are unrealistically pessimistic. One possible alternative approach seems to be hybrid WCET analysis, where measurement data together with an analytical approach is used to estimate worst-case behaviour. Previously, we demonstrated how continuous evaluation of basic block trace data can be used to produce detailed statistics of basic blocks in embedded software. In the meantime it has become clear that the trace data provided by modern SoCs delivers a different type of information. In this contribution, we show that even under realistic conditions, a meaningful analysis can be conducted with the trace data.
Cite as

Boris Dreyer, Christian Hochberger, Alexander Lange, Simon Wegener, and Alexander Weiss. Continuous Non-Intrusive Hybrid WCET Estimation Using Waypoint Graphs. In 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016). Open Access Series in Informatics (OASIcs), Volume 55, pp. 4:1-4:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dreyer_et_al:OASIcs.WCET.2016.4,
  author =	{Dreyer, Boris and Hochberger, Christian and Lange, Alexander and Wegener, Simon and Weiss, Alexander},
  title =	{{Continuous Non-Intrusive Hybrid WCET Estimation Using Waypoint Graphs}},
  booktitle =	{16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)},
  pages =	{4:1--4:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-025-5},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{55},
  editor =	{Schoeberl, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2016.4},
  URN =		{urn:nbn:de:0030-drops-68977},
  doi =		{10.4230/OASIcs.WCET.2016.4},
  annote =	{Keywords: Hybrid Worst-Case Execution Time (WCET) Estimation for Multicore Processors, Real-time Systems}
}
  • Refine by Author
  • 2 Bruse, Florian
  • 2 Lange, Martin
  • 1 Dreyer, Boris
  • 1 Helm, Alexander
  • 1 Hochberger, Christian
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Interactive learning environments
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Program specifications
  • 1 Theory of computation → Quantum complexity theory
  • Show More...

  • Refine by Keyword
  • 1 Hybrid Worst-Case Execution Time (WCET) Estimation for Multicore Processors
  • 1 Quantum walk
  • 1 Real-time Systems
  • 1 Representation technique
  • 1 Subset sum
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2016
  • 1 2018
  • 1 2022
  • 1 2023

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