Published: 31st July 2016
DOI: 10.4204/EPTCS.220
ISSN: 2075-2180

EPTCS 220

Proceedings Cassting Workshop on
Games for the Synthesis of Complex Systems
and 3rd International Workshop on
Synthesis of Complex Parameters
Eindhoven, The Netherlands, April 2-3, 2016

Edited by: Thomas Brihaye, Benoît Delahaye, Loïg Jezequel, Nicolas Markey and Jiří Srba

Preface
Invited Presentation: Boundedness Games
Nathanael Fijalkow
Invited Presentation: Control of Dynamic Discrete-Event-System Games
Jan H. van Schuppen
Invited Presentation: Automated Synthesis: Going Distributed
Anca Muscholl
Invited Presentation: Algorithms for Branching MDPs and Branching Stochastic Games
Kousha Etessami
Invited Presentation: Parametrized Verification of Distributed Broadcast Protocols
Giorgio Delzanno
Invited Presentation: What Population Reveals About Individual Cell Identity: Single-Cell Parameter Estimation of Models of Gene Expression in Yeast
Gregory Batt
Efficient Energy Distribution in a Smart Grid using Multi-Player Games
Thomas Brihaye, Amit Kumar Dhar, Gilles Geeraerts, Axel Haddad and Benjamin Monmege
1
Playing Games in the Baire Space
Benedikt Brütsch and Wolfgang Thomas
13
Two-Buffer Simulation Games
Milka Hutagalung, Norbert Hundeshagen, Dietrich Kuske, Martin Lange and Etienne Lozes
27
A Web-based Tool for Identifying Strategic Intervention Points in Complex Systems
Sotiris Moschoyiannis, Nicholas Elia, Alexandra S. Penn, David J.B. Lloyd and Chris Knight
39
Parametric, Probabilistic, Timed Resource Discovery System
Camille Coti
53
Weighted Branching Simulation Distance for Parametric Weighted Kripke Structures
Louise Foshammer, Kim Guldstrand Larsen and Anders Mariegaard
63
Rate Reduction for State-labelled Markov Chains with Upper Time-bounded CSL Requirements
Bharath Siva Kumar Tati and Markus Siegle
77

Preface

This volume contains the joint proceedings of the Workshop on Games for the Synthesis of Complex Systems (CASSTING'16) and of the 3rd International Workshop on Synthesis of Complex Parameters (SynCoP'16). The workshops were held in Eindhoven, The Netherlands, as satellite events of the 19th European Joint Conferences on Theory and Practice of Software (ETAPS'16). Both workshops are closely related in their topics as well as target audience and they shared a joint invited talk given by Giorgio Delzanno.

Preface to CASSTING'16 proceedings

Cassting is a European research project funded by the European Commission under the FP7 for Information and Communication Technology. The objective of Cassting is to develop a novel approach for analysing and designing collective adaptive systems in their totality, by using games on graphs.

The Cassting workshop on Games for the Synthesis of Complex Systems, held in Eindhoven on 2-3 April 2016, as a workshop of ETAPS 2016, was the final event of the Cassting project. The workshop included five invited talks, four contributed papers, and eight presentations.

Acknowledgements

We would like to thank the program committee for helping us setting up this program. We also thank our subreviewers, Renaud Lambiotte and Chrysostomos Stylios.

We would also like to acknowledge Erik de Vink and Hans Zantema for their help and responsiveness during the preparation of the workshop, and the organizers of the SynCoP 2016 workshop for accepting the idea of sharing an invited talk with us. We also thank all our speakers and attendees for actively participating in the workshop and the editorial board of the Electronic Proceedings in Theoretical Computer Science, and in particular Editor-in-Chief Rob van Glabbeek for his support.

Thomas Brihaye and Nicolas Markey

Program Committee

Organizers and Program Chairs
Thomas Brihaye Mons, Belgium
Nicolas Markey Cachan, France
Program Committee
Rüdiger Ehlers Bremen, Germany
Gilles Geeraerts Brussels, Belgium
Christof Löding Aachen, Germany
Benjamin Monmege Marseille, France
Sophie Pinchinat Rennes, France
Sven Schewe Liverpool, UK
Olivier Serre Paris, France
Jiří Srba Aalborg, Denmark

Preface to SynCoP'16 proceedings

SynCoP aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behavior of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g., timing, probabilities, costs) or discrete (e.g., number of processes). The goal can be to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values.

