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 lan- guage 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 pe- riodic 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.

Alexander Bolotov

Department of Computer Science, University of Westminster, London, W1W 6UW, UK