Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|FormModVizsgaTempLog}} %TOC{depth="3"}% ==Elmélet== ===LTL=== '''PLTL (Propositional Linear Time Temporal Logic)''' * Atomi kijelentések (…”

2012-10-21T19:58:31Z

Új oldal, tartalma: „{{GlobalTemplate|Infoalap|FormModVizsgaTempLog}} %TOC{depth="3"}% ==Elmélet== ===LTL=== '''PLTL (Propositional Linear Time Temporal Logic)''' * Atomi kijelentések (…”

Új lap

{{GlobalTemplate|Infoalap|FormModVizsgaTempLog}}

%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. -- [[GeGe|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>
 
-- [[CsapoT|Csapszi]] - 2006.06.12.

Az andersen.ps-ben (10 of 37) oldalon: <pre> t= x -> t[1/x], t[0/x] -t nevezi a Shannon felbontásnak. </pre>
-- [[AdamO|adamo]] - 2006.06.13. 

==Igaz/Hamis==
==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|adamo]] - 2006.06.10. 
-- [[CsapoT|Csapszi]] - 2006.06.12.

[[Category:Infoalap]]

Temporális logika - Laptörténet

Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|FormModVizsgaTempLog}} %TOC{depth="3"}% ==Elmélet== ===LTL=== '''PLTL (Propositional Linear Time Temporal Logic)''' * Atomi kijelentések (…”