Idioma:

A Complete Fragment of LTL(EB)

Ferrarotti, Flavio ; Rivière, Peter ; Schewe, Klaus-Dieter ; Singh, Neeraj Kumar ; Yamine Aït Ameur

arXiv.org, 2024-01

Texto completo disponível

Citações Citado por

Título:
A Complete Fragment of LTL(EB)
Autor: Ferrarotti, Flavio ; Rivière, Peter ; Schewe, Klaus-Dieter ; Singh, Neeraj Kumar ; Yamine Aït Ameur
Assuntos: Computer Science - Logic in Computer Science ; Temporal logic
É parte de: arXiv.org, 2024-01
Descrição: 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.
Editor: Ithaca: Cornell University Library, arXiv.org
Idioma: Inglês

Links

Voltar para lista de resultados