The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment □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.
@article{arxiv.2401.16838,
title = {A Complete Fragment of LTL(EB)},
author = {Flavio Ferrarotti and Peter Rivière and Klaus-Dieter Schewe and Neeraj Kumar Singh and Yamine Aït Ameur},
journal= {arXiv preprint arXiv:2401.16838},
year = {2024}
}