Author name cluster

Florian Bruse

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

20 papers

2 author rows

I&C Journal 2026 Journal Article

Verifying and interpreting neural networks using finite automata

Marco Sälzer
Eric Alsmann
Florian Bruse
Martin Lange

Verifying properties and interpreting the behaviour of deep neural networks (DNN) is an important task given their ubiquitous use in applications, including safety-critical ones, and their black-box nature. We propose an automata-theoretic approach to tackling problems arising in DNN analysis. We show that the input-output behaviour of a DNN can be captured precisely by a (special) weak Büchi automaton and we show how these can be used to address common verification and interpretation tasks of DNN like adversarial robustness or minimum sufficient reasons.

Details DOI

TIME Conference 2025 Conference Paper

Higher-Order Timed Automata and Tail Recursion

Florian Bruse

Timed Automata (TA) are a popular formalism to model systems in dense linear time. However, due to their finite state-space, they can only model systems with a finitary logical behavior. There are extensions to e. g. , timed pushdown systems and timed recursive state machines. Higher-Order Recursion Schemes (HORS) are another popular model for infinite-state, non-regular systems, naturally stratified by their type-theoretic order. We recently introduced Real-Time Recursion schemes as an approximation of HORS to real-time systems. This paper updates Real-Time Recursion Schemes into Higher-Order Timed Automata, a formalism that defines a tree-shaped timed automaton, which is more suitable to model actual systems. We show that the model-checking problem against the timed version of the modal mu-calculus exhibits the expected complexity bounds, i. e. , an increase by one exponential towards the untimed version. We also show that, in the presence of tail recursion, half an exponential can be recovered, mirroring similar gains in the untimed setting. We also give a matching lower bound for the special case of order-1 HORTA. We conjecture that this can be generalized for all orders.

Details

I&C Journal 2024 Journal Article

Model checking timed recursive CTL

Florian Bruse
Martin Lange

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.

Details DOI

TIME Conference 2024 Conference Paper

Real-Time Higher-Order Recursion Schemes

Eric Alsmann
Florian Bruse

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.

Details

TCS Journal 2024 Journal Article

Weights of formal languages based on geometric series with an application to automatic grading

Florian Bruse
Maurice Herwig
Martin Lange

We present a weight measure on formal languages based on the summands of a geometric series discounted by the fraction of words of certain length in the language, guaranteeing the weight to be a real value between 0 and 1 for any language. We show that this weight measure is computable for regular languages. As an application, we derive a distance metric between languages as the weight of their symmetric difference and show how it can be used in automatic grading of standard exercises in formal language theory classes.

Details DOI

TIME Conference 2023 Conference Paper

The Calculus of Temporal Influence

Florian Bruse
Marit Kastaun
Martin Lange 0001
Sören Möller

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.

Details

I&C Journal 2023 Journal Article

The tail-recursive fragment of timed recursive CTL

Florian Bruse
Martin Lange

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 already in its data complexity, i. e. for a fixed formula. The upper bound is obtained via a model-checking procedure on region graphs combining standard untiming constructions with a tailored algorithm. The lower bound is established by a reduction from a suitable tiling problem.

Details DOI

Highlights Conference 2023 Conference Abstract

Timed Recursive CTL

Florian Bruse

We study the complexity of the model-checking problem of, TRecCTL. This logic is obtained as the merger of two extensions of CTL, Timed CTL and Temporal Logic with Recursion. The former extends CTL by operators to talk about timed aspects of systems defined by timed automata. The latter adds a recursion operator to CTL, greatly increasing the expressive power of the resulting logic. We obtain that the model-checking problem for TRecCTL is 2EXPTIME complete. Moreover, the model-checking problem for the so-called tail-recursive fragment of TRecCTL, obtained by limiting the way recursion is used, is EXPSPACE complete. Notably, the former problem is already 2EXPTIME hard in its expression complexity, and the latter is already EXPSPACE complete in its data complexity. Moreover, the hardness result already holds for timed automata with one clock only. For Timed CTL, the amount of clocks present is important. Contributed talk given by Florian Bruse Lunch Friday 14h00 - 14h48, Contributed Talks Model Theory & Logic | HS 3 | chair: Ramanathan Thinniyam Srinivasan Applications and Other Topics | HS 4 | chair: Supratik Chakraborty Model Theory & Logic | HS 3 | chair: Ramanathan Thinniyam Srinivasan Applications and Other Topics | HS 4 | chair: Supratik Chakraborty

Details

GandALF Workshop 2022 Workshop Paper

Capturing Bisimulation-Invariant Exponential-Time Complexity Classes

Florian Bruse
David Kronenberger
Martin Lange

Otto's Theorem characterises the bisimulation-invariant PTIME queries over graphs as exactly those that can be formulated in the polyadic mu-calculus, hinging on the Immerman-Vardi Theorem which characterises PTIME (over ordered structures) by First-Order Logic with least fixpoints. This connection has been extended to characterise bisimulation-invariant EXPTIME by an extension of the polyadic mu-calculus with functions on predicates, making use of Immerman's characterisation of EXPTIME by Second-Order Logic with least fixpoints. In this paper we show that the bisimulation-invariant versions of all classes in the exponential time hierarchy have logical counterparts which arise as extensions of the polyadic mu-calculus by higher-order functions. This makes use of the characterisation of k-EXPTIME by Higher-Order Logic (of order k+1) with least fixpoints, due to Freire and Martins.

PDF Details DOI

I&C Journal 2022 Journal Article

