Övning 2: Förklara skillnaden mellan F G φ och G F φ

F G φ: Det finns en tidpunkt från vilken φ alltid gäller Exempel: 'Maskinen kommer att stängas av permanent' G F φ: För varje tidpunkt kommer φ att gälla igen senare Exempel: 'Maskinen kommer återkommande att vara ansluten' F G φ ⇒ G F φ men inte tvärtom Svar: F G φ: 'φ kommer så småningom att gälla för alltid'. G F φ: 'φ kommer återkommande att gälla'

Avancerad

Temporallogik

Logik för resonemang om tid, LTL och CTL.

temporallogik LTL CTL tid tillstånd väg

Tänk dig att du tittar på en film - varje bild visar ett ögonblick i tiden, men berättelsen uppstår genom sekvensen av bilder och hur de relaterar till varandra. Temporallogik handlar om att resonera om sådana förändringar över tid. Istället för att bara säga 'lampan är tänd' kan vi säga 'lampan kommer att vara tänd', 'lampan var tänd tidigare' eller 'lampan kommer alltid att vara tänd från och med nu'. Detta gör temporallogik ovärderlig för att beskriva och verifiera system som förändras över tid.

Fördjupning

Temporallogik utökar klassisk logik med operatorer för att uttrycka temporala relationer. Linear Temporal Logic (LTL) betraktar tid som en linjär sekvens av tillstånd, medan Computation Tree Logic (CTL) modellerar förgrenade tidsstrukturer. Temporala operatorer inkluderar 'nästa' (X), 'tills' (U), 'alltid' (G) och 'någon gång' (F). Temporallogik används för att specificera och verifiera egenskaper hos reaktiva system, protokoll och parallella program.

Grundläggande temporala begrepp

Temporallogik lägger till tidsdimensionen till klassisk logik. Vi resonerar inte bara om vad som är sant nu, utan vad som var sant, kommer att vara sant, eller alltid/någon gång är sant.

Tidsstrukturer

Linjär tid: s₀ → s₁ → s₂ → s₃ → ... (en möjlig framtid)

Förgrenad tid: från s₀ kan vi nå s₁ eller s₁' (flera möjliga framtider)

Cyklisk tid: tillstånd kan återkomma (s₀ → s₁ → s₂ → s₀)

Diskret vs kontinuerlig tid: steg-för-steg vs flödande tid

Informella temporala påståenden

· 'Dörren är låst nu'

· 'Dörren kommer att låsas upp'

· 'Dörren kommer alltid att förbli låst'

· 'Dörren var öppen tidigare'

· 'Dörren kommer att öppnas och sedan stängas'

· 'Om alarmet går kommer säkerheten att komma'

Dessa uttrycker olika temporala relationer som vi vill formalisera.

Linear Temporal Logic (LTL)

LTL betraktar tid som en linjär, oändlig sekvens av tillstånd. Varje tillstånd har en unik efterföljare.

LTL-operatorer

X φ (neXt): φ är sant i nästa tillstånd

F φ (Finally): φ kommer att vara sant någon gång i framtiden

G φ (Globally): φ kommer alltid att vara sant från nu och framåt

φ U ψ (Until): φ är sant tills ψ blir sant (och ψ blir sant)

W φ (weak until): som U men ψ behöver inte bli sant

LTL-exempel med trafikljus

Låt R = 'rött ljus', G = 'grönt ljus', Y = 'gult ljus'

· G(R → X(R ∨ G)): 'Efter rött kommer rött eller grönt'

· G(G → F Y): 'Efter grönt kommer gult så småningom'

· G(¬(R ∧ G)): 'Rött och grönt är aldrig på samtidigt'

· F G stopped: 'Systemet kommer så småningom att stoppas permanent'

· G F working: 'Systemet kommer alltid att fungera igen'

Visuell representation av LTL-operatorer på tidslinje

Computation Tree Logic (CTL)

CTL modellerar förgrenade tidsstrukturer där varje tillstånd kan ha flera möjliga framtider.

CTL-kvantifikatorer och operatorer

A φ (All paths): φ gäller för alla möjliga framtider

E φ (Exists path): φ gäller för åtminstone en möjlig framtid

Kombinerat med temporala operatorer:

AX φ: φ gäller i alla nästa tillstånd

EF φ: det finns en väg där φ så småningom gäller

CTL vs LTL - skillnader

CTL-formel: AG EF restart

'På alla vägar gäller att det alltid finns möjlighet att starta om'

LTL-ekvivalent: G F restart

'Det kommer alltid att finnas en restart i framtiden'

Skillnad: CTL talar om möjlighet (det finns en väg), LTL om nödvändighet (det kommer att hända).

Förgrenad tidsstruktur som visar CTL-semantik

Temporala semantiker och modeller

Temporala formler utvärderas över tidsstrukturer - matematiska modeller av hur tid och förändringar fungerar.

Kripke-strukturer för temporallogik

K = (S, R, L) där:

S = mängd av tillstånd (ögonblick i tid)

R ⊆ S × S = övergångsrelation (möjliga nästa tillstånd)

L: S → 2^AP = märkningsfunktion (vilka propositioner som gäller)

En stig π = s₀, s₁, s₂, ... genom strukturen

Semantik för LTL

Låt π = s₀, s₁, s₂, ... vara en stig och πⁱ = sᵢ, sᵢ₊₁, ...

· π ⊨ p iff p ∈ L(s₀)

· π ⊨ X φ iff π¹ ⊨ φ

· π ⊨ F φ iff ∃i ≥ 0: πⁱ ⊨ φ

· π ⊨ G φ iff ∀i ≥ 0: πⁱ ⊨ φ

