Uli Fahrenberg

Introduction to the special issue on distributed hybrid systems

By Alessandro Abate, Uli Fahrenberg, Martin Fränzle

2022-12-08

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. It featured invited talks by Alessandro Abate, Martin Fränzle, Kim G. Larsen, Martin Raussen, and Rafael Wisniewski. The second workshop was held in Palaiseau, France, in July 2018, with invited talks by Luc Jaulin, Thao Dang, Lisbeth Fajstrup, Emmanuel Ledinot, and André Platzer. The third workshop was held in Amsterdam, The Netherlands, in August 2019, associated with the CONCUR conference. It featured a special theme on distributed robotics and had invited talks by Majid Zamani, Hervé de Forges, and Xavier Urbain. The vision and purpose of the DHS workshops was to connect researchers working in real-time systems, hybrid systems, control theory, formal verification, distributed computing, and concurrency theory, in order to advance the subject of distributed hybrid systems. Such systems are abundant and often safety-critical, but ensuring their correct functioning can in general be challenging. The investigation of their dynamics by analysis tools from the aforementioned domains remains fragmentary, providing the rationale behind the workshops: it was conceived that convergence and interaction of theories, methods, and tools from these different areas was needed in order to advance the subject.

Continue reading

Featured games

By Uli Fahrenberg, Axel Legay

2022-11-01

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. We show that all these admit optimal featured strategies, which project to optimal strategies for any product, and how to compute winners and values of such games in a family-based manner.

Continue reading

A Kleene theorem for higher-dimensional automata

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

2022-09-06

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. Interval orders are used as models for concurrent or distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

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. They form a 2-category when a subsumption order and a lax tensor in the form of a non-commutative parallel composition are added, which generalises the interchange monoids used for modelling series-parallel posets. We also study the gluing-parallel hierarchy of iposets, which generalises the standard series-parallel one. The class of gluing-parallel iposets contains that of series-parallel posets and the class of interval orders, which are well studied in concurrency theory, too. We also show that it is strictly contained in the class of all iposets by identifying several forbidden substructures.

Continue reading