Séminaires
Séminaire du 03 juillet 2015
Lieu
CNAM: comment y aller (entrée 2 Rue Conté, Salle 31.2.85)
Programme
14h00-15h00: Sofiène Tahar, Concordia University, Montreal, "Formal Analysis of Physical Systems: A Theorem Proving Approach"
Abstract: Formal methods have been classically used for the verification of software, circuits or protocols. In most cases, verification deals with an abstraction of the underlying physical system (e.g., circuit verification does not model semi-conductors). On the other hand formal verification has been focusing on functional aspects rather than performance and qualitative issues. In this talk, we will briefly review different technologies of formal verification and discuss their advantages and drawbacks. We will also display current and future research directions of formal verification methods. Among them, we will address two research activities carried out at our research group at Concordia University (http://hvg.ece.concordia.ca), on the verification of physical systems. Namely, (1) the performance analysis of probabilistic and statistical systems with applications in telecommunications and microelectronics reliability analysis; and (2) the formal analysis of optical systems with applications in ray, electromagnetic and quantum optics. We will explain how these concepts and their underlying mathematical and physical principles can be formalized (in higher-order logic) as well as the limitations of this approach.
15h00-16h00 : Wojciech Penczek, Warsaw and Sieldce Universities, "Generating None-Plans in Order to Find Plans"
Abstract:
The lecture puts forward a brand new approach to planning.
The method aims at simplifying the task of planning in an abstract
object-oriented domain where entities are added only and never removed.
The approach is based on the synthesis of a family of all sets of actions
that cannot be composed into a plan (called none-plans) in order to prune
the state spa ce searched for plans.
It is shown how to build a propositional formula describing a set of the
none-plans and how to approximate this set when the task of planning
becomes too complex.
A preliminary evaluation of the application of the none-plans synthesis
to the generation of plans in the PlanICS framework is shown.
The experimental results show a high potential of the approach.