Kripke struktur (modellkontroll)
- Den här artikeln beskriver Kripke-strukturer som används vid modellkontroll. För en mer allmän beskrivning, se Kripke semantik .
En Kripke-struktur är en variant av övergångssystemet , ursprungligen föreslagit av Saul Kripke , som används i modellkontroll för att representera ett systems beteende. Den består av en graf vars noder representerar de nåbara tillstånden i systemet och vars kanter representerar tillståndsövergångar, tillsammans med en märkningsfunktion som mappar varje nod till en uppsättning egenskaper som håller i motsvarande tillstånd. Temporala logiker tolkas traditionellt i termer av Kripke-strukturer. [ citat behövs ]
Formell definition
Låt AP vara en uppsättning atomära propositioner , dvs booleska uttryck över variabler, konstanter och predikatsymboler. Clarke et al. definiera en Kripke-struktur över AP som en 4-tuppel M = ( S , I , R , L ) bestående av
- en ändlig uppsättning tillstånd S .
- en uppsättning initialtillstånd I ⊆ S .
- en övergångsrelation R ⊆ S × S så att R är vänstertotal , dvs ∀s ∈ S ∃s' ∈ S så att (s,s') ∈ R .
- en märkning (eller tolkning ) funktion L : S → 2AP .
Eftersom R är left-total är det alltid möjligt att konstruera en oändlig väg genom Kripke-strukturen. Ett dödläge kan modelleras av en enda utgående kant tillbaka till sig själv. Märkningsfunktionen L definierar för varje tillstånd s ∈ S mängden L ( s ) för alla atomära propositioner som är giltiga i s .
En väg av strukturen M är en sekvens av tillstånd ρ = si , , s3 , ... så s2 R (si , si +1 ) att för varje i > 0 gäller . Ordet på banan ρ är en sekvens av uppsättningar av atomsatserna w = L (s 1 ), L (s 2 ), L (s 3 ), ... , som är ett ω-ord över alfabetet 2 AP .
Med denna definition kan en Kripke-struktur (säg, med endast ett initialtillstånd i ∈ I ) identifieras med en Moore-maskin med ett enkeltons inmatningsalfabet, och med utgångsfunktionen som dess märkningsfunktion.
Exempel
Låt mängden atomära propositioner AP = {p, q} . p och q kan modellera godtyckliga booleska egenskaper hos systemet som Kripke-strukturen modellerar.
Figuren till höger illustrerar en Kripke-struktur M = ( S , I , R , L ) , där
- S = {s 1 , s 2 , s 3 } .
- I = {s 1 } .
- R = {(si , s2 ) , (s2 , s1 ) (s2 , s3 ) , (s3 , s3 ) } .
- L = {(s 1 , {p, q}), (s 2 , {q}), (s 3 , {p})} .
M kan producera en väg ρ = s 1 , s 2 , s 1 , s 2 , s 3 , s 3 , s 3 , ... och w = {p, q}, {q}, {p, q}, {q}, {p}, {p}, {p}, ... är exekveringsordet över vägen ρ . M kan producera exekveringsord som hör till språket ({p, q}{q})*({p}) ω ∪ ({p, q}{q}) ω .
Relation till andra föreställningar
Även om denna terminologi är utbredd i modellkontrollsamhället, definierar vissa läroböcker om modellkontroll inte "Kripke-struktur" på detta utökade sätt (eller överhuvudtaget faktiskt), utan använder helt enkelt konceptet med ett (märkt) övergångssystem , som dessutom har en uppsättning Act of actions, och övergångsrelationen definieras som en delmängd av S × Act × S , som de dessutom utökar till att även omfatta en uppsättning atomära propositioner och en märkningsfunktion för tillstånden ( L enligt definitionen ovan.) I detta tillvägagångssätt kallas den binära relationen som erhålls genom att abstrahera bort åtgärdsetiketterna en tillståndsgraf .
Clarke et al. omdefiniera en Kripke-struktur som en uppsättning övergångar (istället för bara en), vilket är ekvivalent med de märkta övergångarna ovan, när de definierar semantiken för modal μ-kalkyl .