SYRF Project
Task 3.1: "Symbolic Abstraction of Automata"
Abstract of deliverable 3.1.1
The basic paradigm for modularity in reactive formalisms consists
in designing the full system/program as a collection of interacting parallel
components. With synchronous reactive systems providing common
clocks and signal broadcast, the addition of a new parallel module preserve
to a large extend the previous behaviour of (the rest of) the system. This
is not always entirely true, but one may get a formal diagnostic of disturbance
by formally comparing two finite state machines: the one representing the
system prior to the addition of the later module, and the one with the
module (but abstracted away on new interface signals possibly brought in
by this extension).
This formal check makes special sense for instance in telephony systems, where modules implement new features, and the problem of transparent addition amounts to feature interactions. But the method has a broader scope, and we have found it widely applicable in a lot of cases, with very little demand on the user concerning the provision of correctness properties (here the submodule is itself its spec). This method uses an algorithm for checking (finite state) machine equivalence, in a context where possibly previous signal hiding introduced non-determinism (while originally synchronous systems exhibit deterministic behaviours as a function of their current state and input events). We call this equivalence symbolic bisimulation, where the adjective symbolic is meant to recall here that, at the concrete representation level, input events are represented symbolically as propositional predicates on signals, while the state structure itself can be either implicit or explicit. Negated litterals retain the fact that transitions may be triggered by the absence of a signal.
The problems of bisimulation checking and minimisation were tackled by two partners, in two different contexts. At Inria Sophia-Antipolis the purpose was to abstract and minimise finite state machines produced from Esterel programs, using symbolic representation methods such as BDDs. At Inria Rennes the scope was to adapt resolution methods on polynomial systems produced from Signal to solve this problem. We describe their achievements in turn.
In presence of symbolic input predicates on transitions the bisimulation checking algorithm must be refined: transitions are not searched for a 1-1 match, but instead a collection of predicates borne on a collection of transitions (from a given state to a set of yet equivalent states, with identical output events), may recover a single predicates from another state. This added complexity is easily coped with in the classical partitioning algorithm, but not in other variations such as Paije-Tarjan or on-the-fly methods.
We implemented the algorithm twice:
Both kinds of descriptions can be produced by the Esterel compiler. We found out that in most cases fc2symbmin performed remarkably well in the (factoring) minimisation of transition numbers, and also in minimisation of states. Further signal hiding improve the reduction ratio. We applied these techniques to a climatic chamber example provided by an industrial partner inside the SYRF project. We provide the theoretical foundations and applications of abstraction on a Steam-Boiler problem in a separate research report.
The equational nature of the multi-clock, data-flow synchronous language Signal makes that it relies on a formal model in terms of polynomial dynamical equations systems (PDS)}, which can be seen as an equational representation of an automaton.
The theory of PDS uses classical tools in algebraic geometry such as ideals, varieties and morphisms. This is the basis of the verification tool Sigali}, developed in the EP-ATR group. The techniques used in consist in manipulating the system of equations instead of the sets of solution, which avoids the enumeration of the state space. Each set of states is uniquely characterized by a polynomial and the operations on sets can be equivalently performed on the associated polynomials.
Therefore, a wide spectre of properties, such as liveness, invariance, reachability and attractivity can be checked. The PDS abstraction is automatically performed by the Signal compiler and the resulting PDS is then used as a formal basis for verification of Signal programs. Many algorithms for computing predicates states are available.
We want here to adapt these original techniques of the Signal environment to the case of symbolic bisimulation (see sections above for full motivation of this work), and we are developing the algorithm for the symbolic bisimulation computation in the Signal environment.
In a separate draft research report, entitled Symbolic methods in the Signal environment, by S. Pinchinat and O. Kouchnarenko, we provide the theoretical background, definitions and practical results.
Publications: