SYRF Project

Task 3.1: "Symbolic abstraction of automata"

Abstract of deliverable 3.1.3

Back to the SYRF Home Page
Back to Deliverables


The deliverable contains contributions from two distinct INRIA sites (INRIA Meije and INRIA Ep-Atr).

Work at INRIA Meije concentrated on important techniques for compositional reductions of Boolean Equation Systems.
Work at INRIA Ep-Atr dealt with two issues: the design of abstraction methods on Implicit Labeled Transition Systems on one hand; controller synthesis and the Supervisory Control Problem on the other hand.
 

INRIA Meije contribution:

Compositional reductions of Boolean Equation Systems

This task was considered as the major activity at INRIA Meije for this third year, and a lot of manpower was devoted to it.

Achieved Results
We conducted extensive research on Compositional reduction of Boolean Equation Systems, in accordance with the original milestones of the project description.  The practical software developments include:

Defining these translations prompted some research work for the following reason:
In the case of Esterel, the netlist part encoding behaviour at the initial instant has to be kept apart from the code for the rest of the behaviour, in the compositional approach. This is so because the code for the first instant may be duplicated several times due to the various preemptions applicable by a reactive context. Thus the two parts of the code have to be split apart and optimized separately. But importantly one main role of the initial instant code is to provide admissible (or reachable) configurations of state registers after initialization phase. Optimizing the rest of the behaviour without this information proved deceiving, specially in comparison with independant optimization of subcomponents in isolation. We thus had to figure out technical ways to introduce the initial code part as a constraint ("care set" in hardware synthesis jargon) on the rest of the code to improve reduction in optimizations. Our solutions now provide optimizations comparable in size of registers to the "isolation" ones, with combinational logic augmented by a factor of roughly 2 only.
We conducted several large-scale experiments of compositional reduction of Boolean Equation Systems, on case studies provided by
development teams at Texas Instruments or Dassault Aviation (unfortunately not on case studies provided by industrial partners in Syrf).

A more detailed presentation of all activities this year of INRIA Meije on compositional reduction of Boolean Equation Systems, with its relevance  to symbolic abstraction of Finite State Machines, is to be found as an annex to the deliverable.

INRIA Ep-Atr contributions:

Abstractions

The proposed approach

Last year, we presented Implicit Labeled Transition Systems (ILTS) as intermediate models for discrete event systems. We have studied operations of parallel composition and event hiding, as well as an equivalence criterion based on strong bisimulation semantics, namely the equivalence called symbolic bisimulation. We also proposed an algorithm that provides the reduced system according to a bisimulation equivalence relation. The aim of the work is to rely on intensional descriptions of the systems for symbolic abstractions purposes, based on behavioral equivalences. The intensional approach we propose has the main advantage to remain at an interesting level of abstraction to handle sets (of states, of events) in which algorithms and properties can entirely be expressed, thus providing us with a high level of expressiveness. This abstract level avoids us to bother with a particular choice of sets implementation, such as Binary Decision Diagrams (BDDs), even if all operations are actually based on this representation for sets. Moreover, the intensional formalism is completely compatible with the symbolic techniques, since intensionally described sets can afterwards be implemented by any kind of methods, e.g. decision diagrams. However, other tools with various implementations for sets might be considered using the same high level framework (e.g. Mathematica, Maple).

Achieved Results

This year, we achieved the design of abstraction methods based on symbolic techniques: classical abstraction by state fusion has been considered (with associated equivalence relation computation). We also introduced other kinds of abstraction, falling into the category of abstraction by restriction: in particular, we studied the use of the controller synthesis methodology to achieve the restriction synthesis[6].

The prototyped functionalities enabling the above mentioned approaches are available in the Sigali tool box, the formal calculus system of the Signal environment [6,2]. These new functionalities of Sigali are still under improvement process but have already been experimented for the case of significant Signal programs. In particular, some experiments have been conducted on EdF partner case study : the power transformer station controller. Unfortunately the Syrf Steam Boiler case, although designed in Signal and studied in our group in the Task 3.4 , turns out to be far too much numerical to be relevant for boolean automata issues.

Supervisory Control Problem

The proposed approach

Control theory of discrete event systems allows to use constructive methods, that ensure, a priori, required properties of the system behavior. Therefore, the validation phase reduces to properties not guaranteed by the control.

Achieved Results

There exist different theories for the control of discrete event systems since the 80's [ramadge89], [holloway97]. Usually, the starting point of these theories is: given a model for the system and the control objectives, a controller must be derived by various means such that the resulting behavior of the closed loop system meets the control objectives.


Publications: Related references: