Technische Samenvatting: Een Beslissingsprocedure voor een Theorie van Eindige Mengen met Eindige Gehele Getallenintervallen

Probleemstelling

In de context van formele verificatie en analyse zijn geautomatiseerde redeneertools essentieel voor het afhandelen van verificatievoorwaarden. Hoewel bestaande tools die gebaseerd zijn op de mengtheorie (bijv. B, ProB) effectief zijn, missen ze vaak beslissingsprocedures voor specifieke fragmenten van de mengtheorie die eindige Mengen combineren met gehele getallenintervallen. Specifiek is de Boolese algebra van eindige Mengen, uitgebreid met kardinaliteitsbeperkingen (aangeduid als $L|\cdot|$), beslisbaar, maar kan deze niet op native wijze eindige gehele getallenintervallen (bereiken) uitdrukken of redeneren over deze, waarbij de grenzen onbeperkte variabelen kunnen zijn. Deze beperking belemmert de automatische verificatie van eigenschappen die Mengenbewerkingen betreffen, zoals het vinden van het minimum of maximum van een Menge, het partitioneren van Mengen op basis van gehele getal-drempels, of het redeneren over array-domeinen die gedefinieerd zijn door intervallen. Het kernprobleem dat wordt aangepakt, is de beslisbaarheid van een theorie die eindige Mengen, kardinaliteitsbeperkingen en eindige gehele getallenintervallen (aangeduid als $L[\ ]$) integreert binnen een kwantorenvrije logica.

Methodologie

De auteurs stellen een beslissingsprocedure voor, SAT $[\ ]$, die de bestaande solver SAT $|\cdot|$ (voor $L|\cdot|$) uitbreidt om gehele getallenintervallen te verwerken. De methodologie vertrouwt op een basistheorie van hereditair eindige Mengen, geïmplementeerd binnen de Constraint Logic Programming (CLP)-taal CLP($SET$) en de tool {log}.

Belangrijke Technische Componenten:

1. Taaluitbreiding ($L[\ ]$):

   • De taal wordt uitgebreid om Meng-termen van de vorm $[k, m]$ op te nemen, die de Menge $\{p \in \mathbb{Z} \mid k \le p \le m\}$ voorstellen.
   • Intervalgrenzen ($k, m$) kunnen lineaire gehele getal-termen zijn, inclusief variabelen.
   • De logica blijft kwantorenvrij, met gebruikmaking van conjuncties en disjuncties van beperkingen die betrekking hebben op Mengenlidmaatschap, vereniging, disjunctiviteit, kardinaliteit en intervallidmaatschap.

2. Kernidentiteit en Reductiestrategie:

   • Het centrale theoretische inzicht is de identiteit: $k \le m \implies (A = [k, m] \iff A \subseteq [k, m] \land |A| = m - k + 1)$.
   • Deze identiteit stelt de procedure in staat om beperkingen die gelijkheid met een interval betreffen, om te zetten in beperkingen die betrekking hebben op deelverzameling-relaties en kardinaliteit.
   • De solver herschrijft formules naar een conjunctie van een standaard $L|\cdot|$-formule ($\Phi_{|\cdot|}$) en een verzameling deelverzameling-beperkingen die intervallen betreffen ($\Phi_{\subseteq[\ ]}$), typisch van de vorm $X \subseteq [p, q]$ waarbij $X$ een variabele is.

3. Het SAT $[\ ]$-Algoritme:

   • Herschrijvingsregels: De solver maakt gebruik van een reeks herschrijvingsregels (STEPS$[\ ]$) die de syntactische complexiteit reduceren. Deze regels behandelen gelijkheid, lidmaatschap, vereniging, disjunctiviteit en kardinaliteitsbeperkingen die intervallen betreffen.
   • Reductie tot Lineaire Gehele Getallen-Arithmetiek: Veel regels herschrijven Mengenbeperkingen die intervallen betreffen direct naar beperkingen van lineaire gehele getallen-arithmetiek (LIA).
   • Controle op Minimale Oplossing: Wanneer irreduceerbare beperkingen van de vorm $X \subseteq [p, q]$ overblijven, faalt de procedure niet simpelweg. In plaats daarvan maakt deze gebruik van het gegeven dat als een formule vervulbaar is, deze een "minimale oplossing" moet hebben (een oplossing waarbij Mengen de minimaal mogelijke kardinaliteit hebben).
     • De solver berekent de minimale oplossing voor het $L|\cdot|$-gedeelte ($\Phi_{|\cdot|}$).
     • Vervolgens controleert deze of deze minimale oplossing voldoet aan de intervalbeperkingen ($\Phi_{\subseteq[\ ]}$).
     • De auteurs bewijzen dat als geen enkele minimale oplossing voldoet aan de volledige formule, dan zal ook geen enkele grotere oplossing dat doen, waardoor de formule onvervulbaar is.

