SYRF Project

Task 3.1: "Symbolic abstraction of automata"

Abstract of deliverable 3.1.2

Back to the SYRF Home Page


Achieved Results:

Automatic verification and model-checking rely on precise formal semantics, as provided in synchronous reactive formalisms. Then many avenues of analysis techniques can be applied, each relying on some form of symbolic abstraction of the underlying reactive automata.

The deliverable contains contribution from three distinct sites (INRIA Meije, INRIA Spectre, and INRIA Ep-Atr).

Work at INRIA Meije focused this year on the development of methods for Compositional reduction of Boolean Equation Systems. Such systems form a natural target for compilation from Esterel, and bear strong ties with synchronous hardware circuits at RTL level. The topic of compositional reduction methods is important here since these reductions can often be drastic in practice, provided the description does not blow up in the middle of the algorithm. Reducing components often helps a great deal. Annex 3.1.2.a is a presentation of the Xeve tool.

Work at INRIA Spectre focused on the formal definition of a new property of interest, called stability. Stable systems are those which may not evolve forever, producing outputs, without further input events. Technical material is provided as annex 3.1.2.b.

Work at INRIA Ep-Atr focused on the study of intensional Labeled Transition Systems as a representation model, and the computation of bisimulation minimal forms on this representation and on discrete event controller synthesis. Technical material is provided as annex 3.1.2.c and annex 3.1.2.d.