30 Jun
2019
30 Jun
'19
2:18 a.m.
Hi all,
A quick (?) question. When I put the following LTL formula into SPOT online: G (G (p
=> Gp ) => Gp) => (FG p => Gp) SPOT says it is equivalent to 1. Therefore I
assume it’s a theorem of LTL. My question: Is there anyway to see the series of rewrites
of the formula to show how it gets form the original formula to “true”?
Thanks, Scott