4. Implementatie in {log}:

   • De procedure is geïmplementeerd in {log} (setlog), een op Prolog gebaseerde tool.
   • De implementatie omvat een memoiserend schema om variabele substituties voor intervallen bij te houden, waardoor redundante herschrijving wordt voorkomen en de efficiëntie wordt verbeterd.
   • Afgeleide beperkingen (bijv. doorsnede, verschil) worden gedefinieerd in termen van primitieve beperkingen om consistentie te behouden.

Belangrijkste Bijdragen

1. Bewijs van Beslisbaarheid: Het artikel levert het eerste bewijs dat de Boolese algebra van eindige Mengen, uitgebreid met kardinaliteitsbeperkingen en eindige gehele getallenintervallen ($L[\ ]$), beslisbaar is.
2. Beslissingsprocedure (SAT $[\ ]$): Een compleet algoritme wordt gepresenteerd dat de vervulbaarheid van $L[\ ]$-formules beslist. De procedure is bewezen correct, compleet en terminerend.
3. Integratie van Intervallen en Mengen: In tegenstelling tot benaderingen die intervallen behandelen als een apart domein of constante grenzen vereisen, integreert dit werk soepel variabel-begrensde gehele getallenintervallen in de mengtheorie. Dit maakt het mogelijk om niet-triviale operatoren uit te drukken (bijv. het $i$-de kleinste element, partitioneren op basis van een drempel) in een kwantorenvrije logica.
4. Implementatie en Tooling: De beslissingsprocedure is geïmplementeerd als een extensie van de {log}-tool, waardoor een dubbele capaciteit wordt geboden als zowel een Constraint Logic Programming-taal als een vervulbaarheidssolver.

Resultaten en Evaluatie

Het artikel presenteert empirisch bewijs en een casestudie om het praktische nut van de aanpak te demonstreren:

• Benchmarks Evaluatie: Een set van 60 $L[\ ]$-formules, die eigenschappen vertegenwoordigen van operatoren gedefinieerd in het artikel (bijv. minimum, maximum, $i$-de element), werd opgelost. {log} loste alle problemen op met een gemiddelde van 0,51 seconde per probleem, waarbij slechts één probleem meer dan 5 seconden in beslag nam.
• Casestudie (Liftalgoritme): De auteurs modelleerden een liftcontrolesysteem waarbij de lift verzoeken in een specifieke richting moet bedienen. Het model gebruikte gehele getallenintervallen om verdiepingen en verzoeken te definiëren.
  • Het systeem omvatte 7 operaties (bijv. verzoeken toevoegen, het volgende verzoek bedienen).
  • {log} werd gebruikt om automatisch 49 invariantielemmata af te handelen (het bewijzen dat staatsoperaties 7 staatsinvarianten behouden) en 7 controles van de beginstaat.
  • Alle bewijzen werden voltooid in ongeveer 0,5 seconde op een standaard laptop.
  • De tool slaagde er succesvol in tegenvoorbeelden te genereren wanneer invarianten opzettelijk werden verzwakt, waardoor de foutopsporingscapaciteiten werden aangetoond.

Betekenis en Claims

De auteurs claimen dat dit werk een belangrijke stap voorwaarts betekent in geautomatiseerd redeneren voor formele verificatie. Door het beslisbare fragment van de mengtheorie uit te breiden om eindige gehele getallenintervallen met variabele grenzen op te nemen, maakt de aanpak automatische verificatie mogelijk van eigenschappen die eerder moeilijk of onmogelijk waren uit te drukken zonder kwantoren.

Het artikel benadrukt dat de aanpak geworteld is in de mengtheorie, wat deze onderscheidt van andere intervallenredeneertools (zoals die gebaseerd zijn op de intervalalgebra van Allen of lattices voor statische analyse), die vaak het vermogen missen om intervallen te combineren met algemene Mengenbewerkingen. De integratie van intervallenredenering in het {log}-kader stelt gebruikers in staat om programma's te schrijven en hun eigenschappen te bewijzen met dezelfde code en tool, gebruikmakend van de dualiteit van formule en programma. De auteurs merken nederig op dat hoewel de aanpak algemeen en coherent is, deze efficiëntiekosten kan opleveren in vergelijking met gespecialiseerde solvers voor specifieke alleen-intervalproblemen, maar dat de ruil het vermogen is om te redeneren over complexe hybride Meng-intervalstructuren.