A Complete Fragment of LTL(EB)
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要