18 citations · 100 across the 22 of their papers we have counts for
24 papers
Verifying And Interpreting Neural Networks using Finite Automata
Marco Sälzer, Eric Alsmann, Florian Bruse +1
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, a…
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…
Fundamental Limits in Formal Verification of Message-Passing Neural Networks
Marco Sälzer, Martin Lange
Output reachability and adversarial robustness are among the most relevant safety properties of neural networks. We show that in the context of Message Passing Neural Networks (MPN…
Reachability In Simple Neural Networks
Marco Sälzer, Martin Lange
We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem…
Reachability Is NP-Complete Even for the Simplest Neural Networks
Marco Sälzer, Martin Lange
We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem…
Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
Eric Alsmann, Florian Bruse, Martin Lange
We investigate the expressive power of the two main kinds of program logics for complex, non-regular program properties found in the literature: those extending propositional dynam…
Local Higher-Order Fixpoint Iteration
Florian Bruse, Jörg Kreiker, Martin Lange +1
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…
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
Arno Ehle, Norbert Hundeshagen, Martin Lange
The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Form…
Existential length universality
Paweł Gawrychowski, Martin Lange, Narad Rampersad +2
We study the following natural variation on the classical universality problem: given a language represented by (e.g., a DFA/RE/NFA/PDA), does there exist an integer $\e…
Multi-Buffer Simulations for Trace Language Inclusion
Milka Hutagalung, Norbert Hundeshagen, Dietrich Kuske +2
We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers befor…
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 te…
Two-Buffer Simulation Games
Milka Hutagalung, Norbert Hundeshagen, Dietrich Kuske +2
We consider simulation games played between Spoiler and Duplicator on two Buchi automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers…
The Arity Hierarchy in the Polyadic -Calculus
Martin Lange
The polyadic mu-calculus is a modal fixpoint logic whose formulas define relations of nodes rather than just sets in labelled transition systems. It can express exactly the polynom…
The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs
Arno Ehle, Norbert Hundeshagen, Martin Lange
We present the Sequent Calculus Trainer, a tool that supports students in learning how to correctly construct proofs in the sequent calculus for first-order logic with equality. It…
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 form…
Buffered Simulation Games for Büchi Automata
Milka Hutagalung, Martin Lange, Etienne Lozes
Simulation relations are an important tool in automata theory because they provide efficiently computable approximations to language inclusion. In recent years, extensions of ordin…
Satisfiability Games for Branching-Time Logics
Oliver Friedmann, Martin Lange, Markus Latte
The satisfiability problem for branching-time temporal logics like CTL*, CTL and CTL+ has important applications in program specification and verification. Their computational comp…
The μ-Calculus Alternation Hierarchy Collapses over Structures with Restricted Connectivity
Julian Gutierrez, Felix Klaedtke, Martin Lange
It is known that the alternation hierarchy of least and greatest fixpoint operators in the mu-calculus is strict. However, the strictness of the alternation hierarchy does not nece…
Model-Checking Process Equivalences
Martin Lange, Etienne Lozes, Manuel Vargas Guzmán
Process equivalences are formal methods that relate programs and system which, informally, behave in the same way. Since there is no unique notion of what it means for two dynamic…
Model-Checking the Higher-Dimensional Modal mu-Calculus
Martin Lange, Etienne Lozes
The higher-dimensional modal mu-calculus is an extension of the mu-calculus in which formulas are interpreted in tuples of states of a labeled transition system. Every property tha…
Extended Computation Tree Logic
Roland Axelsson, Matthew Hague, Stephan Kreutzer +2
We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages. For instance, a language may…
Local Strategy Improvement for Parity Game Solving
Oliver Friedmann, Martin Lange
The problem of solving a parity game is at the core of many problems in model checking, satisfiability checking and program synthesis. Some of the best algorithms for solving parit…
On the Hybrid Extension of CTL and CTL+
Ahmet Kara, Martin Lange, Thomas Schwentick +1
The paper studies the expressivity, relative succinctness and complexity of satisfiability for hybrid extensions of the branching-time logics CTL and CTL+ by variables. Previous co…
The Complexity of Model Checking Higher-Order Fixpoint Logic
Roland Axelsson, Martin Lange, Rafal Somla
Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed λ-calculus and the modal λ-calculus. This makes it a highly expressive temporal logic that is capable of expressin…