Discovering of System’s Invariants by Temporal Reasoning

We present a technique to handle invariants in the branching-time setting, for the specifications written in the formalism called Branching Normal Form (BNF). The language of BNF was previously used as part of the deductive clausal resolution method for a variety of branching-time logics. We show how this framework can tackle useful periodic properties, or invariants. We emphasise the potential power of this approach to the process of reconfiguration of an adaptive system where preserving invariant properties is essential