An LTL formula is true of a stream of states. A stream of states might usually
be modelled as a function from numbers to states. However, in the development
you're referring to, the states are just numbers, so that the first state of the
stream is number 0, the next is number 1 etc. Moreover, th
Call for Participation
==
FMICS 2013
18th International Workshop on
Formal Methods for Industrial Critical Systems
September 23-24, 2013
Hello,
I am very new, started yesterday, to HOL (in fact to theorem
proving itself). I was looking forward to use the Temporal logic
theory in HOL4, but I have a problem:
The definition of NEXT |- !P. NEXT P = \t. P (SUC t) seems a bit
odd.
