|Videos of PSY talks are available here|
|Dietmar Berwanger (LSV, ENS Cachan and CNRS) and Laurent Doyen (EPFL) |
Imperfect-Information Games for System Design. Models, Applications, and Tools
One challenge in the analysis of concurrent systems arises with the uncertainty due to the inability of components to observe all occurring events. We discuss games with imperfect information as a modeling framework for such systems. In the first part of our talk, we survey fundamental models of games with imperfect information, and illustrate motivating scenarios for the analysis of interactive systems, in particular controller synthesis, compositional system design, and verification of cryptographic protocols. We present a classical algorithm for solving a basic, but paradigmatic, model of imperfect-information games.This algorithm performs a reduction to perfect-information games via a power-set construction that involves a state-space explosion. In the second part of the talk, we present a generic symbolic approach for dealing with the state-explosion problem. We show that the structure of the classical reduction can be exploited to design a compact data structure. On this data structure, we can compute some important symbolic operations efficiently, while other operations are shown to be NP-hard. We present symbolic algorithms to compute the winning positions of a game of imperfect information, and we extend them to construct winning strategies. Finally, we present experimental results obtained with the tool Alpaga.
|Satnam Singh (MSR Cambridge)|
C-to-Gates Synthesis of Dynamic Data Structures
C-to-gates synthesis is attractive as a way of allowing software developers to implement their computations on FPGAs for co-processing as well as to hardware engineers to help improve productivity. However, a typical C-to-gates synthesis systems places many restrictions on the subset of C which can be effectively synthesized into hardware. In particular, it is almost impossible to write idiomatic C code using malloc/free and dynamic data structures and have it automatically synthesized into gates. We present the preliminary results of a project that uses recent advances in shape analysis to help us automatically transform some C programs that make use of dynamic memory to represent lists and trees into representations that have the dynamic memory accesses transformed into accesses into a statically allocated collection of heaps. We are only able to perform this transformation when we can statically determine a bound on the amount of dynamic memory used which we are able to do for an interesting collection of examples including a Huffman encoder, a priority encoder, and a network packet processor. The final result of our synthesis flow is a VHDL circuit description which can be further synthesized into an implementation of a circuit that executes on an FPGA.
|Tom Henzinger (EPFL and IST Austria)|
The synthesis of a reactive system requires the solution of a game played on graphs. If the goal is to synthesize a system that satifies a given boolean specification, the corresponding graph game has a boolean objective. While graph games with quantitative objectives, such as mean-payoff games, have long been targets of theoretical investigation, so far they have found relatively little use in synthesis. We show that several natural synthesis questions, such as the synthesis of a system that optimizes resource use and the synthesis of a system that degrades gracefully under faulty environment assumptions, can be answered by solving graph games with quantitative objectives.
|Barbara Jobstmann (EPFL) |
Environment Assumptions for Synthesis
In synthesis, we aim to construct a finite-state reactive system from a given omega-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification G by computing an environment assumption A such that the new specification A -> G is realizable. In this talk, I will give a short introduction into the synthesis problem and the underlying game theory, discuss desired properties of assumptions, and present a two-step algorithm to compute useful environment assumptions. Our algorithm operates on the game graph that is used to answer the realizability question. First, it computes a safety assumption that removes a minimal set of environment edges from the graph. Second, it computes a liveness assumption that puts fairness conditions on some of the remaining environment edges. We use probabilistic games to compute the liveness assumptions. This is joint work with Krishnendu Chatterjee and Tom Henzinger.
|Cliff Jones (Newcastle University)|
Rely/guarantee thinking and its role in splitting atoms safely
I first wrote about rely/guarantee reasoning in the early 80s! Since then, a lot of developments have been made but the basic ideas (that "interference" is the essence of concurrency; if one wants a compositional approach to design, one must record assumptions about interference; and that granularity is a delicate issue) have become widely accepted. More recently, I have been developing ideas about "atomicity refinement"; see "R/G thinking" as wider than any specific set of rules; realised that expressive weakness is a key to success; and appreciated the role of data reification in achieving complex R/G specifications. I'd like to review in this talk my reservations about "ghost variables" and to try to pin down where they are really required.
|Yoad Lustig (Rice) |
Synthesis from Component Libraries
Synthesis is the automated construction of a system from its specification. In the classical temporal synthesis algorithms, it is always assumed the system is “constructed from scratch” rather than “composed” from reusable components. This, of course, rarely happens in real life. In real life, almost every non-trivial commercial system, either in hardware or in software system, relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration, can be modeled as synthesis of a system from a library of components. In this work we de·ne and study the problem of LTL synthesis from libraries of reusable components. We de·ne two notions of composition: data-·ow com- position, for which we prove the problem is undecidable, and control-·ow com- position, for which we prove the problem is 2EXPTIME-complete. As a side bene·t we derive an explicit characterization of the information needed by the synthesizer on the underlying components. This characterization can be used as a specification formalism between component providers and integrators.
|Amir Pnueli (New York University and Weizmann Institute of Science (Emeritus) )|
"Practical" Synthesis of Programs from Temporal Property Specifications|
The current state of the art uses specification of properties in a behavioral form, such as linear temporal logic, mainly for static and dynamic verification of implementations of reactive systems, AFTER they have been constructed. In the talk we consider the more radical approach by which a specification in terms of its desired properties is formed at the beginning of a system development, before any implementation is attempted. After some analysis and validation of this specification, one may apply a synthesis algorithm in order to automatically derive a correct-by-construction implementation. No further verification or testing is required. While this has been considered an unachievable dream for a long time, recent progress in the algorithms for synthesis has made design synthesis from property specification applicable for medium size designs. We provide more details about the problem of synthesizing digital designs from their LTL (and similar) specifications. In spite of the theoretical double exponential lower bound, we show that for many expressive specifications of hardware designs the problem can be solved in time N^3. We describe the context of the problem, as part of the Prosyd European Project which aims to provide a property-based development flow for hardware designs. Within this project, synthesis plays an important role, first in order to check whether a given specification is realizable, and then for synthesizing part of the developed system. The above results were obtained for the synthesis of synchronous systems. In the talk, we will consider the generalization of the problem to the case of asynchronous systems. This will enable the synthesis of programs that communicate with their environments by shared variables. We will mainly report about work in progress, which provides different approaches and heuristics for establishing unrealizability and realizability of asynchronous specifications. This is a joint work with Uri Klein, Nir Piterman, and Yaniv Sa'ar.
|Armando Solar-Lezama (MIT)|
The Sketching Approach to Practical Synthesis|
Sketching is a new programming model that incorporates localized software synthesis to make programming easier. The model is based on the observation that only some aspects of the program require the full insight and expertise of the programmer; the rest are low-level details needed to make the insights work. Sketching allows the programmer to focus the synthesizer on those low-level aspects while maintaining control over the implementation strategy. This makes programming easier while keeping the synthesis process scalable. This talk will describe the sketching programming model and its application to concurrent programming. The talk will describe the basic algorithms behind sketching, and the main insights that allow them to scale to interesting concurrent programming problems.