Theatre

Theatre is a variant of the Actors model of computation whose design addresses the development of distributed, possibly time-dependent, systems. Actors are non-thread objects which communicate to one another by asynchronous message passing. An actor is characterised by a message interface, a local encapsulated state and a behaviour which in general can be a finite state machine. A system is composed of a network of theatres running on different physical processors. Each theatre is identified as a pair <URL, port> and hosts a (customisable) control machine which provides message scheduling and dispatching services, a transport layer, a network class loader, a local actor table, an access point to a global naming service. Actors are at rest until a message arrives. The response to a message depends on the message itself and the current actor state. Basic actions are: creating new actors, sending messages to known actors (acquaintances) including itself, migrating to a different theatre. Actors are provided of location transparent names. When an actor migrates to a new theatre, a proxy is left on the originating theatre which behaves as a forwarder. A mobile actor (agent) which comes back to a theatre where there exists a proxy of itself, will replace the proxy but the actor name is kept unchanged. A key point of Theatre relates to its flexibility to work with different timing models and programming styles. Currently the timing model of Timed/Probabilistic Rebeca (PTRebeca) was adopted, together with a programming style where message reactions are expressed by (reflectively activated) message server methods. Theatre favours model continuity during system lifecycle. The same model can be exploited for early analysis down to design and implementation. Appropriate control structures are developed which support abstract Theatre simulation, preliminary execution and real-time execution. The abstract modelling language of Theatre was, in a case, reduced to the Timed Automata formal language of Uppaal. The reduction makes it possible to model check, using both the exhaustive verifier for non deterministic analysis and the statistical model checker for quantitative analysis, a Theatre model provided of timing constraints and probabilistic aspects. Theatre is actually implemented in Java and is being applied to general distributed computing, general multi-agent systems (MAS), to reasoning to knowledge and commitments in web-based MAS, to cyber-physical and real-time embedded systems, distributed measurement systems, sensor/actuator networks.