Search Results

Documents authored by Bruse, Florian

Document
DOI: 10.4230/LIPIcs.TIME.2024.16
Real-Time Higher-Order Recursion Schemes

Authors: Eric Alsmann and Florian Bruse

Published in: LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024)

Abstract
Higher-Order Recursion Schemes (HORS) have long been studied as a tool to model functional programs. Model-checking the tree generated by a HORS of order k against a parity automaton is known to be k-EXPTIME-complete. This paper introduces timed HORS, a real-time version of HORS in the sense of Alur/Dill'90, to be model-checked against a pair of a parity automaton and a timed automaton. We show that adding dense linear time to the notion of recursion schemes adds one exponential to the cost of model-checking, i.e., model-checking a timed HORS of order k can be done in (k+1)-EXPTIME. This is shown by an adaption of the region-graph construction known from the model-checking of timed CTL. We also obtain a hardness result for k = 1, but we strongly conjecture that it holds for all k. This result is obtained by encoding runs of 2-EXPTIME Turing machines into the trees generated by timed HORS.
Cite as

Eric Alsmann and Florian Bruse. Real-Time Higher-Order Recursion Schemes. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{alsmann_et_al:LIPIcs.TIME.2024.16,
  author =	{Alsmann, Eric and Bruse, Florian},
  title =	{{Real-Time Higher-Order Recursion Schemes}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{16:1--16:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-349-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{318},
  editor =	{Sala, Pietro and Sioutis, Michael and Wang, Fusheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.16},
  URN =		{urn:nbn:de:0030-drops-212236},
  doi =		{10.4230/LIPIcs.TIME.2024.16},
  annote =	{Keywords: Timed Automata, Higher-Order Recursion Schemes, Tree Automata}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TIME.2023
LIPIcs, Volume 278, TIME 2023, Complete Volume

Authors: Alexander Artikis, Florian Bruse, and Luke Hunsberger

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

Abstract
LIPIcs, Volume 278, TIME 2023, Complete Volume
Cite as

30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 1-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{artikis_et_al:LIPIcs.TIME.2023,
  title =	{{LIPIcs, Volume 278, TIME 2023, Complete Volume}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{1--254},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023},
  URN =		{urn:nbn:de:0030-drops-190890},
  doi =		{10.4230/LIPIcs.TIME.2023},
  annote =	{Keywords: LIPIcs, Volume 278, TIME 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TIME.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Alexander Artikis, Florian Bruse, and Luke Hunsberger

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{artikis_et_al:LIPIcs.TIME.2023.0,
  author =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{0:i--0:xiv},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.0},
  URN =		{urn:nbn:de:0030-drops-190907},
  doi =		{10.4230/LIPIcs.TIME.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
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.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.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.TIME.2021.12
Model Checking Timed Recursive CTL

Authors: Florian Bruse and Martin Lange

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
We introduce Timed Recursive CTL, a merger of two extensions of the well-known branching-time logic CTL: Timed CTL is interpreted over real-time systems like timed automata; Recursive CTL introduces a powerful recursion operator which takes the expressiveness of this logic CTL well beyond that of regular properties. The result is an expressive logic for real-time properties. We show that its model checking problem is decidable over timed automata, namely 2-EXPTIME-complete.
Cite as

Florian Bruse and Martin Lange. Model Checking Timed Recursive CTL. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 12:1-12:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.TIME.2021.12,
  author =	{Bruse, Florian and Lange, Martin},
  title =	{{Model Checking Timed Recursive CTL}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{12:1--12:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.12},
  URN =		{urn:nbn:de:0030-drops-147880},
  doi =		{10.4230/LIPIcs.TIME.2021.12},
  annote =	{Keywords: formal specification, temporal logic, real-time systems}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.24
Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures

Authors: Florian Bruse, Marco Sälzer, and Martin Lange

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
The modal μ-calculus can only express bisimulation-invariant properties. It is a simple consequence of Kleene’s Fixpoint Theorem that on structures with finite bisimulation quotients, the fixpoint iteration of any formula converges after finitely many steps. We show that the converse does not hold: we construct a word with an infinite bisimulation quotient that is locally regular so that the iteration for any fixpoint formula of the modal μ-calculus on it converges after finitely many steps. This entails decidability of μ-calculus model-checking over this word. We also show that the reason for the discrepancy between infinite bisimulation quotients and trans-finite fixpoint convergence lies in the fact that the μ-calculus can only express regular properties.
Cite as

Florian Bruse, Marco Sälzer, and Martin Lange. Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.MFCS.2021.24,
  author =	{Bruse, Florian and S\"{a}lzer, Marco and Lange, Martin},
  title =	{{Finite Convergence of \mu-Calculus Fixpoints on Genuinely Infinite Structures}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.24},
  URN =		{urn:nbn:de:0030-drops-144643},
  doi =		{10.4230/LIPIcs.MFCS.2021.24},
  annote =	{Keywords: temporal logic, fixpoint iteration, bisimulation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.23
A Decidable Non-Regular Modal Fixpoint Logic

Authors: Florian Bruse and Martin Lange

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Fixpoint Logic with Chop (FLC) extends the modal μ-calculus with an operator for sequential composition between predicate transformers. This makes it an expressive modal fixpoint logic which is capable of formalising many non-regular program properties. Its satisfiability problem is highly undecidable. Here we define Visibly Pushdown Fixpoint Logic with Chop, a fragment in which fixpoint formulas are required to be of a certain form resembling visibly pushdown grammars. We give a sound and complete game-theoretic characterisation of FLC’s satisfiability problem and show that the games corresponding to formulas from this fragment are stair-parity games and therefore effectively solvable, resulting in 2EXPTIME-completeness of this fragment. The lower bound is inherited from PDL over Recursive Programs, which is structurally similar but considerably weaker in expressive power.
Cite as

Florian Bruse and Martin Lange. A Decidable Non-Regular Modal Fixpoint Logic. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.CONCUR.2021.23,
  author =	{Bruse, Florian and Lange, Martin},
  title =	{{A Decidable Non-Regular Modal Fixpoint Logic}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.23},
  URN =		{urn:nbn:de:0030-drops-144003},
  doi =		{10.4230/LIPIcs.CONCUR.2021.23},
  annote =	{Keywords: formal specification, temporal logic, expressive power}
}
Document
DOI: 10.4230/LIPIcs.TIME.2020.6
Temporal Logic with Recursion

Authors: Florian Bruse and Martin Lange

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)

Abstract
We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments. Unlike other proposals for modal fixpoint logics of high expressive power, we obtain logics that retain some of the appealing pragmatic advantages of CTL and LTL, yet have expressive power beyond that of the modal μ-calculus or MSO. We advocate these logics by showing how the recursion operator can be used to express interesting non-regular properties. We also study decidability and complexity issues of the standard decision problems.
Cite as

Florian Bruse and Martin Lange. Temporal Logic with Recursion. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.TIME.2020.6,
  author =	{Bruse, Florian and Lange, Martin},
  title =	{{Temporal Logic with Recursion}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{6:1--6:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.6},
  URN =		{urn:nbn:de:0030-drops-129748},
  doi =		{10.4230/LIPIcs.TIME.2020.6},
  annote =	{Keywords: formal specification, temporal logic, expressive power}
}
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