by Nicolas Markey
The design of complex systems such as those used in transportation, mobile communication and home automation, raises fundamental challenges: these systems are made of heterogeneous components that interact continuously with each other (collaboratively or as adversaries) and with their environments. Available methods (such as model-based verification, quantitative model-checking, or controller synthesis) only address specific aspects of complex systems. The FP7 project “Cassting” is developing a novel approach for analysing and designing complex systems in their totality, using non-zero-sum games to model their behaviours.
Formal methods for verifying computerised systems offer a powerful approach for validating the adequacy of the systems against their requirements. Based on deep theoretical results in logics and automata, model checking is one such approach. This approach involves modelling a system as a mathematical object (a finite-state automaton in the basic case), and applying algorithms for comparing the behaviour of that model against a logical property. Model checking has now reached maturity [1] through the development of efficient symbolic techniques, state-of-the-art tool support, and numerous successful applications to various areas.
Building on this framework, automatic synthesis techniques have recently been proposed. These techniques allow a model of a system (that is correct in construction) to be built automatically based on certain specifications. This model can then be refined to produce a validated implementation, thereby avoiding a trial-and-error approach of model checking. It is usual - and convenient - to rephrase the problem of automatic synthesis in the framework of game theory. In this metaphor, the system to be synthesized is then represented as a strategy, which should win against any behaviour of the system's environment, represented by the other player. The winning condition is used to express the correctness properties that we want the system to satisfy. This game-based approach to the synthesis of systems interacting with their environment has been greatly developed over the last twenty years, and is approaching maturity [2].
It should be noted, however, that up until now, formal methods have mostly focused on two-player zero-sum games, which only encompass the purely antagonist setting and may only model centralized control. Multiple-player games with non-zero-sum objectives have been considered, e.g., in algorithmic game theory, but they were strategic games, as opposed to the infinite-duration games on graphs that apply particularly well to synthesis.
Within the Cassting project, we are designing a game-based framework for modelling and reasoning about cyber-physical systems. This is much more than just a minor extension of the existing framework: while the basic concept of using game models is preserved, radically new concepts and techniques have to be developed in order to build a powerful formalism, equipped with efficient algorithms and tools for modelling and synthesizing such complex systems. In particular, while winning strategies are the central concept in adversarial games, multiple-player games come with a full range of equilibria for globally characterizing the admissible behaviours of the players. Understanding how this can be adapted to infinite duration games representing cyber-physical systems is already an important part of our work [3]. Setting up a complete framework, with powerful formalisms and efficient algorithms for synthesizing the relevant strategies and the corresponding systems, is thus the main focus of our research. In order to fit to the systems we model, quantitative constraints (in particular on time or energy consumption) are a must-have feature of our modelling formalism: components of cyber-physical systems are often small independent devices with limited resources. Perturbations and imperfect communications are also part of our framework.
To validate our approach, our industrial partners have selected several case studies for us. These cases come from areas of smart buildings and smart grids, trying to optimize energy consumption and harvesting at different levels of scale. In the first case study, we aim at designing distributed, robust controllers for a floor heating system, in order to improve the efficiency of the currently implemented centralized controller. The second case focuses on a home-automation system, with a dynamic set of devices, including HVAC (climate-control) appliances, lighting, etc., with the aim of making the whole system easily reconfigurable. Finally, a third case study is concerned with optimizing energy harvesting and consumption of a whole set of houses equipped with solar panels and heat pumps, taking care of weather forecasts and varying energy prices.
Figure 1: Home automation is one of our target applications.
The Cassting project includes five academic partners: CNRS/Laboratory Specification and Verification, France (Coordinator); University of Mons, Belgium; Université Libre de Bruxelles, Belgium; University of Aalborg, Denmark; RWTH Aachen, Germany. It also has two industrial partners: Seluxit, Denmark (an SME specialized in home automation) and Energi Nord, Denmark (an energy provider). The project started in April 2013, and will run for three years, with a total budget of approximately 2.7 million euros. Cassting is part of the Coordination Action FoCAS (Fundamentals of Collective Adaptive Systems).
Links:
Cassting project: http://www.cassting-project.eu/
FoCAS coordination action: http://www.focas.eu/
References:
[1] M. Edmund et al.: “Turing Lecture: Model Checking: Algorithmic Verification and Debugging”, Communications of the ACM 52(11):74-84 ACM, 2009
[2] C-H. Cheng et al.: “MGSyn: Automatic Synthesis for Industrial Automation”, in proc. of CAV'12, LNCS 7358, Springer, 2012
[3] J. Y. Halpern: “Beyond Nash Equilibrium: Solution Concepts for the 21st century” In K. R. Apt, E. Grädel (eds.), Lectures in Game Theory for Computer Scientists, chapter 8, Cambridge, 2011.
Please contact:
Nicolas Markey
CNRS & ENS Cachan, France
E-mail:
