💻 computer science

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

Dit artikel introduceert TREBL, een relatief compleet logisch kader voor het verifiëren van liveness-condities in Event-B-machines door eigenschappen van traces te formuleren via toestandsinterpretaties, waarbij de geldigheid van afleidingsregels wordt gegarandeerd door het gebruik van verfijnde machines met definieerbare varianttermen.

Oorspronkelijke auteurs: Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière, Neeraj Kumar Singh, Guillaume Dupont, Yamine Aït Ameur

Gepubliceerd 2026-04-22

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière, Neeraj Kumar Singh, Guillaume Dupont, Yamine Aït Ameur

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een zeer complexe machine bouwt, bijvoorbeeld een beveiligingssysteem voor een bank of een verkeersleidersysteem. Je wilt niet alleen weten of de machine nu goed werkt (bijv. "de lichten zijn groen"), maar ook of ze altijd goed blijven werken in de toekomst. Zorgt het systeem ervoor dat elke auto die wacht, uiteindelijk ook mag passeren? Zorgt het ervoor dat een hacker nooit geheime informatie kan stelen, zelfs niet na duizenden stappen?

Dit is het probleem dat dit artikel oplost. Het introduceert een nieuwe manier om te denken over tijd en logica binnen een strikte wiskundige methode die "Event-B" heet.

Hier is de uitleg in simpele taal, met wat creatieve vergelijkingen:

1. Het Probleem: De "Tijdsreis" is te moeilijk

Stel je voor dat je een spoorboekje hebt van een treinreis. In de oude methoden (zoals standaard tijdslogica) moest je het hele spoorboekje van begin tot eind bekijken om te zeggen: "Ja, deze trein komt er ooit aan."
Het probleem is dat dit heel lastig is om wiskundig te bewijzen. Het is alsof je probeert te bewijzen dat een spoorlijn nooit vastloopt, terwijl je de hele lijn in één keer moet zien. De oude regels waren ofwel te simpel (ze konden geen complexe regels zien) ofwel te ingewikkeld (je kon ze nooit volledig bewijzen).

2. De Oplossing: Kijk naar de Start, niet naar de Reis

De auteurs van dit artikel hebben een slimme truc bedacht. Ze zeggen: "Je hoeft niet de hele reis te bekijken. Als je weet waar de trein vertrekt en hoe de regels van de machinist zijn, weet je al precies welke routes de trein kan nemen."

In plaats van te kijken naar een lange lijst van staties (de "sporen"), kijken ze alleen naar de huidige staat van de machine.

De Analogie: Stel je een labyrint voor. In de oude manier moest je door elke gang lopen om te zien of je de uitgang vond. De nieuwe manier (TREBL) zegt: "Als je weet waar je nu staat en welke muren er zijn, kun je wiskundig berekenen of er een uitweg is, zonder dat je door het hele labyrint hoeft te lopen."

Ze hebben een nieuwe logica bedacht, TREBL, die tijdsregels (zoals "altijd", "ooit", "totdat") vertaalt naar regels die je kunt controleren op één enkel moment.

3. De "Varianten": De Telkens Korter Wordende Ladder

Hoe bewijs je nu dat iets ooit gebeurt? Stel je voor dat je een ladder hebt die steeds korter wordt.

Als je op de 10e sport staat, en elke stap die je zet, maakt de ladder 1 sport korter, dan weet je zeker dat je ooit op de grond (sport 0) komt. Je kunt niet oneindig blijven klimmen als de ladder korter wordt.
In de wiskunde noemen ze dit een variant. Het is een getal dat bij elke actie van de machine kleiner wordt.
De Boodschap: Als je kunt laten zien dat er zo'n "telkens korter wordende ladder" bestaat, dan is het bewijs geleverd dat het systeem niet vastloopt en dat het doel bereikt wordt.

Het artikel bewijst iets heel belangrijks: Je kunt voor elke machine die goed werkt, altijd zo'n ladder vinden. Soms moet je de machine wel een beetje "verfijnen" (d.w.z. extra details toevoegen aan het ontwerp) om de ladder zichtbaar te maken, maar het is altijd mogelijk.

4. Waarom is dit zo belangrijk? (De Beveiligings-voorbeeld)

De auteurs gebruiken dit om complexe beveiligingsproblemen op te lossen.

Voorbeeld: Stel je hebt een geheime kluis. Je wilt bewijzen dat een persoon met een lage toegangsrechten (een "kassier") nooit kan zien wat er in de kluis gebeurt als een directeur (een "hooggeplaatste") erbij is.
In de oude methoden was dit een nachtmerrie om te bewijzen omdat je alle mogelijke scenario's moest bekijken.
Met TREBL kunnen ze dit bewijzen met een simpele regel: "Als de directeur iets doet, verandert de staat van de machine op een manier die voor de kassier onzichtbaar blijft." Omdat ze kijken naar de start en de regels, is het bewijs veel korter en sterker.

5. Het Resultaat: "Relatieve Volledigheid"

Dit klinkt als een moeilijke term, maar het betekent simpelweg:

"Als je systeem in de werkelijkheid werkt (het is waar), dan kunnen we dat altijd bewijzen met onze regels, zolang we maar de juiste 'ladders' (varianten) in het ontwerp hebben opgenomen."

Het is alsof ze zeggen: "We hebben een gereedschapskist vol met regels. Als je een machine bouwt die werkt, dan zit er in die gereedschapskist altijd een sleutel die past om te bewijzen dat het werkt. Je hoeft alleen maar de sleutel (de variant) te vinden."

Samenvatting in één zin

Dit artikel introduceert een slimme manier om te bewijzen dat computersystemen in de toekomst veilig en betrouwbaar blijven, door te stoppen met het bekijken van de hele toekomstige reis en in plaats daarvan te kijken naar de huidige staat en een "telkens korter wordende ladder" die garandeert dat het doel bereikt wordt.

Het is een doorbraak omdat het complexe tijdsproblemen maakt tot simpele, bewijsbare wiskundige regels, wat essentieel is voor het bouwen van veilige software in onze moderne wereld.

Titel: TREBL – Een relatief complete temporale Event-B logica (Deel I: Theorie)

Auteurs: Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière, Neeraj Kumar Singh, Guillaume Dupont, Yamine Ait-Ameur.

1. Het Probleem

De verificatie van levendigheidseigenschappen (liveness conditions) is een cruciaal aspect van state-based rigoureuze methoden zoals Event-B. Bestaande methoden ondersteunen goed de verificatie van invarianten (veiligheidseigenschappen), maar de verificatie van eigenschappen die betrekking hebben op volledige traces (bijv. "eventueel gebeurt er iets" of "altijd blijft iets waar") is problematisch.

Beperking van bestaande logica's: Klassieke temporale logica's zoals LTL (Linear-Time Temporal Logic) en CTL zijn proposities-gedreven en beperkt in expressiviteit wanneer ze worden toegepast op systemen met complexe datastructuren (zoals in Event-B).
Expressiviteit vs. Volledigheid: Als men temporale logica uitbreidt naar first-order logica om meer expressief te zijn, verliest men vaak de eigenschap van volledigheid (completeness). Dit betekent dat er geldige formules zijn die niet bewezen kunnen worden met de beschikbare afleidingsregels.
Interpretatieprobleem: In traditionele benaderingen worden temporale formules geïnterpreteerd over traces (sequenties van toestanden). In rigoureuze methoden zoals Event-B wordt echter aangenomen dat een enkele toestand alle mogelijke traces die daaruit voortkomen, bepaalt. De huidige logica's maken geen optimaal gebruik van deze eigenschap, wat leidt tot complexiteit en beperkingen in bewijsvoering.

2. Methodologie

De auteurs introduceren TREBL (TempoRal Event-B Logic), een logica die de expressiviteit van temporale logica combineert met de kracht van de Event-B logica, terwijl de interpretatie behouden blijft over toestanden in plaats van traces.

Uitbreiding van de Event-B Logica ( $L_{ext}$ ):
- De auteurs definiëren een uitgebreide logica waarin update sets (verzamelingen van wijzigingen in toestandsvariabelen) expliciet worden behandeld.
- Ze introduceren modaliteiten $[X]\phi$ , die uitspreken dat na het toepassen van een update set $X$ , de formule $\phi$ geldt.
- Ze definiëren operatoren voor meervoudige stappen ( $USet^*(k, X)$ ) om de effecten van reeksen van gebeurtenissen te modelleren.
Definitie van Temporale Operatoren als Snelkoppelingen:
- In plaats van temporale operatoren als fundamentele bouwstenen te zien, worden ze gedefinieerd als complexe formules in $L_{ext}$ die over toestanden worden geïnterpreteerd.
- Operatoren zoals ALWAYS ( $\square$ ), EVENTUALLY ( $\diamond$ ) en UNTIL ( $U$ ) worden vertaald naar formules die quantificeren over mogelijke update sets en traces die vanuit de huidige toestand vertrekken.
- Dit maakt het mogelijk om ook formules te definiëren die gelden voor alle traces, één specifieke trace, of voor definibele subsets van traces.
Afleidingsregels en Variant Termen:
- Het systeem maakt gebruik van variant termen (well-founded sets) om levendigheidseigenschappen te bewijzen.
- Er worden specifieke varianten geïntroduceerd voor verschillende scenario's:
  - c-varianten: voor convergentie (eventueel stoppen met een eigenschap).
  - d-varianten: voor divergentie (eventueel blijvend vasthouden aan een eigenschap).
  - e-varianten: voor bereikbaarheid.
  - Simultane en conditionele varianten: voor complexere progressie-eigenschappen.
Refinement: Een kernidee is dat als een machine niet voldoet aan de vereisten voor een bewijs (bijv. ontbrekende variant termen), deze machine conservatief kan worden verfijnd (refined) om deze termen expliciet te definiëren.

3. Belangrijkste Bijdragen

Definitie van TREBL: Een fragment van de uitgebreide Event-B logica dat de meest belangrijke levendigheidseigenschappen (invariantie, bestaan, progressie, persistentie, bereikbaarheid) omvat, inclusief varianten voor "alle traces" en "één trace".
Interpretatie over Toestanden: De logica behoudt de interpretatie over toestanden, wat de link met de onderliggende machine direct houdt en de noodzaak elimineert om traces als eerste-orde objecten te behandelen.
Relatieve Volledigheid (Relative Completeness): De auteurs bewijzen dat hun set van afleidingsregels relatief compleet is. Dit betekent dat elke geldige formule in TREBL bewezen kan worden, mits de machine voldoende is verfijnd om de benodigde variant termen te definiëren.
Verwijdering van Beperkingen: In tegenstelling tot eerdere werken (zoals [FRS+24]), worden de restricties op tail-homogeneity (waarbij alle traces hetzelfde gedrag moeten vertonen aan het einde) verwijderd. Dit maakt de logica robuuster voor niet-deterministische systemen.
Bewijs van Bestaan van Refinement: Er wordt aangetoond dat het altijd mogelijk is om een Event-B machine te verfijnen zodat de vereiste variant termen bestaan. Dit garandeert dat de voorwaarde voor relatieve volledigheid altijd haalbaar is.

4. Resultaten

Geluidheid (Soundness): Alle afleidingsregels voor TREBL zijn bewezen geluid. Als een formule afleidbaar is ( $M \vdash \phi$ ), dan is deze ook geldig ( $M \models \phi$ ).
Relatieve Volledigheid: Voor elke geldige formule $\phi$ in TREBL bestaat er een afleiding, mits de machine voldoet aan de "relativity assumptions" (consistentie, inbegrip van bereikbare eigenschappen in invarianten, en voldoende verfijning voor varianten).
Toepassingsvoorbeelden: De theorie wordt geïllustreerd met voorbeelden uit het domein van beveiliging:
- Non-interference: Een complex beveiligingsconcept wordt in TREBL uitgedrukt als een eenvoudige invariantieconditie met een overgangsformule, wat veel eenvoudiger is dan in traditionele LTL/CTL.
- Fairness en Bounded Deducibility: Voorbeelden van progressie en privacy-beperkingen worden succesvol gemodelleerd en bewezen.
Mechanische Ondersteuning: Hoewel dit artikel de theorie behandelt, wordt verwezen naar een tweede deel waarin de integratie met het RODIN-tool en de EB4EB meta-theorie wordt beschreven voor automatische bewijsvoering.

5. Betekenis en Impact

Dit werk vertegenwoordigt een doorbraak in de formele verificatie van state-based systemen:

Overbrugging van de kloof: Het lost het fundamentele dilemma op tussen expressiviteit en volledigheid door temporale logica te integreren in de state-based logica zonder de interpretatie over traces te vereisen.
Praktische Toepasbaarheid: Het biedt een theoretisch fundament voor het mechanisch bewijzen van complexe levendigheidseigenschappen in kritieke systemen (zoals beveiligingsprotocollen), wat tot nu toe vaak te moeilijk was met bestaande tools.
Generaliseerbaarheid: Hoewel de theorie is ontwikkeld voor Event-B, zijn de kernprincipes (interpretatie over toestanden en het gebruik van verfijning voor varianten) toepasbaar op andere rigoureuze methoden zoals Abstract State Machines (ASM), B en TLA+.

Samenvattend biedt TREBL een krachtig, geluid en relatief compleet raamwerk om levendigheidseigenschappen in complexe, niet-deterministische systemen formeel te specificeren en te verifiëren, waarbij de bewijslast verschuift naar het definiëren van geschikte varianten via verfijning.