I detta dokument utsträcks korrespondensen mellan säkra Petrinät och händelsestrukturer, på grund av Nielsen, Plotkin och Winskel, till godtyckliga nät utan självslingor, under den kollektiva symboliska tolkningen. I detta syfte föreslår vi en mer allmän form av händelsestruktur som motsvarar den uttryckskraft som sådana nät har. Dessa nya händelsestrukturer och nät knyts samman genom att de båda begreppen relateras till konfigurationsstrukturer, som kan betraktas som representationer av antingen händelsestrukturer eller nät som fångar deras beteende när det gäller handlingshändelser och orsakssambandet mellan dem, men som är abstrakta från alla hjälpstrukturer. En konfigurationsstruktur kan också betraktas logiskt, som en klass av propositionsmodeller, eller likvärdigt som en propositionsteori i disjunktiv normal från. Att omvandla denna teori till konjunktiv normal form är nyckeltanken i översättningen av en sådan struktur till ett nät. För en mängd olika klasser av händelsestrukturer karakteriserar vi de tillhörande klasserna av konfigurationsstrukturer i termer av deras stängningsegenskaper, liksom i termer av axiomatisability av de tillhörande propositionsteorierna genom formler av enkla föreskrivna former, och i termer av strukturella egenskaper hos de associerade Petri-näten. Syftet med detta dokument är att koppla samman flera modeller av samstämmighet genom att tillhandahålla beteenden som bevarar översättningar mellan dem. I detta dokument generaliseras överensstämmelsen mellan säkra Petrinät och konfigurationsstrukturer till (eventuellt osäkra) nät utan självslingor (de rena näten). För detta ändamål använder vi 1 en mer allmän typ av konfigurationsstruktur än i [11], de inställda systemen. Dessa har en attraktiv alternativ presentation som förslagsteorier [29], som utnyttjas i sin översättning till nät. Vi generaliserar också händelsestrukturerna i [34], så att, återigen, våra konfigurationsstrukturer uppstår som deras familjer av konfigurationer. Kopplingen mellan konfigurationsstrukturer och Scott-domäner är allmän i Van Glabbeek [8], som föreslår övergångssystem som alternativa presentationer av domäner; vi överväger inte dessa frågor vidare i detta dokument. Förhållandet mellan konfigurationsstrukturer, infinita propositionsteorier, händelsestrukturer och Petrinät beskrivs i Avsnitt 1. Vi en-unfold rena nät i rena 1-occurence nät, som generaliserar förekomsten nät av [25], och hävdar att denna 1-unfolding bevarar orsakssambandet och förgrening tid beteendet hos det representerade systemet. Detta gör det möjligt för oss att begränsa uppmärksamheten till rena 1-nät i resten av pappret. Dessutom ger vi översättningar som visar att konfigurationsstrukturer, propositionsteorier och händelsestrukturer är likvärdiga upp till så kallad konfigurationslikvärdighet (som definieras som kartlagt till samma konfigurationsstrukturer) och att alla fyra modellerna, med en liten begränsning, är likvärdiga upp till finansiell ekvivalens. I avsnitt 2 införs en beräkningsmässig tolkning av konfigurationsstrukturer, Petrinät och händelsestrukturer i form av tillhörande övergångsförhållanden; begränsad till rena Petrinät och rena händelsestrukturer kan dessa övergångsförhållanden härledas från relevanta konfigurationer, men inte i allmänhet. I avsnitt 3 ges definitioner av begreppen uppnåeliga och säkra (uppnåeliga i gränsvärdet) konfigurationer och beaktas motsvarande begrepp om likvärdighet genom att begränsa till uppnåeliga eller säkra, och eventuellt finita, konfigurationer. Med den allmänna ram som därmed tillhandahålls, Avsnitt 4 tar hänsyn till de olika varumärken av evenemang strukturer som införts av Winskel och hans medarbetare. De visas motsvara naturliga begränsningar av det allmänna begreppet händelsestruktur, anpassa jämförelserna, å ena sidan, till det ursprungliga begreppet konfiguration och, å andra sidan, till det relevanta från den allmänna teorin. Dessa jämförelser sammanfattas i tabell 1. Det är då naturligt att fråga sig hur begränsningarna i händelsestrukturen återspeglas i motsvarande begränsningar av konfigurationsstrukturer och så vidare; detta är ämnet för avsnitt 5. Avsnitten 5.1 och 5.2 ger sådana jämförelser, som sammanfattas i tabell 2, för konfigurationsstrukturer och förslagsteorier upp till konfigurationslikvärdighet. Restriktioner för konfigurationsstrukturer är naturliga stängningsegenskaper, och de på propositionsteorier gäller formen av formler som förekommer i en axiomatisering. Avsnitt 5.3 gör samma sak, se tabell 3, men nu med jämförelsen baserad på säkra konfigurationer. Avsnitt 5.4 gäller det finansiella fallet, där allmänna jämförelser sammanfattas i tabell 4 och begränsningen till de finita tillgängliga konfigurationer som sammanfattas i tabell 5. Avsnitt 5.5 knyter samman Petri-näten och tillhandahåller motsvarande strukturellt definierade underklasser, men vi lyckades inte göra detta i alla fall. Det viktigaste matematiska arbetet görs i avsnitten 5.1 och 5.2, medan resten av avsnittet anpassar detta arbete till de olika aktuella fallen. Avsnitt 6 innehåller en diskussion om relaterat arbete och ger en del möjligheter till framtida forskning. Slutligen finns det ett index för de många tekniska termer som införs i dokumentet. Papperen [12] och [13] innehåller utdragna sammanfattningar av delar av detta arbete, tillsammans med ytterligare material. I detta avsnitt presenterar vi de fyra modeller av samstämmighet som nämns i inledningen, och ger översättningar mellan dem. Definition 1.1 Ett set system är ett par C = /\ E, C\ / med E en uppsättning och C P (E) en samling undergrupper. När ett set system används för att representera ett parallellt system, kallar vi det en ren konfigurationsstruktur, men i allmänhet släppa ordet "ren". (Vi ser fram emot att införa en bredare klass av konfigurationsstrukturer i framtiden, som motsvarar den uttrycksfulla kraften hos orena nät.) E-elementen kallas sedan händelser och elementen i C-konfigurationer. En händelse representerar en händelse som systemet kan utföra; en konfiguration x representerar ett tillstånd av systemet, nämligen det tillstånd i vilket händelserna i x har inträffat. En uppsättning system kan också betraktas ur en logisk synvinkel: E är tänkt som en samling av förslag och C som samling av modeller. När vi kopplar ihop oss med den beräkningsmässiga synvinkeln förknippar vi med en händelse med påståendet att det har hänt. Denna synpunkt beror på Pratt [18, 29]. Vi kan nu representera ett bestämt system genom de giltiga meningarna, de som håller i alla modeller; detta är lagarna i C. För att göra detta exakt, väljer vi ett språk: oändlig propositionslogik. Med tanke på en uppsättning E-variabler (propositionella) bildar formlerna över E den minsta klassen inklusive E och slutna under ¬ (negation) och (konjunktur av uppsättningar av formler). Vi gör fri användning av andra standard bindväv såsom  på,,  på: de är alla definierbara från ¬ och. Som vanligt är en tolkning av E bara en delmängd av E och man definierar på standardsättet när en tolkning gör en formel sann. / med E en uppsättning propositionsvariabler och T en klass av oändliga propositionella formler över E. iff är det sant i alla delar av C; teorin associerad till C är T (C) : där T (C) betecknar den klass av formler som gäller i C. Likaså, med tanke på en propositionsteori T = är uppsättningen av modeller av T, de tolkningar av E gör varje formel i T sant. Vi säger att T axiomatises M(T). En formel över E är en logisk konsekvens av en teori T om det är sant i någon modell av T; en formel över E innebär iff den senare är en logisk följd av teorin, som lätt ses som fallet iff de har samma logiska konsekvenser. Teorem 1 Låt C = / \ E, C \ / vara ett set system. Då T (C) axiomatises C, d.v.s., M(T (C)) = C. Bevis: Den enda formeln X på X (X) ¬ (E − X) utgör redan en axiomatisering av C. Det kallas disjunktiv normal form av T (C). 2 Således ger T och M en bijective korrespondens mellan set system och infinita propositionsteorier upp till logisk ekvivalens. För alla två undergrupper X, Y av E, låt klausulen X Y förkorta konsekvenserna X Y; vi säger att elementen i X är föregångare till klausulen, och de av Y dess konsekvenser. Sedan för varje set system C = /\ E, C\ /, uppsättningen av klausuler {X  till (E − X)  på X C} utgör en annan axiomatisering av C. En teori som består av en uppsättning klausuler sägs vara i konjunktiv normal form. Definition 1.3 En händelsestruktur är ett par E = /\ E,  till\ / med • E en uppsättning händelser, •  till P(E) × P(E), den möjliggörande relationen. Likt en konfigurationsstruktur beskriver en händelsestruktur ett parallellt system där händelserna representerar händelser. I tidigare begrepp av händelsestruktur [34, 35], hade man bara singleton möjliggör:  på P(E) × E. Här generaliserar vi  på en relation mellan uppsättningar av händelser. Precis som tidigare innebär den möjliggörande relationen vissa begränsningar för vilka händelser som kan inträffa när. Tanken här är att när X är den uppsättning av händelser som hänt hittills, en ytterligare uppsättning U händelser kan hända (samtidigt) iff varje delmängd av X  på U aktiveras av en uppsättning händelser som hände tidigare, dvs. en delmängd av X. Exempel 1 Låt E = {d, e, f } och den aktiverande relationen ges av ∅  till X för alla X med X = E. I det ursprungliga tillståndet av händelsen struktur E = /\ E,  på\ /, var och en av händelserna d, e och f kan hända, och två av dem kan hända samtidigt. Men det finns inte en chans att alla tre händelser någonsin kan hända, eftersom det inte finns några uppsättningar av händelser X med X  till {d, e, f}. Detta är ett fall av ternära konflikter. Exempel 2 Låt E = {a, b, c} och den aktiverande relationen ges av {c} {a, b} och ∅  på X för alla X  till E med X = {a, b}. Inledningsvis kan var och en av händelserna a, b och c inträffa, och händelserna a och c kan även ske samtidigt. Händelserna a och b, å andra sidan, kan initialt inte ske samtidigt, eftersom vi inte har ∅  på {a, b}. Så snart som c inträffar kan dock händelserna a och b inträffa parallellt. Vi säger att konflikten mellan a och b löses genom förekomsten av c. Exempel 3 Låt E = {d, e} och den aktiverande relationen ges av {d} (d, e} och ∅ (X) för alla X  på E med X = {d, e}. Inledningsvis kan både d och e inträffa, men inte parallellt. Efter d har hänt, e kan följa, men när e händer först, d inte följa. Anledningen till detta är att vi inte har X-värde {d, e, } för vissa X-värde {e}. Detta är ett fall av asymmetrisk konflikt [22, 26]. I avsnitt 4 kommer vi att förklara hur dessa händelsestrukturer generaliserar de [25, 34, 35]. I dessa dokument formaliseras beteendet hos en händelsestruktur genom att en familj av konfigurationer associeras till den. Det finns dock flera sätt att göra det (jfr. Avsnitt 3); här betraktar vi bara den enklaste varianten. I avsnitt 2 ger vi en beräkningstolkning av händelsestrukturer med egenskapen att de vänstra slutna konfigurationerna av en händelsestruktur på ett tillfredsställande sätt representerar beteendet hos det representerade systemet för följande klass av "ren" händelsestrukturer: Definition 1.5 En händelsestruktur är ren om X  och Y endast om X  och Y = ∅.
Det skulle också vara intressant att studera vilken typ av konfigurationsstrukturer REF som naturligt kan inkludera vår definition av tillåten konfiguration.
Configuration Structures, Event Structures and Petri Nets
{'venue': 'Theoretical Computer Science 410(41), 2009, pp. 4111-4159', 'journal': None, 'mag_field_of_study': ['Mathematics', 'Computer Science']}