A temporal logic formalism used in model checking. CTL * employs operators, such as A (for all paths), E (there exists a path), X (next time), F (eventually), G (always), U (until), and R (release), that facilitate the construction of temporal logic formulas that correspond to desirable properties of a model.
Published in Chapter:
Formal Development of Reactive Agent-Based Systems
P. Kefalas (CITY College, Greece), M. Holcombe (University of Sheffield, UK), G. Eleftherakis (CITY College, Greece), and M. Gheorghe (University of Sheffield, UK)
Copyright: © 2009
|Pages: 4
DOI: 10.4018/978-1-60566-026-4.ch246
Abstract
Recent advances in both the testing and verification of software based on formal specifications have reached a point where the ideas can be applied in a powerful way in the design of agent-based systems. The software engineering research has highlighted a number of important issues: the importance of the type of modelling technique used; the careful design of the model to enable powerful testing techniques to be used; the automated verification of the behavioural properties of the system; and the need to provide a mechanism for translating the formal models into executable software in a simple and transparent way. An agent is an encapsulated computer system that is situated in some environment and that is capable of flexible, autonomous action in that environment in order to meet its design objectives (Jennings, 2000). There are two fundamental concepts associated with any dynamic or reactive system (Holcombe & Ipate, 1998): the environment, which could be precisely or ill-specified or even completely unknown and the agent that will be responding to environmental changes by changing its basic parameters and possibly affecting the environment as well. Agents, as highly dynamic systems, are concerned with three essential factors: a set of appropriate environmental stimuli or inputs, a set of internal states of the agent, and a rule that relates the two above and determines what the agent state will change to if a particular input arrives while the agent is in a particular state. One of the challenges that emerges in intelligent agent engineering is to develop agent models and agent implementations that are “correct.” The criteria for “correctness” are (Ipate & Holcombe, 1998): the initial agent model should match the requirements, the agent model should satisfy any necessary properties in order to meet its design objectives, and the implementation should pass all tests constructed using a complete functional test-generation method. All the above criteria are closely related to stages of agent system development, i.e., modelling, validation, verification, and testing.