Temporális logikák és modell ellenırzés
Temporális logikák • Modális logika: kijelentések különböző „módjainak” tanulmányozására vezették be (eredetileg filozófusok). Ilyen módok: „esetleg”, „mindig”, „szükségszerűen”, „valamikor biztosan” • Temporális logikák: a modális logikák egy formális rendszerét képezik arra, hogy kijelentések igazságának időbeli (sorrendiségi) változását vizsgálhassuk. • Erre a célra temporális operátorok állnak rendelkezésünkre (pl. „mindig P” – akkor igaz, ha a P kijelentés minden jövőbeli pillanatban igaz, „valamikor Q” – akkor igaz, ha van olyan jövőbeli pillanat, amikor Q igaz. • Az időbeliség logikai időre, az időpillanatok sorrendiségére vonatkozik (a valós idő múlását az operátorok nem kezelik)
Temporális logikák • Elsősorban folyamatosan működő rendszerek (pl. operációs rendszerek, beágyazott rendszerek stb.) tulajdonságainak leírására használjuk. Ezekben a rendszerekben a bemenetek és kimenetek kapcsolata nem adható meg transzformációként, a helyesség nem fogalmazható meg a kezdeti és végállapotokra vonatkozó elő- és utófeltételek formájában (pl. nem értelmezhető a végállapot) • A tulajdonságok egy része lokális, tehát egy-egy aktuális időpillanathoz köthető, más részük elérhetőségi, azaz a működés során jövőbeli időpillanatokra vonatkozik. Utóbbiakat a biztonság illetve élőség kategóriákba soroljuk. • Biztonsági tulajdonságok: veszélyes, nemkívánatos helyzetek elkerülését fogalmazzák meg, univerzális kvantorokat alkalmaznak az időpillanatokra („minden pillanatban igaz, hogy a rendszer biztonságos állapotban van”). Induktív módszerekkel bizonyíthatóak. Pl. egy többprocesszes rendszer esetében ilyenek: holtpontmentesség (minden időpillanatban van egy futásra kész processz), kölcsönös kizárás (soha nincs két processz egyszerre kritikus szakaszban), adatbiztonság (soha nincs jogosulatlan hozzáférés)
Temporális logikák • Az élő jellegű tulajdonságok bizonyos kívánatos helyzetek elérését írják elő (pl. kérésre válasz érkezik, eredmény előáll stb.). Ezeket az időpillanatokon alkalmazott egzisztenciális kvantorokkal lehet megfogalmazni. Nehézség, hogy induktív módon nem levezethetőek. Általában azt kell megmutatni, hogy a rendszer mindig „közelebb kerül” a kívánatos helyzethez. Például: • Elküldött üzenet megérkezik (ha egy üzenetküldés történt, akkor valamikor bekövetkezik az az időpillanat, amikor az üzenet megérkezik) • Kérés kiszolgálása megtörténik • Nincs kiéheztetés (minden processz előbb-utóbb futhat, létezik olyan jövőbeli időpillanat amikor a processz futó állapotba kerül) • Terminálás: a program előbb-utóbb eléri végállapotát
• Egyes tulajdonságok (pl. egy adott helyzet végtelenül sokszor fennáll) nem sorolhatóak ezekbe a kategóriákba
Temporális logikák osztályozása • Kijelentés- illetve elsőrendű logikák: a temporális kijelentéslogikák a temporális operátok mellett a klasszikus kijelentéslogika eszköztárát használják, hasonlóan az elsőrendű temporális logikák a temporális operátorok mellett alkalmazzák az elsőrendű logikák eszköztárát • Pont- illetve intervallumlogikák: a pont logikák jellemzője, hogy a temporális operátorokat egy-egy időpillanatban értékeljük ki, míg az intervallumlogikák esetében időintervallumokra definiáljuk és értékeljük ki őket • Diszkrét- illetve folytonos idejű logikák: a legtöbb esetben (pl. programok vagy állapotgépek vizsgálata) elégséges az idő diszkrét kezelése (egymás utáni időpillanatokat feleltetünk meg a természetes számok sorozatának), de hibrid (pl. analóg elemeket is tartalmazó) valósidejű rendszerek esetében szükséges lehet a folytonos idő kezelése)
Temporális logikák osztályozása • Lineáris- illetve elágazó idejű logikák: az első esetben az egymás utáni időpillanatokat mint lineáris rendszert kezeljük: minden időpillanatnak csak egy-egy rákövetkező időpillanata értelmezett (egyféle jövőt veszünk figyelembe). A második esetben az egymás utáni időpillanatok egy elágazó fastruktúrát alkotnak, minden pillanatnak több rákövetkezője értelmezett (többféle lehetséges jövő) • Lineáris idejű temporális logika (LTL – Linear Time Temporal Logic): az időpillanatok egy idővonal mentén követik egymást, erre az idővonalra vonatkoztatjuk a temporális operátorokat • Elágazó idejű temporális logikák (BTL – Branching Time Temporal Logic): az időpillanatok fa struktúrában elágazó idővonalak mentén követik egymást, az operátok az elágazásokra is vonatkoznak, nemcsak a vonalakra (pl. kifejezhető: valami minden elágazásra igaz, valami legalább egy idővonalra igaz) • Múlt illetve jövő kezelése: általában a jövőre vonatkoznak, de néhány tulajdonság leírásának megkönnyítése érdekében a múltra is vonatkozhatnak
Temporális logikák modelljei • Esetünkben a temporális logikák által leírt tulajdonságokat (pl. „az útkereszteződésben a lámpa valamikor zöld lesz”) diszkrét állapotokkal és akciókkal (műveletekkel) rendelkező rendszereken (pl. számítógépes programok, állapotgépek – pl. a közlekedési lámpa vezérlője) szeretnénk ellenőrizni • A jelen időpillanat az aktuális állapotot vagy akciót, a jövő időpillanatok pedig rákövetkező állapotokat vagy akciókat jelölnek, tehát az egymás utáni időpillanatok az állapotok vagy akciók egymásutániságának (szekvenciájának) felelnek meg. • A temporális logikák modelljeiként matematikailag jól kezelhető struktúrákat és formalizmusokat alkalmazunk, és módszereket amelyek lehetővé teszik a temporális logikai kijelentések igazságának ellenőrzését. A modellek általában származtathatóak a tervezéshez közelebb álló félformális modellekből (állapottérképek, adatfolyam gráfok)
Temporális logikák modelljei Kripke struktúrák: • Legyen AP atomi kijelentések véges halmaza (az alkalmazásban tovább nem bontható kijelentések, pl. „a lámpa piros”, „x>25”, „a processz kritikus szakaszban van” stb. A kijelentéseket P, Q,… nagybetűkkel jelöljük
• Egy adott AP mellett a Kripke-struktúra a következő hármas: M=(S, R, L), ahol • S az állapotok véges halmaza • R⊆S×S állapotátmeneti reláció • L:S→2AP az állapotok címkézése atomi kijelentésekkel. Egy állapotot több kijelentés is címkézhet. Minden s állapotra true∈L(s) és false∉L(s) • Kripke struktúrát alkalmazunk, ha rendszerünk működését legjobban állapotok segítségével tudjuk leírni, az állapotokat lokálisan az adott állapotra igaz kijelentésekkel tudjuk jellemezni. A temporális logika segítségével leírt tulajdonságokat az egyes állapotokra érvényes lokális kijelentések alapján értékeljük ki.
Temporális logikák modelljei Kripke struktúrák példa:
• Jelzőlámpa: • AP = {zöld, sárga, piros, villogó sárga} {zöld}
{sárga}
{piros}
{piros, sárga}
s1
s2
s3
s4
s5 {villogó_sárga}
Temporális logikák modelljei Cimkézett állapotátmeneti (tranzíciós) rendszerek (LTS – Labeled Transition systems):
• Az állapotátmenetekhez akciókat rendelünk, melyek tovább nem bonthatóak, és általában egy-egy alkalmazás-specifikus műveletet (üzenetet, a környezettel való kölcsönhatást) jelentenek, kisbetűkkel jelöljük őket (a,b,c) • Egy LTS a T=(S, Act, →) hármas, ahol: • S az állapotok véges halmaza • Act=(a,b,c,…) az akciók véges halmaza • → ⊆S×Act× S címkézet állapot-átmeneti reláció. Egy állapotátmenetet egy akció címkézhet •
LTS modelleket használunk, ha rendszerünket leginkább az állapotátmenetek során bekövetkezett akciók sorozatával tudjuk leírni (az egyes állapotokat kevésbé tudjuk lokálisan jellemezni). Pl. kommunikációs (üzenetet küldő/fogadó) rendszerek. A temporális logikák segítségével leírt tulajdonságok igazságát a lehetséges akciósorozatok alapján értékeljük ki
Temporális logikák modelljei LTS példa:
• Italautomata: pénz
tea
kávé
Temporális logikák modelljei Kripke állapot-átmeneti rendszerek (KTS - Kripke Transition Systems): • Az állapotokat kijelentésekkel, az átmeneteket akciókkal címkézzük. Adott AP és Act mellett tehát a KTS a K=(S,→,L) hármas. • KTL modelleket használunk programok esetén az utasítások (akciók) és változók (állapotokhoz rendelt kijelentések) egyidejű megadására. • Példa:
{true} z:=0; i:=0; while (i!=y) do z:=z+x; i:=i+1; end
z:=0
i:=0 i:=i+1
{z=i*x}
[i!=y]
[i=y]
z:=z+x {i!=y, z=i*x}
{z=y*x}
Temporális logikák modelljei Automaták véges szavakon: • Véges hosszúságú szavakon értelmezhetjük az A=(Σ, S, S0, ρ, F) automatát, ahol: • Σ - az ábécé (a betűk nem üres halmaza) • S az állapotok véges, nem üres halmaza • S0⊆S a kezdőállapotok halmaza • ρ: S× Σ → 2S az állapot-átmeneti reláció (egy beérkező betű hatására új állapotba lép az automata) • F az elfogadó állapotok halmaza • Egy ω = (a0,…,an-1) szót elfogad az automata, ha létezik rá elfogadó futás. Az automata által elfogadott nyelv: L(A)={ω ∈Σ | ω elfogadott} • Ilyen automatákat használhatunk pl. véges hosszúságú bemenetek feldolgozásának leírására. A temporális logika segítségével leírt tulajdonságokat az elfogadott nyelv alapján értékeljük ki.
Temporális logikák modelljei Büchi automaták: • Végtelen hosszúságú szavakon értelmezzük, így módosítanunk kell az elfogadás kritériumát, mivel nincsen végállapot • Az A automata futása egy beérkező a0,a1… végtelen betűsorozat (szó) hatására az r=(s0,s1,…) állapotsorozat, ahol s0∈S0 és 0≤ i –re si+1=ρ(si,ai). • A végtelen futás jellemzője azon s∈S állapotok halmaza, amelyeket a futás végtelenül sokszor érint: lim(r) = {s|s=si végtelenül sokszor} • Egy futást elfogadónak nevezünk, ha lim(r) ∩ F ≠ ∅. Egy ω végtelenül hosszú szót elfogad az automata, ha létezik rá elfogadó futás. A Büchi automata által elfogadott nyelv: L(A)={ω ∈ Σ∞ | ω elfogadott} • A temporális logika által leírt tulajdonságokat az elfogadott nyelv alapján értékeljük ki.
