8.8 Some Properties Involving a Reduction to PITL with Finite Time

We now present some derived inference rules which come in useful when completeness for PITL with finite time is assumed. Recall that any valid implication of the form finite f is allowed and that we designate such a step by using PITLF. PITL Theorem BfFinStateEqvBox below illustrates this technique.


Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023