pith. sign in

arxiv: 2509.01462 · v2 · submitted 2025-09-01 · 💻 cs.LO

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

Klaus-Dieter Schewe , Flavio Ferrarotti , Peter Rivi\`ere , Neeraj Kumar Singh , Guillaume Dupont , Yamine A\"it Ameur This is my paper

Pith reviewed 2026-05-18 19:46 UTC · model grok-4.3

classification 💻 cs.LO
keywords Event-Btemporal logicliveness propertiesrelative completenessderivation rulesformal verificationsecurity properties
0
0 comments X

The pith

TREBL is a fragment of temporal Event-B logic whose sound derivation rules are relatively complete for liveness once the machine is refined enough to define the needed variant terms.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Verifying that systems eventually satisfy desired conditions is central to rigorous design of state-based models. The paper extends Event-B logic so that properties of possible traces can be stated, yet formulas are still evaluated directly on states because each state fixes the set of traces that can start from it. It isolates the TREBL fragment that suffices for all liveness conditions of interest and supplies a collection of sound derivation rules for that fragment. Relative completeness is proved: every valid entailment admits a derivation provided the underlying machine has been refined until the required variant terms become definable inside it. The paper further shows that such refinements can always be constructed.

Core claim

The paper shows that the logic of Event-B can be enlarged to a temporal logic whose formulas talk about traces but are interpreted over single states. Within this enlarged logic the fragment TREBL captures every liveness condition that matters in practice. A set of derivation rules is defined and proved sound for TREBL. These rules are relatively complete in the following sense: for any valid entailment of a formula φ there exists a derivation whenever the Event-B machine has been refined so that certain variant terms become expressible in the refined machine, and the paper proves that such a refinement exists for every starting machine.

What carries the argument

The TREBL fragment of the temporal Event-B logic together with its sound derivation rules, whose relative completeness depends on the existence of a refinement that makes the necessary variant terms definable.

If this is right

  • All liveness conditions of interest in Event-B machines become provable by the derivation rules once a suitable refinement is chosen.
  • Refinements that render the required variant terms definable can be constructed for any given Event-B machine.
  • Security properties expressed as liveness conditions can be verified inside the TREBL fragment using the given rules.
  • The entire logic stays interpreted over states rather than explicit traces, preserving the original state-based semantics.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the construction of the required refinements can be made algorithmic, liveness verification could be integrated into existing Event-B tool chains without manual intervention.
  • The same pattern of relative completeness via definable variants might apply to other state-based modeling languages that support refinement.
  • A practical check could be added to refinement tools: determine whether the current machine already defines the variants needed for a given liveness goal.

Load-bearing premise

That for every Event-B machine there exists a refinement in which the variant terms needed for the completeness argument are definable.

What would settle it

An Event-B machine together with a valid TREBL entailment for which no derivation can be found in any refinement of that machine.

read the original abstract

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $\varphi$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces TREBL, a fragment of a temporal logic extending the Event-B logic to express liveness properties of traces while interpreting formulae over machine states (since a state determines all traces starting from it). It defines a set of sound derivation rules for TREBL and establishes relative completeness: for every valid entailment of a formula ϕ a derivation exists provided the Event-B machine M is sufficiently refined so that required variant terms become definable. The authors claim such refinements always exist and illustrate the approach with security examples.

Significance. If the relative-completeness argument is supported by an explicit, semantics-preserving construction of the required refinements, the result would be a useful addition to liveness verification in Event-B. The state-based encoding of trace properties is technically economical, and the security examples help demonstrate applicability. The load-bearing claim, however, is the universal existence of refinements that make the necessary variant terms definable without changing the observable traces of the original machine.

major comments (2)
  1. [§5] §5 (Relative Completeness): The claim that 'such refinements always exist' is central to the relative-completeness theorem. The manuscript must supply an explicit, semantics-preserving construction that, for any machine M and any valid ϕ, produces a refinement M′ in which the required variant terms are definable while leaving the set of traces and the state-to-trace mapping unchanged. Without this construction the completeness statement does not apply to arbitrary Event-B machines.
  2. [§4] §4 (Soundness of Derivation Rules): Soundness is asserted for the TREBL rules, yet the text provides neither proof sketches nor concrete derivation examples for the key rules (e.g., those involving variant terms or liveness operators). A short soundness argument or at least one fully worked derivation would allow independent verification of the soundness claim.
minor comments (2)
  1. [Notation] Notation: The distinction between the original machine M and its refinements should be made explicit in every statement of the completeness theorem; currently the variable M is sometimes overloaded.
  2. [Examples] Examples: The security examples would be strengthened by including the concrete Event-B machine, the target formula ϕ, and the corresponding derivation tree in at least one case.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address the two major comments point by point below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [§5] §5 (Relative Completeness): The claim that 'such refinements always exist' is central to the relative-completeness theorem. The manuscript must supply an explicit, semantics-preserving construction that, for any machine M and any valid ϕ, produces a refinement M′ in which the required variant terms are definable while leaving the set of traces and the state-to-trace mapping unchanged. Without this construction the completeness statement does not apply to arbitrary Event-B machines.

    Authors: We agree that an explicit construction would make the relative-completeness result more transparent. While the manuscript proves existence of the required refinements, we will add, in the revised version, a fully explicit, semantics-preserving construction: for any machine M and valid ϕ we construct M′ by adjoining a finite number of auxiliary variables whose values encode the necessary variant terms. The construction is defined so that the observable events, guards, and actions of M remain unchanged, the set of traces is identical, and the state-to-trace mapping is preserved. We will prove that M′ is a valid refinement of M and that the variant terms become definable in M′. This addition will ensure the completeness statement applies to arbitrary Event-B machines. revision: yes

  2. Referee: [§4] §4 (Soundness of Derivation Rules): Soundness is asserted for the TREBL rules, yet the text provides neither proof sketches nor concrete derivation examples for the key rules (e.g., those involving variant terms or liveness operators). A short soundness argument or at least one fully worked derivation would allow independent verification of the soundness claim.

    Authors: We accept that the soundness section would benefit from additional detail. In the revision we will insert a dedicated subsection containing (i) a concise soundness argument for each key rule, with particular attention to the rules that manipulate variant terms and the liveness operators, and (ii) at least one fully worked derivation that starts from a security-related liveness property and applies the rules step by step. These additions will allow readers to verify the soundness claim independently. revision: yes

Circularity Check

0 steps flagged

No circularity: relative completeness rests on explicit semantics-preserving refinement construction

full rationale

The derivation defines TREBL directly over Event-B state semantics and trace properties, introduces sound rules for the fragment, then proves relative completeness by exhibiting a construction of refinements that make required variant terms definable while preserving the original trace semantics. This construction is internal to the paper, independent of the target entailments, and does not reduce any prediction or completeness statement to a fitted parameter, self-definition, or prior self-citation chain. The claim that such refinements always exist is therefore a genuine theorem rather than a tautology or load-bearing assumption imported from the authors' earlier work.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on the standard semantics of Event-B machines and on the existence of refinements that make variant terms definable; no free parameters or new postulated entities are introduced in the abstract.

axioms (2)
  • domain assumption Event-B machine semantics determine all traces from a given state
    Used to justify interpreting trace properties on states rather than full traces.
  • ad hoc to paper Sufficiently refined machines with definable variant terms always exist
    Central to the relative-completeness argument; stated as always constructible but not shown in the abstract.

pith-pipeline@v0.9.0 · 5743 in / 1575 out tokens · 48210 ms · 2026-05-18T19:46:07.729782+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

  • IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula ϕ one can find a derivation, provided the machine M is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine.

  • IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    Hoang and Abrial showed that conv(φ) can be derived by means of variant terms... var_c(t, φ) ... t(¯v) takes values in some well-founded set V with minimum 0

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

25 extracted references · 25 canonical work pages

  1. [1]

    The B-book - Assigning programs to meanings

    Jean-Raymond Abrial. The B-book - Assigning programs to meanings . Cambridge University Press, 2005

    work page 2005

  2. [2]

    2010.Modeling in Event-B: system and software engineering

    Jean-Raymond Abrial. Modeling in Event-B -- System and Software Engineering . Cambridge University Press, 2010. URL: https://doi.org/10.1017/CBO9781139195881

    work page doi:10.1017/cbo9781139195881 2010

  3. [3]

    Security in Computing Systems - Challenges, Approaches and Solutions

    Joachim Biskup. Security in Computing Systems - Challenges, Approaches and Solutions . Springer, 2009. https://doi.org/10.1007/978-3-540-78442-5 doi:10.1007/978-3-540-78442-5

    work page doi:10.1007/978-3-540-78442-5 2009

  4. [4]

    orger and Robert St\

    Egon B\"orger and Robert St\" a rk. Abstract State Machines . Springer, Berlin Heidelberg New York, 2003

    work page 2003

  5. [5]

    Clarke and E

    Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs , volume 131 of Lecture Notes in Computer Science , pages 52--71. Springer, 1982. https://doi.org/10.1007/BFB0025774 doi:10.1007/BFB0025774

    work page doi:10.1007/bfb0025774 1982

  6. [6]

    and Schneider, Fred B

    Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur. , 18(6):1157--1210, 2010. https://doi.org/10.3233/JCS-2009-0393 doi:10.3233/JCS-2009-0393

    work page doi:10.3233/jcs-2009-0393 2010

  7. [7]

    A complete fragment of LTL(EB)

    Flavio Ferrarotti, Peter Rivi\` e re, Klaus-Dieter Schewe, Neeraj Kumar Singh, and Yamine A\" t Ameur . A complete fragment of LTL(EB) . In Arne Meyer and Magdalena Ortiz, editors, Foundations of Information and Knowledge Systems (Proc. FoIKS 2024) , volume 14589 of LNCS , pages 237--255. Springer, 2024. an extended version is available at http://arxiv.or...

    work page arXiv 2024

  8. [8]

    Modal extensions of the logic of abstract state machines

    Flavio Ferrarotti and Klaus-Dieter Schewe. Modal extensions of the logic of abstract state machines. In Silvia Bonfanti et al., editors, Rigorous State-Based Methods ( ABZ 2024) , volume 14759 of Lecture Notes in Computer Science , pages 123--140. Springer, 2024. https://doi.org/10.1007/978-3-031-63790-2\_8 doi:10.1007/978-3-031-63790-2\_8

    work page doi:10.1007/978-3-031-63790-2 2024

  9. [9]

    A unifying logic for non-deterministic, parallel and concurrent Abstract State Machines

    Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec, and Qing Wang. A unifying logic for non-deterministic, parallel and concurrent Abstract State Machines . Ann. Math. Artif. Intell. , 83(3-4):321--349, 2018. https://doi.org/10.1007/s10472-017-9569-3 doi:10.1007/s10472-017-9569-3

    work page doi:10.1007/s10472-017-9569-3 2018

  10. [10]

    Temporal team semantics revisited

    Jens Oliver Gutsfeld, Arne Meier, Christoph Ohrem, and Jonni Virtema. Temporal team semantics revisited. In Christel Baier and Dana Fisman, editors, 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022) , pages 44:1--44:13, 2022. https://doi.org/10.1145/3531130.3533360 doi:10.1145/3531130.3533360

    work page doi:10.1145/3531130.3533360 2022

  11. [11]

    Reasoning about liveness properties in Event-B

    Thai Son Hoang and Jean-Raymond Abrial. Reasoning about liveness properties in Event-B . In Shengchao Qin and Zongyan Qiu, editors, Formal Methods and Software Engineering ( ICFEM 2011) , volume 6991 of Lecture Notes in Computer Science , pages 456--471. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24559-6\_31

    work page doi:10.1007/978-3-642-24559-6 2011

  12. [12]

    Temporal Logic and State Systems

    Fred Kr \" o ger and Stephan Merz. Temporal Logic and State Systems . Texts in Theoretical Computer Science. An EATCS Series. Springer, 2008

    work page 2008

  13. [13]

    Specifying Systems, The TLA ^+ Language and Tools for Hardware and Software Engineers

    Leslie Lamport. Specifying Systems, The TLA ^+ Language and Tools for Hardware and Software Engineers . Addison-Wesley, 2002

    work page 2002

  14. [14]

    Temporal logic: The lesser of three evils, 2010

    Leslie Lamport. Temporal logic: The lesser of three evils, 2010. Presentation at the Amir Pnueli Memorial Symposium. URL: https://cs.nyu.edu/acsys/pnueli/

    work page 2010

  15. [15]

    Proving noninterference and functional correctness using traces

    John McLean. Proving noninterference and functional correctness using traces. J. Comput. Secur. , 1(1):37--58, 1992. https://doi.org/10.3233/JCS-1992-1103 doi:10.3233/JCS-1992-1103

    work page doi:10.3233/jcs-1992-1103 1992

  16. [16]

    On the logic of TLA ^+

    Stephan Merz. On the logic of TLA ^+ . Computers and Artificial Intelligence , 22(3-4):351--379, 2003

    work page 2003

  17. [17]

    Adequate proof principles for invariance and liveness properties of concurrent programs

    Zohar Manna and Amir Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comput. Program. , 4(3):257--289, 1984. URL: https://doi.org/10.1016/0167-6423(84)90003-0

    work page doi:10.1016/0167-6423(84)90003-0 1984

  18. [18]

    Bounded-deducibility security

    Andrei Popescu and Peter Lammich. Bounded-deducibility security. Arch. Formal Proofs , 2014, 2014. URL: https://www.isa-afp.org/entries/Bounded\_Deducibility\_Security.shtml

    work page 2014

  19. [19]

    CoCon : A confidentiality-verified conference management system

    Andrei Popescu, Peter Lammich, and Thomas Bauereiss. CoCon : A confidentiality-verified conference management system. Arch. Formal Proofs , 2021, 2021. URL: https://www.isa-afp.org/entries/CoCon.html

    work page 2021

  20. [20]

    CoCon : A conference management system with formally verified document confidentiality

    Andrei Popescu, Peter Lammich, and Ping Hou. CoCon : A conference management system with formally verified document confidentiality. J. Autom. Reason. , 65(2):321--356, 2021. https://doi.org/10.1007/S10817-020-09566-9 doi:10.1007/S10817-020-09566-9

    work page doi:10.1007/s10817-020-09566-9 2021

  21. [21]

    18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977 , pages =

    Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (FoCS 1977) , pages 46--57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32

    work page doi:10.1109/sfcs.1977.32 1977

  22. [22]

    Formalising liveness properties in Event-B with the reflexive EB4EB framework

    Peter Rivi\` e re, Neeraj Kumar Singh, Yamine A\" t Ameur , and Guillaume Dupont. Formalising liveness properties in Event-B with the reflexive EB4EB framework. In Kristin Yvonne Rozier and Swarat Chaudhuri, editors, NASA Formal Methods - 15th International Symposium ( NFM 2023) , volume 13903 of Lecture Notes in Computer Science , pages 312--331. Springe...

    work page doi:10.1007/978-3-031-33170-1 2023

  23. [23]

    Formalizing the Logic of Event-B

    Matthias Schmalz. Formalizing the Logic of Event-B . PhD thesis, ETH Z\"urich, 2012

    work page 2012

  24. [24]

    St\" a rk and Stanislas Nanchen

    Robert F. St\" a rk and Stanislas Nanchen. A logic for abstract state machines. Journal of Universal Computer Science , 7(11):980--1005, 2001

    work page 2001

  25. [25]

    a \"a n \

    Jouko V \"a \"a n \"a nen. Second-order and Higher-order Logic . In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy . Metaphysics Research Lab, Stanford University, W inter 2024 edition, 2024

    work page 2024