Emergent Tendencies in
MultiAgentbased Simulations
using Constraintbased
Methods to Effect Practical Proofs
over Finite Subsets of
Simulation Outcomes
OSWALDO RAMON TERAN VILLEGAS
A thesis submitted in partial fulfilment of the requirements of the
Manchester Metropolitan University for the degree of Doctor of Philosophy
Centre for Policy Modelling
the Manchester Metropolitan
University
2001
2 Chapter 2  Simulation and Modelling,
2.3 Zeigler’s Formal Representation of
a System,
2.3.1 Zeigler’s Levels of Specification
of Systems,
2.3.2 Example: MASbased Simulation,
2.3.3 Morphism between Systems.
Simplifying,
2.4 Homomorphism and the Idea of
Metarules,
2.5 Systems Exhibiting Structural
Change,
2.6.1 In Traditional Simulation,
2.6.2 In Simulation of Structural
Change,
2.7 Verification and Validation of a
Simulation,
2.9 Simulation of Systems with Variable
Structure,
2.10 Towards Alternative Methods for
Analysing the Dynamics of Simulations of Complex Systems,
3 Chapter 3  Proving Theorems in Computational
Models,
3.2 Proving: an Ancient Problem,
3.2.1 Basic Concepts and (Logical) Model
Search/Construction,
3.3 Simulation, Logicprogramming, and
Theoremproving,
3.4.2 Herbrand Universe and Herbrand’s
Theorem,
3.5.1 Syntactic (clausal)based
Inference Procedures,
3.5.1.1 Robinson’s Principle for FirstOrder Logic (Chang and
Lee),
3.5.1.4 The Set of Support Strategy,
3.5.1.6 Strategies or Heuristics,
3.5.1.7 Forwardchaining Search,
3.5.2 Semantic (interpretation)based
Theoremprovers,
3.5.2.2 Prologbased Logical Models,
3.6 Classification of Theoremprovers,
3.6.2 Bonacina’s Taxonomy of
Theoremprover Strategies,
3.8 MetaLevel Reasoning and Proving
Tendencies,
4 Chapter 4  Understanding Phenomena and
Simulation Dynamics,
4.2 Subject’s Bounded Rationality and
the SubjectObject Dichotomy,
4.3 Objective Causes of Complexity:
Levels of Complex Systems,
4.3.1 Level 1: Matter, Inanimate
Systems,
4.3.2 Level 2: Adaptive Systems: Living
Organisms,
4.3.3 Level 3: Selfaware Systems or
Systems able to Reason,
4.3.4 Level 4: The Level of Metabeings,
4.4 Subjective Notion of Complexity,
4.5.1 Objectivistic Notion of Emergence
of Tendencies,
4.5.2 Subjectivist Notion of Emergence
of Tendencies,
4.5.3 Emergence of Tendencies: a
Tradeoff between Subjective and Objective Factors,
4.6 Tendencies in a Simulation,
5 Chapter 5  Mapping the Envelope of
Simulation Trajectories via a Constraintbased Exploration,
5.2 Factors Driving the Dynamics of a
Simulation,
5.3 Enveloping Outputs in Simulation
Trajectories,
5.4 (Logical) ModelConstrained
Exploration of Simulation Trajectories,
5.5 (Logical) Model Exploration for
Proving the Necessity of a Tendency,
5.6 Modeller Beliefs and Proving a
Tendency
5.6.1 A Review of the Concepts of
Explaining, Understanding, and Proving,
5.6.2 A Proof of a Tendency in a
Simulation Theory and a Subject’s, Knowledge
5.6.3 Interaction between a Subject’s
Cognitive Model and a Simulation Model,
5.7 Sources of Constraints: Bounds of
the Searched Space of Trajectories,
5.9 Implementation of a Method for a
Constraintbased Search of Tendencies in MAS,
5.9.1 Using SDML and Declarative
Programming Paradigm,
5.9.2 SDML’s Inference Mechanism,
5.9.3 An Efficient Translation of a
MASbased Model into a Single DatabaseRulebase (DBRB) Pair,
5.9.3.1 First Step. Revealing Dependencies,
5.9.3.2 A Problem Appears: The Growth of the Space of Searched
Data,
5.9.3.3 Dealing with this Difficulty: Unwrapping the Rules,
5.9.5 Speeding up of the
Simulation,
5.10 Morphism and Valid Translation of
Simulation Models,
5.10.1 Translating a MASbased Model into a
(Logical) Model Constraintbased Model,
6 Chapter 6  Transforming MAS to Improve
Efficiency of Constraint Logicprogramming,
6.1 Introduction: A Hierarchy of MAS
Architectures,
6.4 Possible further Translation for
Attempting Syntactic Proofs – Lower Architectural Level,
6.4.1 Comparing the Architectures,
6.5 Modelling Process using
Architectural Transformations,
7 Chapter 7  A Case Study: A Simple
TraderDistributor Model,
7.2 MAS Model using the Strictly
Declarative Simulation Language (SDML),
7.2.1 List of the Most Relevant
Predicates used in the Model,
7.2.2 Outline of the Most Relevant Rules
used in the Model,
7.3 Exploration of Simulation
Trajectories using the MASbased (Simulation) Model,
7.4 Envelopes of a Tendency in a
Subspace of the Simulation Trajectories,
7.5 A First Attempt to Prove in OTTER,
7.6 Facilities for Proving Tendencies
into SDML,
7.7 A first Attempt to Prove in SDML:
Resembling the Experiments in OTTER,
7.8 Drawbacks of this Implementation: A
More Efficient Implementation is Needed,
7.9 An Efficient Implementation in
SDML: a (Logical) Model Constraintbased Architecture,
7.9.1 Towards an Automatic Translation
of a MASbased Model into a Constraintbased Model,
7.10 Comparing the Traditional and the
Efficient MASbased Implementations,
7.11 Proving Necessity and Understanding
of an Emergent Tendency,
7.12 Comparison with other Approaches,
7.12.1 Theoremprovers: OTTER,
7.12.2 Proving in MAS: DESIRE,
7.12.3 Constraint Logicprogramming,
8 Chapter 8  Some Implications of this
Research,
8.2 Discussion about the Conditions of
how this Thesis works in relation to other Methods,
8.2.1 How this Methodology would work in
Simulation Platforms Different from SDML,
8.2.3 Tradeoff between Complexity and
Usefulness of the Techniques Proposed in this Thesis,
8.2.4 Complexity of a Constraint
Exploration of Simulation Trajectories in Some Applications,
8.2.4.1 Robot Agents (as different from computational agents),
8.2.4.2 ALife and Microsimulation,
8.2.4.3 Eventdriven Simulation,
8.2.6 Enveloping Tendencies: A New
Approach for Characterising Simulation Outputs,
8.2.7 Enveloping Outputs in Simulations
of Chaotic Systems,
8.3 Implications for the Modelling of
Complex Systems,
8.4 Implications for the Social
Simulation Community,
8.5 Implications for the MAS Community,
8.6 Bringing Ideas from other Areas of
Research: The Conception of Emergent Tendencies,
8.7 Implications for Policy Analysis,
8.8 Proving Tendencies in MASbased
Models and Constraint Logicprogramming,
10 Appendix 1 – Code of the Programmes,
10.2 SDML Code, after Unwrapping Rules,
11 Appendix 2
 Dependency Graphs,
