Extend liveness specification capabilities in CIF: add reachability requirement annotation

Proposed extension of CIF

Introduction

Currently, CIF has marker predicates that are used for synthesis to specify a form of liveness requirements. That is, it is an implicit requirement that every reachable state must be able to reach a marked state. States that are marked, or from which a marked state can be reached, are called non-blocking. States that do not satisfy this properly are called blocking states. Marking is a very weak form of liveness, as you must be able to reach a marked state, so any of them will do.

Synthesis may remove large parts of the state space to ensure safety, removing so much that you lose relevant behavior. You can check whether all relevant behavior is still present, through simulation. However, that is practically infeasible to do exhaustively, for most real-world systems. An alternative is to use model checking, to check whether all the behavior you want to be present is present. For instance, you could check stronger liveness requirements.

Alternatively, you can use synthesis to ensure that certain behavior is always possible. Currently, with marking, you can ensure that certain states must always be reachable, thus indicating a form of desired behavior that you want to keep. However, synthesis may only remove states and transitions, and hence enforcing non-blockingness entails removing all states that are blocking, and via controllability also all states that can reach blocking states via a transition for an uncontrollable event, etc. Still, synthesis ensures that the controlled system state space is non-blocking. If this is not possible, you get an empty supervisor and you know that what you asked isn't possible. This is a good thing, as then you know directly that there is no way to satisfy all your requirements, rather than having to check this afterwards using simulation or model checking. In a way, the more synthesis removes, the easier it is to see that you're missing relevant behavior.

Using model checking, very complex liveness requirements can be checked. With synthesis, only the weak marking liveness can be enforced. The idea of this issue is to extend the liveness requirements that can be expressed in CIF and can be enforced by data-based synthesis. We could allow complex temporal logics, such as mu-calculus, but this is too complex and subtle for most practitioners to use correctly. Hence, we propose to add a simple yet practically useful extension.

Reachability annotations

Syntactically, we propose to add an @reachable annotation, which expresses a reachability requirement:

• It can be added to components (specifications, groups, automata) and component definitions (group definitions and automata definitions).
• It can be added to these elements as many times as you want.
• It has exactly one argument, which is a predicate (boolean expression).

Semantically, each such annotation indicates a predicate p for which the CTL formula AG EF p must hold from all initial states in the controlled system. This can be read as: 'always-globally', there 'exist a future state', where 'p' holds.

Relation to marking

Implicitly, marking in CIF imposes the CTL requirement AG EF marked, where marked is the global marker predicate of the specification. This global marking predicate is the conjunction of all marker predicates from components, conjuncted with the marking predicate of each automaton, where each automaton's marker predicate is a disjunction of the marker predicates of its locations, where a location's marker predicate is loc => m, where m is the conjunction of the marker predicates specified in the location, with no marker predicates in a location meaning false and thus loc => false a the locations marker predicate.

In essence, an @reachable annotation adds an extra AG EF p predicate, independent of marking. You could say this enables to have many different forms of marking, that must all independently be satisfied.

Data-based synthesis

Data-based synthesis will be extended to enforce all reachability requirements specified through @reachable annotations. For each such annotation with predicate p, it will perform an additional backward reachability fixed-point computation from p, bounded to the current controlled behavior, as we also do for the global marker predicate.

The fixed-point computations order option would be extend with an extra element, to allow users to specify the order that the various fixed-point computations are performed each round. Currently, it allows to specify the order for non-blockingness, controllability, and forward reachability (in this order). It would get an extra value for the reachability requirements. I propose that the default is to make it the 2nd computation, after non-blockingness and before controllability.

Alternatives

We considered alternatives:

• We could allow richer temporal logics, such as CTL, CTL*, mu-calculus, etc. However, these are too subtle and complex for most practitioners. Also, there are other issues with supporting them, such as there being no unique supremal controller, losing the guarantee of maximal permissiveness.
• We could allow different categories/colors of marking predicates. However, marker predicates require that you specify them in every component, or else the global marker predicate is 'false'. With the @reachable annotations as proposed, users can easily specify additional reachability requirements, in a much simpler way.

We believe the proposed addition provides users with a feature to enforce stricter liveness requirements in the form of reachability requirements, that is easy to understand conceptually, easy to specify, easy to use in a correct way, and practically relevant.

Steps

• Add requirement:reachable annotations to CIF. (!1435 (merged), !1445 (merged))
• CIF data-based synthesis warns about state invariants and reachability requirement predicates that can never be satisfied at the same time. This would lead to an empty supervisor. It could also print additional debug output for the input model for this.

The future

The idea is to implement this feature and ship it in %v10.0, such that users can experiment with it.

We plan to take a further look at liveness in the future, to see what else we can support in a practical, usable way, ideally without losing any of the current synthesis guarantees.

Original description

Consider the following part of a CIF model:

plant System:
    controllable c_e;
    disc int[0..3] x = 1;

    location S1:
        initial;
        marked;
        edge c_e do x := 1 goto S2;

    location S2:
        marked;
        edge c_e do x := 2  goto S1;
end

To ensure both locations S1 and S2 remain reachable after synthesis, the current approach is to mark both locations. However, this doesn't fully capture the intended liveness requirement, as a supervisor can restrict c_e without violating the non-blockingness property. The non-blockingness property only guarantees that a marked state is always reachable, not all marked states. For instance, a supervisor could restrict c_e to c_e when false, which would still satisfy the non-blockingness property since the initial state is marked.

Being able to express such liveness properties can reduce the validation time of the controlled system, as no model checkers or simulations are required to verify whether a certain state is always reachable.

This issue has been addressed in the literature using multitasking/coloured automata, as introduced in Multitasking Supervisory Control of Discrete-Event Systems and further explained/used in Supervisory control with absent-state explanations for coloured finite automata. The multitasking/colouring method assigns a colour to each state and ensures that a state from all colours is always reachable. For example, you can guarantee the reachability of both S1 and S2 by colouring one of the locations:

plant System:
    controllable c_e;
    disc int[0..3] x = 1;

    location S1:
        initial;
        marked;
        edge c_e do x := 1 goto S2;

    location S2:
        colour(blue);
        edge c_e do x := 2  goto S1;
end

Synthesis then ensures the reachability of S1 through the non-blockingness property and S2 through colouring.

However, I propose a more suitable alternative for CIF: enforcing the CTL property AG EF (some predicate). As stated in Supervisory Control of Labeled Transition Systems Subject to Multiple Reachability Requirements via Symbolic Model Checking, multitasking/colouring is equivalent to the CTL formula AG EF (a location). The authors implemented this feature in a NuSMV extension called SynthSMV. Enforcing AG EF (some predicate) is more useful, as it can be applied to any arbitrary predicate over variables and locations. For instance, we could implement an annotation @reachable(some predicate) for complex components, allowing us to specify the reachability of x = 2 in the previous example:

@reachable(x=2)
plant System:
    controllable c_e;
    disc int[0..3] x = 1;

    location S1:
        initial;
        marked;
        edge c_e do x := 1 goto S2;

    location S2:
        edge c_e do x := 2  goto S1;
end

I have implemented a prototype of this feature in CIF version 8.0 as part of my thesis. The patch is available here. I used the following CIF models to test the prototype: reachable_tests.zip. Once my thesis is complete, I will attatch it to this issue.