International audience

We show how to efficiently solve problems involving a quantitative measure, here called energy , as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm 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 platforms TChecker and Spot.

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.

We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

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.

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.

Abstract 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 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.

Abstract We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step, we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.

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 distributed development of modern systems, contracts play a vital role in ensuring interoperability of components and adherence to specifications. It is therefore often desirable to verify the satisfaction of an overall property represented as a contract, given the satisfaction of smaller properties also represented as contracts. When the verification result is negative, designers must face the issue of refining the subproperties and components. This is an instance of the classical synthesis problems: “can we construct a model that satisfies some given specification?” In this work, we propose two strategies enabling designers to synthesize or refine a set of contracts so that their composition satisfies a given contract. We develop a generic algebraic method and show how it can be applied in different contract models to support top-down component-based development of distributed systems.

We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time.

We develop a *-continuous Kleene omega-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on *-continuous Kleene omega-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and Büchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.

In this paper we study one-clock priced timed automata in which prices can grow linearly (dp/dt = k) or exponentially (dp/dt = kp), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).