Event-B and Linear Temporal Logic

Abstract. In this chapter we consider when temporal logic properties can be carried through Event-B refinement chains. We also identify conditions on temporal logic properties that make them suitable for use in a refinement chain, since not all properties are preserved by Event-B refinement. In particular we identify the particular notion of β-dependence for an LTL property: that only the events in the set β need to be checked to determine whether an execution meets the property. Such properties are not affected by the introduction of new events in a refinement step, which means they will carry through a refinement chain and will hold for any resulting refinement which is deadlock-free and does not contain anticipated events. The chapter presents a Lift example refinement chain to illustrate the results and how they are applied.