![]() |
![]() |
![]() On the Canonical Reactivity Form for Past LTLAdd to your list(s) Download to your calendar using vCal
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:Note that ex-directory lists are not shown. |
Other listsEPS - College Research and KT Support Activities Condensed Matter Physics Seminars Lab LunchOther talksTBA Life : it’s out there, but what and why ? TBC Quantum Sensing in Space Ultrafast Spectroscopy and Microscopy as probes of Energy Materials The tragic destiny of Mileva Marić Einstein |