CNAM: comment y aller (entrée 2 Rue Conté, Salle 31.2.85)
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.
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.