Iteration: finite, infinite, or either

Speaker: Ian Hayes

When: 10:00, Friday, 19 January 2007

Venue: 78-420

We look at a simple model of real-time programs as a relation, R, between before and after traces. To allow for nonterminating real-time programs the traces may have infinite domain. We study finite (R^*), infinite (R^infinity) and either (R^omega) iteration operators, and their application to possibly nonterminating real-time loops. These are related by

R^omega = R^* \/ R^infinity

If R is well founded we get R^infinity is the empty relation and hence R^omega = R^*.

For a single-state predicate P, we can represent the fact that a program (relation) R maintains P as an invariant by

R => [P0 => P]

where P0 is P on the before-state and P is on the after state, and we get useful properties like

R* => [P0 => P].

That R is terminating is represented by an invariant

R => [t0 < infinity => t < infinity]

where t0 stands for the start time and t the finish time. Hence R^* => [t0 < infinity => t < infinity].

If for some strictly positive time d, R => [t0 + d <= t], then R^i => [t0 + i*d <=t] and R^infinity => [t = infinity].

These operators can be used to define a real-time loop and derive rules for reasoning about such loops.

Hospitality: David Carrington

Contact: Phil Cook (SSE seminar co-ordinator) (philc@itee.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html