The SynCoP workshop was held in Eindhoven on April 3rd, 2016, as a workshop of ETAPS 2016. The workshop included two invited talks, three contributed papers, and six presentations.

The scientific subject of the workshop covers (but is not limited to) the following areas:

Acknowledgements

SynCoP 2016 is partially supported by project PACS ANR-14-CE28-0002.

We thank the authors for their contributions, the program committee members for reviewing and selecting the papers, the invited speakers for accepting our invitations and providing inspiring presentations and the ETAPS organizing committee Jan Friso Groote, Erik de Vink and Anton Wijs for their support. We would also like to thank Étienne André and the SynCoP Steering Committee for their support. Finally, we would like to thank the editorial board of the Electronic Proceedings in Theoretical Computer Science, and in particular Editor-in-Chief Rob van Glabbeek for his support.

Benoît Delahaye and Jiří Srba

Program Committee

Organizers and Program Chairs
Benoît Delahaye Nantes, France
Jiří Srba Aalborg, Denmark
Program Committee
Nikola Beneš Brno, Czech Republic
Nathalie Bertrand Rennes, France
Alexandre Donzé Berkeley, USA
Goran Frehse Grenoble, France
Peter Habermehl Paris, France
Holger Hermanns Saarland, Germany
Joost-Pieter Katoen Aachen, Germany
Marta Kwiatkowska Oxford, UK
Radu Mardare Aalborg, Denmark
Wojciech Penczek Warszawa, Poland
Karin Quaas Leipzig, Germany
Olivier H. Roux Nantes, France
Ocan Sankur Rennes, France
Tayssir Touili Villetaneuse, France
Lijun Zhang Beijing, China
Proceedings chair
Loïg Jezequel Nantes, France
Steering Committee
Parosh Abdulla Uppsala, Sweden
Étienne André Villetaneuse, France
Kim G. Larsen Aalborg, Denmark
Didier Lime Nantes, France
Wojciech Penczek Warszawa, Poland
Laure Petrucci Villetaneuse, France

Boundedness Games

Nathanael Fijalkow

We consider two-player games played over graphs equipped with one or multiple counters. The term boundedness refers to the idea that one player tries to keep the values of the counters bounded, while the other one tries to make them diverge to infinity. There are several variants of boundedness games, which appeared in essentially two contexts; either for synthesis, or as a proof object for boundedness logics. In this talk, I will survey the results that we know, and the unbounded number of questions that remain to be solved!


Control of Dynamic Discrete-Event-System Games

Jan H. van Schuppen

Control of discrete-event systems (DES) is studied under the name of supervisory control within the research area of control and system theory. The approach was initiated by W.M. Wonham (U. of Toronto, now retired) and developed by him, his former Ph.D. students, and other researchers. Within this setting, control of dynamic discrete-event-system games was formulated, motivated by decentralized control.

The control problem for a dynamic discrete-event-system game asks for a tuple of supervisory controls such that, for the closed-loop system, each controller maximizes its cost criterion. In control theory one refers to the system as a control system, each member of a set of multiple players is called a controller, and attention is restricted to the finite-string framework. The closed-loop system consists of the control system in closed-loop with the tuple of supervisory controls. The cost criterion of the problem may be taken as the closed-loop language which takes values in a partially-ordered set and which makes the problem a nonzero sum game. For the decentralized control all controllers have the same cost criterion but different observations for their supervisory controls. The control problem for dynamic discrete-event-system games was first treated in a paper by J.R. Buchi and L.H. Landweber (1969) for an infinite-string framework.

Because there is no solution procedure for this problem in general, one often considers the concept of a Nash equilibrium of a tuple of supervisory controls. That concept is defined as a tuple of supervisory controls such that no player can deviate from his supervisory control unilaterally, meaning while the other controllers keep their supervisory control of the equilibrium. For the decentralized control problem described above there is then a theorem stating that, if a strong Nash equilibrium exists, then this is also a global maximum. This theorem is of importance because it shows that a maximal supervisory tuple can be obtained as a Nash equilibrium. The result is an extension of a corresponding theorem of team theory where convexity of the cost criterion is needed.

The next problem is then: How to compute a Nash equilibrium of supervisory controls? A procedure to compute a Nash equilibrium will be formulated. But the procedure may not converge in general as will be shown by an example. The computation of Nash equilibria is an active research area and the speaker does not claim to have a full overview of the current literature. Decidability and complexity issues of the problem will be discussed.

