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, the streams are conflated with the numbers of their first states, so that number 1 doesn't just stand for state 1, but in fact the whole stream that starts from 1 and keeps going. And, importantly, the first state of "stream 1" is simply the number 1.
So, when you look at
NEXT P
the definition tells you that it is true of a stream (represented as the number
t), if and only if P is true of the stream t + 1 (another number). Again,
remember that the first state of stream t is the number t, and that the second
element of stream t is the number t + 1, the third t + 2, etc.
One "problem" with the Temporal_LogicTheory is that it doesn't define lifted
propositional connectives. For example, you will see things like (\t. P t /\ Q
t) for the operation of conjoining two LTL formulas. To fix that, you could do
something like
Define`lconj P Q t = P t /\ Q t`;
set_mapped_fixity {term_name = "lconj", fixity = Infixr 400, tok = "&&"};
and then you can prove theorems like
ALWAYS P = P && NEXT (ALWAYS P)
which is a nicer form of the existing ALWAYS_REC.
Michael
On 31/08/13 08:43, Avinash Malik wrote:
> 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.
> According to LTL, M |= NEXT P, iff P |= s1, where s1 is the
> first state in the linear path $\pi$. But, in the definition of
> NEXT (in Temporal logic theory of HOL4), the "t", which I am
> guessing stands for the time step (or some state in path $\pi$)
> is unconstrained, i.e., if I apply NEXT P to any state sN, it
> says that the successor state (sN+1) has to satisfy the
> proposition P. This might look correct on a cursory glance, but,
> NEXT P is only satisfied on the state s1 of the path, i.e., in
> \t. P(SUC t). "t" needs to be constrained to be the very first
> time-step "t0", else, to my possibly ignorant eyes, it looks
> dodgy.
> Please, correct me, since I don't know anything about HOL and
> how this theory is being satisfied.
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Learn the latest--Visual Studio 2012, SharePoint 2013, SQL 2012, more! Discover the easy way to master current and previous Microsoft technologies and advance your career. Get an incredible 1,500+ hours of step-by-step tutorial videos with LearnDevNow. Subscribe today and save! http://pubads.g.doubleclick.net/gampad/clk?id=58040911&iu=/4140/ostg.clktrk
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