11.1 For Module Model (after Splitting),
11.2 For Module Meta (after Splitting),
11.3 For Module Prover (after Splitting),
11.4 For the whole Model before Splitting,
12 Appendix 3  Set of Rules before and after
Splitting,
13 Appendix 4  Runs/Result Tables,
14 Appendix 5  Estimation of Speedingup Gained
from Unwrapping Rules,
15 Appendix 6  Complexity of the Search,
16 Appendix 7  Mapping the Envelope of Social
Simulation Trajectories,
Figure 2.2. Graphic representation of a morphism for example 2.1,
Figure 2.3. Graphic representation of a homomorphism,
Figure 2.4. Morphism between systems S and S’ under a similar
observation frame,
Figure 2.6. Graphical representation of several control levels where structural
change takes place,
Figure 3.2. A tableau for example 36,
Figure 4.1.Increasing objectivism in subjects’ beliefs,
Figure 4.2. Emergence of tendencies for a subject observing a system,
Figure 5.1. Theory given by simulation trajectories,
Figure 5.3. A model constraintbased exploration of the dynamics of a simulation,
Figure 5.4. Interaction between a subject’s
cognitive model and a simulation model,
Figure 5.5. Transformation of a MAS into a single
databaserulebase pair,
Figure 5.6. Rulebase dependencies for the 2^{nd} example,
Figure 5.7. Rulebase dependencies for the 3^{r} example (Case 1),
Figure 5.8. Database for the 3^{r} example (Case 1),
Figure 5.9. Rulebase dependencies for the 3^{r} example (Case 2),
Figure 5.10. Rulebase dependencies for the 3^{r} example (Case 3),
Figure 5.11. SDML’s inference mechanism,
Figure 5.12. Illustrating how agents and time levels become explicit in the new architecture,
Figure 5.16. Splitting of rule for prices,
Figure 5.18. Overview of the efficient implementation,
Figure 6.1. Sequence of modelling architectures,
Figure 6.2. Interactive use of the architectures by a modeller,
Figure 7.1. An overview of the model,
Figure 7.2.The whole procedure of revealing dependencies and unwrapping rules
Figure 7.3. Tendency observed in a
trajectory,
Figure 15.1. Boolean circuit for the target problem,
Table 4.1. A summary of part of Heylighen’s hierarchy of systems’ complexity,
Table
6.1. A Comparison of the
Architectures,
Table 13.1. Runs/Result Tables,
This thesis suggests a methodology for studying complex systems. This method is intended to be particularly useful for searching and proving tendencies (whether considered emergent or not) in those systems whose dynamics seem to be strongly dependent on the system’s components’ interaction (such as social systems). These systems are commonly simulated in MultiAgent Systems (MAS).
It begins by examining the formal notions of simulation, modelling, and theoremproving. Then it reviews some notions of complexity and proposes a notion of the emergence of tendencies as based on the tradeoff between subjective and objective factors of complexity. It next moves on to investigate the dynamics of a system via a platform consisting in a (logical) model constraintbased exploration of the dynamics of a simulation. This platform is suggested for systematically exploring the subspace of simulation trajectories associated with a range of parameters of the model, a range of choices of the processes (e.g., agents’ choices), and the logic of the simulation program. Following this, we suggest using this architecture in addition to the higher architectural level given by a MAS and an even lower level, a syntactic constraintbased architecture, as complementary means to investigate aspects of the dynamics of a MAS simulation. The proposed methods are compared with other approaches for exploring the dynamics of a simulation. In particular, differences in terms of the notions of morphism among models, the generality of the conclusions, and the measures of behaviour that each approach allows are emphasised. In addition, enveloping the simulation outputs is proposed as an alternative to statistical summaries. This seems to be especially convenient for studying complex systems and for analysing outputs in case of applying theoremproving techniques.
This model constraintbased architecture is applied to a MASbased model exemplifying a typical interaction traderdistributor. A tendency is identified in the MASbased model and then a constrained proof is performed in the model constraintbased architecture. Afterwards, some implications of this thesis for related areas of science are reviewed. Finally, the appendices include an analysis of the complexity of this model constraintbased exploration of trajectories and two papers particularly relevant to the social simulation and the MAS communities.
No portion of the work
contained in this thesis has been submitted in support of an application for
another degree or qualification of this or any other university or other
institution of learning.
The author obtained a first degree in Systems Engineering at the University of the Andes in Venezuela in 1992. Then he started lecturing at the Department of Operation Research of the Systems Engineering School and took a Master in Applied Statistics at the same University. He is a Member of the Centre for Simulation and Modelling (CESIMO: Centro de Simulación y Modelado) (http://cesimo.ing.ula.ve/) of that university. He has some involvement in the areas of Simulation and Numerical Analysis. His research at CESIMO includes Simulation Methodologies and Simulation of structural change following Carlos Domingo’s ideas.
I would like to thanks my director of studies, Bruce Edmonds, for his tolerance, patience, and wise guidance; my supervisor Scott Moss for his assistance and stimulating discussions; and the other members of the CPM team: Steve Wallis, Juliette Rouchier, Richard Taylor, and Olivier Barthelemy for their support in many ways. I would also like to acknowledge the encouragement and assistance received from CESIMO’s members, especially Giorgio Tonella, Carlos Domingo, and Jacinto Dávila.
Similarly, I would like to thanks CONICIT (the Venezuelan Governmental Organisation for promoting Science), the University of Los Andes in Venezuela, and the Faculty of Management and Business of the Manchester Metropolitan University, for supporting the reserach reported in this thesis.
For my parents, brothers,
sister, nephews, and for Jasmina.
Computer simulation has been widely used for studying and understanding systems. It is of particular importance in the analysis of the dynamics of a simulation. For example, discovering emergent phenomena and demonstrating their existence in social simulations have been recognised as key factors in the understanding of social systems (Nigel et al., 1998; Conte et al., 1997; Edmonds et al., 1998).
Already simulation tools such as MultiAgent System (MAS)based Simulation have proved valuable in the analysis of socioeconomic domains where the agents have bounded rationality (Edmonds et al., 1998; Edmonds, 1999b, 1999c). Different simulation architectures, methodologies, and techniques have been used in these studies. Some simulation communities have been interested in studying ‘complex systems’ and ‘composite complex systems’. A MASbased simulation consists of generating in a computer the dynamics of a complex system as resulting from the interaction of simpler agents. The idea is to resemble complex behaviour observed in empirical systems as the product of the interaction of individuals. For example, a social modeller might be interested in generating certain aspects of overall behaviour observed in a society via the interaction of simple models of individuals (e.g., people).
Now, the social simulation community is going beyond bounded rationality to explore how ‘social artefacts’, such as roles, norms, and organisational design, place bounds on social cognition (Carley et al., 1998). This experimentation is potentially useful, for example: for detecting gaps, inconsistencies, or errors in organisational theories (Moss, 1998; Axtell, 1996); for providing insight into organisational behaviour (Carley et al., 1998); for testing, verifying, and improving models of artificial social agents (Moss, 1998; Moss et al., 1998a); for investigating the interdependence between social factors and agents’ cognitive models (Carley et al., 1998), and for aligning models (Mihavics et al., 1996; Axtell, 1996).
Apart from the social simulation community, other examples of research communities for which studying and analysing the dynamics of the simulation are important are: ALIFE (Langton, 1989; http://alife.org/), and microsimulation applications in traffic (Nagel et al., 1998 and 2000).
Usually a MASbased simulation exhibits very complex dynamics – in this fact lies its promise but it also means that its analysis might also be difficult. Behaviour difficult to capture by a modeller but key for understanding empirical complex systems is resembled in the simulation in the hope of obtaining hints to improve such an understanding from the simulation experimentation. Nevertheless, commonly it is still little understood how such significant dynamics appear from the agents’ interaction. To develop methodologies for helping in understanding the dynamics of a MASbased simulation becomes a crucial task.
As will be seen in Chapter 3, there are two
means by which a modeller can seek to understand the dynamics of computer
simulations: through design and through observation of the dynamics using a post hoc analysis. In MAS, careful
design procedures based on wellunderstood formal models of agent behaviour can
help a modeller to understand the behaviour of individual agents and, in
special cases, larger parts of MAS. However, understanding the behaviour of
interacting groups of autonomous agents by formal design methods has its
limitations, and even the most carefully designed MAS can exhibit behaviour
unforeseen by its designers as the simulation dynamics become subtle over the
state transitions and large number of data manipulations. Additionally, noted
as factors associated with this difficulty are the facts that systems simulated
in a MAS are of a high level of complexity and that a modeller (in this case,
the observer) has bounded rationality (see Chapter 3). An observer’s bounded
rationality is associated with limited capabilities for capturing and
processing information from the observed system (e.g., the target system or the
simulated one).
Because of this the second way in which a simulation can be analysed, namely by inspecting the dynamics in a post hoc analysis, becomes the most used approach for studying MAS. Among the existing methodologies for doing such post hoc analysis are: scenario analysis (Domingo et al., 1996b), where one single MAS trajectory at a time is examined and analysed, and the Monte Carlo approach (Zeigler, 1976), where the MAS is repeatedly run and statistics are collected about general trends over a sample of trajectories.
However, neither of these traditional ways of analysing computer dynamics is satisfactory for MASbased Simulations (MABS). On the one hand, it is usually prohibitive in terms of computational resources to explore all simulation trajectories using single scenario analysis. Moreover, its use is restricted to certain ‘arbitrarily’ and subjectively chosen trajectories. Scenario analysis can help by exposing possibilities for the dynamics of the simulated system. Its value for training the modeller or the policy analyst about ‘possible future worlds’ has been recognised in simulation applications related to policy analysis (Axtell et al., 1996; Wack, 1985; Domingo, 1996b). Nevertheless the fact that arbitrarily unexplored trajectories are left aside makes difficult the generalisation of conclusions and the analysis’s application in wider theory.
On the other hand, in Monte Carlo techniques the analysis of the simulation is made using a sample of the trajectories. Consequently, an arbitrary (in this case the arbitrariness is random) exploration of trajectories is also carried out. The use of statistics supports only probabilistic generalisations but not mathematically (or logically) valid proofs. Hence the usefulness of these techniques in theoretical applications is limited  they do not give definitive answers but only probabilistic ones.
Consequently there is a need to advance the search for new computational methodologies and techniques that allow a more rigorous exploration of the dynamics of simulations of complex systems.
The main aim of this thesis is to help in
filling the gap apparent in the need for better computational methods for
studying MAS dynamics, as was pointed out in the last section. It is of
particular interest to develop a methodology for proving emergent tendencies in
MultiAgent Systems. The following subgoals of the thesis can be stated as
part of an effort for developing methodologies and techniques to help in the
exploration and proof of emergent tendencies in simulation of MultiAgent
Systems.
o To develop a methodological approach for exploring and proving emergent tendencies in computational models
The intention is to show that it is possible to prove theorems about social simulation models. The idea is to prove that emergent tendencies are (or are not) general under certain conditions when varying certain factors of the simulation dynamics. This methodology will allow a modeller to elaborate conclusions about the behaviour observed in the dynamics of a simulation theoretically stronger than those that traditional explorations of simulation trajectories are able to support (e.g., Monte Carlo techniques permit one to infer only probabilistically valid conclusions; for more details about traditional approaches and their drawbacks, see Chapter 2 and especially sections 2.6 and 2.10).
o To develop some techniques for implementing such a methodology
The purpose is to apply the methodology in a particular simulation example and to give an indication of how it could be automatically implemented. Appropriate techniques for implementing the methodology in a particular simulation language would be developed. The language SDML for writing MAS is chosen for such implementation because of the relevance of MASbased models for studying complex systems in, e.g., social and economic systems, and because this language is suitable for implementing formal proofs (e.g., it is a declarative language with a wellgrounded underlying logic). These advantages give SDML advantages over many other existing simulation languages, where usually only traditional explorations of simulation trajectories are allowed (e.g., traditional eventdriven simulation languages, e.g, SLAM; see Pritsker, 1995, for more details with reference to this point; this argument is better explained in Chapter 2).
o To investigate the tradeoff between complexity and the usefulness of these techniques
Factors and criteria for this tradeoff will be identified relative to a conception of complexity. This conception will be strongly linked to a notion of what are considered as emergent tendencies in complex systems. In addition, the computational complexity of the task which the approach in this thesis suggests, i.e., proving in a computational model, will be investigated and presented (see Appendix 6  Complexity of the Search). This investigation allows a discussion of the tradeoff between computational complexity and factors related to the usefulness of the technique. On the other hand, difficulties for implementing the technique and modelling approach (MASbased and constraintbased simulation and proving) in a particular language (SDML) will be examined. Further, how different such difficulties would be in case of modelling in other simulation languages will also be discussed. In particular, for analysing simulation outputs, enveloping of tendencies will be proposed as an alternative to central measures and other statistical summaries. The idea of using an envelope is to present an alternative to statistical summarises and to overcome some of their drawbacks for studying complex systems (for example, that pointed out by Crutchfield, 1992, p. 35; aspects of this tradeoff will be discussed in section 8.2).
o
To develop a particular case study
An abstract simulation based on a ‘need problem’ will be focused upon. The idea is to apply the developed methodology and techniques in a typical model of an empirical system. The intention is to use this typical example to show that the developed methodology and techniques effectively work. Consequently, it must be possible to arrive at stronger conclusions about behaviour in the dynamics of the model than those possible when using traditional methods; i.e., conclusions must find stronger support in the theory of the simulation model than in those allowed by existing techniques (this case is presented in Chapter 7).
o To
review the conception of emergent tendencies
Conceptions of emergent phenomena useful for understanding emergent tendencies in computational models will be reviewed. Of special interest will be criteria for testing whether certain tendencies can be considered as emergent by an observer (e.g., by a modeller). The intention is to achieve a more ‘practical’ notion of the emergence of tendencies, one more practically useful for modelling complex systems. Existing modelling approaches like those named above as well as modelling in different areas of research (e.g., in physics) traditionally consider the emergence of tendencies only from an objectivist point of view. They are usually linked to objective notions of the complexity of a system. However, it also seems convenient, especially when modelling certain complex systems such as human systems, to examine the relevance of subjective factors for a tendency to be considered as emergent by a modeller. These factors seem to be sourced on a modeller’s bounded rationality. The idea is to consider both the objective and subjective factors and to reflect on their tradeoff (Chapter 4 is specially dedicated to examining these aspects; a further discussion about the usefulness of this concept is presented in section 8.2.5).
This thesis is focused on (and limited to) the computational modelling of computer systems. The terminology and concepts are intended with respect to this domain. This bias applies throughout the thesis (except in the discussion in sections 4.24.3 and 8.6) and should be held in mind when reading the discussion involving highly polemical terms such as ‘complexity’ and ‘emergence of tendencies’.
This thesis is born out of the following disciplines:
Social simulation. This is one of the areas where a need for better methodologies for analysing and understanding better the dynamics of computational programs has been identified (Conte et al., 1997; Edmonds et al.,1999).
Multiagent systems (MAS), in particular their use for simulation of complex systems conceived as made up from the interaction of subsystems with certain autonomy (Weiss, 1999).
Automatic reasoning and theoremproving, specifically their application for analysing the dynamics of computational programs. In the application to be considered in this thesis, it will be useful for studying the dynamics of simulation programs; in particular, the interest is in modelbased exploration of simulation programs (Wos, 1988).
Artificial Intelligence.
This discipline of research includes modelling using MAS, Automatic Reasoning,
and other subdisciplines of research to be assessed in this thesis (Stuart,
1995).
Computational modelling of complex systems. It includes areas of research relevant to this thesis, such as modelling of social systems and, in general, MultiAgentbased Simulation (Casti, 1992; Holland, 1998). Methodologies to be developed in this thesis will be useful not only in social systems but also in different subareas of computational modelling of complex systems.
Systems theory, more specifically notions of systems from an evolutionary perspective, as is conceived by the group working in Principia Cybernetics at the Center Leo Apostol in Belgium (http://pespmc1.vub.ac.be/CLEA/). Heylighen’s ideas will be accorded special importance (Heylighen, 1992 and 2000c; http://pespmc1.vub.ac.be/HEYL.html).
Broadly speaking, the example model will be a
representation of a traderdistributor relationship. However, in order to
facilitate the development of a technique for exploring and proving in the
dynamics of the simulation, a more abstract and limited model will be
considered. The case study to be developed will be typical but not necessarily
representative of a particular empirical system. This will remove unnecessary
timeconsuming activities during the research, for example, data collection and
validation of the model. traders and distributors in the model will be
simplified to agents whose main activities are price and salessetting, and priceimitating,
in the first case; and ordersetting in the second case. It is hoped to apply
this technique in future studies using more elaborate examples.
It is foreseen that the methodology and techniques in this
thesis will be applied to other areas of MASbased Simulations, especially when
studying complex systems. It is hoped they can be implemented automatically in
some MAS. In order for this to be possible, these systems must have certain
capabilities for exploring computational program dynamics such as those found
in theoremproving and constraint logicprogramming (Moss et al., 1997;
Abdennadher et al., 1995;
Abdennadher, 1999; Frühwirth et al.,
1992; Rainer et al., 1988; Marriott, 1998).
First, in Chapter 2, a review of basic concepts and the formal aspects of simulation and modelling are presented. We begin by considering basic concepts in classical systems theory in order to set a first ‘world view’ for the thesis. Then Zeigler’s foundational theory for simulation and modelling will be examined. Afterwards other aspects of simulation (which Zeigler’s theory does not consider), such as structural change and modelling in MultiAgent Systems, will be considered. Following this, concepts related to the formal use of simulation results including validation, verification, and simplification of models are examined. At the end of the chapter, the main drawbacks of traditional post hoc analysis of simulation outputs for studying complex systems are pointed out and theoremproving is suggested as a promising area for alternative approaches.
Following, in Chapter 3, formal aspects of theoremproving are reviewed, including the most common approaches: the modelbased (semantic) approaches and the resolutionbased (syntactic) ones. A comparison of these methods is presented. Chapter 3 also includes references to OTTER as an example of a successful theoremprover. Its more relevant characteristics are described later in the chapter (OTTER is used in the implementation of the case study in Chapter 7).
Chapter 4 offers a review of some conceptions with respect to understanding simulation dynamics. Special attention is given to the concept of emergent tendencies. Some definitions of this, using different ideas of complexity and the notion of bounded rationality, are presented. Special emphasis is placed on a tradeoff between the objective aspects (grounded in an observed system) and the subjective factors (grounded in an observer’s language).
Chapters 5 and 6 present a methodological approach to the study of complex systems using MultiAgent Systems. Chapter 5 suggests a model constraintbased exploration of tendencies in a subspace of simulation trajectories. Compared to existing approaches, this method allows a modeller to apply stronger notions of morphisms for comparing models, to reach more general conclusions about the dynamics of a model, and to use other measures of behaviour than statistical summaries. This chapter also discusses aspects of how an analysis of the simulation outputs can help a modeller in better understanding aspects of the simulation and, by extrapolating, of the empirical system. In addition, it proposes enveloping tendencies as an alternative to traditional methods for studying simulation outputs. Then, Chapter 6 proposes a platform consisting of a hierarchy of architectures for understanding MASbased models. The platform is: at the first level, the MASbased model; at the intermediate level, the model constraintbased architecture proposed in Chapter 5; and, at the lowest level, a syntactic constraintbased architecture. This platform is intended to assist a modeller in understanding the simulated complex system by showing complementary aspects of the dynamics of the model.
Chapter 7 offers a case study where the methodology suggested in Chapter 5 is applied. The model consists of a MASbased model of a typical traderdistributor interrelationship.
Chapter 8 discusses some implications of this research in related areas such of modelling and simulation. It includes a discussion about how the methodology and techniques developed in the thesis may be implemented in other platforms and about the tradeoff between the usefulness of such techniques and the complexity of their implementation. Conclusions are offered in Chapter 9.
Finally, the appendices and a bibliographic review are presented. Appendices include a review of the speedup achieved in the case study when the model is translated from the MAS to the constraintbased architecture (both in SDML), an examination of the computational complexity of the search proposed in this constraintbased architecture, and two papers relevant to the social simulation and MAS research communities.
The aim of this thesis is to develop tools and a methodology helpful for understanding simulation of social systems and other complex systems. It is of special interest to apply such a methodology in the simulation of social systems using MAS. Given the difficulties for understanding a MASbased model from its design, the method commonly used is to inspect the dynamics of the simulation in a post hoc analysis.
Understanding of a simulation is closely related to simplification, validation, and alignment of models. They rest in a post hoc analysis of simulation trajectories, and in a mathematical notion of homomorphism. Because of the difficulties involved in evaluating the formal notion of homomorphism in simulation, weaker notions are used in the existing techniques. As will be seen, to circumvent these difficulties, the idea of approximation is used instead of that of strict morphism. Among the widely used techniques based on this notion of approximation are scenario analysis and Monte Carlo studies. However, as pointed out in the Introduction to this thesis, they both have serious drawbacks.
It is our intention in this chapter to review existing formal simulation approaches and the notion of homomorphism used there, in order to make more explicit the drawbacks of these techniques and then illustrate the advantages of the approach to be proposed in this thesis. In particular, we seek to develop a methodology that allows a modeller to prove emergent tendencies in computer simulation of complex systems. This will lend support to the implementation of the strongest notion of morphism, more so than the weak one commonly used in the named existing techniques.
As a starting point, in this chapter basic notions about simulation and modelling will be presented, to help, as said, in clarifying, for example, drawbacks in the existing techniques and desirable properties in alternative techniques. Then, in the next chapter, concepts related to the proving of theorems in computer models will be reviewed, in order to establish a background helpful for developing a methodology for proving tendencies in a simulation. In Chapter 4, before presenting a methodology for proving a theorem in a simulation in Chapter 5 notions related to the understanding of emergent tendencies in the dynamics of a simulation will be discussed.
In the first part of this chapter, basic aspects of Systems Theory will be described as part of the framework (‘world view’) of this thesis § 2.1). This will be used throughout the whole thesis, but it will be of particular value as a basic reference for discussing notions of understanding and emergence in Chapter 4, where this discussion and the development of a ‘world view’ will be extended. Then, in the second part of the chapter, the fundamental theoretical aspects of simulation and modelling, starting from Zeigler’s formalism and progressing to MAS, will be reviewed. In addition, simplification, integration and alignment of models will be discussed. These are important considerations when modelling complex systems. Finally, in section 2.10 some drawbacks of traditional simulation for modelling complex systems will be discussed.
The basic notion for the ‘world view’ taken in this thesis will be presented as understood in classical systems theory (Heylighen, 1992; Ashby, 1964; Checkland, 1981; Checkland et al., 1999; Churchman, 1968; Domingo et al., 2000; Fuenmayor, 1986).
The basic entity identified in reality is called an object. Its basic characteristics or attributes, e.g., colour, size, are called properties.
In this view, objects are one of the basic semantic units. This is one of the more basic notions of object, one widely used in computer science and logic. It is useful for describing more abstract concepts as made up of objects. However, its value is quite limited because processes (e.g., evolution) cannot be passively represented. So, a move towards a higher level of abstraction is necessary in order to identify a basic entity useful for abstracting and modelling processes. Such an entity is the system. More elaborated notions of ‘object’ will be considered in Chapter 4.
In classical systems theory, a system can be thought of as a kind of object with additional properties. Among the special attributes a system presents are:
·
A distinction
between the whole, its components, and the interrelations among these
components. A component can be a subsystem (a system in itself) or an object.
For example, consider a model of a traderdistributorconsumer interaction. The
model will represent the whole thing. Among the components are traders,
distributors and consumers, and among the interrelations are orders from
consumers to distributors and from distributors to traders; sales from traders
to distributors and from distributors to consumers; and traders’ and
distributors’ pricesettings.
Other notions of systems found in the literature will be reviewed below.
A subject is defined as a system with a
vicarious mechanism (Heylighen, 1991a). A vicarious mechanism selects among
alternative actions in order to satisfy a particular system’s goal. This goal
might be, e.g., surviving, or perhaps increasing economic benefits. In some
subjects, e.g., human beings, this vicarious mechanism rests on genetics and
internal models. The genetics provide useful information for surviving as they
are passed from individuals to their descendants. This process is actuated for
an internal mechanism, which is out of rational control by the subject. Some
subjects enjoy a second mechanism at a higher level of complexity, internal
models of their environment allowing them to take choices. Some subjects, e.g.,
animals, benefit primarily from the first kind of mechanism. The vicarious
mechanism is important as it allows the system to take actions in advance of
other actions in the environment, in order to adapt in some degree by itself
and decrease the likelihood of risky ‘corrective’ actions from its surroundings
(see section 4.3).
In this thesis, the term ‘agent’ is used of a kind of system with certain characteristics. Different notions of agents can be found in the literature. For example, in researches in biological and social systems, an agent may be defined as an object with a vicarious mechanism, i.e., a subject; while for people working in physics, an agent may be any entity able to influence others in its surroundings. For instance, when studying the solar system, the earth as a body attracting and rejecting other bodies in the solar system will be an agent. This notion is shared in some modelling computer programs such as the simulation language SDML (Moss et al., 1998a), where an object might be any entity with a rulebase and a database. An agent in SDML is just an object interacting with other objects or an object useful for providing the context (environment) where other objects interact.
It seems useful to check in a dictionary the most common conceptions of agent (MerrierWebster; http://www.mw.com/):
Main Entry: agent
Pronunciation: 'Aj&nt
Function: noun
Etymology: Middle English, from Medieval Latin agent,
agens, from Latin, present participle of agere to drive, lead, act, do; akin to
Old Norse aka to travel in a vehicle, Greek agein to drive, lead
Date: 15th century
1: one that acts or exerts power
2 a: something that produces or is capable of producing an
effect: an active or efficient cause b: a chemically, physically, or
biologically active principle
3: a means or
instrument by which a guiding intelligence achieves a result
Here,
the notion of agent is linked to the notion of influencer. An influencer might
be thought of as an object influencing elements in a broader system, but this
object does not necessarily have to be considered as a component of the system.
While an agent is defined in terms of its actions towards its surroundings, a
subsystem is defined as part of the interacting elements defining a system.
The conception of agent is more closely linked to the idea of an active entity
influencing the environment a subject is studying, but it is not necessarily a
key element for helping a subject’s understanding. On the other hand, a system
is more closely related to the notion of evolving entity, which is of interest
for a subject, as it helps him to model and understand relevant parts of its
surroundings.
In general a model is a representation of an object (‘realist position’) or of an idea (‘idealist position’) that a subject has created. In the case of modelling physical systems, a realistic position is taken and there will be a relation of correspondence between the original entity in the environment and the model an agent has elaborated. However, when modelling social systems, which are of particular interest in this thesis, such a physical reference is not clear and the modelling process becomes more subtle as ideas from theoretical and abstract grounds are also appropriate to build the models. Nevertheless, in any case, a model is considered helpful (in practical terms) only if it is simpler or at least easier to manipulate than the corresponding entity it is modelling. So, a model might be an object, for example a picture, or something as elaborate as a system.
People working in social simulation are interested in computational models of the internal representation or models a subject has of its environment in order to reason, make decisions, act, and adapt. Here, models are basically a representation of the subject’s perceiving phenomena, taking decisions, and then acting. Even more, a model might be a representation of good action. A subject with an internal model might have several models of certain aspects of its environment, and will take actions in accordance with a chosen model. It in of interest in this thesis also to consider a subject’s internal model, which may be conceived as a population of submodels of its surroundings evolving along with perceived phenomena (experience) and reasoning.
So far, a world view where a subject is a
particular kind of object has been developed. It is an object that perceives
and reasons about its environment. It does this to achieve its goals. It is
also a system where ‘evolutionary processes’ are going on. These processes may
involve a population of developing models of its environment. A subject’s
internal model is useful for abstracting and modelling processes going on in
its environment.
On the other hand, the environment is also considered as a particular kind of object. It is and evolving object; e.g., it is an object with behaviour where not only quantitative but also qualitative changes take place.
Finally, an agent is conceived of as a system with special properties. An agent can be seen either as a subject or as a subsystem part of the environment. This is in line with MASbased Simulation, where the model of the whole system comes up as the interaction of agents. Each of these agents is a component of the model (system), but each agent also has an internal model of its environment, and consequently, it can be conceived of as a subject.
In this section Zeigler’s formalism will be recapitulated, though the examples and related discussion are not from him. The idea is to provide in this introductory chapter a formal description of a system as seen in simulation. Zeigler’s seems to be one of the first and more successful descriptions of a system in simulation. A description of both a system’s structure and a system’s dynamics will be given. Originally, its basic formalism is intended to describe simulation models whose structure is fixed, which are common in simulations of systems in industry, e.g., queue systems. However, its ideas can be extended easily to MAS. In fact, each agent in a MAS can be described as a system in Zeigler’s formalism and the entire MAS as a composite of a hierarchy of basic and composite agents.
The main parts in his formalism are represented in Figure 2.1. There an input value x, and output value y, an internal state q at two time steps, and the transition from the former time_{1} to time_{2}, are identified. The output is a function defined by an observer, e.g., something that the observer is interested in. The output function’s domain is an internal state of the system. It is supposed there is a function l generating the output x from the state of the system q. In addition, there is a change in the system over time (e.g., there is a process): the system’s state and the input change over time. Time is introduced as the independent variable.
More formally, Zeigler’s (1976) notation for a system S is: S =
< T, X, W, Q, Y, d, l >. Where:
T: Time base (T = Reals or T = Integers).
X: Input value set (each input is a sequence of values)
W: Input segment set, subset of (X, T), W = {w / w: < 0, t > ® X, t Î T}.
Q: State set.
d: State transition function. d: Q x W ® Q.
l: Output function, l: Q ® Y.
Y: Output value set. (there should exist a set of output segments{r / r: < 0, t > ® Y, t Î T})


Figure 2.1. Basic notions in Zeigler’s formalism: input values x_{1},_{ }x_{2}; system states q_{1}, q_{2}; output volues y_{1}, y_{2;} output function l; and transition function d, changing initial state q_{1} into a new state q_{2} 
Example 2.1. Let us consider a linear system
_{}: a real vector of size n,
_{}: a real vector of size l,
_{} : a real vector of size k,
_{}: (state) at time t_{2} would be given by the application of d at time t_{1}_{ }(t_{2} > t_{1})_{ }
The set of instances for vectors x and y gives a sequence of values over time:


Where t represents t_{1}, t+1 represents t_{2,}_{ }and A, B, C are real matrices. More explicitly (see also Figure 2.2): 


Where: n = number of states q_{i};_{ }l = number of inputs x_{j}; k = number of observation variables or outputs y_{p}
The set <T, X, W, Q, Y, d, l> is called the system structure. The subset <X, W, Q, Y> gives the static structure and the rest of the specification, d and l, the dynamic structure. The dynamic structure gives the laws of change of states. Notice that there are no laws of change either for the static or for the dynamic structure, that is, this formalism does not consider systems with variable structure.
Experimental Frame: Zeigler calls the experimental frame ‘the limited set of circumstances under which the real system is to be observed or experimented with’ (Zeigler, 1976, p. 30). He associates an experimental frame with a subset of the inputoutput behaviour. More precisely, he formalises an experimental frame E as the subset < W, Y, l, V>_{E}, where the first three components are as given above and V is a subset of Y determining the range of validity of the experimental frame. This subset of Y (i.e., V) contains the control variables of the experiment. The remaining variables in Y are those of interest in the experimentation (Zeigler, 1976, p. 298). Constraints are placed in accordance with the modeller’s particular interest. In the example, a frame would be given by <W, _{}, l, _{}>, where Y=_{} and l are given as in the example, W is (_{}, T), where T is defined as the positive integers (e.g., 1, 2, …) and V=_{}, e.g., there are not constraints.


Figure 2.2. Graphic representation of a morphism for example 2.1 
The idea is to have a hierarchy of systems’ descriptions by increasing levels of elaboration in the sense that the higher the level, the more detail there will be in the specification of the system (e.g., more aspects of his structure will be known). This would be valuable for comparing models’ descriptions and to know the degree of specification a model has.
At a first level (level 0), a collection of inputs and outputs is known over time, but there is no idea about the relationship among them. In a second level, an inputoutput relation is known. Different outputs have been associated with the same input, and, vice versa, different outputs have been related to the same input. A third level of specification will be useful for associating an input with an output, that is, there is a function relating in a unique manner an input with an output. This level is the most commonly used in science, e.g., in mathematics and physics. Notice that still the notion of process is poor  the weak notion of process is in the output, which can be specified as a function over time. At this level simulation is not an important tool, as the output can be generated only as far as the input and the function inputoutput are known. This level is not rich enough for helping in those cases where the behaviour of the system is difficult to model via a function, but depends subtly on internal variables (e.g., the state) of the system (e.g., in a social system, or in a queue system). It is in these cases where simulation becomes helpful. In the fourth level (level three in the specification), it is supposed that a function for changing the internal state of the system is known. The specification of change over time of a system’s state brings in clearly the notion of process. Other aspects of a system, such as the output, can be defined in terms of a system’s internal state. In the higher level, e.g., at level four, a system is defined as the composite of interacting systems at level two. This level is useful to describe, for example, an agent in a MAS composite of more elemental subagents. In fact, it can be used to describe a hierarchy of agents, e.g., a MAS.
More formally, from Zeigler (1976):
Level 0: Observation Frame, S = < T, X, Y >. The sets of inputs and outputs are distinguished but it is not known how they interrelate.
Level 1: Input/0utput (I/O) Relation Observation (IORO), S = < T, X, W, Y, R>, (R Í W _{} (Y,T), where (w,r) Î R ® (implies) dom((w) = dom (r )). The relation between the input and output sets is distinguished, but it is not possible to differentiate among the different outputs associated with one input and vice versa.
Level 2: I/O Function Observation (IOFO), S = < T, X, W, Y, F >, (f Î F ® (implies) f Í W _{} (Y,T) is a function, and if f = (w,r) then dom (w) = dom (r )). At this level, there is a function between input and output sets which permits one to differentiate between the different outputs associated with an input. It is granted by the knowledge of the initial state. Until this level, a move from a lower level to a higher one allows more predictability about the output, given the input, but still there is no knowledge of the system’s states.
Level 3: I/O System Specification, S = < T, X, W, Q, Y, d, l >. At this stage, the state set, the transition and output functions are known, but still there is no distinction of the system’s components.
Level 4: Coupling of Systems. Here a system is specified as a coupling of several subsystems or components. Four elements are given: the name of the subsystems, the specification for each component at level 3, the influencers of each one (other components), and the interface function specifying the input of each component as a function of the outputs of its influencers and the input to the system.
In Zeigler’s formalism, it is supposed that the transition function is invariant over time (e.g., a system’s dynamic structure is invariant); that is, whenever it is applied over the same initial state and input segment, the same output segment will be generated.
Also, notice that the specification at level
zero only gives a pair of the sets of inputs and outputs plus the idea that
they are changing over time. There is no specification of structure. This seems
to be one of the simplest specifications of a system that can be found in the
literature.
Heylighen also formulates specifications of very simple (plain) systems, for example, systems for which it is not necessary to specify their components or even their states (Heylighen, 1995). He brings in the example of an electron. An electron is considered as a system though no structure has been identified and only the notion of certain behaviour gives its identity. However, ‘It has states given by positions, energy or momenta … and their evolution can be expressed by the Schrödinger equation’ (Heylighen, 1995, http://pespmc1.vub.ac.be/papers/MSTConVar.pdf, p. 4). In fact, this model will be at least at level three, as the transition function is known. Heylighen considers that a system is an entity suffering internal change while keeping stability in the sense that it shows differentiation with respect to the environment as an individual unit. He expands this notion, summarising a system as a ‘constrained variety or constraint on variety’. This idea can be used for describing systems of order zero: ‘The total set of connections (Cartesian product of the set of possible inputs and set of possible outputs) might be interpreted as a maximal possible variety, the subset defining the system as a limited variety, to which actually occurring inputoutput transitions are constrained’ (idem, p. 5).
When modelling in traditional economics, the
economic system is usually represented at level 4 but the economic agents
(e.g., organisations or people) are simplified to level 2. In social simulation
this system is modelled at a higher specification level, as the relevant
aspects of an economic subject with bounded rationality, namely, its internal
(cognitive) model, are modelled at level 4. One interesting question is whether
the simplification made in traditional economics is well justified in the
dynamic economic environment of today.
MAS has been successfully applied to the modelling of complex systems described in terms of components.
A MAS consists basically of a hierarchy of agents. Each agent can be described as a system according to Zeigler’s formalism, as was briefly shown in the example given in section 2.6.1. The lower level of agents in a MAS, that of agents without subagents, will be described at level 3 in Zeigler’s formalism (see paragraph 2.3.1). The other, higher levels (the containers) could be described at level 4.
Agents change as their rulebase changes over time. A relevant example is the evolution of their cognitive models given via a set of rules. The change of rules over time allows more creative and subtle processes than those happening when only elimination and introduction of agents are implemented.
In declarative programming, laws of behaviour are given as a
set of rules, which are ‘atomic’ components admitting to be modified,
eliminated, created, and replaced. This is appropriate for evolving the dynamic
structure of agents.
Now a criterion for comparing models will be reviewed. This comparison is based on the concept of experimental frame: ‘equivalence’ among models is always relative to an experimental frame. This conception of equivalence is based on the mathematical concept of morphism. A weaker notion of model equivalence will be presented in section 2.6.1. This will be useful for simplification, validation, and alignment of models.
Evaluating morphism consists in checking if the same outputinput set a modeller is interested in (e.g., the experimental frame) is observed in two models. It might consist also in checking if a subset of the output a model offers under certain conditions (this gives an experimental frame) coincides with the correspondent outputs other models generate under the same conditions; in such a case it is said that there is a morphism between these two models. As a system’s output depends on the system’s state, also ‘equivalence’ between the compared system’s states has to be checked. In fact, a system S will be called ‘equivalent’ to a second system S’ (that is, a morphism exists from the second to the first system) if the state and output of system S can be accessed via a mathematical transformation (the morphism function) from the state and output, respectively, of system S’ at any time and under certain conditions of experimentation (e.g., under an experimental frame).
Notions discussed in this section can be used to classify and assess homorphisms appropriately when using the methodology to be developed in Chapter 5 for comparing models. Notions of homomorphism associated with this methodology will be discussed in section 5.10.
Consider now the notion of morphism as given by Zeigler. There is a morphism between S = < T, X, W, Q, Y, d, l > and S’ = < T’, X’, W’, Q’, Y’, d’, l’ >) if there exist functions g, h, k such that (Zeigler, 1976):

Each evaluation of d takes the state q and the input x at time t and generates the new state q for the next time step t+1. The output function l takes the state at time t to generate the output, also, at time t. This is represented in Figure 2.3.


Figure 2.3. Graphic representation of a homomorphism 
If S and S’ have the same observation frame, that is: T = T’, X = X’, Y= Y’, W = W’, and _{}is equal to Q, then g and k are the identity functions. The graph in Figure 2.2 becomes as shown in Figure 2.4, and equations 4 and 5 turn out to be:
S’ is an image morphism of S, and the function h is called a homomorphism. If in addition h is
one to one, it is said that there is an
isomorphism between S and S’ (or that S and S’
are isomorphic).


Figure 2.4. Morphism between systems S and S’ under a similar observation frame 
Zeigler (1984, p. 251): explains a valid simplification in these terms: ‘We say that a lumped model [for us, S’] is a valid simplification of a base model [for us, S] in frame E [for us, an observation function l] if the two models are equivalent in E [e.g., a morphism from S to S’ exists] and the lumped model is simpler than the base model with respect to some measure of complexity.’ Example 2.3 Continuing with the example of the linear system, we define H as: 



_{}’ is the state of the system S’ given as a vector of size m. It is supposed that the number of states in S’ is smaller than the number of states in S (that is m < n). So, at any t: 



Or, more explicitly: 



And for S’: 



The two systems have the same number of outputs and inputs. However, system S’ has a smaller number of states. Now, we can look for conditions to satisfy transition and output function preservation (4a. and 5a.; see also Figure 2.5)(here it is assumed time variables _{}, _{}, and_{}are evaluated at time t): 

_{} 

As is known from previous equations: 



Vectors _{}, and _{} are evaluated at time t. For any t and
arbitrary vectors x and q, 4a, and 5a, are true
if: 



Example 2.1. A
case where n = 3, m = 2, k = 3, and l = 2 is: 

Example 2.2.
Again a case where n = 3, m = 2, k = 3, and l = 2:



It is easy to verify conditions 4 and 5. Systems S and S’ have a similar number of inputs and outputs. The size of the space of states is different, three for S and two for S’. We notice the exhaustive partition that function H makes in the space of states of S. The first component of _{}’ depends on the first component of _{}, and the second component of _{}’ depends on the remaining two and three components of _{}. As the relation among states is not one to one, this is not an isomorphism (see Figure 2.5).
Assume a simplified system for S: S’ = < T’, X’, W’, Q’, Y’, d’, l’ >, is given. S’ would be smaller in the sense that Q’ could be inferred from Q, but the opposite would not necessarily follow.
Zeigler identifies at least 4 ways to simplify a model:
1. Dropping of components, descriptive variables, or relations.
2. Replacing one or more deterministically controlled variables by random ones.
3. Coarsening the range set of one or more descriptive variables.
4. Grouping components into blocks and aggregating the descriptive variables also into blocks.
If S’ is a homomorphic image of S, the behaviour of (S’)’ is a subset of the behaviour of (S)’. In fact, it is possible to generate any state and any output of S’ from S, using the homomorphism function h. Should S’ be a valid simplification in a given experimental frame, either of the models generates the behaviour of interest, but it would be cheaper in computational terms to simulate system S’. Moreover, in this experimental frame, the behaviour of (S’)’ is the behaviour of (S)’ constrained. In declarative programming, where functions are given in terms of rules, S’ might be seen as S plus some constraining ‘metarules’ (as behaviour of S’ is accessible form S). This notion of metarules is used by Holland (1998). In the example, those metarules will constrain the space of states of S, eliminating some sort of redundancy.
In such an example a redundancy occurs when given both values q_{2} and q_{3} because only one value, the total q_{2} + q_{3}, is sufficient for calculating the required output, as the simplified system S’ shows. The metarule that would have to be added to S in order to get S’ will imply this condition. Note that columns two and three of C’ are identical. Such a condition would be expressed mathematically as:
The resulting output and the transition from two states differing only in the
two components (q_{2}, q_{3}) will be similar
(under the experimental frame defined above) if the sum of q_{2}
and q_{3} gives the same result.
In this particular example S’ is simpler than S, as the systems are of a similar nature (linear systems) but less memory is necessary to keep information about the states of S’ and less calculations are necessary to generate a simulation state transition  the size of the matrices and vectors involved are smaller than those in S. If S’ and S had different natures, such a comparison might not be so straightforward. Here the measure of complexity is defined in terms of computational resources, namely in terms of the amount of memory necessary to keep a system’s state and the number of manipulations required for a simulation step transition.
Given an experimental frame (e.g., the sort of inputoutput behaviour of interest) and a transition function, the homomorphism might be defined in several ways corresponding to alternative manners of simplifying. However, given a system and an experimental frame, it might not be easy or even possible to find the ideal simplest system, S’, of S under such a experimental frame (assuming it exists). A notion of satisfying seems to be convenient. In addition to the experimental frame and modeller’s goal, available theories, methodologies, and modelling tools (e.g., for simulation) seem to be other factors involved in simplifying.
This formal definition of system homomorphism has been useful in simulation. However, generally in practice this formal (mathematical) notion of homomorphism cannot be applied, as no homomorphism as seen in Zeigler’s formalism exists and alternative weaker notions of homomorphism have to be used for comparing systems. This point will be addressed in more detail in section 2.6, where an illustrative example will be given.
Call S(t) and S’(t) the structures of systems S and S’ respectively at time t. Extrapolating our notion of morphism for a system with static structure, S’ is a simplification of S if S’(t) is an image of S(t) under a suitable morphism. However, to require morphism equivalence at any time instant seems to be too strong, and even unrealistic in practical applications. A weaker notion of ‘similar’ evolution among structures might be more convenient where evolution of the structures at different time instants is allowed. To account for this, more relaxed conditions for a valid simplification when the systems are under structural evolution would have to be looked for.
The homomorphism function might change over time, e.g., h
= h(t). If the function h(t) is given in terms of rules, its change
over time can be implemented by modifying only some rules rather than by
redefining the whole function h(t), as would be done in a procedural
program. This gives a sort of modularity and flexibility. Consequently, to
follow the structural evolution of two systems and express homomorphism between
them seems to be easier in a declarative program than in a procedural one.
MAS built in languages like SDML are an example. Structural change such as elimination and/or introduction of components of the system specified at level 4 (as seen above) or modification of components’ interrelations can be made in modularly. In addition, processes, e.g., dynamic laws of systems, can be modified by changing, aggregating, and/or eliminating rules. Also rules can be shared among agents and processes. This gives a sort of modularity at the level of process implementation useful for considering changes in the dynamical properties of a system. Rules could be seen as an object that might be created, shared, inherited, aggregated, and destroyed. Rules can also be grouped conveniently and reused in different modelling specifications (e.g., a module hierarchy in SDML).
This sort of structural change, though far beyond what is allowed by known simulation languages in industry (e.g., SLAM II, Pritsker, 1995), is still very limited compared with structural change in empirical systems. In empirical systems structural change occurs at ‘infinite’ levels. Even more, in highly evolved systems (or systems at a high level of complexity; see Chapter 4), this process might be creative (Domingo et al., 1996a).
Validation is a particular case of weak homomorphism between two systems. A sort of equivalence under a weaker criterion than the mathematical morphism defined above is applied to check agreement between two systems. A weak notion of homomorphism will be described in subsection 2.6.1. It is supposed there is a bigger system S, e.g., reality, and the model or system to be validated S’. S’ will be a valid model if it is a homomorphic image of S under the chosen weak homomorphism criterion.
Aggregation of models consists in integrating several models representing complementary aspects of a system rather than each component. Simulating each of these components usually requires a lot of computational resources, and so it is convenient to find a way to simplify them. Again, the idea of a weak homomorphism is applied, first to simplify the components, and then to validate the new, ‘bigger’ model resulting from that aggregation. Some researchers in social simulation have proposed creating a cascade of integrated models (Moss et al., 1998b). They describe it as a ‘bottom up’ modelling procedure in contrast to the ‘top down’ modelling procedure used in classical models of economics and climate change. They also argue that validation might be done against collected data in reality or ‘domain experts’.
Finally, two models are aligned if there is a weak homomorphism among them, the idea being to compare models in different platforms, although one model is not necessarily simpler than the other. This notion is used in Axtel et al. (1996) for comparing two programs built independently for modelling a similar case. The criterion used in this work for checking homomorphism is weaker than the one given by Zeigler and discussed above (this criterion will be discussed in subsection 2.6.2).
Several factors are involved in the
difficulties associated with proving homomorphism, among them are: lack of
precision in measuring the phenomena, error propagation in the computer, and
factors little understood in the empirical system an commonly modelled as
random processes. Usually, it is not possible to cancel these restrictions, and
the criterion of perfect agreement in a relation of homomorphism has to be
replaced for one of approximation in practical applications.
In this section the relaxation of the validation procedure for the case of simulations of models with fixed structure will be reviewed (Zeigler, 1976).
‘The validation criterion becomes one of ‘REASONABLE’ agreement between the systems’ outputs The notion of reasonable agreement is formalised in a concept of tolerance. Basically, it is defined as a metric ( . ), over the difference between the outputs (behaviour of interest) of the two systems, S and S’. This difference is required to be smaller than a predefined tolerance. One of the most popular metrics is the square mean.
To calculate this measure of agreement exactly, it is usually necessary to sum over all outputs of interest. Consequently, this requires a post hoc analysis of all trajectories. However, it is not usually possible to generate all the outputs of a system via examination of the simulation trajectories. Alternative looser simplification procedures are needed. Techniques where only a limited number of trajectories are analysed are associated with post hoc inspection of trajectories where weak notions of morphism are applied. Among the existing techniques for doing this looser post hoc analysis are scenario analysis and Monte Carlo techniques. Given certain drawbacks of these existing techniques, additional methods are an open area of research (see section 2.10). It is the main aim of this thesis to propose alternative methods, but yet practical, for analysing simulation dynamics, which rest in stronger notions of morphism than the weak ones to be described in this section (see Chapters 5 to 7).
Different weak homomorphism criteria can be defined. Taking a phrase from Zeigler (1976, 330) (he uses f for  . ): ‘f picks out those aspects of the output CONSIDERED TO BE IMPORTANT FOR DETERMINING ACCEPTABLE AGREEMENT’. As pointed out before, in Zeigler’s simulation theory only quantitative change in the system’s outputs is taken into account, this is also true when checking a weak homomorphism.
Example 2.4. A simplification using a
weaker homomorphism criterion
Suppose there are two MASbased models of a
traderdistributor interaction. There will be two principal types of agents:
Trader and Distributor. Each model is defined as the interaction of several
traders and distributors. A distributor’s main task is: to place orders to a
trader. A trader’s main tasks are price and salessetting, and
priceimitating. The experimental frame will be to observe changes in prices,
sales, and orders over time.
Assume now that in a first model the agent trader contains subagents warehouses and trucks, where trucks are used for delivering goods to distributors and warehouses are employed to keep control of the inputoutput of goods.
Now suppose that in the second model warehouses and trucks do not exist as agents. Data and rules kept in warehouses in the first model are now kept in the trader’s database and the rulebase respectively (e.g., now the level of goods can be represented as: goodLevel(Warehouse, Amount)). Trucks are just obviated and delivering is modelled using a delay function.
The first model of trader needs to be specified at level four (as it has components), while the second model can be specified at level three (see the next diagram for an overview of the first model of a trader).
Other facts about this first model are:
The input of a subagent (truck or warehouse) depends on the output of some of the other subagents (the influencers). In this example, the interaction between a warehouse and trucks serving it is simple: a truck takes produce from a warehouse in accordance with the level of this product, and a warehouse updates its level of product in accordance with the amount taken by the trucks. The states of warehouses and trucks are considered accessible by their container (trader).
Now, let us see how a trader is modelled in the simplified model
traderdistributor:
A simplification between these two models
cannot be based on a homomorphism as it was originally defined, but only on a
weaker criterion. Proofs of strict homomorphism might be more difficult than
the simulation itself and quite unlikely to be achieved successfully. As
previously stated, no strict homomorphism exists in practice. Let us assume
that Monte Carlo techniques are chosen as the weak method for comparing the two
models.
Our experimental frame (see above) specifies interest in observing the behaviour of prices, sales, and orders. Consequently, the evaluation criterion has to be based on these outputs.
The comparison may be made following these steps:
1. A random set of simulation trajectories for each model is generated. It can be implemented using different random seeds for calculating random variables for different trajectories. Random variables are used for modelling certain littleknown aspects in the simulation model. For example, assume that for pricesetting a trader imitates other traders’ prices. Then, a random variable can be introduced for modelling a trader’s choice of another trader.
2. Data of interest are collected from the generated trajectories. In this case data about sales, orders, and prices are gathered.
3. Then a statistical test (here the weak criterion for comparing the two models) is applied to check the hypothesis that the two samples (e.g., each pair of samples of orders, sales, and prices) are coming from a similar statistical distribution and so are statistically similar. Among the methods for making this comparison is the nonparametric Rank Sum Test (Hoel, 1966). Should the test prove successfully, it would be said that the models are equivalent in accordance with this weak notion of homomorphism. As the second model is simpler than the first one (notice that it has less components and less variables), there would also be a valid simplification.
Notice the weakness of this procedure in that the conclusions valid for the explored subset of trajectories are extrapolated by using probabilities to the whole space of trajectories, even though unexpected things can happen at the randomly left trajectories. As previously stated, it is the purpose of this thesis to propose alternative ways for doing the searching for trajectories, and then, based on this, to define alternative notions of morphism.
In simulations where the structure of the model undergoes qualitative change, the experimental frame is generally defined not only in terms of quantitative outputs but also in terms of the structural change of the system; that is, qualitative changes are an aspect of interest. For example, in a MASbased simulation where agents are eliminated and introduced, the behaviour of interest might be the number of agents of a certain type appearing at the end of a simulation. Notice that in this case quantitative measures can be defined over the qualitative change.
So, a way for doing the qualitative comparison is by defining quantitative measures over qualitative behaviour. Illustrations already exist in the literature, for instance, that given by Axtell et al. (1996) for the alignment of models. They compare the average number of stable regions observed in the simulation of a model of cultural transmission. In this experiment, the factors are the number of cultural attributes, the attribute’s levels, and the size of the territory where the interaction happens. The statistical comparison is made only at one time instant of the simulation (at the end of it). Axtell et al. also mention an alternative procedure using statistics: to observe if certain internal relationships among variables hold in both models. They call this comparison ‘relational’ equivalence, and the statistical one ‘distributional’ equivalence.
In a simulation processes of three types can be identified, (1) those programmed or explicit in the simulation design (which can be used for verification); (2) those not clearly given in the design but desirable in the model as well as being well known in the modelled system (which can be used for validation); and (3) those called open aspects, which are little understood in the target system and about which a simulation might give hints and help a modeller hypothesise about the behaviour of the model and, extrapolating, about the behaviour of the target system.
For example, in an eventdriven simulation of a queue system, the process of arrival of entities into the queue might have been programmed to follow a probabilistic distribution. This first sort of behaviour can be foreseen and so is not of interest for validation. This is an aspect to be verified. Verification can be achieved by comparing the design of the model with some formal specification. In fact, verifying a model consists in comparing the structure of the model with some specification given by a theory.
On the other hand, in the eventdriven simulation a modeller might notice certain behaviour about the size of the queues not directly given in the simulation design. Checking if the corresponding behaviour in the target system  which may supposedly be measured in some way (e.g., via a statistical sample of the behaviour of interest)  coincides with behaviour in the simulation is what is called validation of the model.
Finally, there should exist many other features a subject (a modeller) does not comprehend well in the dynamics of the modelled system and which he wishes to understand better by observing the simulation. For example, some special features called emergent tendencies are worthy of special attention in social simulations.
Strategies in eventdriven simulations are based on the use of a future event list (FEL). Each event is associated with: the time when it will be activated (activation time), possibly additional conditions for the event to be activated once the timecondition is satisfied, and the consequences of the event (namely changes to be made in the system’s state and the scheduling of further events). Events in the list are ordered by their activation time. For example, in a queue system, the event ‘arrival of an entity into the system’ will be associated with the arrival time (activation time of this event), other conditions for such an arrival to happen, changes to be implemented in the state of the system (for example, to place the entity in the queue if the queue is smaller than a certain size), and, finally, the scheduling in the FEL of a new arrival.
As can be seen from these examples, the FEL is used for guiding the state transitions over time. Size of time steps is taken as the difference between the time of activation of each pair of consecutive events in the FEL. Two of the most popular strategies in eventdriven simulation are simulation by events and simulation by processes. In eventdriven simulation each event is programmed in a separate module and a main program executes that module corresponding to the next event in the FEL. In simulation by processes, the process an entity carries out is the key aspect. The program consists in a sort of net for the ‘lifecycle’ of the entity. For example, in a queue system, the entities are those units queuing and their cycle of life is given by a succession of events: to arrive, to queue, to be served, to leave. The program consists of a net of nodes following the temporal order given by the entity’s lifecycle, where the consequences of each event (as well as possible decisions the entity has to take or decisions of the system, e.g., gates) are programmed. An event fires as the entity reaches the associated node(s). So nodes are used to represent: entrance to the system, queue, service, output of the queue, and exit (destruction of the entities). Examples of languages where these strategies have been implemented are SIMAN, SLAM, GLIDER, and SPSS. This sort of simulation is common in industry.
The basic aspects of a system with variable structure and its simulation will be reviewed in conformity with the ideas of Domingo et al. (1996, 2000); Testa et al. (1999), and Heylighen (Heylighen, 1989, 1991, and 1995). Then speculation about simulating structural change according to Domingo’s ideas and a MAS will be presented.
Testa et al. consider it fundamental to recognise change at both levels: at the level of the static structure (what he calls form) and at the level of the dynamic structure (function). They call this change ‘fluctuation’. More precisely, they talk about ‘fluctuation within a probabilistic range’. They argue that there is a mutual dependence among the two changes and note that such an interdependence cannot be ordered either hierarchically or causally. They describe the processes of dissolvence and emergence as the two facets of the same coin where a whole (system) arises from its components (subsystems). The first is the rise of new properties of the whole and the second the constraint of its components ‘in a synergic process of integration and reorganisation’. Examples of biological systems are given.
In Domingo et al. (2000), another concise idea of structural change is found, for here they affirm that ‘in structural change systems change the behaviour, the components and the relations among them.’ They identify other processes leading structural change in addition to that of aggregation described by Testa et al. Among them are bottomup and topdown changes. In the former case the process of structural change is driven from above  the whole system drives the constraint in, e.g., properties of the components and elimination or introduction of new components. In the latter case, the parts are responsible for directing that process. Moreover, they argue that the two processes can be present simultaneously. For example, a revolution can be a bottomup change led by members (components or actors) of a state (e.g., groups, associations, people) creating changes in the whole system (the state). The opposite happens when there are economic associations among countries. Then the new rules for the economic interchange among the involved countries are elaborated at the top level and then ‘imposed’ upon the lower levels of the system (the economic actors). However, the systems these examples refer to can present both kinds of changes over a time period of enough length. For example, in the case of a revolution, after the new political force takes power, it starts promoting changes from above (topdown) as it implements, for instance, its economic and educational policies.
Domingo identifies two main problems for the simulation of structural change (SC):
· First, those related to the laws of change, that is, aspects related concerning when to change the structure and how the variation selection of structures will be given.
· Second, that of the level of aggregation. In nature, the aggregation of subsystems seems to happen at many levels (perhaps at infinite levels) starting from small atomic levels possibly still unknown in physics. Obviously, its modelling in a computer cannot be attempted. In this device only certain levels of aggregation of structural change can be modelled (the relevant ones for certain purposes and in accordance with the available modelling tools).
A graphical representation of several levels of control, where structural change is allowed, is given in Figure 2.6.


Figure 2.6. Graphical representation of several control levels where structural change takes place 
Example 2.5. MASbased
Simulation: A Weak Case of Simulation of structural change.
In MAS some levels of aggregation are at the level of agents. Agents can be created, destroyed, and their rulebase modified. There are several levels of aggregation but the number of levels is finite. Moreover, these structures (agents) and levels of aggregation are fixed. Another level of aggregation is that of the cognitive model of the agent. Examples of agents’ internal models are presented in Moss et al. (1998a). Here aggregation occurs at the level of rules. In the following pages we will present examples of how the problems averted to by Domingo have been handled in MAS.
At the level of aggregation of agents, since structures are fixed, the first problem, (namely the process of variation selection) is solved in an easy way – it is simply obviated. At the level of cognitive models more elaborate procedures have been used: evolutionary programming. Here rules are evolved using genetic algorithms or genetic programming (Edmonds, 1998). These two examples of simulation of SC are part of two strategies Domingo et al. propose to solve the named problems. Structural change in the case of an agent can be a decision either of the environment or of the agent itself. For instance, a trader in a market might be eliminated by the economic environment (e.g., if his profits are too low) or he may choose to leave the market. A cognitive model can suffer structural change when the agent undergoes a new experience[1].
Both Heylighen and Domingo recognise the importance of a metamodel when modelling structural change. The metamodel, or controller, would be responsible for solving the problems Domingo has indicated: namely, to decide when the change happens, to implement the process of variation selection of structures, and to choose the aggregation level (see also Heylighen, 1991b; Domingo et al., 1996a). Several aspects of their proposal coincide with the strategy followed in a technique to be presented in Chapter 5 and implemented in the example contained in Chapter 7.
A post hoc analysis of a simulation consists in examining outputs obtained from the simulation (as has already been described in this chapter). This is the strategy used in many simulation studies to understand a simulation after it has occurred owing to difficulties in studying it from its design. Conclusions of this analysis can be extrapolated to the modelled ‘real system’ (if it exists) under certain conditions (e.g., the morphism criterion discussed in previous sections). In this thesis a post hoc analysis is of special interest for assisting in explaining emergent tendencies in a simulation.
Usually it is not possible to include all possible simulation trajectories in a post hoc analysis of a modelbased simulation, as might be suggested by a strong notion of morphism like that of Zeigler introduced in section 2.3.3. An exhaustive generation of simulation trajectories in a simulation is generally impracticable owing to the limited computational resources available to a modeller. It might also produce too much information and make the analysis of the outputs difficult. Because of this, alternative approaches have been developed along the weak idea of morphism offered by the notion of approximation introduced in section 2.6. Among these alternative methods are scenario analysis and Monte Carlo techniques.
Scenario analysis consists in analysing a modeller’s selected subset of trajectories. On the other hand a Monte Carlo Analysis consists in analysing a randomly chosen subset of trajectories. In a Monte Carlo study, conclusions from a ‘big enough’ sample of trajectories are probabilistically extrapolated to unexplored trajectories (see section 2.6.1).
Both of these methods leave unexplored trajectories. Neither of these explorations is exhaustive. In the first method the omitted trajectories depend on the ‘subjective criteria’ a modeller applies to choose the trajectories to be explored and, in the second one, they are left randomly. Because of this the analysis is limited, as the conclusions cannot be generalised and applied in wider theory – only probabilistic generalisations are allowed (in the second method).
On the other hand, probabilistic extrapolation is valid only if small changes in the settings of the simulation produce small changes in the outputs of the simulation – e.g., if outputs are continuous with the settings of the model. As this assumption is not valid in complex systems (e.g., in systems with chaotic behaviour), a Monte Carlo analysis of a simulation of a complex system might omit trajectories likely to happen in the ‘real system’ where the behaviour of interest might be quite different to that observed in the explored ones. This arbitrariness in the chosen trajectories engenders difficulties for generalising conclusions when simulating complex systems.
The dynamics of complex systems are usually very sensitive to changes in the properties of the components and, in general, to the evolution of the structure of the system itself, since small changes in the properties of the system might result in big changes in the outcomes of the system. For example, the behaviour of a chaotic system is very sensitive to changes in the initial conditions of the simulation; a slight change in the initial conditions may produce big alterations in the processes this system is undergoing (e.g., that system (in weather forecasting) defined as the surrounding of a geographical area determining the weather conditions of this area). Another example is a social system. In a social system chaotic behaviour is present because of its high level of complexity. It is sourced mainly in the high number of entities (humans) interacting in a society and in the complexity of each of these entities (see the discussion concerning modelling systems at high levels of complexity in Chapter 4, especially section 4.3.3).
Similar susceptibility is expected to be present in the dynamics of a simulation of a complex system. For example, phenomena in a MASbased simulation of a social system might be unexpectedly contingent on changes in the parameters of the model and the choices of the agents, so that small changes in parametersettings or in agents’ decisions might result in significant changes in the simulation outputs. This inappropriateness of modelling complex systems by using classical modelling approaches based, e.g., on averages, has already been discussed by many thinkers. One of them, Crutchfield (see, e.g., Crutchfield, 1992), argues that in these systems, ‘fluctuations dominate behaviour and averages need not be centred in around the most likely value of its behaviour. This occurs for high complexity processes … since they have the requisite internal computational capacity to cause the convergence of observable statistics to deviate from the Law of Large Numbers’ (Crutchfield, 1992, p. 35, in the version of the paper available at http://www.santafe.edu/projects/CompMech/papers/SATTitlePage.html). In this statement, Crutchfield seems to be considering systems at a high level of complexity, e.g., those with a vicarious mechanism (whose ability and activity he refers to as ‘internal computational capacity’), such as human systems. Aspects of these systems and their simulation are examined in section 4.3.3.
All this creates doubts about the appropriateness of techniques that arbitrarily leave simulation trajectories unexplored as well as about the use of statistical summaries for studying simulation outputs. This thesis is aimed at developing alternatives to such existing methods, for studying complex systems: on the one hand, stronger notions than that of approximation for overcoming drawbacks in existing techniques but more practical than Zeigler’s original notion of morphism (for this, ‘constraintbased exploration of simulation trajectories’ and a ‘platform of simulation architectures’ will be suggested), and, on the other hand, alternatives to the use of ‘statistical summaries’ for analysing simulation outputs are needed (in this sense, the ‘envelope of simulation trajectories’ will be proposed).
Ideas not commonly used in simulation such as those implemented in theoremproving and Automatic Reasoning (described in Chapter 3) will be introduced for exploring the dynamics of a system. A proof of a theorem in a simulation rests in a more exhaustive exploration of the dynamics of a simulation than that carried out in the traditional methods named above (see Chapter 5 and, in particular, section 5.5). A proof will allow a modeller, on the one hand, to explore a fragment of a simulation theory, and, on the other hand, it will permit the implementation of measures of behaviour other than averages in the explored simulation theory. As we are interested in studying emergent tendencies, we propose, as an alternative measure of behaviour, the envelope of the tendency in the explored fragment of the simulation theory. Hence, the methodology to be proposed should be a valid alternative to existing methods for analysing the simulation of a complex system.
In addition, this methodology will be in line with Heylighen’s call for computational mechanisms for helping a social agent (in this case a modeller) to cope with the complexity of the social system it inhabits (see section 4.3.4).
One of the main purposes of this thesis is to develop a methodology to analyse and understand the dynamics of simulation in MAS. It is of interest to analyse regularities in the dynamics of a simulation not explicitly given in the simulation design and which are relevant for understanding the modelled system, despite being poorly comprehended by the modeller (these regularities will be called ‘emergent’). As observed in section 2.10, existing methods for analysing the dynamics of simulations of complex systems have serious drawbacks and this thesis aims at looking for alternative approaches.
As
was shown in the previous chapter, those existing methods for investigating
simulation behaviour allow one to draw only limited conclusions about the
dynamics of the simulation in only very specific spaces of the simulation
theory. Those methods explore only a single simulation trajectory at a time and
use the notion of approximation for proving morphisms. It is the intention in
this thesis to investigate about more powerful methods for analysing such
dynamics, that will permit one to reach more general conclusions and to define
stronger notions of morphism than those allowed when using the notion of approximation.
Concretely, this thesis aims at developing methods for proving theorems about
the dynamics of a simulation. As it is usually difficult to explore the whole
dynamics of a simulation (e.g., about the whole simulation theory), this thesis
seeks to find methods to prove theorems with respect to a subspace of the
space of the simulation dynamics and, correspondingly with respect to a
fragment of the simulation theory.
Though in this thesis a methodology for proving theorems in a simulation will be developed, this work is also exploratory in the application of theoremproving strategies for proving tendencies in the dynamics of a simulation. There have been no previous developments in this line, as far as is know. Because of this, a review of a wide variety of existing methods, not only those directly related to the strategy to be proposed in this thesis, will be considered in this chapter. This review might be used for classifying: the theoremproving strategy followed in the theoremprover to be used to implement an example (e.g., OTTER), existing methods for simulation, and the theoremproving strategy for proving theorems about the dynamics of a MAS to be presented in the next two chapters.
The introduction to simulation given in the previous chapter, together with the review of formal aspects of logicprogramming and theoremproving to be presented in this chapter, will provide the theoretical background for a move towards the methodological developments to be given in the next chapters of this thesis. The main intention of this chapter is to provide a review of the different strategies for theoremproving.
First, in section 3.2, basic conceptual
aspects of proving theorems, using computational algorithms, will be shortly
addressed. Then, the difficulties that have been found for finding a good and
general computational algorithm to prove satisfiability/unsatisfiability of a
formula will be briefly touched upon. Also, in this section, a basic conceptual
framework related to proving theorems in a theory useful for the rest of the
presentation will be offered.
Then (in section 3.3), similarities/differences between exploring dynamics of a computational program in theoremproving and in a simulation will be reviewed. The intention is to preview the most straightforward similarities between simulation runs and explorations in theoremproving. Direct parallels between the search strategy called ‘model exploration’ in theoremproving and generation of trajectories in simulation will be found.
Section 3.4 will discuss in brief seminal work for proving in computational models. The initial interpretationbased exploration of ‘logical models’ in a theory, namely Herbrand’s universe and Herbrand’s theorem, will be addressed. Herbrand’s theorem is the basis for the more efficient methods for checking falsity of a set of clauses in firstorder logic. This theorem became the fundamental reference for developing resolution, the most widely used procedure for proving. This section provides the starting point for a more comprehensive review of theoremproving strategies in section 3.5, whose methods are based on these two achievements of Herbrand.
Having presented Herbrand’s foundational work for theoremproving in section 3.4, the main strategies for theoremproving will be reviewed in section 3.5. It will include a consideration of the most popular search procedures and strategies in theoremproving. Two main branches of theoremproving approaches will be presented in accordance with the orientation of their inference procedure, which might be either predominantly semantic or predominantly syntacticoriented. Simultaneously, examples of theoremprovers using these procedures and strategies will be offered. First, the syntactic methods will be presented. These have been the most successful ones. In this group is the theoremprover OTTER. OTTER will be used to program the case study of this thesis and so will be an important reference as a source of ideas for developing the methodology to be presented in Chapters 5 and 6. This review may be used to describe the main aspects of OTTER and other theoremprovers found in the literature. However, neither the simulation method to be proposed in the next chapter nor the common simulation methods correspond well to a syntacticdriven proof. Then, the other group of strategies, that consisting of the predominantly semanticoriented, will be reviewed (in subsection 3.5.2). In this group will be found the socalled modelbased exploring approaches and, among them, tableaux. This sort of search has similarities with the method to be proposed in the next chapters, but again this method does not fit completely well in the sort of search described in this subsection.
However, the given taxonomy, as also happens with any other given classification, is somewhat arbitrary, as most of the theoremprovers are in part semantically and in part syntactically oriented. Hence, it will be worth going further and analysing strategies for theoremproving using additional criteria.
To this purpose section 3.6 will be offered. In this sense, in subsection 3.6.1 additional criteria for classifying theoremprovers are given. Then, using the criteria provided so far, the main aspects of Bonacina’s (1998, 1999) classification are recapitulated in section 3.6.2. As, once again, neither the proving strategy to be developed in this thesis nor other simulation methods fit well in the given (Bonacina’s) taxonomy, a further discussion will be presented in subsection 3.6.3.
Having opened the panorama of theoremproving strategies, the main aspects of a new tendency in logicprogramming  constraint logicprogramming and its variant, rulebased constraint logicprogramming  will be considered (see, e.g., Frühwirth et al., 1992). This new area of research seems to be relevant to achieving efficient methods for exploring dynamics in simulations. There, inference procedures using a constraintdriven search as an alternative to unification are implemented. It appears that there, novel and promising ideas for efficient implementations of exploration of behaviour in a simulation can be found.
Finally, the usefulness of metareasoning for
an efficient exploration of the dynamics in a computational program and, in
particular, for implementing contextdriven inference procedures will be
highlighted. Contextoriented search seems to be convenient for exploring and
proving theorems in the dynamics of a simulation.
The problem consists in finding a proof procedure to verify the validity or inconsistency of a formula or a theorem with respect to a theory. In simulation, a theorem might represent a tendency in the dynamics of the simulation.
According to some authors (e.g., Chang and Lee, 1973), such a problem was first tried by Leibniz, then by Peano, and, in this century by Herbrand’s school. Nevertheless, a general procedure for proving theorems in a theory was proved impossible by Church and Turing in 1936 (Chang and Lee, 1973). In any sufficiently expressive formal system, there will always be invalid formulas for which these procedures will never decide. For example, ‘in certain cases the generation of clauses never stops, because no finite database satisfies all clauses, but a contradiction does not arise either. This is because of the ‘undecidability of satisfiability’ (Stickel, 1988). However, there are procedures that are useful for attempting to prove certain valid formulas.
In logicprogramming, a method or program able to provide an answer (in this case, to the dichotomic question of whether a formula is satisfiable or not) within a finite delay is called an algorithm, while those that can provide and answer when such an answer is positive but there is no guarantee of getting an answer when it is negative, are called semialgorithms or procedures (Gochet et al., 1988). Similarly, it is said that a theory is decidable if it admits a decision algorithm and semidecidable, or partially decidable, if it only admits a decision procedure. Methods for proving the validity of a theorem (e.g., resolution) for firstorder logic are procedures (Gochet et al., 1988).
In consequence, in this chapter the aim is to discuss appropriate procedures for proving in particular situations. As a preliminary step towards this goal, the main ways to check the validity of a theorem with respect to a computational theory will now be reviewed.
According to Chang and Lee (1973, p. 45) there is no guarantee of finding any procedure to check the invalidity of an invalid formula. On the other hand, no general procedure exists for verifying the validity of a valid formula. However, it is always possible to find a specific procedure for checking the validity of a particular valid formula.
The most important approach for proving
validity of formulas in theoremproving was given by Herbrand in the 1930s. The
first algorithm for implementing Herbrand’s method was given by Gilmore in
1960. Then, this algorithm was modified, the most important improvement being
that given by Robinson. These algorithms verify the validity of a formula by
detecting inconsistency of the negation of the formula. The important point
here is that: if the formula is valid – and obviously such detection is not
possible  the program will halt after a finite number of steps (Chang and Lee,
1973).
In this thesis the phrase ‘logical model’ will be used to refer to the concept of model in the context of logic. This will help to prevent confusion, as the notion of model in logic and in logicprogramming is different from the concept of model in modelling and simulation, which has been used until now in this thesis.
First, some basic concepts will be defined in order to provide a context for the notion of model in logicprogramming (Gochet et al., 1988). However, only some notions will be covered and other more basic concepts, such as predicate, clause, literal, function, term, constant, proposition, unification, and predicate, will be assumed as known.
Seven terms that will be frequently used below and have a special significance for understanding the notion of theory (e.g., that implicit in a simulation) and proofs in a theory are now defined:
Signature: collection of predicate and functional constants.
Language: set of terms and formulas generated by the signature through the syntactical rules of predicate calculus.
Structure: relative to a language is an interpretation of this language.
Theory: relative to a language is a set of formulas of this language.
Axioms of a theory: that set of formulas in a language defining the theory.
Theorem in a theory: logical consequence of the axioms defining the theory.
Logical model of a theory: a structure for which all formulas of the theory are valid.
A logical model of a theory in predicate logic might be given with reference to ground terms of the language, that is, specifying whether each ground term is true or false. Then, the definition of interpretation given in the semantic specification of the language for variables and formulas can be used to determine whether a variable or a formula is valid under a certain logical model or under some interpretation. Alternative techniques for defining a logical model or a set of logical models are: specifying only the set of valid ground terms (the remaining ones are assumed to be false by default), or by a formula. Figure 3.1 illustrates the interrelationship among these concepts


Figure 3.1. Graphic representation of the relation among the concepts: Language, Signature, Theory, Axioms of a theory, and Theorems in a theory 
Example 31: Signature: collection of predicate and functional constants.
Signature: P( , ), Q( , ), R( )
Language: any formula A ¦ B, where A
can be P, Q, or R valued on certain variables, and ¦ can be any
of the operators commonly used in the literature for defining a propositional
firstorder logic {v, ʌ,
…}
An example of a theory is S = {(1)~ P(x,
y) v ~ Q(y,z) v R(x), (2) P(x,y) v R(y,z), (3) Q(x.y) v R(x)}
A theorem for this theory is R(x).
Assuming a propositional language, S = {(1)~ P v ~ Q v R, (2) P v R, (3) Q v R}:
An interpretation (signature) would be {R = Q= true, P = false}
The formula R can be used to represent the set of logical models M = {R = true, Q = V_{1}, R = V_{2}} where V_{1} and V_{2} are in the domain {false, true}.
In general, a logical model search procedure for proving is an interpretationguided exploration of logical models. An example of a logical model search using backwardchaining is tableaux. Also, forwardchaining logical model procedures have been implemented, for example eventdriven simulation and partitioning of rules in some declarative MAS, as will be seen below.
Logicprogramming and theoremproving can be applied to many research subjects. In this thesis its particular interest is its use for proving tendencies in the dynamics of a simulation. To make clear the relation between simulation on the one hand and, logicprogramming (and especially theoremproving) on the other, the relevant aspects of the dynamics of a simulation and inference procedures in logicprogramming and theoremproving will be reviewed. The main similarity is found between what in simulation is called a ‘trajectory’ and what in logics is called the logical model of a theory.
A trajectory of a simulation corresponds to a logical model or valid interpretation of a theory in logics. In fact, the generation of trajectories in a simulation can be seen as a particular case of logical model generation. It is a generation of logical models for the theory represented by the simulation program. However, it is not always required to know all valid facts in a logical model, as is the case in tableaux, in order to check theorems in a trajectory. A simulation implemented using declarative programming will be expressed in terms of clauses and there may exist alternative ways of generating logical models corresponding to the different possible simulation trajectories. A formula will be a theorem of the simulation program if it is true in all simulation trajectories. A semantic proof of certain regularity in a simulation can be implemented by generating all trajectories and observing whether the regularity holds in all of them (this is a ‘logical model checking’). This assumes that, as is common in simulation, a finitestate structure representing all logical models exists.
Simulation trajectories are usually generated following an eventdriven or at discrete, equally spaced intervals of the independent variables. This is the general case, for example, in MAS and finite difference methods for solving differential equations. Its generation usually consists in a time and/or spacedriven generation of states starting from a certain initial state. This is a sort of forwardchaining inference. For instance, in the simulation of a differential equation, the simulation might follow a temporal and/or a spatial order. Consider, for instance, the case of a twospace heated plaque whose temperature at the internal points changes over time and is different for different points. The differential equation might be like this:
_{}; where: T represents the temperature, x and y are the spatial variables, and t represents time. These sorts of equations are solved using finite differences: the partial derivatives are replaced by finite difference approximations, then a set of finite values in the range of interest is chosen for the independent variables x, y, and t, and, finally, T is obtained for the chosen points of the independent variables stepbystep, starting from the known values of T in the boundaries of the plaque. Should this flux be null, time is no longer a variable of interest, although it may still be interesting to know the plaque’s temperature at each point; then the simulation steps would only be over the spatial edges. In this case the simulation steps follow only a spatial sequence. In the case of the simulation of processes involving humans (for example, simulation of a queue system in industry, in a road, or in a bank, or simulation of social interaction in a market), the dynamics is usually carried out following a temporal sequence.
Similarly to what happens in simulation, many logicbased computational systems follow a forwardchaining strategy. Consequences are generated as the antecedent of inference rules match facts already existing in the database. This is a strategy also used in theoremproving. Generations of trajectories over time or in temporal logical model exploration have been formalised in Temporal Logics. See, for example, Fisher et al.’s proposal of a clausal resolution procedure for discrete temporal logic (Fisher et al., 2000). Obviously, theoremprovers that use forwardchaining inference have similarities with simulation.
A common strategy for proving in computational models, which is extendible to simulation, is to add the negation of the theorem into the database and then show that this causes a contradiction. A drawback of this sort of search is that many irrelevant facts (for the proof) may be generated before the contradiction appears. To handle this problem, heuristic strategies have been developed. More details about these procedures will be given below.
In contrast to this, searches in logicprogramming (e.g., in Prolog) are not usually forwardchaining but backwardchaining or goaldriven. A goal is managed as a question to be answered with respect to new goals or facts. Assume this is a goal at level 1. If this goal matches the head of a rule (consequent), the body (antecedent) of the rule (with the respective update of the variables according to the variable unifications) becomes the new goal in a next level (level 2). This new goal might consist in a conjunction of predicates. In this case, each of those predicates would be a subgoal to be satisfied at the new level – thus, a new list of subgoals is constructed. The next task is to check if each of these goals is satisfied. Then, one of them is taken as the goal to be treated. Once the head of a rule matches this subgoal, then a new list of subgoals at another level (level 3, given by the antecedent of the matching rule) is set. The search stops as soon as all resulting goals become true, that is, as soon as all the goals are shown to be facts.
If during that search new subgoals have priority over previous targetgoals to be tested (e.g., goals are listed in order LIFO: LastIn FirstOut), the search is called depthfirst. On the other hand, if new subgoals are considered only after previous target goals (e.g., goals are arranged in order FIFO: FirstIn FirstOut), the search is called breadthfirst. Generally a depthfirst search generates less data than a breadthfirstsearch. It is the search commonly implemented in logicprogramming (e.g., in Prolog).
Despite these differences in how the inference is driven, the inference procedures in both logicprogramming and resolutionbased theoremprovers are variants of the semantic and syntactical methods to be explored below.
To summarise, in some aspects simulation is closer to logical model generation in logicprogramming and theoremprovers than to logicprogramming languages such as Prolog, as those procedures and simulation usually follow forwardchaining inference procedures while Prolog’s inference procedure works in backwardchaining. On the other hand, however, simulation also has similarities with certain backwardchaining search procedures like tableaux, as they both follow a logical model generation strategy. Accordingly, in principle it seems convenient to try proving in simulation using procedures already implemented in forwardchaining theoremprovers and in logical model generation. Nevertheless, syntactic backwardchaining methods appear attractive to lessen certain problems (e.g., the huge amount of accumulated data) appearing when implementing logical model generation and forwardchaining methods. A recently developed approach is constraint logicprogramming, which seems promising because of its flexibility for driving the search by exploiting semantic information in the data rather than using only traditional unification. Aspects of this approach will be utilised in this thesis as the methodology to be proposed in Chapter 5 consists in certain constraintbased explorations of trajectories.
The first attempts for checking the unsatisfiability of a set of clauses before, in the next section, going on to those commonly used in theoremproving will be presented in this section. It is common to attempt to prove the unsatisfiability of clauses. A theorem is proved by showing that its (classical) negation is unsatisfiable.
The barest procedure for proving the falsity of a set of clauses S is to check if they are false under all possible interpretations of the theory. Evidently, there might be a huge number of possible interpretations making this task impossible. This is only realistic in a few cases and not in those of interest in this thesis.
Notice that this procedure is not syntactic but semantic. Each interpretation for which a theory is valid is a logical model of the theory. Other approaches for proving based on interpretations will be reviewed in section 3.5.
In order to improve the previous procedure, it seems convenient to find a subdomain SD of all possible domains D of clause interpretations, so that, to know if a set of clauses S is unsatisfiable, it is necessary and sufficient to check the interpretations of S in SD. The first answer came from Herbrand and the subdomain is called Herbrand universe of S (for more details, see Chang and Lee, 1973; Wos, 1988; Gochet et al., 1988). Chang and Lee (idem, p. 52) define it in this way:
‘Let H_{0} be the set of constants appearing in S. If no constant appears in S, then H_{0} is to consist of a single constant, say H_{0} ={a}. For i = 0, 1, 2, … let H_{i+1} be the union of H_{i }and the set of all terms of the form f^{n}(t_{1}, …, t_{n}) for all nplace functions f^{n }occurring in S, where t_{j}, j = 1, …, n, are members of the set H_{i. }Then each H_{i }is called ilevel n constant set of S, and H_{¥}_{,} or lim_{i}_{®}_{¥}_{ }H_{i,} is called the Herbrand universe of S.’
Examples:
a) if S = {P(a)}, then H_{0} = {a};
b) if S = {P(a), P(f(x)), Q(g(y))}, then
H_{0}
= {a};
H_{1}={a,
f(a), g(a)};
H_{2}=
{a, f(a), g(a), f(f(a)),f(g(a)), g(f(a), g(g(a))};
H_{2}= {a, f(a), g(a), f(f(a)),f(g(a)), g(f(a), g(g(a)),f(f(f(a))),… }.
Instances of a clause C obtained by replacing variables in the clause C by members of the Herbrand universe are called ground instances. In the second example above, P(g(a)) and P(f(g(f(a)))) are examples of ground instances of clause P(f(x)).
However useful Herbrand universe is, it is usually hard to check all interpretations over it because it is still too big. Further steps toward more useful procedures were encouraged by Herbrand’s theorem. Chang and Lee offer a version of it:
Herbrand’s Theorem. A set of clauses S is unsatisfiable if and only if there is a finite unsatisfiable set S’ of ground instances of clauses of S.
The importance of the theorem is that it will be sufficient to have a finite set S’ of unsatisfiable ground instances of S to know that the whole set S is unsatisfiable. This theorem has become fundamental for developing resolution, the most widely used procedure for proving. The main difficulty for applying this theorem is the requirement of ground clauses. A resolution goes forwards; it has to be applied not only over grounded clauses but also over ungrounded ones (Chang and Lee, 1973).
In this section some of the main approaches in theoremproving will be considered. First, those implementing syntacticdriven procedures based on clause manipulation will be outlined, followed by those that are semanticdriven since they are founded in logical model generation. Among the resolution methods and heuristics to be listed below, there were used in the examples presented in this thesis (see Chapter 7): hyperresolution, the set of support strategy (a particular case of semantic resolution), subsumption, fewestliteral preference strategy, and demodulators. Other, alternative methods currently used in theoremproving or in declarative programming will be presented.
The great advantage of resolution is that it can be applied over clauses having variables. Therefore, the size of the universe of clauses over which it works is usually smaller than when using Herbrand’s universe while the number of interpretations to be considered is still the same. Actually, as resolution can be applied over clauses having variables, many or even an infinite number of interpretations can be considered at a time.
Resolutionbased theoremproving has become a very important area of research since 1965, after the introduction of resolution by Robinson (Chang and Lee). Further refinements and search strategies have been developed, e.g.: hyperresolution (Robinson himself), semantic resolution (Slagle), the set of support strategy (Wos, Robinson, and Carlson), lock resolution (Boyer), and linear resolution (Loveland, 1970; Luckham, 1970) (more details will be given below).
Many successful resolutionbased theoremprovers have been developed. One to be used in this thesis is OTTER (see McCune, 1995; also see wwwunix.mcs.anl.gov/AR/otter/).
The important point in Robinson’s resolution principal is that it generates a new clause from two existing ones. The generated clause will replace the two existing clauses. Then, Robinson’s resolution, also called binary resolution because it uses two clauses to generate the new one, can be seen as an inference rule (Wos et al., 1988). In fact, binary resolution can be applied in different forms; for example, it can be seen as a generalisation of the inference rule that gives (P or R) from: (P v Q) Ù (~Q v R). Moreover, it can be considered as a generalisation of ‘modus ponens’ and ‘syllogism’ (Wos, 1988). Applying it iteratively, a chain of clauses can be generated. If the original set of clauses is inconsistent, then a contradiction occurs in the chain  this is called the completeness of the method. Binary resolution is complete. Obviously, completeness is a desirable attribute for resolution methods. If the set of clauses is satisfiable (there is no proof), binary resolution will halt once no more clauses can be generated. Nevertheless, complete proofs methods are only available for a restricted range of relatively inexpressive logics.
The main advantage of binary resolution is that it is complete and that it does not put restrictions on either of the resolvents. So it is one of the most generally applicable resolution variants. However, it might be inefficient in the sense that other resolution methods might do certain proofs in shorter manner in terms of time or generated data. Moreover, other resolution procedures might be more recommendable in certain situations, for instance, in keeping with the characteristics of the clauses over which the proof is going to be executed. For example, when translating a simulation program into a theoremprover, it may be convenient to see the original data of the simulation program (e.g., that given the initial state) as unit clauses and the rules of the simulation program as multiunit clauses and then apply hyperresolution (see below) in the search so that the multiunit clauses operate as the inference rules (see below and Wos, 1988). Sometimes, theoremprovers allow the user to choose the resolution method(s) to be applied.
In the following some alternative resolution methods will be informally reviewed as some of them are used in the theoremprovers of interest in this thesis, e.g., in OTTER. Then, the different strategies used together with resolution for improving the search in a theoremprover will be considered. These strategies are heuristics aiming to make the search shorter and computationally less expensive.
Semantic resolution is one of the first improvements over binary resolution in the search for methods to decrease the number of redundant clauses.
The main idea is to divide the set of clauses S into two subsets S1 and S2, preventing resolution within clauses in a subset. This can be explained by using an example from Chang and Lee:
Example 33.
S = {(1)~ P v ~ Q v
R, (2) P v R, (3) Q v R, (4) ~R}
<