Temporális logika

Ez az oldal a korábbi SCH wiki-ről lett áthozva. Az eredeti változata itt érhető el.

Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor kérlek javíts rajta egy rövid szerkesztéssel.

Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót

%TOC{depth="3"}%

Elmélet

LTL

PLTL (Propositional Linear Time Temporal Logic)

• Atomi kijelentések (AP elemei)
• Boole logikai operátorok: & (ÉS), V (VAGY), ¬ (NEGÁLÁS)

// ∧ (fejletöre állitott V) helyett & és ∨ helyett V mert ie alatt nem látszanak. -- GeGe997 - 2006.06.14.

• Temporális operátorok:
  • F p: ( *F* uture) "Valamikor p", egy elérhető állapotban igaz lesz p
  • G p: ( *G* lobally)"Mindig p", minden elérhető állapotban igaz lesz p
  • X p: (ne *X* time)"Következő p", a következő állapotban igaz lesz p
  • p U q: ( *U* ntil)"p amíg q", egy elérhető állapotban igaz lesz q, és addig minden állapotban igaz p ("strong until")

Az érvényes PLTL kifejezések halmaza a következő szabályokkal képezhető: (formális szintaxis)

• L1: Minden P atomi kijelentés egy kifejezés.
• L2: Ha p és q egy-egy kifejezés, akkor p&q illetve ¬p is
• L3: Ha p és q egy-egy kifejezés, akkor p U q illetve X p is

Ezekből származtathatók:

• p V q jelentése ¬((¬ p)&(¬q))
• p => q jelentése (¬p) V q
• p ≡ q jelentése (p=>q)&(q=>p)
• true jelentése pV(¬p) (minden állapotra igaz),
• false jelentése p&(¬p) (egy állapotra sem igaz)
• F p jelentése true U p
• G p jelentése ¬F(¬p)
• pRq jelentése ¬(¬pU¬q)
• pBq jelentése ¬(¬pUq) & Fq

A szintaxis szabályok alapján képzett kifejezésekhez megadható a formális szemantika: Egy p kifejezést az M=(S,R,L) Kripke-struktúra egy [math] \pi =(s_{0}, s_{1} ,s_{2} ,s_{3} ,... ) [/math] útvonalán értelmezzük, ahol az [math] s_{0} [/math] a kezdőállapot és [math] (s_{i} ,s_{i+1}) \in R [/math].

• M, pi |= p jelentése: az M struktúrában a pi útvonlara p igaz.
• A #pi;^i jelölése a pi útvonal i-edik elemétől kezdődő része.

Ekkor a három szabály:

• L1: M,π |= P a.cs.a. P∈L(s0)
• L2: M,π |= p&q a.cs.a. M,π ||= p és M,π ||= q
  M,π ||= ¬q a.cs.a. M,π = q nem igaz.
• L3: M,π |= (p U q) a.cs.a. Létezik j (pi^j ||= q és bármely k<j => pi^k ||=p)
  M,π ||= X p a.cs.a. π^1 = p

LTS

(Labeled Transition System) az állapotátmenetek címkézhetők egy-egy ún. akcióval, egy átmeneten csak egy akció szerepelhet:

(S, Act , --> ) , ahol

• S= {s1 ,s2 ,...sn} állapotok halmaza
• Act= {a,b,c,...} akciók (címkék) halmaza
• S Act címkézett állapotátmenetek.
• --> része SxActxS

Állapotátmenetek szokásos jelölése: s_{i}-->s_{j}

CTL

(Computational Tree Logic) Egy-egy állapotban megvizsgálható, hogy az útvonalakra vonatkozó követelmény hány onnan kiinduló útvonal mentén teljesülhet. Állapotokra vonatkozó operátorokat mindig közvetlenül meg kell előznie útvonal kvantoroknak. Állapotokra vonatkozó operátorok nem kombinálhatók.

• E p (Exists p): Létezik legalább egy útvonal, ahol a p követelmény teljesül
• A p (forAll p): Minden útvonalra fennáll, hogy a p követelmény teljesül

Állapotokon értelmezhető összetett operátorok:

• EX p: létezik útvonal, aminek következő állapotán p
• EF p: létezik útvonal, aminek egy állapotán p
• EG p: létezik útvonal, aminek minden állapotán p
• E(p U q): létezik útvonal, amin p amíg q
• AX p: minden útvonal következő állapotán p
• AF p: minden útvonal egy-egy elérhető állapotán p
• AG p: minden útvonal minden állapotán p
• A(p U q): minden útvonalon p amíg q

formális szitaxis

• Állapot-kifejezések:
  • S1, S2, S3 szabályok (lásd CTL*) változatlanok.
• Útvonal-kifejezések:
  • P1, P2, P3 helyébe egy új P0 szabály lép:
  • P0: Ha p és q állapot-kifejezések, akkor X p és p U q útvonal-kifejezések.

Következmények:

• Útvonal-kifejezések nem kombinálhatók
• Az S3 szabály miatt X p és p U q útvonal-kifejezések elé rögtön egy útvonal kvantor kerül → összenőtt operátorok.

CTL*

