Verification of LTL on B event systems

Abstract

This paper proposes a way to verify temporal properties expressed in LTL (Linear Temporal Logic) on B Event Systems. The method consists in generating a B representation of the Büchi automaton associated with the LTL property to verify. We establish the consistency of the generated event system implies the satisfaction of the LTL property on the executions of the original event system. We also characterize the subset of LTL preserved by the B refinement and we propose another refinement relation, with necessary and sufficient condition for preserving any given LTL property.