On the Canonical Reactivity Form for Past LTL

Add to your list(s) Download to your calendar using vCal

• Dimitar Guelev
• Tuesday 19 January 2010, 13:00-14:00
• CS 124.

If you have a question about this talk, please contact Dan Ghica.

We present a new proof of the fact that every formula in discrete time linear temporal logic with past is equivalent to a conjunction of formulas of the form <>[] A=> <>[] B where A and B are past formulas. This form is known as the general canonical reactivity form. The original proof is based on the 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 relies on the theorem of Krohn-Rhodes about cascade decomposition of finite automata. A shorter proof yet not purely syntactical proof was outlined by Mark Reynolds in 2000. That proof involved adding an 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 discrete flow of time. This theorem has a proof that is based on equivalence transformations too. Therefore the new proof entails an algorithm to obtain the canonical form without resorting to constructions outside discrete time LTL with past operators such as automata.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 124
• Lab Lunch

Note that ex-directory lists are not shown.