Formal modeling of dynamic environments for real-time agents

Abstract

Application of agent technology to dynamic environments makes developers to take into account some considerations that common agent-based systems need not meet. ARTIS agent architecture is our proposal for agent-based systems that require bounded response times. This kind of systems are characterised by their sensitivity to the moment in which the response is obtained. If the answer does not arrive on time, the consequences for the systems are catastrophic. They are hard, real-time systems. This paper proposes a formalisation, using an extension of RTCTL logic, to specify the ARTIS agent behaviour. It does not pretend to be a formal validation prove for the agent, but a way that allows the designer to check the fulfilment of the agent's design goals.