Active Index Definition

Definition 1: An index cell is described by ic = (X,Y,S,so,A,tmax,f,g) where:

X is the (possibly infinite) set of input messages including dummy input d.

Y is the (possibly infinite) set of output messages including dummy output d.

S is the (possibly infinite) set of states. S includes a set of ordinary states S and a special state sdead called the dead state. If an index cell is in the dead state, it is a dead index cell. Otherwise it is a live index cell.

so in S is the initial state of the index cell ic.

A is the set of action sequences that can be performed by this index cell.

tmax is the maximum time for the cell to remain live, without receiving any messages. If tmax is infinite, the cell is perennial.