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.

Program Committee

Organizers and Program Chairs

Program Committee

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:

• parameter synthesis,
• parametric model checking,
• regular model checking,
• robustness analysis,
• parametric logics, decidability and complexity issues,
• formalisms such as parametric timed and hybrid automata, parametric time(d) Petri nets, parametric probabilistic (timed) automata, parametric Markov decision processes, networks of identical processes,
• interactions between discrete and continuous parameters, and
• tools and applications to major areas of computer science, biology and control engineering.

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.

Program Committee

Organizers and Program Chairs

Program Committee

Proceedings chair

Steering Committee

Boundedness Games

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

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

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

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

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

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.