A Complete Fragment of LTL(EB)

TL;DR

The paper tackles the problem of verifying liveness properties for Event-B models by introducing a fragment $\square$LTL that combines the UNTIL fragment of LTL with Event-B state-formulae. It defines LTL(EB), then constructs a robust semantic and syntactic framework, including variant terms, to prove convergence and divergence within tail-homogeneous, sufficiently refined machines. A complete set of derivation rules for $\square$LTL is developed, extending first-order logic with invariance, existence, progress, and persistence reasoning, and completeness is established for the fragment under the stated restrictions. The work enables mechanical verification of common liveness properties such as invariance, existence, and persistence in Event-B, and suggests directions for extensions to CTL(EB) and other state-based formalisms.

Abstract

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment $\square$LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli's linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of derivation rules is developed, which is also complete under mild restrictions for Event-B machines.

Theorems & Definitions (18)

• lemma 1
• proof
• lemma 2
• proof
• lemma 3
• proof
• lemma 4
• proof
• theorem 1
• lemma 5