💻 computer science

Langshaw: Declarative Interaction Protocols Based on Sayso and Conflict

Dit artikel introduceert Langshaw, een declaratieve protocoltaal die gebruikmaakt van "sayso", "nono" en "nogo" constructen om flexibiliteit en semantische helderheid in multi-agent interacties te balanceren, terwijl het formele semantiek, veiligheids-/liveness-verificatie en methoden voor het genereren van asynchrone berichtgeoriënteerde protocollen biedt.

Oorspronkelijke auteurs: Munindar P. Singh, Samuel H. Christie V, Amit K. Chopra

Gepubliceerd 2026-06-30

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Munindar P. Singh, Samuel H. Christie V, Amit K. Chopra

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 een groep vrienden voor die een verrassingsfeestje probeert te organiseren. Ze moeten het eens worden over de gastenlijst, het budget, het eten en de locatie. In de wereld van de informatica zijn deze vrienden "agenten" (softwareprogramma's) en het feestplan is een "protocol".

Het artikel introduceert een nieuwe manier om deze feestplannen te schrijven, genaamd Langshaw. De auteurs stellen dat de huidige manieren om deze plannen te schrijven ofwel te rigide zijn (zoals een strikt script waarin je niet kunt improviseren) ofwel te rommelig (moeilijk te begrijpen wat iedereen eigenlijk probeert te zeggen).

Hier is hoe Langshaw werkt, uitgelegd via eenvoudige analogieën:

1. Het kernprobleat: Wie beslist wat?

In een normaal gesprek, als twee mensen tegelijkertijd over hetzelfde ding proberen te beslissen, wordt het chaotisch.

De oude manier: De meeste computertalen proberen dit te stoppen door iedereen op hun beurt te laten wachten (synchroon) of door de regels zo complex te maken dat het moeilijk is om te weten wie wat mag doen.
De Langshaw-manier: Langshaw accepteert dat mensen (agenten) tegelijkertijd dingen kunnen proberen te doen. In plaats van het te stoppen, gebruikt het twee speciale hulpmiddelen om de chaos te beheersen: Sayso en Conflict.

2. De magische hulpmiddelen

Sayso: De regel "Wie heeft het laatste woord"

Stel je voor dat de vrienden discussiëren over het menu.

Het concept: Langshaw introduceert een construct genaamd Sayso. Dit is een vooraf afgesproken regel die zegt: "Als het gaat over het eten, heeft de Chef het laatste woord. Als het gaat over de muziek, heeft de DJ het laatste woord."
Hoe het werkt: Als de Chef en de DJ op exact hetzelfde moment het menu proberen te veranderen, controleert het systeem de "Sayso"-lijst. Omdat de Chef "Sayso" heeft over het eten, wint de keuze van de Chef en wordt de poging van de DJ genegeerd. Dit voorkomt een rommelige discussie zonder dat er een scheidsrechter nodig is om het gesprek te stoppen.

Nogo en Nono: De "Niet mengen"-regels

Soms kunnen twee acties simpelweg niet tegelijkertijd plaatsvinden, zoals het proberen te "Annuleren van het feest" en "Versturen van de uitnodigingen" op hetzelfde moment.

Nogo (Stopteken): Dit is een eenrichtingsregel. "Als je het feest Annuleert, kun je de uitnodigingen niet Versturen." Het is als een verkeerslicht: als het licht rood is (Annuleren), kun je niet gaan (Versturen).
Nono (Wederzijdse uitsluiting): Dit is een tweerichtingsregel. "Je kunt het feest niet Annuleren EN de uitnodigingen Versturen." Ze zijn wederzijds uitgesloten. Je moet één pad kiezen.

3. Het "Sociale Artefact": Het gedeelde whiteboard

Langshaw stelt zich voor dat de interactie van de groep plaatsvindt op een groot, gedeeld Sociaal Whiteboard.

Elke keer als iemand iets doet (zoals "Koper stuurt een offerte"), wordt dit op het bord geschreven.
De regels (Sayso en Conflict) zorgen ervoor dat zelfs als iedereen tegelijkertijd op het bord schrijft, het uiteindelijke plaatje op het bord logisch is.
Veiligheid (Safety): Het systeem controleert of het bord in een defecte staat terechtkomt (bijv. "Feest geannuleerd" en "Feest gaande" naast elkaar geschreven staan). De regels van Langshaw voorkomen dit.
Levendigheid (Liveness): Het systeem controleert of het feest ook daadwerkelijk wordt afgerond. Het zorgt ervoor dat de groep niet vast komt te zitten in een eindeloze lus van discussiëren zonder ooit een uitnodiging te versturen.

4. Van "Perfecte timing" naar "Het echte leven"

De auteurs doen iets slims met tijd:

De Ideale Wereld (Synchroon): Eerst schrijven de auteurs de regels uitgaande van de aanname dat iedereen in dezelfde kamer is en direct met elkaar praat. Dit maakt het gemakkelijk om te controleren of de regels logisch en veilig zijn.
De Echte Wereld (Asynchroon): Vervolgens gebruiken ze een "compiler" (een vertaaltool) om die perfecte, directe regels om te zetten naar een formaat dat werkt op het echte internet, waar berichten vertraagd kunnen worden, verloren kunnen gaan of in de verkeerde volgorde kunnen aankomen.
- Analogie: Het is als het schrijven van een perfect script voor een toneelstuk waarbij acteurs direct spreken. Daarna vertaalt de regisseur dat script naar een reeks tekstberichten en e-mails die de acteurs vanuit verschillende steden kunnen sturen, waarbij ervoor wordt gezorgd dat het verhaal nog steeds logisch blijft, zelfs als de e-mails te laat aankomen.

5. Waarom dit ertoe doet

De auteurs hebben een tool (een "verifier") gebouwd die een Langshaw-protocol kan bekijken en je direct kan vertellen:

"Dit plan is veilig; niemand zal per ongeluk de regels breken."
"Dit plan is levendig; het proces zal daadwerkelijk worden afgerond."
"Hier is de code die je nodig hebt om dit op het echte internet te draaien."

Ze hebben dit getest op verschillende voorbeelden (zoals een "Aankoop"-protocol voor het kopen van artikelen) en ontdekten dat hun tool snel en accuraat is.

Samenvatting

Langshaw is een nieuwe taal voor het ontwerpen van hoe computerprogramma's met elkaar communiceren. In plaats van ze te dwingen om op hun beurt te wachten of verwarrende code te schrijven, gebruikt het Sayso (prioriteitsregels) en Conflict (niet-mengen-regels) om hen vrij te laten samenwerken. Het begint met een eenvoudig, perfect model en vertaalt dit vervolgens naar een formaat dat werkt op het rommelige, trage internet, waardoor gegarandeerd wordt dat zelfs wanneer dingen tegelijkertijd gebeuren, het resultaat altijd correct is.

Technische Samenvatting: Langshaw – Declaratieve Interactieprotocollen Gebaseerd op Sayso en Conflict

1. Probleemstelling

In gedecentraliseerde multi-agent systemen (MAS) moeten agenten op een losjes gekoppelde manier interageren om interoperabiliteit te bereiken. Bestaande talen voor het specificeren van deze protocollen staan voor een fundamentele afruil: ze ofwel overbeperken de uitvoering van protocollen (wat de flexibiliteit beperkt), ofwel compliceren ze de vastlegging van betekenis (wat redeneren bemoeilijkt).

Traditionele berichtgebaseerde modellering is problematisch om twee redenen:

Lage complexiteit: Berichten zijn de kleinste operationele eenheden, wat leidt tot een explosie in mogelijke berichtvolgordes en coördinatiecomplexiteit.
Mapping-problemen: Er is vaak geen natuurlijke koppeling tussen specifieke berichten en hun onderliggende sociale of mentale betekenissen.

Bestaande benaderingen mengen informatie-inhoud vaak met coördinatielogica (bijv. BSPL, HAPN) of vertrouwen op externe "synchronisatoren" (infrastructurele entiteiten) om conflicten willekeurig op te lossen, wat faalt in het vastleggen van de sociale aard van interacties tussen agenten.

2. Methodologie: De Langshaw-taal

De auteurs stellen Langshaw voor, een declaratieve protocoltaal geïnspireerd door de taalhandelingstheorie van Austin ("zeggen maakt dat het zo is"). Langshaw scheidt communicatieve handelingen van zowel berichten als betekenissen, en modelleert interacties direct via sociale acties.

Kernconstructen

Langshaw introduceert drie nieuwe primitieven om informatie en coördinatie te beheren:

Sayso (Prioriteit): Een construct dat vastlegt wie prioriteit heeft bij het instellen van specifieke attributen.
- Agenten kunnen proberen attributen te binden. Als meerdere agenten hetzelfde attribuut proberen te binden, slaagt de agent met de hogere gerangschikte sayso; anderen falen (worden no-ops).
- Dit maakt flexibele, gelijktijdige pogingen mogelijk terwijl een consistente sociale staat wordt gewaarborgd door middel van geprioriteerde autoriteit in plaats van willekeurige infrastructurele ordening.
Nono (Wederzijdse Uitsluiting): Een construct dat tweezijdige conflicten tussen acties vastlegt.
- Als twee acties een nono-constraint hebben, zijn ze wederzijds uitgesloten voor dezelfde bindingen. Dit voorkomt inconsistente sociale staten (bijv. een agent kan niet zowel een bestelling "Accepteren" als "Afwijzen").
Nogo (Asymmetrische Blokkering): Een construct dat asymmetrische conflicten vastlegt.
- Als actie $A$ een nogo heeft over actie $B$ , voorkomt de uitvoering van $A$ dat $B$ wordt uitgevoerd, zelfs als ze gelijktijdig of in verschillende volgordes worden geprobeerd.

Syntaxis en Semantiek

Syntaxis: Protocollen definiëren rollen, attributen (met sleutels), sociale acties (uitgevoerd door rollen), sayso-rangschikkingen, nono-paren en nogo-constraints.
Formele Semantiek: Het artikel biedt een synchrone semantiek die wordt gekaderd als inferentieregels (semantic tableaux).
- De systeemtoestand is een verzameling uitgevoerde acties.
- Transities vinden plaats via gezamenlijk haalbare verzamelingen van gelijktijdige acties.
- Haalbaarheid wordt bepaald door sayso-dominantie (het oplossen van conflicten), het naleven van nono/nogo-constraints en consistentie met bestaande sociale staat-bindingen.
- Dit synchrone model vereenvoudigt specificatie en redeneren, terwijl het erkent dat echte MAS vaak asynchroon opereren.

3. Belangrijkste Bijdragen

A. Formele Taal en Verificatie

De auteurs introduceren Langshaw en bieden:

Formele Semantiek: Een rigoureuze definitie van protocoluitvoering gebaseerd op updates van de sociale staat.
Beslissingsprocedures: Efficiënte algoritmen om veiligheid (afwezigheid van integriteitsschendingen) en liveness (garantie van voltooiing) te verifiëren.
- Veiligheid wordt geverifieerd door te controleren of geen enkele tak in het semantic tableau conflicterende acties bevat (bijv. een nono-schending).
- Liveness wordt geverifieerd door te waarborgen dat elk mogelijk uitvoeringspad leidt naar een staat waarin voltooiingscriteria (specifieke attributen) gebonden zijn.

B. Het overbruggen van de Synchrone en Asynchrone Werelden

Een belangrijke bijdrage is de compilatie van Langshaw-protocollen naar asynchrone berichtgeoriënteerde protocollen (specifiek BSPL - Blindingly Simple Protocol Language).

De Kloof: Synchrone semantiek is gemakkelijker te redeneren over, maar echte MAS draaien op asynchrone infrastructuren (zoals het Internet).
De Oplossing: De auteurs presenteren een compiler die de hoogwaardige declaratieve regels van Langshaw vertaalt naar BSPL-berichten.
- Sayso wordt gemodelleerd via delegatie (bijv. een agent met een lagere prioriteit moet een delegatiebericht ontvangen van een agent met een hogere prioriteit om een attribuut te binden).
- Nono/Nogo-constraints worden gemodelleerd met nil-parameters (blokkerende parameters) die de berichtoverdracht voorkomen totdat aan specifieke voorwaarden is voldaan.
Correctheid: Het artikel bewijst dat elke asynchrone uitvoering die door het gecompileerde BSPL-protocol wordt geproduceerd, overeenkomt met een geldige synchrone uitvoering in de oorspronkelijke Langshaw-semantiek.

C. Optimalisatie (Tableau Reductie)

Om de potentiële exponentiële explosie van het semantic tableau aan te pakken, stellen de auteurs een reductietechniek voor:

Zij identificeren interferentie (acties die anderen blokkeren of vertragen) en groeperen niet-interfererende acties.
Met behulp van graafkleuring-benaderingen consolideren zij de takken om alle semantisch onderscheidende mogelijkheden te dekken zonder elke interleaving te enumereren, wat een hanteerbare verificatie garandeert.

4. Resultaten

De auteurs hebben een verifieerder in Python geïmplementeerd en getest op verschillende protocollen uit de literatuur (bijv. Purchase, Refund, RFQ-Quote).

Prestaties: De verifieerder controleerde succesvol liveness en veiligheid voor diverse protocollen in milliseconden (bijv. 480ms voor het "Purchase" protocol).
Schaalbaarheid: De reductietechniek beheerde de toestandsruimte effectief, waarbij het aantal knopen en takken beheersbaar bleef, zelfs voor complexe protocollen.
Validatie: De compiler genereerde succesvol BSPL-protocollen die de oorspronkelijke Langshaw-constraints respecteerden, wat de haalbaarheid van de synchrone-naar-asynchrone vertaling aantoont.

5. Betekenis en Claims

Het artikel claimt betekenis op de volgende gebieden:

Sociale Abstractie: Langshaw dwingt ontwerpers om na te denken over coördinatie in sociale termen (autoriteit, conflict, betekenis) in plaats van laag-niveau berichtvolgorde. Dit sluit aan bij de "zeggen maakt dat het zo is"-doctrine, waardoor protocollen intuïtiever zijn voor belanghebbenden.
Flexibiliteit vs. Correctheid: Door sayso te gebruiken om conflicten sociaal op te lossen in plaats van via willekeurige infrastructurele synchronisatoren, ondersteunt Langshaw maximale concurrentie terwijl de protocolcorrectheid behouden blijft. Het stelt agenten in staat om gelijktijdig acties te proberen, waarbij het systeem conflicten oplost op basis van verklaarde prioriteiten.
Het Overbruggen van de Kloof: Het werk demonstreert dat een synchrone semantiek een levensvatbaar pad kan vormen naar asynchrone uitvoering. Dit omzeilt de traditionele discussie tussen synchroniteit en asynchroniteit door te laten zien dat hoogwaardige synchrone specificaties rigoureus gecompileerd kunnen worden naar robuuste asynchrone implementaties.
Engineering Nut: De aanpak biedt een methode om geïmplementeerde MAS te realiseren door de intuïties van belanghebbenden vast te leggen en deze te vertalen naar uitvoerbare code (via BSPL), waarmee de kloof tussen semi-formele notaties (zoals AUML) en engineeringdoelen wordt overbrugd.

De auteurs concluderen dat hoewel er native programmeermodellen voor Langshaw nodig zijn, de huidige beste aanpak is om een Langshaw-protocol te verifiëren, het te compileren naar BSPL, en het uit te voeren met bestaande BSPL-programmeermodellen (bijv. Kiko).