State requirement invariants

Before synthesis, the entire CIF specification is converted to Binary Decision Diagrams (BDDs), a representation of predicates that allows for efficient synthesis. The state requirement invariants of the specification thus also need to be part of the BDD representation of the specification. These requirements can be enforced by applying them to the BDDs in multiple ways:

  1. Controlled behavior:

    All state requirement invariants are enforced via the 'controlled behavior' BDD. This BDD represents all states of the controlled system. Since the controlled system has to adhere to the state requirement invariants, these invariants can be put directly into the controlled behavior BDD.

  2. Edge guard or controlled behavior:

    The decision how to enforce state requirement invariants is made per per edge. For each edge with a controllable events, the invariants are enforced via the guards of the edge, by strengthened the existing guards with sufficient extra conditions that ensure that after taking the edge the state requirement invariants hold. The initialization predicate of the controlled system is restricted as well, to ensure the state requirement invariants also hold in initial states. As synthesis may not restrict the guards of edges with uncontrollable events, for those edges the extra restrictions are put into the controlled behavior BDD instead.

By default, all state requirement invariants are enforced via the controlled behavior. This can be changed by using the State requirement invariant enforcement option (see the options section).

The effect of the different approaches on the computational effort of synthesis can be quite complex:

Both approaches have potential benefits and drawbacks, making for a trade-off between their various effects. Which approach is most efficient depends on the model.

For more information, see the scientific publication by [Thuijsman et al. (2021)], where the two approaches are compared.