Published: 18th February 2011|
|Preface Bernd Finkbeiner and Johannes Reich|
|Experimental Aspects of Synthesis Rüdiger Ehlers||1|
|Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives Christian von Essen and Barbara Jobstmann||17|
|A LTL Fragment for GR(1)-Synthesis Andreas Morgenstern and Klaus Schneider||33|
|Memory Reduction via Delayed Simulation Marcus Gelderie and Michael Holtmann||46|
|Synchronizing Objectives for Markov Decision Processes Laurent Doyen, Thierry Massart and Mahsa Shirmohammadi||61|
The focus of the iWIGP workshop is the interrelation between interactions, games and protocols. How does computer science deal with nondeterministic interactions where the actions a system takes are not (completely) determined by the interactions the system is involved in? In computer science, nondeterministic interactions are usually described by protocols. However, these interactions can also be viewed as games. As to be expected, games have become an increasingly important modeling tool wherever nondeterministic interactions are involved -- from foundations in game semantics and reactive systems to applications in communication protocols and electronic business applications. The goal of this workshop has been to bring researchers from industry and academia together and to explore how a better understanding of the interrelation between interactions, games and protocols leads to better-designed and more reliable nondeterministic interacting systems.
iWIGP 2011 was collocated with ETAPS 2011 in Saarbruecken, Germany. The programme consisted of three invited talks, by Kim Larsen, Marielle Stoelinga and Viktor Kuncak, and five refereed papers, selected by a strong programme committee of international reputation. The refereed papers are contained in this volume.
In his article ''Experimental aspects of synthesis'' Ruediger Ehlers presents a comparison of four existing synthesis tools for LTL: ANZU, LILY, ACACIA and UNBEAST. There are many challenges in comparing the tools, such as different specification languages, different semantics (Moore/Mealy), different preprocessing, etc. Ruediger Ehlers proposes a framework that facilitates future experimental comparisons of such tools.
When constructing a system from a specification, it is often the case that several different systems satisfy the specification. Christian von Essen and Barbara Jobstmann examine in their paper ''Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives'' how to automatically construct a system that satisfies a quantitative specifications under a given environment model in an ''optimal'' way.
In their article ''A LTL Fragment for GR(1)-Synthesis,'' Klaus Schneider and Andreas Morgenstern propose to use a syntactical criterion that identifies LTL formulas whose models can be recognized by deterministic Buechi or deterministic co-Buechi automata. This is useful for the synthesis of systems via the GR(1) approach, where the input is composed of two sets of deterministic Buechi automata, one set representing hypothesis on the behaviors of the environment and one set representing guarantees that the controller must enforce against any behavior of the environment satisfying the assumptions.
Decision-making in situations where outcomes are only partly under the control of a decision maker are often modeled by Markov decision processes. Laurent Doyen, Thierry Massart and Mahsa Shirmohammadi define in their article ''Synchronizing Objectives for Markov Decision Processes'' a new class of objectives for Markov decision processes, which specify sequences of distributions in which the probability tends to accumulate in a single state. The main result of the paper is that pure strategies with finite memory are sufficient for achieving the synchronizing objectives.
One issue of the application of infinite games in the synthesis of reactive systems is memory consumption. Marcus Gelderie and Michael Holtmann describe in their article ''Memory Reduction via Delayed Simulation'' a method for reducing the memory that is needed for representing strategies in infinite games with two particular interesting winning conditions, namely request-response and Streett. Instead of calculating a strategy directly from the game graph, they use an automaton view of that graph. This automaton is then reduced on the basis of an equivalence relation on configurations. Furthermore, for the cases of specifications represented by "request-response"-requirements and general "fairness" conditions, the authors show a potential exponential gain in the size of memory.
Special thanks go to the invited speakers
We thank the organizers of ETAPS 2011 for their support and the EPTCS editorial board for publishing the proceedings. And, last but not least, we thank all participants for attending the iWIGP 2011 workshop.
Bernd Finkbeiner and Johannes Reich
Walldorf and Saarbruecken, February 2011