Local higher-order fixpoint iteration

Florian Bruse
Jörg Kreiker
Martin Lange
Marco Sälzer

Local fixpoint iteration describes a technique that restricts fixpoint iteration in function spaces to needed arguments only. It has been studied well for first-order functions in abstract interpretation and also in model checking. Here we consider the problem for least and greatest fixpoints of arbitrary type order. We define an abstract algebra of simply-typed higher-order functions with fixpoints in order to express fixpoint evaluation problems as they occur routinely in various applications, including program verification. We present an algorithm that realises local fixpoint iteration for such higher-order fixpoints, prove its correctness and study its optimisation potential in the context of several applications. We also examine a particular fragment of this higher-order fixpoint algebra which allows us to pre-compute needed arguments, as this may help to speed up the fixpoint iteration process.

Details DOI

TIME Conference 2022 Conference Paper

The Tail-Recursive Fragment of Timed Recursive CTL

Florian Bruse
Martin Lange 0001
Étienne Lozes

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.

Details

MFCS Conference 2021 Conference Paper

Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures

Florian Bruse
Marco Sälzer
Martin Lange 0001

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.

Details

TIME Conference 2021 Conference Paper

Model Checking Timed Recursive CTL

Florian Bruse
Martin Lange 0001

Details

I&C Journal 2021 Journal Article

Temporal logic with recursion

Florian Bruse
Martin Lange

We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments, thus obtaining 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 show 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.

Details DOI

GandALF Workshop 2020 Workshop Paper

Local Higher-Order Fixpoint Iteration

Florian Bruse
Jörg Kreiker
Martin Lange
Marco Sälzer

Local fixpoint iteration describes a technique that restricts fixpoint iteration in function spaces to needed arguments only. It has been studied well for first-order functions in abstract interpretation and also in model checking. Here we consider the problem for least and greatest fixpoints of arbitrary type order. We define an abstract algebra of simply typed higher-order functions with fixpoints that can express fixpoint evaluation problems as they occur routinely in various applications, including program verification. We present an algorithm that realises local fixpoint iteration for such higher-order fixpoints, prove its correctness and study its optimisation potential in the context of several applications.

PDF Details DOI

TIME Conference 2020 Conference Paper

Temporal Logic with Recursion

Florian Bruse
Martin Lange 0001

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.

Details

GandALF Workshop 2016 Workshop Paper

A Canonical Model Construction for Iteration-Free PDL with Intersection

Florian Bruse
Daniel Kernberger
Martin Lange

We study the axiomatisability of the iteration-free fragment of Propositional Dynamic Logic with Intersection and Tests. The combination of program composition, intersection and tests makes its proof-theory rather difficult. We develop a normal form for formulae which minimises the interaction between these operators, as well as a refined canonical model construction. From these we derive an axiom system and a proof of its strong completeness.

PDF Details DOI

GandALF Workshop 2016 Workshop Paper

Alternation Is Strict For Higher-Order Modal Fixpoint Logic

Florian Bruse

We study the expressive power of Alternating Parity Krivine Automata (APKA), which provide operational semantics to Higher-Order Modal Fixpoint Logic (HFL). APKA consist of ordinary parity automata extended by a variation of the Krivine Abstract Machine. We show that the number and parity of priorities available to an APKA form a proper hierarchy of expressive power as in the modal mu-calculus. This also induces a strict alternation hierarchy on HFL. The proof follows Arnold's (1999) encoding of runs into trees and subsequent use of the Banach Fixpoint Theorem.

PDF Details DOI

GandALF Workshop 2014 Workshop Paper

The Fixpoint-Iteration Algorithm for Parity Games

Florian Bruse
Michael Falk
Martin Lange

It is known that the model checking problem for the modal mu-calculus reduces to the problem of solving a parity game and vice-versa. The latter is realised by the Walukiewicz formulas which are satisfied by a node in a parity game iff player 0 wins the game from this node. Thus, they define her winning region, and any model checking algorithm for the modal mu-calculus, suitably specialised to the Walukiewicz formulas, yields an algorithm for solving parity games. In this paper we study the effect of employing the most straight-forward mu-calculus model checking algorithm: fixpoint iteration. This is also one of the few algorithms, if not the only one, that were not originally devised for parity game solving already. While an empirical study quickly shows that this does not yield an algorithm that works well in practice, it is interesting from a theoretical point for two reasons: first, it is exponential on virtually all families of games that were designed as lower bounds for very particular algorithms suggesting that fixpoint iteration is connected to all those. Second, fixpoint iteration does not compute positional winning strategies. Note that the Walukiewicz formulas only define winning regions; some additional work is needed in order to make this algorithm compute winning strategies. We show that these are particular exponential-space strategies which we call eventually-positional, and we show how positional ones can be extracted from them.

PDF Details DOI

Highlights Conference 2013 Conference Abstract

Polynomial guarded transformation for the modal mu-calculus is still open

Florian Bruse
Oliver Friedmann
Martin Lange

Guarded normal form requires occurrences of fixpoint variables in a μ-calculus formula to occur under the scope of a modal operator. The literature contains guarded transformations that effectively bring a μ-calculus formula into guarded normal form. We show that the known guarded transformations can cause an exponential blowup in formula size, contrary to existing claims of polynomial behaviour. We also show that any poly- nomial guarded transformation for μ-calculus formulas in the more relaxed vectorial form gives rise to a polynomial solution algorithm for parity games, the existence of which is an open problem.

PDF Details