Automata based formulation:
Definitions (continued...) 
Automata based formulation:
Definitions (continued...)
A Chronobot is a 6-tuple (M, S, f, s0, F, DB)
Where
M is a non-empty set of messages (the message space)
S is a non-empty set of states (the state space), S = Sc * Ds * Da
Where
Sc is a nonempty set of states of the Chronobot
Ds is a nonempty set of self-models of the Chronobot, and
Da is a nonempty set of alien-models of the Chronobot
f : Sc * (M * M)* -> Sc is the state transition function. Given the current state of the Chronobot and the history of messages exchanged between the Chronobot initiating the bid and the Chronobots participating in the bidding process, f specifies the next state
s0 in S is the initial state of the Chronobot
F, a subset of S, is the nonempty set of final states
DB is the Database that stores the history of all the Chronobots involved in the Time/Knowledge Exchange