· π ⊨ φ U ψ iff ∃i ≥ 0: πⁱ ⊨ ψ och ∀j < i: πʲ ⊨ φ

Specifikation av system

Temporallogik används för att specificera önskade egenskaper hos system som förändras över tid.

Säkerhetegenskaper (Safety)

Säkerhetsegenskaper säger att 'något dåligt aldrig händer':

· G ¬(critical₁ ∧ critical₂): 'Två processer är aldrig i kritiska sektionen samtidigt'

· G (request → ¬grant U authorize): 'Ingen tillgång beviljas innan auktorisering'

· G (temp > 100 → alarm): 'Alarm aktiveras alltid när temperaturen är för hög'

Livegenskaper (Liveness)

Liveegenskaper säger att 'något bra kommer att hända':

· G (request → F grant): 'Varje förfrågan kommer så småningom att beviljas'

· G F connected: 'Systemet kommer återkommande att ansluta'

· G (start → F finish): 'Varje startad process kommer att avslutas'

Exempel på safety- och liveness-egenskaper

Model checking och verifiering

Model checking är den automatiserade processen att verifiera om ett system uppfyller temporala specifikationer.

Model checking-algoritm

1. Modellera systemet som en Kripke-struktur

2. Uttryck önskade egenskaper som temporala formler

3. Kör model checking-algoritm

4. Om egenskapen inte gäller, få en motexempel-stig

5. Analysera motexemplet för att förstå problemet

Bounded model checking

Idé: Begränsa sökningen till stigar av längd k

· Översätt temporal formel till boolesk formel

· Använd SAT-solver för att hitta motexempel

· Om inget motexempel hittas för k, öka k

· Effektivt för att hitta buggar i början av exekvering

Vanliga misstag

❌ Förväxla 'någon gång' och 'alltid'

F φ betyder 'φ kommer att vara sant någon gång', G φ betyder 'φ kommer alltid att vara sant'

Exempel: G safe ≠ F safe. Det första betyder 'alltid säker', det andra 'säker någon gång'

❌ Glömma tillståndets varaktighet

I diskret temporallogik varar varje tillstånd exakt ett tidssteg

Exempel: X X φ betyder 'φ gäller två steg framåt', inte 'nästa gång φ kommer att vara möjligt'

❌ Förväxla CTL och LTL semantik

CTL kvantifierar över vägar (A/E) medan LTL har implicit universell kvantifiering

Exempel: AG φ (CTL) vs G φ (LTL) - båda betyder 'alltid φ' men över olika strukturer

Tillämpningar

Reaktiva system

System som kontinuerligt interagerar med sin miljö

Exempel: Operativsystem, webbservrar, inbyggda system i bilar och flygplan

Protokollverifiering

Säkerställa att kommunikationsprotokoll fungerar korrekt

Exempel: TCP/IP, säkerhetsprotokoll, distribuerade algoritmer

Hårdvaruverifiering

Verifiera att processorer och kretsar beter sig korrekt

Exempel: Cache-koherens, pipeline-korrekthet, minnesmodeller

Biologiska system

Modellera biologiska processer som utvecklas över tid

Exempel: Genreglering, celldifferentiering, ekosystemdynamik

Övningar

1 Lätt

Uttryck 'lampan blinkar' i LTL (lampan växlar mellan på och av)

Tips

Använd G och X operatorer för att uttrycka att lampan alltid växlar tillstånd

Visa facit

Om lampan är på nu, är den av nästa steg: G(on → X ¬on)
Om lampan är av nu, är den på nästa steg: G(¬on → X on)
Båda villkoren måste gälla: konjunktion med ∧
Detta säkerställer att lampan alternerar mellan på och av

Svar: G(on → X ¬on) ∧ G(¬on → X on)

2 Medel

Förklara skillnaden mellan F G φ och G F φ

Tips

Tänk på när φ börjar gälla permanent vs när φ gäller återkommande

Visa facit

F G φ: Det finns en tidpunkt från vilken φ alltid gäller
Exempel: 'Maskinen kommer att stängas av permanent'
G F φ: För varje tidpunkt kommer φ att gälla igen senare
Exempel: 'Maskinen kommer återkommande att vara ansluten'
F G φ ⇒ G F φ men inte tvärtom

Svar: F G φ: 'φ kommer så småningom att gälla för alltid'. G F φ: 'φ kommer återkommande att gälla'

3 Svår

Modellera en enkel trafikljus och verifiera att 'gult ljus alltid följs av rött'

Tips

Skapa en Kripke-struktur med tillstånd för varje ljuskombination

Visa facit

Tillstånd: S = {s_r, s_g, s_y} för rött, grönt, gult
Övergångar: R = {(s_r,s_g), (s_g,s_y), (s_y,s_r)}
Märkning: L(s_r) = {red}, L(s_g) = {green}, L(s_y) = {yellow}
Formel att verifiera: G(yellow → X red)
Verifiering: I s_y gäller yellow, och s_y → s_r, så X red gäller ✓

Svar: Kripke-struktur med cykliska övergångar: Red → Green → Yellow → Red

Sammanfattning

Temporallogik utökar klassisk logik med operatorer för att resonera om förändring över tid. Linear Temporal Logic (LTL) använder linjära tidssekvenser med operatorer som X (nästa), F (så småningom), G (alltid) och U (tills). Computation Tree Logic (CTL) hanterar förgrenade tidsstrukturer med vägkvantifikatorer A (alla vägar) och E (någon väg). Temporallogik är avgörande för att specificera säkerhet- och liveegenskaper hos reaktiva system och används inom model checking för automatisk verifiering av system som förändras över tid.