*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h00                     *
*                  Salle Info 5, etage -2, Batiment Rateau          *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************


***  Vendredi 4 Decembre 2009, 14h00-15h00 ************************

Efficient Synthesis of Asynchronous Systems

Uri Klein, NYU

Re'sume'/ Abstract:

We investigated a development process for reactive programs, in which
the program is automatically generated (synthesized) from a high-level
temporal (property) specification. The method is based on previous
results that proposed a similar synthesis method for the automatic
construction of hardware designs from their temporal specifications.
Thus, our work can be viewed as a generalization of existing methods for
the synthesis of synchronous reactive systems into the synthesis of
asynchronous systems.

In the synchronous case it was possible to identify a restricted yet
expressive subclass of formulas and present an algorithm that solves the
synthesis problem for these restricted specifications in polynomial
time. Here, due to a possibly exponential increase in complexity of the
synthesis problem, the results are less definitive in the sense that we
can offer some heuristics that may provide polynomial-time solutions
only in some of the cases. The approach taken here is to extract from
the specification two new specifications that, in some sense, provide an
upper and a lower bound to the specification. The upper bound
(over-approximation) specification could be used to determine that the
original specification is unrealizable.  On the other hand, the lower
bound (under-approximation) could be used in order to determine that the
original specification is realizable, and to actually produce an
implementation of this specification. As mentioned above, the
realizability analysis of these two approximations can be performed in
polynomial time for the case that the original asynchronous
specification falls into the restricted class.

Joint work with Amir Pnueli.


***  Vendredi 18 Decembre 2009, 14h00-15h00 ************************

Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics

Colas Le Guernic, ENS

Re'sume'/ Abstract:

This talk is devoted to the problem of computing reachable sets of
linear and hybrid systems. In the first part, after exposing existing
approaches for reachability analysis of linear systems, we present a new
algorithmic scheme for linear time-invariant systems that definitely
outperforms existing algorithms. As the exact implementation furnishes a
representation of the reachable sets that is sometimes hard to
manipulate, we propose an approximate version that is not subject to the
wrapping effect, an uncontrolled growth of the approximation errors. We
also discuss a variant of this algorithm specialized to support
functions, a functional representation of convex sets. In the second
part, we extend this work to hybrid systems. We first show how to deal
with the constraints on the continuous dynamics imposed by the
invariants. Then, we present algorithms for approximating the
intersection of the continuous reachable sets with hyperplanar guards.



*********************************************************************
Pour recevoir l'annonce par courrier electronique:
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************