• Útvonal kvantorok (E, A),
• útvonalakon az állapotokra vonatkozó operátorok (F, G, X, U) tetszőleges kombinációja

Útvonalak kvantorai (állapotokon értelmezett):

• A: (for all futures), minden lehetséges útra az adott állapotból kiindulva
• E: (for some future), legalább egy útra az adott állapotból kiindulva

Állapotok operátorai (útvonalakon értelmezett):

• F p: (future), valamikor az útvonal egy állapotán
• G p: (always), az útvonal minden állapotán
• X p: (nexttime), a következő állapotban
• p U q: (p until q), az útvonal egy állapotán igaz lesz q, és addig minden állapotban igaz p

formális szitaxis

• Állapotokra vonatkozó kifejezések (állapot-kifejezések):
  • (S1) minden P atomi kijelentés egy állapot kifejezés;
  • (S2) ha p és q állapot-kifejezések, akkor p&q és ¬p is;
  • (S3) ha p egy útvonal-kifejezés, akkor Ep és Ap állapot-kifejezések.
• Útvonalra vonatkozó kifejezések (útvonal-kifejezések):
  • (P1) minden állapot-kifejezés egyben egy útvonal kifejezés is;
  • (P2) ha p és q útvonal-kifejezések, akkor p&q és ¬p is;
  • (P3) ha p és q útvonal-kifejezések, akkor Xp és pUq is.

Fair-CTL

lásd jegyzet.

HML

lásd jegyzet.

Kérdések

1.

Mi a Kripke-struktúra formális definíciója? (2p)
KS (S, R, L) hármassal definiáljuk az AP halmaz felett, ahol:

• AP= P,Q,R,... atomi kijelentések halmaza (domén-specifikus)
• S= s_{1} ,s_{2} ,s_{3} ,...s_{n} állapotok halmaza
• R része SxS: állapotátmeneti reláció
• L: S->2^{AP} állapotok címkézése atomi kijelentésekkel.

2.

Definiáld a Fp és pRq LTL logikai operátorokat az alapoperátorok felhasználásával!
Fp = ¬(G ( ¬p)) vagy Fp = true U p
pRq = ¬(¬p U ¬q)

3.

Formálisan definiálja a pUq LTL-kifejezés szemantikáját! (2p)
M,π |= (p U q) a.cs.a. Létezik j (pi^j ||= q és bármely k < j => pi^k =p)

L3 a formális szementikából. (tanszéki temporalis1.pdf 22.oldal)

4.

Definiálja formálisan a CTL kifejezések szintaxisát! (Avagy hogyan épülnek fel a jól formált CTL* logikai kifejezések?)
Def lásd az elméletnél.

5.

Definiáld az Ap CTL kifejezés szemantikáját!
M, s |= Ap a.cs.a. létezik egy pi =(s1,s2,s3,...) teljes útvonalra M-ben, ahol s=s0, fennáll az M , pi=p állítás.

6.

Definiáld formálisan az Ep (létezik útvonal, melyre p) CTL kifejezés szemantikáját!
M, s |= E p a.cs.a. létezik egy pi=(s1,s2,s3,...) teljes útvonal M-ben s=s0 mellett, hogy M, pi = p.

7.

írd fel EFp -t elemi szintre bontva
E(trueUp)

8.

írd fel AGp –t elemi szintre bontva
A(¬(F(¬p))

10.

Mit jelent az átlapolás (interleaving) és a szinkronizáció fogalma Kripke-struktúra esetén?
Átlapolás: a két folyamat közül pontosan az egyik lép
Szinkronizáció: a két folyamat egyszerre lép

11.

Hogyan definiálható a logikai függvények Shannon-felbontása?
Előadáson így írta fel P.A.:
[math] f(x_1, x_2, ... x_n) = x_i \cdot f(x_1, ... x_{i-1}, 1, x_{i+1}, ... x_n) \; \vee \; \neg x_i \cdot f(x_1, ... x_{i-1}, 0, x_{i+1}, ... x_n) [/math]
-- Csapszi - 2006.06.12.

Az andersen.ps-ben (10 of 37) oldalon:

 t= x -> t[1/x], t[0/x] -t nevezi a Shannon felbontásnak. <br/>

-- adamo - 2006.06.13.

Példák

Mintapélda

Két processzből álló rendszer: P1 és P2
Processz állapotok a követelmények szempontjából:

• Kritikus szakaszban van: C1, C2
• Nem-kritikus szakaszban van: N1, N2
• Kritikus szakaszba belépésre kész: W1, W2

Atomi kijelentések:
AP = {C1, C2, N1, N2, W1, W2}

• Egyszerre csak egy processz lehet a kritikus szakaszban:
  AG (¬(C1 & C2))
• Ha egy processz be akar lépni a kritikus szakaszba, akkor előbb-utóbb beléphet:
  AG (W1 ⇒ AF(C1))
  AG (W2 ⇒ AF(C2))
• A processzek felváltva kerülnek a kritikus szakaszba; egyikük kilép majd a másik lép be:
  AG(C1 ⇒ A(C1 U (¬C1 & A((¬C1) U C2))))

-- adamo - 2006.06.10.
-- Csapszi - 2006.06.12.