Na Seminaru za matematičku logiku i osnove matematike, u utorak 22.04.
od 17 sati u predavaonici 002 PMF-MO,

Grgur Petric-Maretić (ETH, Zurich) će održati predavanje

Rastav usidrene linearne temporalne logike.

Gabbayev teorem o rastavu je fundamentalan rezultat o linearoj temporaloj
logici (LTL). Pokazat ćemo da je rastav tzv. usidrenih LTL formula
elementarne sloĹženosti ako i samo ako je prijelaz iz LTL u linearnu
temporalnu logiku samo s budućim temporalnim veznicima elementaran. U
tu svrhu definirat ćemo kanonski rastav za LTL, te uspostaviti vezu
između kanonskog rastava usidrenih formula i ω-automata koji ih prepoznaju.

Nadalje, konstruktivno ćemo dokazati da je safety zatvarač bilo kojeg svojstva

izraženog u LTL također izraziv u LTL,
odakle slijedi teorem o dekompoziciji za LTL: svaka LTL formula je
ekvivalentna konjunkciji safety formule i liveness formule. Koristeći
kanonski rastav usidrenih formula, okarakterizirat ćemo safety,
liveness, absolute liveness, stable, i fairness svojstva u LTL. 

     V. Čačić