Uli Fahrenberg

Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg et al.

In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing constraints and variable energy rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy rates. We also consider the optimization problem of identifying the minimal upper bound that will permit the existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.

Uli Fahrenberg

We introduce a new formalism of higher-dimensional timed automata, based on van Glabbeek's higher-dimensional automata and Alur's timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also show how to use tensor products to combat state-space explosion and how to extend the setting to higher-dimensional hybrid automata.

Uli Fahrenberg, Krzysztof Ziemiański

We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular if and only 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. Lastly, we develop analogues of the Myhill-Nerode construction and of determinacy for HDAs with interfaces.

Uli Fahrenberg, Axel Legay

Feature-based SPL analysis 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. In their FASE'20 paper, ter Beek et al.\ introduce parity games with variability in order to develop family-based mu-calculus model checking of featured transition systems. We generalize their model to general featured games and show how these may be analysed in a family-based manner. We introduce featured reachability games, featured minimum reachability games, featured discounted games, featured energy games, and featured parity games. We show how to compute winners and values of such games in a family-based manner. We also show that all these featured games admit optimal featured strategies, which project to optimal strategies for any product. Further, we develop family-based algorithms, using late splitting, to compute winners, values, and optimal strategies for all the featured games we have introduced.

Uli Fahrenberg, Axel Legay

A featured transition system is a transition system in which the transitions are annotated with feature expressions: Boolean expressions on a finite number of given features. Depending on its feature expression, each individual transition can be enabled when some features are present, and disabled for other sets of features. The behavior of a featured transition system hence depends on a given set of features. There are algorithms for featured transition systems which can check their properties for all sets of features at once, for example for LTL or CTL properties. Here we introduce a model of featured weighted automata which combines featured transition systems and (semiring-) weighted automata. We show that methods and techniques from weighted automata extend to featured weighted automata and devise algorithms to compute quantitative properties of featured weighted automata for all sets of features at once. We show applications to minimum reachability and to energy properties.

Rafael Olaechea, Uli Fahrenberg, Joanne M. Atlee et al.

A software product line is a family of software products that share a common set of mandatory features and whose individual products are differentiated by their variable (optional or alternative) features. Family-based analysis of software product lines takes as input a single model of a complete product line and analyzes all its products at the same time. As the number of products in a software product line may be large, this is generally preferable to analyzing each product on its own. Family-based analysis, however, requires that standard algorithms be adapted to accomodate variability. In this paper we adapt the standard algorithm for computing limit average cost of a weighted transition system to software product lines. Limit average is a useful and popular measure for the long-term average behavior of a quality attribute such as performance or energy consumption, but has hitherto not been available for family-based analysis of software product lines. Our algorithm operates on weighted featured transition systems, at a symbolic level, and computes limit average cost for all products in a software product line at the same time. We have implemented the algorithm and evaluated it on several examples.

Uli Fahrenberg, Fabrizio Biondi, Kevin Corre et al.

We propose a new similarity measure between texts which, contrary to the current state-of-the-art approaches, takes a global view of the texts to be compared. We have implemented a tool to compute our textual distance and conducted experiments on several corpuses of texts. The experiments show that our methods can reliably identify different global types of texts.