Notions of Behavioral Equivalence

Behavioral equivalences are at the basis of program semantics in formal methods. But there’s a lot of such notions.

My research is about making the spectrum of behavioral equivalences easily usable through algorithms and tools.

Weak Behavioral Equivalences

For models with internal behavior, one usually uses so-called weak notions of equivalence that abstract away “internal” aspects.

My research interest lies with the weakest forms of bisimilarity, namely coupled similarity and contrasimilarity.

Causality and Event Structures

Often one does not only want to model what may happen in a system but also the dependencies and causalities between events.

I take particular interest in counterfactuals—a formal way of capturing what would need to change in order for statements to be true.

Real-Time Systems

Real-world systems and distributed algorithms rely heavily on concepts of real-time and timeouts.

At the beginning of my studies, I was concerned with the translation of Timed CSP to Timed Automata.

Distributed Algorithms

Distributed algorithms are at the core of our networked world.

I’ve contributed to Isabelle/HOL formalizations of distributed consensus algorithms (and of the impossibility of asynchronous consensus with faulty processes).

Functional Programming and Verification

A lot of elegance and robustness can be achieved by expressing programs mathematically.

I love using Scala for my programming and Isabelle/HOL for formal verifications and also teach the use of such tools.

Software Engineering

At the end of the day, we’re all software engineers.

I give courses touching upon Scrum project management, object-oriented programming, game dev, and quality assurance.

