Global and local invariants in transition systems

Given a transition system and a cover P of the set of its states, a set of local invariants with respect to P is defined as a set of predicates in bijection with the set of the blocks of P and in such a way that a local invariant be true every time the system is in a state belonging to the corresponding block of the cover. This definition is proved to be sufficiently general in the sense that any proof made by using global invariants can be also made by using sets of local invariants with respect to any cover P. The same result is proved for two more restrictive definitions of the notion of local invariant by using well-known properties of connections between lattices. Finally, it is shown that the notion of invariant assertion, commonly used for proving programs, can be deduced from the definition of local invariant when a transition system represents a program. In this case, the fixed point equations characterizing local invariants can be simplified to obtain semantical equations of programs