BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:On the Canonical Reactivity Form for Past LTL - Di
mitar Guelev
DTSTART:20100119T130000Z
DTEND:20100119T140000Z
UID:TALK236AT
URL:/talk/index/236
DESCRIPTION:We present a new proof of the fact that every form
ula in discrete time linear temporal logic with pa
st is equivalent to a conjunction of formulas of t
he form <>[] A=> <>[] B where A and B are past for
mulas. This form is known as the general canonical
reactivity form. The original proof is based on t
he fact that a finite automaton recognizes an LTL-
definable omega-language iff it is counter-free (a
result from Lenore Zuck's thesis in 1986) and rel
ies on the theorem of Krohn-Rhodes about cascade d
ecomposition of finite automata. A shorter proof y
et not purely syntactical proof was outlined by M
ark Reynolds in 2000. That proof involved adding a
n infinity time point to the discrete flow of time
and syntactical transformations using separation
for Dedekind-complete time. The new proof involves
only equivalence transformations and makes use of
Gabbay's separation theorem for the standard disc
rete flow of time. This theorem has a proof that i
s based on equivalence transformations too. Theref
ore the new proof entails an algorithm to obtain t
he canonical form without resorting to constructio
ns outside discrete time LTL with past operators s
uch as automata.
LOCATION:CS 124
CONTACT:Dan Ghica
END:VEVENT
END:VCALENDAR