Additional research problems for dynamic DES games are mentioned. The first problem is signalling of information in decentralized control which is a special case of the dynamic DES game. In such a problem a player can, by his control actions, signal information to other players via the control system. An example will be shown and the research issue discussed. A second problem is: What information should a player use for control? A third problem is to reformulate the control system and the corresponding control problem as a coordination control problem, possibly with many levels. A fourth problem concerns the system theory of dynamic DES games.

The research is based on research of the speaker with Ard Overkamp, Jan Komenda, and Tomas Masopust.


Automated Synthesis: Going Distributed

Anca Muscholl

Synthesis is particularly challenging for concurrent programs. At the same time it is a very promising approach, since concurrent programs are difficult to get right, or to analyze with traditional verification techniques. The talk provides an introduction to distributed synthesis in the setting of Mazurkiewicz traces, and its applications to decentralized runtime monitoring.


Algorithms for Branching MDPs and Branching Stochastic Games

Kousha Etessami

We survey several recent results on efficient algorithms for quantitative and qualitative analysis of multi-type branching processes (BPs), Branching Markov decision processes (BMDPs), and Branching simple stochastic games (BSSGs).

BPs are classic stochastic processes with many applications. They are also intimately related to probabilistic extensions of well-studied infinite-state models in automata/language theory, verification, and process algebra, including: stochastic context-free grammars, probabilistic stateless pushdown automata, 1-exit recursive Markov chains, and probabilistic BPPs and BPAs.

BMDPs (and BSSGs) extend BPs with a controller (two players, respectively). Two key objectives for these models are optimizing (maximizing/minimizing): the probability of eventual extinction, an of eventually reaching a target type. Computing these optimal probabilities (game values, respectively) turns out to be equivalent to computing, respectively, the least fixed point (LFP), and greatest fixed point (GFP), solution vector for corresponding max/min probabilistic polynomial systems of equations (max/minPPSs), which are their Bellman optimality equations. These solutions are in general irrational values, and one goal is to compute them within desired additive error.

We have obtained the first polynomial time algorithms for computing, to within arbitrary desired accuracy, the LFP (and GFP) solutions of given systems of (max or min) PPS equations, and thus P-time algorithms for computing the (optimal) extinction and reachability probabilities for BPs (and BMDPs). These results also imply efficient algorithms for key problems for other closely related models mentioned above. Our P-time algorithms for BMDPs involve, among other things, a generalization of Newton's method that uses linear programming in each iteration. These results also yield FNP upper bounds for the same analyses of BSSGs. In this talk I will survey some of this work. (Based on a series of joint works with Alistair Stewart and Mihalis Yannakakis.)


Parametrized Verification of Distributed Broadcast Protocols

Giorgio Delzanno

We report on a recent research lines related to parameterized models of concurrent and distributed systems with broadcast communication. In the presentation we consider transition systems as a common language to describe different operational models for broadcast communication. Transition systems are a natural model to extend the operational semantics of basic models of concurrent computation like Petri nets to richer models like graph-based rewriting or automata communicating via broadcast messages and channels. We will also consider models that combine graph-based interaction models with symbolic representation of data path via equality and inequality constraints. In this context we will discuss verification algorithms for restricted classes of models that exploit finite-state reductions, the theory of well-structured transition systems instantiated to different types of graph orderings, e.g. subgraph and induced subgraph, and reachability algorithms based on labeling procedures.


What Population Reveals About Individual Cell Identity: Single-Cell Parameter Estimation of Models of Gene Expression in Yeast

Gregory Batt

Significant cell-to-cell heterogeneity is ubiquitously observed in isogenic cell populations. Consequently, parameters of models of intracellular processes, usually fitted to population-averaged data, should rather be fitted to individual cells to obtain a population of models of similar but non-identical individuals. Here, we propose a quantitative modeling framework that attributes specific parameter values to single cells for a standard model of gene expression. We combine high quality single-cell measurements of the response of yeast cells to repeated hyperosmotic shocks and state-of-the-art statistical inference approaches for mixed-effects models to infer multidimensional parameter distributions describing the population, and then derive specific parameters for individual cells. The analysis of single-cell parameters shows that single-cell identity (e.g. gene expression dynamics, cell size, growth rate, mother-daughter relationships) is, at least partially, captured by the parameter values of gene expression models (e.g. rates of transcription, translation and degradation). Our approach shows how to use the rich information contained into longitudinal single-cell data to infer parameters that can faithfully represent single-cell identity.