Like all sophisticated process languages, LCC specifications can be complex so it is not always easy for the designer of an interaction to be certain that the specification generates the interaction that he or she had in mind when writing it. To raise confidence that it does behave as intended it is useful to be able to explore the LCC behaviours prior to deploying the interaction on the OpenKnowledge system. There are numerous ways of doing this but here we explore three of these: the first is simulation via trace generation from the LCC specification; the second is temporal property checking of these traces; the third is the inclusion of a (virtual) real-time environment in the simulation.

• 1 Generating Behavioural Traces (Meta-Interpretation)

  LCC is an executable specification language and the style of execution of LCC in the OpenKnowledge kernel is based on the idea of unfolding the clauses of each peer's role definition as a means of representing change in the state of the interaction. Although the kernel is Java based for portability, Prolog is a more elegant language in which to describe unfolding. For this reason the behavioural trace generator (and the other related LCC mechanisms in Section 3) are implemented as Prolog meta-interpreters. A detailed description of the process of unfolding to generate a trace is given in the LCC operational semantics definition. The basic idea, however, is that the meta-interpreter "walks" through the role definitions, sending messages in sequence and simulating concurrency via non-deterministic choice. For example, the LCC interaction model:

  a(r1, X) ::
      ( m1 => a(r2, Y) or m2 => a(r2, Y) ) then
      M <= a(r2, Y).
  
  a(r2, Y) ::
      ( m1 <= a(r1, X) then m3 => a(r1, X) ) or
      ( m2 <= a(r1, X) then m4 => a(r1, X) ).
  

  would be capable of generating the following two traces for peer p1 in role r1 and peer p2 in role r2:

  [m(p1, m1 => a(r2, p2)), m(p2, m1 <= a(r1, p1)), m(p2, m3 => a(r1, X)), m(p1, m3 <= a(r2, p2))]
  [m(p1, m2 => a(r2, p2)), m(p2, m2 <= a(r1, p1)), m(p2, m4 => a(r1, X)), m(p1, m4 <= a(r2, p2))]
  

  where each element of the trace above is either a message, M, being sent from peer S to peer R (m(S, M => R)) or is a message being received by peer R from peer S (m(R, M <= S)).

  The source code for a generating traces from LCC specifications (along with some example specifications can be downloaded as a zipped folder.

  This sort of simulator is useful both for exhaustively exploring the state space for interactions (a ropic of the following section) and for running multiple simulations of interactions with random selections of events at choice points in the trace generation. This latter method was used in developing our peer rank algorithm (used in our bioinformatics testbed) because it gave us a way of rapidly running thousands of interactions in concert with the peer rank reputation mechanism without having to set up a much more complex (and less easily controlled) test harness for the OpenKnowledge kernel. The peer rank algorithm eventually was provided as a service for the kernel but only after this initial testing phase. A description of peer ranking and some of the simulation results appears in our technical report on peer rank simulation. The full source code for the peer rank simulator, plus test interactions, downloaded as a zipped folder.

• 2 Checking Temporal Properties of Interactions (Tabled Resolution)

  In Section 1 our concern was to be able to generate individual traces corresponding to a permitted behaviour in an interaction specification. Sometimes, however, we are interested in knowing whether some temporal property can occur across the space of all interaction behaviours (for example if a particular message is always eventually followed by some other particular message; or if a given sequence can never occur).

  A basic temporal property checker that utilises a trace generator, as described in Section 1, applied to business process examples is described in our technical report on constraint verification. This provided a way of checking the following properties of traces (each of these is given formally in Section 5 of our technical report):

  • Safety : If B represents some undesirable condition, a model is said to satisfy the safety property with respect to B, if in all the runs of the model, the condition B is never satisfied.
  • Liveness : If A represents some desirable condition, a model is said to possess the liveness property in any run, if at some point in the run the condition A is met.
  • Deadlock : indicates a situation in which two or more processes wait for each other and are unable to proceed on their tasks as each is waiting for the other. For LCC, each process waiting for a message
    from the other process before it can proceed with its part of the interaction gives a deadlock.
  • Correctness: aims at meeting all the functional requirements expected of the given model, where the conjunction of all constraints is implied by the conjunction of all the property specifications and
    the conjunction of all constraints holds in the integrated behavioural model.
  • Termination : requires the completion of all roles in an interaction. In LCC this means that all the roles associated with the messages of an interaction should be closed.

  Although our basic temporal property checker can analyse important properties of LCC interaction specifications, it explores the search space of possible interaction traces using a standard Prolog search strategy. This limits the efficiency of search space exploration because it involves a high proportion of redundant search. In OpenKnowledge we addressed this problem by using a tabled resolution based Prolog system: XSB. This allowed us to perform more complex forms of property checking on larger LCC specifications. More surprisingly, it allowed us to perform limited but useful forms of property checking in only a few seconds of real time which makes it possible to check LCC interaction models not only in advance of their deployment (the traditional approach) but also, in some circumstances, during their deployment. This provides a novel form of trust-related verification. The XSB-based property checker is described in detail in our technical report on runtime verification of trust models and the code used to implement it can be downloaded as source code.

• 3 Virtual Environments (Unreal Tournament)

  All of the analytical methods described so far in this section assume that the environment on which interactions is run need not be modelled as part of the analysis, other than in terms of constraints satisfied by the LCC interaction model (or, as in Section 2, by a combination of LCC and service specifications). In some cases, however, we are interested in detailed simulation of environments. This is especially the case when we want to assess performance of LCC as a coordination medium in real-time systems, where response times in a rapidly changing environment are of utmost importance. To perform these sorts of analyses one needs a simulator for the dynamic environment. A popular source of this sort of simulator comes from the computer gaming world where commercial success has depended on providing semi-realistic environments in which to play.

  One of the standard gaming simulators is Unreal Tournament which is a popular gaming environment in its own right but also provides an accessible game engine that can be used by developers to introduce automated game playing agents ("bots" in UT jargon) into the game. It also provides a rich source of complex virtual environment topologies, courtesy of the environment design community that has built up around the game. We have built a means of linking a LCC interpreter to UT-bots so that LCC can be used to coordinate message passing between them. This allows us to use LCC to define collaborative strategies for game playing which we then test by playing teams of coordinated "LCC-enabled" bots against teams of individually superior but uncoordinated conventional bots. We have been able to produce remarkably fluid and effective team play by this means.

  A description our most recent work with the Unreal Tournament environment is available as a Quicktime movie with a set of accompanying notes. The second half of this video shows the environment in action (note that the movie is a comparatively large file, 75MB, so may take several minutes to download). The bots that you see in this video are highly autonomous,using machine learning algorithms fed by data from the environment to develop their individual behaviours as the game proceeds. The LCC being used to coordinate them is simple and reactive (in fact the system uses a reactive subset of LCC for speed of response) as can be seen from the accompanying notes. In the long term, we hope that this sort of architecture could develop into a framework for behaviour-based software system development analogous to the subsumption architectures used to combine behavioural modules in robotic systems.