Uli Fahrenberg

A Myhill-Nerode theorem for higher-dimensional automata

By Uli Fahrenberg, Krzysztof Ziemiański


In Application and theory of petri nets and concurrency (PETRI NETS)

Abstract We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular precisely if it has finite prefix quotient. HDAs extend standard automata with additional structure, making it possible to distinguish between interleavings and concurrency. We also introduce deterministic HDAs and show that not all HDAs are determinizable, that is, there exist regular languages that cannot be recognised by a deterministic HDA. Using our theorem, we develop an internal characterisation of deterministic languages.

Continue reading

Catoids and modal convolution algebras

Abstract We show how modal quantales arise as convolution algebras Q^X of functions from catoids X, that is, multisemigroups with a source map \ell and a target map r, into modal quantales Q, which can be seen as weight or value algebras. In the tradition of boolean algebras with operators we study modal correspondences between algebraic laws in X, Q and Q^X. The class of catoids we introduce generalises Schweizer and Sklar’s function systems and object-free categories to a setting isomorphic to algebras of ternary relations, as they are used for boolean algebras with operators and substructural logics.

Continue reading

Closure and decision properties for higher-dimensional automata

By Amazigh Amrane, Hugo Bazille, Uli Fahrenberg, Krzysztof Ziemiański


In 20th international colloquium on theoretical aspects of computing (ICTAC’23)


Continue reading

Energy problems in finite and timed automata with Büchi conditions

By Sven Dziadek, Uli Fahrenberg, Philipp Schlehuber-Caissier


In International symposium on formal methods (FM)

Abstract We show how to efficiently solve energy Büchi problems in finite weighted automata and in one-clock weighted timed automata. Solving the former problem is our main contribution and is handled by a modified version of Bellman-Ford interleaved with Couvreur’s algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source tools TChecker and Spot.

Continue reading

Higher-dimensional timed and hybrid automata

By Uli Fahrenberg


In Leibniz Transactions on Embedded Systems

Abstract We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata. The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.

Continue reading

Introduction to the special issue on distributed hybrid systems

By Alessandro Abate, Uli Fahrenberg, Martin Fränzle


In Leibniz Transactions on Embedded Systems

Abstract This special issue contains seven papers within the broad subject of Distributed Hybrid Systems, that is, systems combining hybrid discrete-continuous state spaces with elements of concurrency and logical or spatial distribution. It follows up on several workshops on the same theme which were held between 2017 and 2019 and organized by the editors of this volume. The first of these workshops was held in Aalborg, Denmark, in August 2017 and associated with the MFCS conference.

Continue reading

Featured games

By Uli Fahrenberg, Axel Legay


In Science of Computer Programming

Abstract Feature-based analysis of software product lines and family-based model checking have seen rapid development. Many model checking problems can be reduced to two-player games on finite graphs. A prominent example is mu-calculus model checking, which is generally done by translating to parity games, but also many quantitative model-checking problems can be reduced to (quantitative) games. As part of a program to make game-based model checking available for software product lines, we introduce featured reachability games, featured minimum reachability games, featured discounted games, featured energy games, and featured parity games.

Continue reading

A Kleene theorem for higher-dimensional automata

By Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański


In 33rd international conference on concurrency theory (CONCUR 2022)

Abstract We prove a Kleene theorem for higher-dimensional automata (HDAs). It states that the languages they recognise are precisely the rational subsumption-closed sets of interval pomsets. The rational operations include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce HDAs with interfaces as presheaves over labelled precube categories and use tools inspired by algebraic topology, such as cylinders and (co)fibrations. HDAs are a general model of non-interleaving concurrency, which subsumes many other models in this field.

Continue reading

Posets with interfaces as a model for concurrency

Abstract We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternatively, taking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of a poset. We show that iposets under gluing composition form a category, which generalises the monoid of posets under serial composition up to isomorphism.

Continue reading