2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
Equivalence Problems as Games
ISCAS, Beijing (2024-09)
Equivalence Problems as Games
Talk
Higher-Order Diadic µ-Calculus for Checking Process Equivalences
MTV TU Berlin (2024-08)
Higher-Order Diadic µ-Calculus—An Efficient Framework for Checking Process Equivalences?
Advising Valentin Stöcker Supervisors: Uwe Nestmann, Martin Lange
Accelerating Process Equivalence Energy Games using WebGPU
MTV TU Berlin (2024-04)
Accelerating Process Equivalence Energy Games using WebGPU
Advising Gabriel Vogel Supervisors: Uwe Nestmann, Stephan Kreutzer
Measuring expressive power of HML formulas in Isabelle/HOL
MTV TU Berlin (2024-04)
Measuring expressive power of HML formulas in Isabelle/HOL
Advising Karl Mattes Supervisors: Uwe Nestmann, Stephan Kreutzer
One Energy Game for the Weak Spectrum One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics
Paper Benjamin Bisping, David Jansen
Contrasimilarity through Games, Modal Logic, and Complexity Characterizing Contrasimilarity through Games, Modal Logic, and Complexity
Article Benjamin Bisping, Luisa Montanari
Write, Review, and Publish (Master seminar)
MTV TU Berlin (2024-04)
Write, Review, and Publish (Master seminar)
Course
Models of Dynamic Systems
MTV TU Berlin (2024-05)
Models of Dynamic Systems
Course
Concurrency Formalisms as Games Concurrency Formalisms as Computer Games
Talk
Integration eines generischen Äquivalenzprüfers in CAAL
MTV TU Berlin (2023-10)
Integration eines generischen Äquivalenzprüfers in CAAL
Advising Fabian Ozegowski Supervisors: Uwe Nestmann, Stephan Kreutzer
Process Equivalence Problems as Energy Games
CAV'23, LNCS 13964 (2023-08)
Process Equivalence Problems as Energy Games
Paper Benjamin Bisping
Games to Decide All Behavioral Equivalences Games to Decide All Behavioral Equivalences at Once
Talk
Process Equivalence Problems as Energy Games
CAV 2023, Paris (2023-07)
Process Equivalence Problems as Energy Games
Talk
Energy games to navigate the landscape of equivalences Energy games to navigate the landscape of behavioural equivalences
Talk
Coupled Similarity and Contrasimilarity, and How to Compute Them
AFP 2023 (2023-08)
Coupled Similarity and Contrasimilarity, and How to Compute Them
Artifact Benjamin Bisping, Luisa Montanari
Linear-Time–Branching-Time Spectroscopy Accounting for Silent...
arXiv (2023-05)
Linear-Time–Branching-Time Spectroscopy Accounting for Silent Steps
Paper Benjamin Bisping, David N. Jansen
Nonlinear Counterfactuals in Isabelle/HOL
MTV TU Berlin (2023-12)
Nonlinear Counterfactuals in Isabelle/HOL
Advising Johannes Hauschild Supervisors: Uwe Nestmann, Bernd Finkbeiner
Computer game about counterfactual truth conditions
MTV TU Berlin (2023-01)
An educational computer game about counterfactual truth conditions
Advising Bruno Lönne Supervisors: Uwe Nestmann, Stephan Kreutzer
Research at Work (Master project course)
MTV TU Berlin (2023-10)
Research at Work (Master project course)
Course
Models of Dynamic Systems
MTV TU Berlin (2023-04)
Models of Dynamic Systems
Course
MD Basic
X-mas project (2023-01)
MD Basic
Tool
Deciding All Behavioral Equivalences at Once Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy
Article Benjamin Bisping, David N. Jansen, Uwe Nestmann
An educational tool for Linear-time–Branching-time Spectroscopy
MTV TU Berlin (2022-07)
Developing an educational tool for Linear-time–Branching-time Spectroscopy
Advising Thanh Mai Duong Supervisors: Uwe Nestmann, Stephan Kreutzer
A Video Game about Reactive Bisimilarity
MTV TU Berlin (2022-12)
A Video Game about Reactive Bisimilarity
Advising Eloi Sandt Supervisors: Uwe Nestmann, Stephan Kreutzer
Automatisierte Reduktion von reaktiver zu starker Bisimilarität
MTV TU Berlin (2022-11)
Automatisierte Reduktion von reaktiver zu starker Bisimilarität
Advising Zead Alshukariri Supervisors: Uwe Nestmann, Stephan Kreutzer
Simulation fehlertoleranter Konsensalgorithmen in Hash.ai
MTV TU Berlin (2022-11)
Simulation fehlertoleranter Konsensalgorithmen in Hash.ai
Advising Roy Adler Supervisors: Uwe Nestmann, Stefan Schmid
The Software Horror Picture Show
MTV TU Berlin (2022-10)
The Software Horror Picture Show
Course
pr.mtv.tu-berlin.de
TU Berlin (2022-07)
pr.mtv.tu-berlin.de
Website
Models of Dynamic Systems
MTV TU Berlin (2022-04)
Models of Dynamic Systems
Course
HML Synthesis of Distinguished Processes
MTV TU Berlin (2021-12)
HML Synthesis of Distinguished Processes
Advising Johanna England Supervisors: Uwe Nestmann, Stephan Kreutzer
Linear-Time−Branching-Time Spectroscopy as an Educational Web...
MTV TU Berlin (2021-11)
Linear-Time−Branching-Time Spectroscopy as an Educational Web Browser Game
Advising Mariusz Trzeciakiewicz Supervisors: Uwe Nestmann, Stephan Kreutzer
Let's decide all equivalences at once! Let's decide all equivalences at once!
Talk Benjamin Bisping
Video: A Game for Linear-time–Branching-time Spectroscopy Video: A Game for Linear-time–Branching-time Spectroscopy
Talk Benjamin Bisping
A Game for Linear-time–Branching-time Spectroscopy
TACAS 2021, LNCS 12651 (2021-03)
A Game for Linear-time–Branching-time Spectroscopy
Paper Benjamin Bisping, Uwe Nestmann
Linear-time–Branching-time Spectroscope TACAS'21 Edition
Zenodo (2021-01)
Linear-time–Branching-time Spectroscope: TACAS 2021 Edition
Artifact
A Game Characterization for Contrasimilarity A Game Characterization for Contrasimilarity
Paper Benjamin Bisping, Luisa Montanari
Kontrasimulation als Spiel
MTV TU Berlin (2021-05)
Kontrasimulation als Spiel
Advising Luisa Montanari Supervisors: Uwe Nestmann, Stephan Kreutzer
Reducing Strong Reactive Bisimilarity to Strong Bisimilarity
MTV TU Berlin (2021-06)
Reducing Strong Reactive Bisimilarity to Strong Bisimilarity
Advising Maximilian Pohlmann Supervisors: Uwe Nestmann, Stephan Kreutzer
Introduction into interactive theorem proving (Isabelle-Lab)
MTV TU Berlin (2021-09)
Introduction into interactive theorem proving (Isabelle-Lab)
Course Florian Kammüller, Benjamin Bisping
Statically analysing Elixir programs
MTV TU Berlin (2021-01)
Statically analysing inter-process communication in Elixir programs
Advising Jonas Bulik Supervisors: Uwe Nestmann, Florian Kammüller
The Software Horror Picture Show
MTV TU Berlin (2021-10)
The Software Horror Picture Show
Course
concurrency-theory.org
(2021-07)
concurrency-theory.org
Website Benjamin Bisping, Pedro D’Argenio
Models of Dynamic Systems
MTV TU Berlin (2021-04)
Models of Dynamic Systems
Course
Charting the jungle of process calculi encodings
MTV TU Berlin (2020-12)
Charting the jungle of process calculi encodings
Advising Tobias Wittig Supervisors: Uwe Nestmann, Kirstin Peters
Spiel zu Verhaltensäquivalenzen
MTV TU Berlin (2020-09)
Ein Computerspiel zum Erlernen von Verhaltensäquivalenzen
Advising Michael Wrusch Supervisors: Uwe Nestmann, Manfred Hauswirth
Linear-time–Branching-time Spectroscope
(2020-08)
Linear-time–Branching-time Spectroscope
Tool
Coupled Similarity: The First 32 Years Coupled Similarity: The First 32 Years
Article Benjamin Bisping, Uwe Nestmann, Kirstin Peters
Coupled Similarity as an automated checker for mCRL2
MTV TU Berlin (2020-05)
Implementing Coupled Similarity as an automated checker for mCRL2
Advising Hùòng Ngoc Lê Supervisors: Uwe Nestmann, Stephan Kreutzer
Process equivalences as a video game
MTV TU Berlin (2020-05)
Process equivalences as a video game
Advising Dominik Peacock Supervisors: Uwe Nestmann, Manfred Hauswirth
Visualising and Model Checking Counterfactuals
MTV TU Berlin (2020-09)
Visualising and Model Checking Counterfactuals
Advising Jannik Moritz Reichert Supervisors: Uwe Nestmann, Stephan Kreutzer
Counterfactuals, Dispositions, and Hyperproperties
D-CON 2020 (2020-03)
Counterfactuals, Dispositions, and Hyperproperties
Talk
Introduction into interactive theorem proving (Isabelle-Lab)
MTV TU Berlin (2020-09)
Introduction into interactive theorem proving (Isabelle-Lab)
Course Florian Kammüller, Benjamin Bisping
Models of Dynamic Systems
MTV TU Berlin (2020-10)
Models of Dynamic Systems
Course
Models of Dynamic Systems
MTV TU Berlin (2020-04)
Models of Dynamic Systems
Course
Computing Coupled Similarity
TACAS 2019, Prague (2019-04)
Computing Coupled Similarity
Talk
Computing Coupled Similarity
TACAS 2019, LNCS 11427 (2019-04)
Computing Coupled Similarity
Paper Benjamin Bisping, Uwe Nestmann
Isabelle/HOL proof and Apache Flink program for TACAS 2019 paper
Figshare (2019-03)
Isabelle/HOL proof and Apache Flink program for TACAS 2019 paper
Artifact
Introduction into interactive theorem proving (Isabelle-Lab)
MTV TU Berlin (2019-08)
Introduction into interactive theorem proving (Isabelle-Lab)
Course Florian Kammüller, Benjamin Bisping
Models of Dynamic Systems
MTV TU Berlin (2019-10)
Models of Dynamic Systems
Course
Models of Dynamic Systems
MTV TU Berlin (2019-04)
Models of Dynamic Systems
Course
Computing Coupled Similarity
TU Berlin (2018-04)
Computing Coupled Similarity
Master thesis Supervisors: Uwe Nestmann, Holger Hermanns
Computing Coupled Similarity – When Weak Bisimulation Is Too ... Computing Coupled Similarity – When Weak Bisimulation Is Too Strong
Talk
Coupled Sim Fiddle
(2018-02)
Coupled Sim Fiddle
Tool
Models of Dynamic Systems
MTV TU Berlin (2018-10)
Models of Dynamic Systems
Course Benjamin Bisping, Uwe Nestmann
Coupled Similarity Coupled Similarity
Talk
Event Structures with Higher-Order Dynamics
TU Berlin (2017-12)
Event Structures with Higher-Order Dynamics
Contribution to work by David S. Karcher
Tooltorial for HD-Event Structures Tooltorial for HD-Event Structures
Talk Benjamin Bisping, Paul-David Brodmann, David S. Karcher
HDES Tool – Analyzing Higher-order Dynamic-causality Event St... HDES Tool – Analyzing Higher-order Dynamic-causality Event Structures
Tool Supervisor: David S. Karcher
Mechanical Verification of a Constructive Proof for FLP Mechanical Verification of a Constructive Proof for FLP
Paper Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann
A Constructive Proof for FLP
AFP 2016 (2016-05)
A Constructive Proof for FLP
Artifact Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann
Analysis and implementation of hierarchical mutually recursiv...
(2015-10)
Analysis and implementation of hierarchical mutually recursive first class modules
Contribution to work by Judith Rohloff
Implementing Control Flow Analysis for a Functional Language ...
TU Berlin (2014-04)
Implementing Control Flow Analysis for a Functional Language with First-Class Modules
Bachelor thesis Supervisors: Peter Pepper, Stefan Jähnichen
Modeling and verification of distributed algorithms in theore...
TU Berlin (2013-09)
Modeling and verification of distributed algorithms in theorem proving environments
Contribution to work by Philipp Küfner
Exercise: Algorithmic and functional solution of discrete pro...
SESE TU Berlin (2013-10)
Exercise: Algorithmic and functional solution of discrete problems
Course Supervisor: Sabine Glesner
SL2 Module System
ÜBB TU Berlin (2013-07)
SL2 Module System
Tool Benjamin Bisping, Rico Jasper, Sebastian Lohmeier, Friedrich Psiorz Supervisor: Christoph Höger
Exercise: Data structures and algorithms in imperative progra...
CG TU Berlin (2013-04)
Exercise: Data structures and algorithms in imperative programming
Course Supervisor: Marc Alexa
Mechanical Verification of Parameterized Real-Time Systems
SESE TU Berlin (2012-05)
Mechanical Verification of Parameterized Real-Time Systems
Contribution to work by Thomas Göthel
Exercise: Algorithmic and functional solution of discrete pro...
ÜBB TU Berlin (2012-10)
Exercise: Algorithmic and functional solution of discrete problems
Course Supervisor: Peter Pepper
Exercise: Data structures and algorithms in imperative progra...
RBO TU Berlin (2012-04)
Exercise: Data structures and algorithms in imperative programming
Course Supervisor: Oliver Brock
tcsp2ta: Automatic translation of Timed CSP to Timed Automata
DFG Project VATES (2011-05)
tcsp2ta: Automatic translation of Timed CSP to Timed Automata
Tool Supervisors: Thomas Göthel, Sabine Glesner
Exercise: Algorithmic and functional solution of discrete pro...
SESE TU Berlin (2011-10)
Exercise: Algorithmic and functional solution of discrete problems
Course Supervisor: Sabine Glesner
Exercise: Data structures and algorithms in imperative progra...
RBO TU Berlin (2011-04)
Exercise: Data structures and algorithms in imperative programming
Course Supervisor: Oliver Brock
Exercise: Algorithmic and functional solution of discrete pro...
ÜBB TU Berlin (2010-10)
Exercise: Algorithmic and functional solution of discrete problems
Course Supervisor: Peter Pepper