Oana Andrei
email: oana.andrei@glasgow.ac.uk

Hélène Kirchner
email: helene.kirchner@inria.fr

Runtime Verification for Biochemical Programs

Keywords: Biochemical calculus, Rewriting strategies, Autonomous systems, Runtime verification

The biochemical paradigm is well-suited for modelling autonomous systems and new programming languages are emerging from this approach. However, in order to validate such programs, we need to define precisely their semantics and to provide verification techniques. In this paper, we consider a higher-order biochemical calculus that models the structure of system states and its dynamics thanks to rewriting abstractions, namely rules and strategies. We extend this calculus with a runtime verification technique in order to perform automatic discovery of property satisfaction failure. The property specification language is a subclass of LTL safety and liveness properties.

Introduction

More and more complex distributed computing systems are employed in large computer networks where direct human intervention would become easily overwhelmed. Then self-managing properties for such systems became highly desirable and the autonomic computing framework [START_REF] Kephart | The Vision of Autonomic Computing[END_REF] was designed for this purpose. Autonomous systems are initially provided with some high-level instructions from administrators and should require minimal human intervention during their functioning if none. There is crucial need for theories and formal frameworks to model computation, to define unconventional languages for programming and to establish foundations for verifying properties of these systems, for instance security-related properties.

Our work fits into the unconventional programming languages approach such as the chemical paradigm [START_REF] Berry | The Chemical Abstract Machine[END_REF][START_REF] Giavitto | MGS: a Rule-Based Programming Language for Complex Objects and Collections[END_REF][START_REF] Banâtre | Programming Self-Organizing Systems with the Higher-Order Chemical Language[END_REF]. The chemical paradigm captures the intuition of a collection of freely interacting atomic values where interactions are modelled by rules and has been applied to modelling self-managing systems [START_REF] Banâtre | Programming Self-Organizing Systems with the Higher-Order Chemical Language[END_REF], computer networks, grid infrastructures [START_REF] Banâtre | Towards "Chemical" Desktop Grids[END_REF], web services [START_REF] Pazat | Towards a Chemistry-Inspired Middleware to Program the Internet of Services[END_REF]. We extended this paradigm with structured objects instead of atomic values and defined a higher-order formalism, the Abstract Biochemical Calculus [START_REF] Lipshteyn | A Port Graph Calculus for Autonomic Computing and Invariant Verification[END_REF]. An autonomous system is modelled as a biochemical program with the structural part described by a collection of objects and behavioural part as a collection of transformations (rewrite rules) over collections of objects, both at the same level. Objects and rewrite rules are generically called molecules and collections of molecules are also molecules. Higher-order rewrite rules over molecules introduce new rewrite rules in the behaviour of the system. More expressive power is gained in modelling a system's evolution via strategies which control the application order of a set of rewrite rules.

In [START_REF] Echahed | A Rewriting Calculus for Multigraphs with Ports[END_REF] we proposed the visual structure of port graph, as well as port graph rewrite rules and a rewriting relation on port graphs for modelling complex systems with dynamical topology, whose components interact in a concurrent and distributed manner. Nodes with ports represent components (or objects), while edges correspond to interactions (or communications). Then port graph rewrite rules are used for modelling the system evolution by creating new nodes and connections among them at specific points (ports), breaking connections, merging, splitting, or deleting nodes, or performing any combination of these operations. By instantiating the structure of the objects in the Abstract Biochemical Calculus with port graphs, we obtained the Port Graph Calculus and we showed its capabilities of modelling autonomous systems and biochemical networks in [START_REF] Andrei | A Rewriting Calculus for Graphs: Applications to Biology and Autonomous Systems[END_REF][START_REF] Kirchner | A Higher-Order Graph Calculus for Autonomic Computing[END_REF]. An implementation of the port graph calculus is provided by the PORGY environment [START_REF] Andrei | PORGY: Strategy Driven Interactive Transformation of Graphs[END_REF].

At this stage, our aim is to improve the confidence in biochemical models of autonomous systems by ensuring that the current execution is consistent with the expected properties of the system and by detecting violations of safety properties in order to recover from problematic situations. Runtime verification fits well in this context as a verification technique that increases confidence in the correctness of the system behaviour with respect to its formal specification. We have already proposed a method for verifying invariant properties of biochemical program [START_REF] Lipshteyn | A Port Graph Calculus for Autonomic Computing and Invariant Verification[END_REF]. An invariant property is encoded as a special rule in the biochemical program modelling the system and such rule is dynamically checked at each execution step. We obtained a kind of runtime verification technique which allows the running program to detect its own structural failures.

In this paper, we enrich the abstract biochemical calculus with a verification technique where properties are expressed in linear temporal logic (LTL) [START_REF] Pnueli | The Temporal Logic of Programs[END_REF]. We concentrate here on safety properties ("Something bad never happens") that include invariant properties as subclass, and liveness properties ("Something good will happen eventually"). We consider a set of LTL formulae built using one temporal modal operator, which is enough to express a fair amount of properties, and we use a three-valued semantics for the LTL formulae [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF]. In order to illustrate our approach and the proposed concepts, in this paper we develop a simple example of service orchestration based on library loaning services.

The paper is organised as follows. In the next section, we give an overview of the abstract biochemical calculus, syntax and semantics. Section 3 discusses the Kripke structure associated to a biochemical program and the set of temporal formulae we consider. In Section 4, we formalise runtime verification in this context and extend the calculus to perform simultaneously computation and verification steps. Further perspectives are drawn in Section 5.

The Abstract Biochemical Calculus

The Abstract Biochemical Calculus [START_REF] Lipshteyn | A Port Graph Calculus for Autonomic Computing and Invariant Verification[END_REF] is based on two main formalisms: the ρ-calculus (also called the rewriting calculus) [START_REF] Cirstea | The Rewriting Calculus -Part I and II[END_REF] and the γ-calculus [START_REF] Banâtre | Higher-Order Chemical Programming Style[END_REF]. It extends the chemical model of the γ-calculus by embedding higher-order capabilities of the rewriting calculus and by considering an abstract structure OBJ for the basic chemical objects of the γ-calculus. The structure OBJ is required to allow modelling connections between objects as well as creating and removing such connections. The result is an abstract biochemical calculus based on rewriting structured molecules, called the ρ OBJ -calculus and presented in the rest of this section.

Syntax

The syntax of the Abstract Biochemical Calculus is given in Fig. 1. In the following we detail each class of entities.

The structure of objects OBJ is an abstract one; for instance objects may be terms, records, graphs, etc. We only require that for any object O ∈ OBJ , we can retrieve the set of its variables denoted by Var(O), we can select a subobject, and that there always exists a procedure for matching objects w.r.t. a given congruence. We assume that a matching algorithm Sol for OBJ as well as a structural congruence relation ≡ on objects are given as parameters of the calculus. Following the intuition of chemical solutions, collections of objects are built using an associative and commutative juxtaposition operator • . We also define an object stk to be used later as failure object.

The collection of objects can be transformed using rules of the form L ⇒ R where L and R are objects such that Var(R) ⊆ Var(L). Objects and rules are grouped together in molecules which are bags built using the same associative-commutative (AC) juxtaposition operator • as for objects. The structural congruence relation on molecules is defined as the union of structural congruence relation on OBJ and the AC properties of the juxtaposition operator on objects and molecules.

Transformations of molecules are defined as higher-order abstractions M ⇛ K. A rule is a first-order abstraction that abstracts only on (collections of) objects while the general higher-order abstractions act on objects as well as on rules. Hereafter, we use the symbol ⇛ ⇒ to denote either ⇒ or ⇛. The application operator @ takes an abstraction and a molecule to build a reactive molecule. Higher-order abstractions, also called strategies, may contain in their right-hand side reactive molecules. Collections of molecules and abstractions are called configurations. Then all molecules and abstractions describing the structure and behaviour of the system to be modelled are put in a configuration to obtain a biochemical program, which we also refer to as (system) state. We introduce the program entity in order to distinguish between global and local configurations by making explicit the square brackets for the former ones. This distinction is needed in the formalisation of the calculus.

(Objects) O ::= stk | OBJ | X | O • O (Molecules) M ::= O | O ⇒ O | M • M | Y (Configurations) K ::= M | M ⇛ K | (M ⇛ K)@K | K • K (Biochemical program) P ::= [K]
Example 2.1 We illustrate the calculus with a toy example of a loaning service model provided by a university library for students in the Departments of Mathematics and Computer Science. The entities of this model are students as users, libraries as service providers, textbooks as resources (or services), and a global clock:

• student S (id , dpt, state), where id is a unique student identity, dpt takes a value of M or CS, and state takes a value of 1 for requesting, 2 for pending, 3 for reading;

• library L(dpt, SID, BID), where SID and BID are sets of student and book identities respectively;

• book B (b, sid , tick ), where b is the book identity, and sid takes the value of the identifier of the student who borrowed it at non-nullary time stamp tick , otherwise nil if tick is 0.

We model each entity as a node with ports in a port graph [START_REF] Kirchner | A Higher-Order Graph Calculus for Autonomic Computing[END_REF], where some ports have states or maximum arity greater than one. A library node has the port SID where several students from the same department may connect and the port BID where all book nodes from the same department are connected, a student node can be connected with a book node, and the two libraries are connected. Let ≡ denote the isomorphism relation on port graphs. The juxtaposition operator • is not represented for port graph objects. The library service example has three basic actions illustrated as port graph rewrite rules in Fig. 2: BReq: a student requests a book at the departmental library within one time unit; BBrw: a student borrows an available book from the library within one time unit; BRet: a student returns a book instantaneously to the departmental library after holding it for at most 5 time units;

DBRet: a student returns a book instantaneously to the library of another department after holding it for at most 3 time units.

Semantics of Biochemical Programs

The evaluation mechanism of the calculus relies on solving the fundamental problem of matching a pattern to a molecule, i.e., finding an injective morphism between the pattern and the molecule. Let Sol be a function that returns the set of substitutions

′ , denoted M ≪ M ′ . A submatching problem M ≺ ≺ M ′ is a matching problem from M to a sub-molecule M ′′ of M ′ . Definition 2.2
The structural congruence on configurations is the least equivalence relation on configurations such that it includes the structural congruence relation on molecules and the following equations:

(Application) (M ⇛ ⇒ K)@M ′ ≡ ς(K) if ς ∈ Sol(M ≺ ≺ M ′ ) (Application Fail) (M ⇛ ⇒ K)@M ′ ≡ stk if Sol(M ≺ ≺ M ′ ) = ∅ (Stuck) stk • K ≡ K
If the matching problem between the left-hand side of the abstraction M ⇛ ⇒ K and the molecule M ′ has solutions, the equation (Application) is used and one substitution is chosen from the solution set and applied on the right-hand side of M ⇛ ⇒ K; otherwise, if the matching problem has no solution, the application fails and it is reduced to the failure object stk according to equation (Application Fail).

A stk object is deleted from a juxtaposition of configurations according to (Stuck).

Definition 2.3 A configuration is in normal form if it is irreducible with respect to the equations (Application), (Application Fail) and (Stuck) ordered from left to right. A program [K] is in normal form if configuration K is in normal form.
The following evaluation rule defines the operational semantics of biochemical programs, more specifically, the interaction between abstractions and molecules:

(Interaction) [K ′ • (M ⇛ ⇒ K) • M ′ ] -→ [K ′ • ς(K)] if ς ∈ Sol(M ≺ ≺ M ′ ) and [K ′ • (M ⇛ ⇒ K) • M ′ ] is in normal form
The interaction evaluation rule chooses an abstraction M ⇛ ⇒ K, a molecule M ′ in the current program and a substitution ς solution of the matching problem M ≺ ≺ M ′ , and then replaces M ⇛ ⇒ K and M ′ with the configuration obtained from applying the substitution ς to K. The variable K ′ captures the context in which the rule M ⇛ ⇒ K and the molecule M ′ interact, thanks to the AC properties of • .

We define a new evaluation rule on biochemical programs

[K] -→ ≡ [K ′ ] as syntactic sugar for [K] -→ [K ′′ ] and [K ′′ ] ≡ [K ′ ] with [K ′ ] in normal form.

Strategies

It is important to emphasise that we can model a non-deterministic (and possibly non-terminating) behaviour for the application of abstractions in a biochemical program, or introduce some control to compose or to choose the rules to apply. For this purpose we introduce strategies in the calculus by expressing them as higherorder abstractions. Strategies may be used in various ways: to sequentialise or order the application of several abstractions, to exploit failure information, to define persistent rules that are not consumed when applied, to implement case analysis and iteration. More details can be found for instance in [START_REF] Andrei | A Rewriting Calculus for Graphs: Applications to Biology and Autonomous Systems[END_REF][START_REF] Lipshteyn | A Port Graph Calculus for Autonomic Computing and Invariant Verification[END_REF].

Most strategies are encoded as abstractions of the form Y ⇛ K, where Y is a molecule variable and it corresponds to a higher-order function, i.e. to a lambda expression λY.K. When Y ⇛ K is applied to a molecule M , we obtain a reactive molecule (Y ⇛ K)@M which is structurally congruent to K where each occurrence of Y has been replaced by M .

In Fig. 3 we recall the encoding of some strategies as higher-order abstractions in the ρ OBJ -calculus, where T, T 1 , T 2 , T 3 range over abstractions. The strategies id and fail represent the identity and failure strategies. The seq(T 1 , T 2 ) strategy applies sequentially the two abstractions T 1 and T 2 , while first(T 1 , T 2 ) tries first to apply T 1 and in case of application failure it applies the second abstraction T 2 . The application of not(T ) fails if the application of T 1 does not fail, otherwise it does nothing. The strategy ifThenElse(T 1 , T 2 , T 3 ) applies the first strategy: if it does not fail, it applies the second strategy, else it applies the third strategy; it fails if both applications of T 2 and T 3 fail.

id Y ⇛ T fail Y ⇛ stk seq(T 1 , T 2 ) Y ⇛ T 2 @(T 1 @Y ) first(T 1 , T 2 ) Y ⇛ (T 1 @Y ) • (stk ⇛ (T 2 @Y ))@(T 1 @Y ) not(T ) Y ⇛ first(stk ⇛ Y, Y ′ ⇛ stk)@(T @Y ) ifThenElse(T 1 , T 2 , T 3 ) Y ⇛ first(stk ⇛ T 3 @Y, Y ′ ⇛ T 2 @Y )@(T 1 @Y ) Fig. 3

. Strategy operators encoded as higher-order abstractions

A strategy T can be applied as long as it is does not fail using the recursive strategy: repeat(T ) µX.first(seq(T, X), id). The recursion operator µ is encoded using the fixed-point combinator of the λ-calculus following the procedure done for encoding iterators in the ρ-calculus [START_REF] Cirstea | The Rewriting Calculus -Part I and II[END_REF].

In the (Interaction) evaluation rule, a strategy (or a rule) M ⇛ ⇒ K is consumed by a non-failing interaction with a molecule M ′ . The persistent strategy combina-tor defined by T ! µX.seq(T, first(stk ⇒ stk, Y ⇛ Y • X)), when applied to a molecule, applies T to the molecule and T ! is replicated; if the application of T fails, then the failure stk is returned.

Example 2.4

We extend the library service model with an action DBReq depicted in Fig. 2 which allows a library to dispatch a book request to the other library if the latter has available books resulting in a student borrowing a book from the other department's library. A library can dispatch a request only when it has no book available by considering a strategy which gives a higher priority to BBrw than DBReq; therefore we replace the rules BBrw and DBReq by seq(BBrw, DBReq).

The initial state of the biochemical program modelling the library service is a juxtaposition of student nodes in requesting state, two connected library nodesone for each department, book nodes available for each library, and the persistent strategies BReq!, seq(BBrw, DBReq)!, BRet1! and BRet2!.

Rewrite rules and strategies used in biochemical programs are indeed essential concepts to express evolution of autonomous systems. The same concepts can be reused for developing verification techniques for autonomous systems.

A first approach for embedding verification in models of autonomous systems, described in [START_REF] Lipshteyn | A Port Graph Calculus for Autonomic Computing and Invariant Verification[END_REF], consists in expressing an invariant property of the system as an abstraction with identical sides, M ⇛ ⇒ M , and relying on the matching process for testing the presence of a molecule M . The failure of the invariant is handled by a failure port graph Error that does not allow the execution to continue. The strategy verifying such an invariant is first(M ⇛ ⇒ M, X ⇒ Error)!. We can also express the unwanted occurrence of a molecule M using the strategy (M ⇒ Error)!. In both cases above, instead of yielding the failure Error signalling that a property of the system is not satisfied, the problem can be "repaired" by associating to each property the necessary rules or strategies to be inserted in the system in case of failure. Such ideas open a wide field of possibilities for combining runtime verification and self-healing capabilities and we explore them further in Sect. [START_REF] Kirchner | A Higher-Order Graph Calculus for Autonomic Computing[END_REF].

Building up on this simple idea, our goal is to generalise invariant verification towards the proof of safety and liveness properties. This is natural since the evaluation rule of biochemical programs can be seen as a reduction relation in a state transition system -more specifically an Abstract Reduction System (ARS). For verification, we consider properties expressed as formulae in a three-valued linear temporal logic and interpreted over traces in the ARS associated to the program. First we show how to encode the properties into adequate rewrite strategies, which allows us to embed them in each state of an extended ARS. For that purpose, the structure of programs is enriched by guards and another reduction relation is defined on guarded programs. Then property satisfaction is checked on each transition state via the evaluation mechanism of the rewrite strategies.

Linear Temporal Logic for Biochemical Reductions

In this section, we first review the basic concepts underlying an Abstract Reduction System. Then we define a set of structural formulae for reasoning about the molecular structures in configurations. Finally, we review the set of LTL formulae [START_REF] Pnueli | The Temporal Logic of Programs[END_REF] defined over the Abstract Reduction System whose states are biochemical programs and whose transitions are determined by the interaction evaluation rule in the ρ OBJ -calculus.

Abstract Reduction Systems

An Abstract Reduction System (ARS) [START_REF] Kirchner | Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70[END_REF] is a labelled oriented graph (S, s 0 , R) with S a finite set of nodes called states, s 0 ∈ S the initial state, and R a binary relation over S × S called transition relation. Let A be the ARS built over biochemical programs using the interaction evaluation relation. Then (s, s ′ ) ∈ R if s -→ ≡ s ′ in the ρ OBJ -calculus. We call s -→ ≡ s ′ a reduction steps or transition. If we consider a function labelling states with atomic propositions, we obtain the definition of a Kripke structure.

A computation path or trace in the ARS A is a path in the graph starting from the initial state s 0 , i.e., an infinite non-empty sequence s 0 s 1 s 2 . . . of states in S where s i -→ ≡ s i+1 for all i ≥ 0. Let Path(A) denote the set of paths of A. A finite trace is a non-empty sequence s 0 s 1 . . . s n with n ≥ 0. A finite trace u = s 0 s 1 . . . s n can be concatenated with an infinite sequence of states w = s ′ 0 s ′ 1 . . . with s ′ j -→ ≡ s ′ j+1 , for all j ≥ 0, to obtain a new infinite trace if and only if s n -→ ≡ s ′ 0 and we say that w is a continuation of u. For a path w = s 0 s 1 s 2 . . ., we denote by w[i] the ith state of the path, namely s i-1 , and by w i the suffix of the path w starting at state w[i], i.e., w i = s i-1 s i . . .. We say that a state s in the ARS A is final (or irreducible) if there is no state s ′ such that s -→ ≡ s ′ . We denote a final state s by s ↓ .

Structural Formulae and Structural Satisfaction

Based on molecule definition and Boolean connectors, in the following we define the formulae characterising the molecular structure of states in A.

Definition 3.1 The set of structural formulae F(M) is constructed inductively as follows:

ϕ

::= true | false | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ | ◊ ϕ
with true, false, ¬, ∧, ∨ and → the usual boolean connectors, and ◊ ϕ read as "somewhere" ϕ.

Definition 3.2

The semantics of a structural formula ϕ ∈ F(M) with respect to a molecule M , denoted by M |= ϕ, is defined inductively as follows:

M |= true M |= ϕ 1 ∧ ϕ 2 ⇔ M |= ϕ 1 and M |= ϕ 2 M |= false M |= ϕ 1 ∨ ϕ 2 ⇔ M |= ϕ 1 or M |= ϕ 2 M |= M ′ ⇔ M ′ ≪ M M |= ϕ 1 → ϕ 2 ⇔ M |= ϕ 1 or M |= ϕ 2 M |= ¬ϕ ⇔ M |= ϕ M |= ◊ ϕ ⇔ ∃M ′ ≺ ≺ M. M ′ |= ϕ
We say that a state s of the ARS A satisfies a structural formula ϕ and write

s |= ϕ if s ≡ [M • K ′ ] and M |= ϕ.
The structural satisfaction problem between a molecule M and a formula M ′ reduces to successfully solving the matching problem M ′ ≪ M . A molecule M structurally satisfies a formula ◊ ϕ if M has a submolecule M ′ satisfying ϕ. The following proposition states that the structural satisfaction is up to the structural congruence relation on states. The proof is immediate using induction over the structure of ϕ.

Temporal Formulae

In order to express safety or liveness properties, we need a temporal logic. The set of LTL formulae over F(M) is inductively defined by:

φ ::= true | false | ϕ | ¬φ | φ ∧ φ | φ ∨ φ | φ → φ | X φ | φ U φ
where ϕ ranges over the set of structural formulae F(M). Three more path operators are available as syntactic sugar: the eventually operator F (future) with Fφ ≡ true U φ, the always operator G (globally) with Gφ ≡ ¬(F¬φ), and the release operator R with φ 1 Rφ 2 = ¬(¬φ 1 U¬φ 2 ).

The LTL formulae are interpreted over traces in the ARS A and their semantics is defined inductively as follows: We consider only LTL formulae in positive normal form, i.e. negations only occur in front of structural formulae. This is possible since every operator in the LTL syntax presented above has a dual. In particular we have the following equivalences:

w |= true w |= false w |= ϕ iff w[0] |= ϕ w |= ¬φ iff w |= φ w |= φ 1 ∨ φ 2 iff w |= φ 1 or w |= φ 2 w |= φ 1 ∧ φ 2 iff w |= φ 1 and w |= φ 2 w |= φ 1 → φ 2 iff w |= φ 1 or w |= φ 2 w |= Xφ iff w 1 |= φ w |= Fφ iff ∃i ≥ 0 . w i |= φ w |= Gφ iff ∀i ≥ 0 . w i |= φ w |= φ 1 Uφ 2 iff
¬(Xφ) = X(¬φ), ¬(Fφ) = G(¬φ), ¬(Gφ) = F(¬φ), ¬(φ 1 U φ 2 ) = ¬φ 1 R¬φ 2 .

Embedding Runtime Verification in the Abstract Biochemical Calculus

In this section we extend the reduction relation defined for the biochemical calculus with LTL formulae as guards of the computation. The aim is to check at runtime that, after each interaction step induced by the interaction evaluation rule, a set of properties expressed as simple LTL formulae is satisfied.

In runtime verification a trace is also called run and a finite trace an execution. Monitoring a property at runtime can only be formally defined over finite traces. The LTL 3 [START_REF] Bauer | Monitoring of Real-Time Properties[END_REF], a variant of LTL with a three-valued semantics, was designed to overcome this gap between monitoring finite and infinite traces. In an automaton approach, a finite trace is a good prefix if any infinite continuation of the trace will always be accepted, a bad prefix if there is no continuation of the trace to build an accepting trace, and an ugly prefix otherwise. A good, bad or ugly prefix of an LTL formula is evaluated to true, false or inconclusive (denoted by ?) respectively. The semantics of a LTL 3 formula φ with respect to a finite trace u in an abstract reduction system A is defined as follows:

[u |= φ] =      true if ∀ w continuation for u, uw |= φ false if ∀ w continuation for u, uw |= φ ? otherwise
We adopt the following approach. We start with an inconclusive guard and we check that a property φ is satisfied by the current execution by applying a strategy encoding the formula. If no decision can be made, either to state that the property is satisfied or not, we pass on the inconclusive guard meaning that all along the current execution there is no state that makes the property not satisfied.

Syntax

We consider the following set of LTL formulae defined over the set of structural formulae F(M):

φ ::= true | false | ϕ | ¬φ | φ ∧ φ | φ ∨ φ | φ → φ | F ϕ | G ϕ | ϕ U ϕ | ϕ R ϕ
We define guarded biochemical programs with the guard being an LTL formula φ over molecules, prefixed by a satisfaction operator (either |=, |= or |= ? ), or a conjunction of such formulae:

(Satisfaction operators) α ::= |= | |= | |= ? (Guards) H ::= α φ | H ∧ H (Guarded biochemical programs) GS ::= [K] H | (M ⇛ K)@[K] H
The atomic guard |= φ ( |= φ) states that the formula φ is satisfied (not satisfied respectively) by the current execution, whereas |= ? φ corresponds to a consistent inconclusive satisfaction answer all along the current execution. We consider guards α φ with φ in positive conjunctive normal form and we decompose guards such that the LTL formula φ is not a conjunction. The structural congruence relation on atomic guards, denoted also ≡, is defined inductively as follows:

ously borrowed by two students or the liveness property F( ◊ B (id , nil , 0 ) for a book to be available at some point.

Semantics of Guarded Biochemical Programs

A structural formula ϕ in F(M) is mapped to a strategy τ (ϕ) and it is interpreted over a molecule M from a program configuration as the result of the strategy application τ (ϕ)@M . We define the mapping τ from structural formulae to strategies inductively as follows: Intuitively, if the application of the strategy encoding ϕ on a molecule M fails, then the formula is not satisfied by M . The above proposition shows the soundness and completeness of encoding the semantics of structural formulae via the evaluation mechanism of strategies. The proofs of these last two results can be found in [START_REF] Andrei | A Rewriting Calculus for Graphs: Applications to Biology and Autonomous Systems[END_REF].

τ (true) id τ (false) fail τ ( ◊ M ) M ⇒ M τ (¬ϕ) not(τ (ϕ)) τ (ϕ 1 ∧ ϕ 2 ) seq(τ (ϕ 1 ), τ (ϕ 2 )) τ (ϕ 1 ∨ ϕ 2 ) first(τ (ϕ 1 ), τ (ϕ 2 )) τ (ϕ 1 → ϕ 2 ) Y ⇛ ⇒ seq(τ (ϕ 1 ), first(stk ⇛ ⇒ Y, τ (ϕ 2 )))@Y
For s 0 the initial state of the ARS A and φ a temporal property that we want to verify along the execution of the system, we start with the initial guarded biochemical program s 0 |= ? φ . In the following we define a new reduction relation on guarded programs denoted =⇒ which encompasses the reduction relation -→ ≡ on biochemical programs and verifies at each step the satisfaction of the guard.

The process of verifying the satisfaction of a guard along an execution trace consumes it: an LTL formula and a state s generate another LTL formula. To define the consumption of an LTL formula φ by the reduction relation in the calculus, we use derivatives [START_REF] Sen | Generating Optimal Linear Temporal Logic Monitors by Coinduction[END_REF] for LTL. The evaluation of derivations provide a way of determining if a prefix is good or bad for a formula. For s a state and φ an LTL formula, the derivative of φ in state s, denoted by φ{s}, has the property that for any finite trace u, su |= φ iff u |= φ{s} and su |= φ iff u |= φ{s}. Theorem 4.6 (Derivative [START_REF] Sen | Generating Optimal Linear Temporal Logic Monitors by Coinduction[END_REF]) For any LTL formula φ and for any finite trace u = s 0 s 1 . . . s n , u is a good (bad) prefix for φ if and only if φ{s 0 }{s 1 } . . . {s n } evaluates to true (false).

The recursive definition of the operator { } is:

false{s} = false true{s} = true (¬φ){s} = ¬(φ{s}) (φ 1 ∨ φ 2 ){s} = φ 1 {s} ∨ φ 2 {s} (φ 1 ∧ φ 2 ){s} = φ 1 {s} ∧ φ 2 {s} (φ 1 → φ 2 ){s} = φ 1 {s} → φ 2 {s}
The definition of derivatives for the rest of temporal formulae is given together with the definition of the reduction relation =⇒ on guarded biochemical programs. The latter is defined by structural induction on the LTL formulae by associating a strategy Θ(φ) to each formula φ. Definition 4.7 The reduction relation on guarded biochemical programs extends the interaction relation on biochemical programs with an evaluation of all atomic guards:

[K] α 1 φ 1 ∧...∧αnφn =⇒ [K ′ ] α ′ 1 φ 1 ∧...∧α ′ n φn if [K] α i φ i =⇒ [K ′ ] α ′ i φ i for all i [K] |= ? φ =⇒ (Θ(φ)@[K ′ ] |= ? φ )@[K] |= ? φ if [K] -→ ≡ [K ′ ] [K] |=φ =⇒ [K ′ ] |=φ if [K] -→ ≡ [K ′ ] [K] |=φ =⇒ [K ′ ] |=φ if [K] -→ ≡ [K ′ ]
where Θ(φ) is the strategy associated to the formula φ.

In order to address the case where the current execution reaches an irreducible program with an inconclusive guard, we need to extend the congruence relation on guarded biochemical programs as follows:

[K] |= ? φ ≡ Θ ↓ (φ)@[K] |= ? φ if [K] is irreducible
To achieve the complete definition of the reduction relation on guarded biochemical programs, we have to define strategy mappings Θ and Θ ↓ for each type of LTL formulae φ used as a guard, relying in the intuition provided by derivatives. This is the purpose of the following five subsections.

Strategy encoding for structural formulae

The derivative of a structural formula ϕ in a state s is true if s |= ϕ and false otherwise. The strategy encoding the temporal formula ϕ evaluates the application of the strategy τ (ϕ) on the current state s and returns the guard |= ϕ if s |= ϕ, otherwise the guard |= ϕ.

Θ(ϕ) [Z] |=

? ϕ ⇛ ⇒ ifThenElse(τ (ϕ), W 1 ⇛ ⇒ [Z] |=ϕ , W 2 ⇛ ⇒ [Z] |=ϕ ) Θ ↓ (ϕ) ifThenElse(τ (ϕ), [Z] |= ? ϕ ⇛ ⇒ [Z] |=ϕ , [Z] |= ? ϕ ⇛ ⇒ [Z] |=ϕ )

Strategy encoding for Gϕ formulae

The derivative of the globally operator for a non-final state s and a final state s ↓ is defined as follows:

(Gϕ){s} = false if ¬ϕ{s} Gϕ otherwise (Gϕ){s ↓ } = false if ¬ϕ{s ↓ } true otherwise
The strategy encoding Gϕ tests the satisfaction of ϕ in the current state: if the answer is positive then the guard is inconclusive for the current execution and the verification continues with the same guard, otherwise the guard is negative meaning that the temporal formula Gϕ is not satisfied by the current execution. If the current state is final, then the inconclusive guard turns into a positive one if this state satisfies ϕ as well, since the formula ϕ is satisfied in every state of the execution. The strategies Θ and Θ ↓ encoding Gϕ for non-final and final states are:

Θ(Gϕ) [Z] |= ? Gϕ ⇛ ⇒ ifThenElse(τ (ϕ), W 1 ⇛ ⇒ [Z] |= ? Gϕ , W 2 ⇛ ⇒ [Z] |=Gϕ ) Θ ↓ (Gϕ) ifThenElse(τ (ϕ), [Z] |= ? Gϕ ⇛ ⇒ [Z] |=Gϕ , [Z] |= ? Gϕ ⇛ ⇒ [Z] |=Gϕ )

Strategy encoding for Fϕ formulae

The derivative of the eventually operator for a non-final state s and a final state s ↓ is defined as follows:

(Fϕ){s} = true if ϕ{s} Fϕ otherwise (Fϕ){s ↓ } = ϕ{s ↓ } = true if ϕ{s ↓ } false otherwise
The strategy encoding Fϕ tests if the current state satisfies ϕ. If it does, then one state satisfying ϕ in the current execution has been found, hence the inconclusive guard is turned to a positive one. Otherwise, the guard is passed to the next state as inconclusive. If the current state is final and it satisfies ϕ, then the execution satisfies the temporal formula Fϕ; otherwise, the execution does not satisfy Fϕ.

The strategies Θ and Θ ↓ encoding Fϕ for non-final and final states are the following respectively:

Θ(Fϕ) [Z] |= ? Fϕ ⇛ ⇒ ifThenElse(τ (ϕ), W 1 ⇛ ⇒ [Z] |=Fϕ , W 2 ⇛ ⇒ [Z] |= ? Fϕ ) Θ ↓ (Fϕ) ifThenElse(τ (ϕ), [Z] |= ? Fϕ ⇛ ⇒ [Z] |=Fϕ , [Z] |= ? Fϕ ⇛ ⇒ [Z] |=Fϕ ) 4
Θ(ϕ 1 Uϕ 2 ) [Z] |= ? ϕ 1 Uϕ 2 ⇛ ⇒ ifThenElse(τ (ϕ 2 ), W 1 ⇛ ⇒ [Z] |=ϕ 1 Uϕ 2 , W 2 ⇛ ⇒ ifThenElse(τ (ϕ 1 ), W 3 ⇛ ⇒ [Z] |= ? ϕ 1 Uϕ 2 , W 4 ⇛ ⇒ [Z] |=ϕ 1 Uϕ 2 )) Θ ↓ (ϕ 1 Uϕ 2 ) ifThenElse(τ (ϕ 2 ), [Z] |= ? ϕ 1 Uϕ 2 ⇛ ⇒ [Z] |=ϕ 1 Uϕ 2 , [Z] |= ? ϕ 1 Uϕ 2 ⇛ ⇒ ifThenElse(τ (ϕ 1 ), W 3 ⇛ ⇒ [Z] |=ϕ 1 Uϕ 2 , W 4 ⇛ ⇒ [Z] |=ϕ 1 Uϕ 2 )) 4
Θ(ϕ 1 Rϕ 2 ) [Z] |= ? ϕ 1 Rϕ 2 ⇛ ⇒ ifThenElse(τ (ϕ 2 ), W 1 ⇛ ⇒ ifThenElse(τ (ϕ 1 ), W 2 ⇛ ⇒ [Z] |=ϕ 1 Rϕ 2 , W 3 ⇛ ⇒ [Z] |= ? ϕ 1 Rϕ 2 ), W 4 ⇛ ⇒ [Z] |=ϕ 1 Rϕ 2 ) Θ ↓ (ϕ 1 Rϕ 2 ) ifThenElse(τ (ϕ 2 ), [Z] |= ? ϕ 1 Rϕ 2 ⇛ ⇒ [Z] |=ϕ 1 Rϕ 2 , [Z] |= ? ϕ 1 Rϕ 2 ⇛ ⇒ [Z] |=ϕ 1 Rϕ 2 )
The properties of the strategy definitions above are summarised by the next proposition: Proposition 4.8 Let s |= ? ϕ be the current guarded biochemical program. If the next biochemical program computed by the evaluation rule is s ′ , then its guard is computed, according to Def. 4.7, as the normal of the application (Θ(φ)@s ′ |= ? φ )@s |= ? φ . Otherwise, if the biochemical program s is irreducible, then its guard is computed by reducing to normal form the application (Θ ↓ (φ)@s |= ? φ ). Figure 4 lists these computations when the current guard φ ranges over ϕ, Gϕ, Fϕ, ϕ 1 Uϕ 2 and ϕ 1 Rϕ 2 .

We are now ready to prove the correctness of our encoding of the runtime verification of LTL formulae in the calculus using strategies, based on the result of Theorem 4.6. Theorem 4.9 (Correctness) For any LTL formula φ guarding a biochemical program s 0 and for any finite trace u = s 0 s 1 . . . s n , u is a good prefix for φ if and only if either:

Θ(ϕ) Θ(Gϕ) Θ(Fϕ) Θ ↓ (ϕ) Θ ↓ (Gϕ) Θ ↓ (Fϕ) s |= ϕ s ′ |=ϕ s ′ |= ? Gϕ s ′ |=Fϕ s |=ϕ s |=Gϕ s |=Fϕ s |= ϕ s ′ |=ϕ s ′ |=Gϕ s ′ |= ? Fϕ s |=ϕ s |=Gϕ s ′ |=Fϕ Θ(ϕ 1 Uϕ 2 ) Θ ↓ (ϕ 1 Uϕ 2 ) s |= ϕ 2 s ′ |=ϕ 1 Uϕ 2 s |=ϕ 1 Uϕ 2 s |= (ϕ 1 ∧ ¬ϕ 2 ) s ′ |= ? ϕ 1 Uϕ 2 s |=ϕ 1 Uϕ 2 s |= (ϕ 1 ∨ ϕ 2 ) s ′ |=ϕ 1 Uϕ 2 s |=ϕ 1 Uϕ 2 Θ(ϕ 1 Rϕ 2 ) Θ ↓ (ϕ 1 Rϕ 2 ) s |= (ϕ 1 ∧ ϕ 2 ) s ′ |=ϕ 1 Rϕ 2 s |=ϕ 1 Rϕ 2 s |= (¬ϕ 1 ∧ ϕ 2 ) s ′ |= ? ϕ 1 Rϕ 2 s |=ϕ 1 Rϕ 2 s |= ϕ 2 s ′ |=ϕ 1 Rϕ 2 s |=ϕ 1 Rϕ 2
Fig. 4. Normal forms of (Θ(φ)@s ′ |= ? φ )@s |= ? φ and (Θ ↓ (φ)@s |= ? φ ) for s |= ? φ the current guarded biochemical program and s ′ the next unguarded biochemical program • ∃i, 0 ≤ i ≤ n, such that for all j < i, s j-

= G( ◊ S (id , dpt, 2 )∧ ◊ B (b, nil , 0 )))
which requires that a student should always be able to borrow a book from any departmental library. However, this guard may become false if P evolves to a state where both libraries lent all their textbooks and a Maths (resp. CS) student demands a book. In order to solve this problem and offer the students an equal chance to study, exceptionally a CS (resp. Maths) student is forced to return a book if borrowed from the other department, otherwise a student from the same department. Such behaviour is modelled by the strategy R = try(FRet1, FRet2) with FRet1 and FRet2 depicted in Fig. 5. Therefore we provide the guard φ with the repairing Fig. 5. Rewrite rules describing a student returning a book to the library of another department and of the same department strategy above and have in the calculus:

s |=φ(R) ≡ (R@s) |= ? φ(R)
such that, every time the guard φ is not satisfied, the guard is transformed into an inconclusive guard and the repairing rule is injected into the program.

On LTL Formulae Guards with Two Modal Operators

We have seen by now how to encode the LTL formulae built with at most one path operator using strategies such that their verification during the program execution amounts to strategy evaluation. However there are plenty of interesting LTL formulae with two modal operators. For instance, in the library example the formula G( ◊ S (id , dpt, 2 ) → F( ◊ S (id , dpt, 3 ))) says that always a student request of a book is eventually fulfilled.

In the following we sketch a methodology of encoding guards consisting of LTL formulae built using at most two modal operators such as

G(ϕ 1 → Xϕ 2 ), G(ϕ 1 ∧Xϕ 2 ), G(ϕ 1 ∨ Xϕ 2 ), F(ϕ 1 → Xϕ 2 ), F(ϕ 1 ∧ Xϕ 2 ), F(ϕ 1 ∨ Xϕ 2 ), G(ϕ 1 → Fϕ 2 ), G(ϕ 1 Uϕ 2 ), or F(ϕ 1 Rϕ 2 )
. The keys of this encoding are the use of derivatives and LTL formulae consumption [START_REF] Sen | Generating Optimal Linear Temporal Logic Monitors by Coinduction[END_REF].

During the execution of a guarded program s |= ? φ , the guard φ is consumed or reduced to a residual LTL formula φ ′ , in order to reduce the satisfaction problem of an LTL formula with two modal operators or with the next operator X to the satisfaction problem of a simpler LTL formula. Here we want to reduce to a formula with at most one modal operator and without the next operator, whose satisfaction problem has been handled in Sect. 4.2. However, by consuming the guard φ, the information about the initial temporal formula to be tested may be lost. We avoid this by annotating the guards along the program execution with the initial guard: for φ ′ the residual guard and φ the initial guard, we denote by φ ′ /φ the annotated guard.

In the following we define the execution of Xϕ-guarded programs. The derivatives of Xϕ in a non-final state s and in a final state s ↓ respectively are defined as follows: Having illustrated the consumption of guards on encoding the formula Xϕ, we define in the following the strategy encoding a two-temporal modal operator LTL formula F(ϕ 1 ∧ Xϕ 2 ) for a non final-state s. Its derivative is defined as: The other LTL formulae mentioned at the beginning of section can be carefully encoded using strategies, by following the top-down decomposition approach, according to the temporal operator on top, until reaching a residual LTL formula consisting of a structural formula, and by keeping track of the decomposition history.

F(ϕ 1 ∧ Xϕ 2 ){s} = ϕ 2 /F(ϕ 1 ∧ Xϕ 2 ) if ϕ 1 {s} F(ϕ 1 ∧ Xϕ 2 ) otherwise

Conclusions and Future Work

The main contributions of this paper are an abstract biochemical calculus to model autonomous systems with runtime verification capabilities for critical properties and a self-repairing method for the calculus when critical properties are violated.

In Sect. 4.4 we only gave a glimpse of how to define strategies encoding LTL formulae built using two temporal operators. Based on these ideas, we can synthesise a methodology or, even better, an automatic procedure which takes as input an LTL formula built using at most two temporal operators and produce the encoding strategy. A challenge will be then to encode even more complex LTL formulae.

Fig. 1 .

 1 Fig. 1. The syntax of the Abstract Biochemical Calculus

Fig. 2 .

 2 Fig. 2. Rewrite rules describing the actions in the library loaning service σ solutions of a given matching problem between two molecules M and M ′ , denoted M ≪ M ′ . A submatching problem M ≺ ≺ M ′ is a matching problem from M to a sub-molecule M ′′ of M ′ .

Proposition 3 . 3

 33 If s |= ϕ and s ≡ s ′ then s ′ |= ϕ.

Lemma 4 . 4

 44 Let ϕ be a structural formula in F(M) and M a molecule. Then the normal form of τ (ϕ)@M is either M or stk. Proposition 4.5 If M is a molecule and ϕ a structural formula in the calculus, then (i) M |= ϕ if and only if τ (ϕ)@M ≡ M , and (ii) M |= ϕ if and only if τ (ϕ)@M ≡ stk.

(

  Xϕ){s} = ϕ/Xϕ (ϕ/Xϕ){s} = true if ϕ{s} false otherwise (Xϕ){s ↓ } = false (ϕ/Xϕ){s ↓ } = true if ϕ{s ↓ } false otherwiseIt is worth noticing that the derivative of Xϕ reduces to the residual formula ϕ while carrying along its original formula Xϕ. Then the strategies encoding the next operator are:Θ(Xϕ) [Z] |= ? Xϕ ⇛ ⇒ (W ⇛ ⇒ [Z] |= ? ϕ/Xϕ ) Θ(ϕ/Xϕ) [Z] |= ? ϕ/Xϕ ⇛ ⇒ ifThenElse(τ (ϕ), W 1 ⇛ ⇒ [Z] |=ϕ/Xϕ , W 2 ⇛ ⇒ [Z] |=ϕ/Xϕ ) Θ ↓ (Xϕ) [Z] |= ? Xϕ ⇛ ⇒ [Z] |=Xϕ Θ ↓ (ϕ/Xϕ) ifThenElse(τ (ϕ), [Z] |= ? ϕ/Xϕ ⇛ ⇒ [Z] |=ϕ/Xϕ , [Z] |= ? ϕ/Xϕ ⇛ ⇒ [Z] |=ϕ/Xϕ )with |= (ϕ/φ) ≡ |= φ and |= (ϕ/φ) ≡ |= φ.Theorem 4.10 For any LTL formula Xϕ guarding a biochemical program s 0 and for any finite trace u = s 0 s 1 .

Then the encoding strategies of F(ϕ 1 ∧

 1 Xϕ 2 ) are the following:Θ(F(ϕ 1 ∧ Xϕ 2 )) [Z] |= ? F(ϕ 1 ∧Xϕ 2 ) ⇛ ⇒ ifThenElse(τ (ϕ 1 ), W 1 ⇛ ⇒ [Z] (|= ? ϕ 2 /F(ϕ 1 ∧Xϕ 2 )) ∧ (|= ? F(ϕ 1 ∧Xϕ 2 )) , W 2 ⇛ ⇒ [Z] |= ? F(ϕ 1 ∧Xϕ 2 ) ) Θ(ϕ 2 /F(ϕ 1 ∧ Xϕ 2 )) [Z] |= ? ϕ 2 /F(ϕ 1 ∧Xϕ 2 ) ⇛ ⇒ ifThenElse(τ (ϕ 2 ), W 1 ⇛ ⇒ [Z] |=ϕ 2 /F(ϕ 1 ∧Xϕ 2 ) , W 2 ⇛ ⇒ [Z] |=ϕ 2 /F(ϕ 1 ∧Xϕ 2 ) )

  .2.4 Strategy encoding for ϕ 1 Uϕ 2 formulae The derivatives of ϕ 1 Uϕ 2 for non-final and final states respectively are defined as Uϕ 2 ) if ¬(ϕ 2 {s}) and ϕ 1 {s} false if ¬(ϕ 2 {s}) and ¬(ϕ 1 {s})(ϕ 1 Uϕ 2 ){s ↓ } = true if φ 2 {s ↓ } or (¬(ϕ 2 {s ↓ }) and ϕ 1 {s ↓ }) false if ¬(ϕ 2 {s ↓ }) and ¬(ϕ 1 {s ↓ })The strategy encoding the temporal formula ϕ 1 Uϕ 2 tests first if the current state satisfies ϕ 2 : if it does, then the inconclusive guard is transformed into a positive guard; otherwise, it tests if the current state satisfies ϕ 1 : if it does, then we continue with an inconclusive guard (hence all previous and current states in the execution satisfy ϕ 1 ), else we found a state where neither ϕ 1 or ϕ 2 are satisfied, hence the formula ϕ 1 Uϕ 2 is not satisfied by the execution. The strategies Θ and Θ ↓ encoding ϕ 1 Uϕ 2 for non-final and final states are the following respectively:

	follows:
		   true	if ϕ 2 {s}
	(ϕ 1 Uϕ 2 ){s} =	(ϕ 1
		
		

  .2.5 Strategy encoding for ϕ 1 Rϕ 2 formulae The derivatives of ϕ 1 Rϕ 2 for non-final and final states respectively are defined as Rϕ 2 ) if ϕ 2 {s} and ¬(ϕ1 {s}) Rϕ 2 ){s ↓ } = true if φ 2 {s ↓ } false if ¬(ϕ 2 {s ↓ })The strategy encoding the temporal formula ϕ 1 Rϕ 2 tests first if the current state satisfies ϕ 2 : if it does, then the inconclusive guard is transformed into a positive guard; otherwise, it tests if the current state satisfies ϕ 1 : if it does, then we continue with an inconclusive guard (hence all previous and current states in the execution satisfy ϕ 1 ), else we found a state where neither ϕ 1 or ϕ 2 are satisfied, hence the formula ϕ 1 Rϕ 2 is not satisfied by the execution. The strategies Θ and Θ ↓ encoding ϕ 1 Rϕ 2 for non-final and final states are the following respectively:

	follows:
		   true	if ϕ 2 {s} and ϕ 1 {s}
	(ϕ 1 Rϕ 2 ){s} =	  (ϕ 1 false	if ¬(ϕ 2 {s})
	(ϕ 1

  We obtain a similar result for a bad prefix if we replace the guard |= φ by |= φ.4.3 Example: Repairing a property of the loaning service specificationConsider a biochemical program P describing the library loaning service from Examples 2.1 consisting of: the library of the Maths department with 6 Statistics textbooks and 6 Maths students, the library of the CS department with 3 Statistics textbooks and 6 CS students, and the strategies given in Example 2.4. We guard the program P with the safety formula φ

1 |= ? φ =⇒ s j |= ? φ and s i-1 |= ? φ =⇒ s i |=φ , or • s 0 |= ? φ =⇒ s 1 |= ? φ =⇒ . . . =⇒ s n |= ? φ and s n |= ? φ ≡ s n |=φ .

  . . s n , u is a good prefix for Xϕ if and only if n ≥ 1 and s 0 |= ? Xϕ =⇒ s 1 |= ? ϕ/Xϕ =⇒ s 2 |=Xϕ . The finite trace u is a bad prefix for Xϕ if and only if n = 0 or n ≥ 1 and s 0 |= ? Xϕ =⇒ s 1 |= ? ϕ/Xϕ =⇒ s 2

	|=Xϕ

Andrei and Kirchner

For future work we plan to implement the runtime verification technique described in this paper in the PORGY system [2], an environment for visual modelling of complex systems through graphs and graph rewriting rules. PORGY is still under development but already provides tools to visualise traces of rewriting, and a strategy language has been designed in particular to guide the construction of the derivation tree. We envisage applications to wireless sensor networks and biochemical signalling pathways to accompany their formal model development by analysing random executions and critical properties.

α φ 1 ≡ α φ 2 if φ 1 and φ 2 are syntactically equivalent

We introduce an intermediate form of guarded programs, (M ⇛ K)@[K] H , consisting of the application of an abstraction on a guarded program of the form [K] H . We need it to define the new extended reduction relation for guarded program.

Let Z and W denote respectively sets of variables for configurations and for guarded programs. We define new abstractions over guarded programs of the form W ⇛ ⇒ GS and [Z] H ⇛ ⇒ GS where W ∈ W, Z ∈ Z and GS a guarded program. Definition 4.1 The structural congruence relation on guarded biochemical programs is the least equivalence relation on guarded biochemical programs generated by the equation:

and by the following equations oriented from left to right:

where {Z → K ′ }K denotes the replacement of all occurrences of the variable Z in K by K ′ .

In the following we explain each of the three application reductions included in the definition of the structural congruence relation above. First, the application of an abstraction M ⇛ ⇒ K on a guarded program [K ′ ] H is equivalent to the application of the abstraction to the top-level configuration of the guarded program since the abstraction M ⇛ ⇒ K as no effect on the guard H. Second, the application of an abstraction with a guarded program variable as left-hand side on any guarded program returns its right-hand side: the matching substitution associates W to [K ′ ] H ′ and the application result is the right-hand side [K] H (the matching substitution does not modify it). Third, the application of an abstraction [Z] H ⇛ ⇒ [K] H on a guarded program [K ′ ] H ′ produces a matching substitution associating variable Z to K ′ and returns the right-hand side [K] H of the abstraction where every occurrence of the variable Z is replaced by K. Example 4.3 An example of safety formula in the library service model is the property that a student should always be able to borrow a book from any departmental library G( ◊ S (id , dpt, 2 ) ∧ ◊ B (b, nil , 0 ))) with formula S (id , dpt, 2 ) standing for a student connected to a library in requesting mode and formula B (b, nil , 0 ) standing for an available book. We can formulate other formulae such as: ¬G( ◊ B (b, SID, i ) ∧ ◊ B (b, SID, j )) stating that a book cannot be simultane-


Hui-Boon Tan

-Boon

Eng-Tuck Cheah

Johnnie E V Johnson

Markets < G1 -General Financial Markets < G -Financial Economics, F36 -Financial Aspects of Economic Integration < F3 -International Finance < F -International Economics, C22 -Time-Series Models < C2 -Econometric Methods: Single Equation Models

Keywords: Stock Market Capitalization, Financial Integration, Cointegration, Granger Causality, Speed of Adjustment

The stock market capitalization (SMC) of a country, defined as the aggregated market value equity of companies in the respective equity market, is commonly used to measure the widening and deepening of stock market activity. SMC also influences economic growth predictions and public consensus concerning the value of the stock market. However, no previous work has examined the role this variable plays in the process of financial integration. This paper provides an argument for the use of SMC as a means of deciding which countries are acting as leaders in creating a fully integrated equity market in the Asia Pacific region. A total of twelve countries in the Asia Pacific region were divided into 'Emerging Market' and ' Advanced Market' equity blocks. We examine the relative size of the speed of adjustments derived from the error correction models following the Engle-Granger two-step procedure framework and apply the Granger causality test. The results suggest that Hong Kong SAR possesses the necessary credentials to act as market leader. In fact, Hong Kong SAR appears to be the only contender for market leader of both the 'Emerging Market' and ' Advanced Market' equity blocks.

STOCK MARKET CAPITALIZATION AND FINANCIAL INTEGRATION IN THE ASIA PACIFIC REGION I. INTRODUCTION

Arguably, the significant economic growth experienced by Asia Pacific countries following financial integration (prior to the Asian financial crisis) arose from an inflow of equity investments into the emerging markets. Financial integration increased opportunities for cross-border investment and have led portfolio managers to resort to using a country's total stock market capitalization (SMC) as a criterion for highlighting potential investment opportunities. For example, [START_REF] Freeman | A regional platform for trading Southeast Asia equities: viable option or lofty "red herring?[END_REF] argued that most Asian Pacific equity markets, with the exceptions of Malaysia and Singapore, are not considered by fund managers due to their relatively small size. As policy makers in the Asia Pacific region were aware of the fact that in order to attract foreign equity market participants to invest in their respective countries, efforts to widen and deepen their respective equity markets were undertaken.

Consequently, a larger equity market (higher SMC) reflects a more mature and developed equity market.Therefore, in order to enjoy the benefits from a unified group of equity markets, governments in the Asia Pacific region have initiated financial integration processes to remove financial barriers, such as capital control measures. This appears to occur even though an integrated financial market implies that a financial crisis or post-crisis recovery experienced in one country is likely to quickly transmit to others [START_REF] Click | Stock market integration in ASEAN after the Asian financial crisis[END_REF].

A country's SMC, the aggregated market value equity of companies in the respective equity market, has traditionally been used as a measure of stock market activity [START_REF] Torre | Stock market development under globalization: whither the gains from reforms[END_REF]Rajan&Zingales, 1998). It is also used to reflect a country's level of credit and economic growth, in anticipation of future growth in the equity market. This arises because equity 3 markets capitalize the present value of future growth opportunities (Rajan&Zingales, 1998).

SMC is also used by investors as a measure of public consensus and confidence in the value of an equity market. However, no prior studies have used SMC to measure the degree of financial integration among financial markets within an international setting.

This paper is the first to use SMC to determine the potential leader in the Asia Pacific region's financial integration process. The identification of a leader in this process is important since it can help to establish a properly coordinated policy for removing trade and financial barriers, to allow for wider investor participation. In addition, in the event of a financial or economic crisis, the leader can be looked upon to provide the necessary policy recommendations and the smooth execution of these policies to ensure a return to stability.

The paper has two objectives: First, to use SMC to provide empirical evidence concerning the dynamics of financial integration in the Asia Pacific region. Second, to identify the potential leader in the region; that equity market which is likely to propel the region into the next stage of financial integration. These objectives are achieved by dividing the twelve countries in the region into an "Emerging" and "Advanced" Markets Blocks (EMB and AMB).

Cointegration analysis is then conducted between the SMC of each country and the equity blocks. We perform a Granger causality test to explore whether the SMC of a country Granger-causes the growth in SMC of the equity blocks. An individual country is identified as a potential leader in the financial integration process in the Asia Pacific region if it is an attractor (one which has a larger absolute speed of adjustment coefficient estimate than the absolute speed of adjustment coefficient estimate of the respective equity block) and

Granger-causes the growth in the respective equity blocks. Our results reveal that Hong Kong SAR is the most likely leader in the region. The structure of this paper is as follows: A brief review of the financial integration literature is provided in Section 2. In Section 3, the data is described and the methodology is discussed.

The short-run causal impact of the bivariate relationships between the respective equity blocks and the individual equity markets are investigated and discussed (via pair-wise error correction models) in Section 4. The important results of the paper and their implications are discussed in the conclusion (Section 5).

II. FINANCIAL INTEGRATION

Previous work on financial integration has focused on developed countries (Arshanapalli&Doukas, 1993). Research on financial integration across the Asian economies has produced contradictory conclusions [START_REF] Click | Stock market integration in ASEAN after the Asian financial crisis[END_REF]or, at best, mixed conclusions [START_REF] Cavoli | A survey of financial integration in East Asia: how far? How much further to go? Discussion Paper 0401[END_REF]. For example, [START_REF] Ng | Stock market linkages in South-East Asia[END_REF] found no cointegrating relationship among ASEAN-5 equity markets, whereas, [START_REF] Click | Stock market integration in ASEAN after the Asian financial crisis[END_REF] found cointegrating relationships between ASEAN-5 equity markets and [START_REF] Daly | Southeast Asian stock market linkages: evidence from pre-and post-October 1997[END_REF] reports mixed findings. However, these studies take a partial and abstracted view of the financial integration process. Finally, some studies have examined the degrees of financial integration in the region, without identifying a leader with the potential to spearhead the process.

Consequently, it is now timely to examine which country is likely to lead in the next phase of the financial integration process in the Asia Pacific region.

In this study, we use SMC to measure the degree of financial interdependence in Asia Pacific equity markets and to identify a potential leader to bring these distinct equity markets into a larger, more unified equity block. This approach is motivated by the fact that the use of equity market size in general, and SMC in particular, has been the subject of much recent debate (e.g., [START_REF] Desai | Taxes, dividends and international portfolio choice[END_REF]. In order to identify the Asia Pacific region's potential leading equity market, two criteria were applied: First, the equity market must act as an "attractor equity market"; i.e. the equity market must assume a stronger role in pulling the natural logarithm of the SMC of other equity markets towards the long run equilibrium path. Second, the lagged SMC growth rates of the equity market must Granger-cause the SMC growth rate of the equity block in question (and not vice versa).

F
We employed the well-established two-step cointegration procedure, introduced by Engle and [START_REF] Engle | Cointegration and error correction: representation, estimation and testing[END_REF]. In particular, we employed the unrestricted dynamic modeling approach so that the estimates derived for the long-run relationship are unbiased using the appropriate t-and F-statistics. Since the number of variables in the model does not exceed two, there is no justification for employing the [START_REF] Johansen | Statistical analysis of cointegration vectors[END_REF] approach to test for cointegration. To test for stationarity in the weekly series, the Augmented Dickey-Fuller (ADF) and Phillips-Perron (PP) were used.

Before developing the respective error correction models, it is essential to determine whether the stochastic trends in the natural logarithm of the weekly SMC variable for the 12 countries' equity markets and the two equity blocks (that contained the unit root in the level) ε are the error terms to be tested for stationarity.

The Granger Representation Theorem [START_REF] Engle | Cointegration and error correction: representation, estimation and testing[END_REF] indicates that if two (or more) variables are linked to form an equilibrium relationship spanning the long-run, or are cointegrated, then there exists an error-correction representation of the data; even though the series themselves may contain stochastic trends. In essence, the theorem safeguards the error-correction model from the problem of spurious regression.Therefore, if y t and t

x are I(1), the following error-correction models can be established, respectively, as:

1 1 1 1 1 2 2 1 1 2 ( ) ( ) ( ) ( ) t t t t t t t t L y L x u L x L y u λ α ε η π α ε ϕ - - - - ∆ = + ∆ + ∆ = + ∆ + (2)
where ( )

L λ , ( ) L η , ( ) L π and ( ) L ϕ
are polynomials in the lag operator L, given as 8 system in the current period from its equilibrium. In other words, the speed of adjustment is a mechanism which enables the system to correct the disequilibrium in the system quickly, by forcing the system to return to its long-run steady-state growth path.

1 1 ( ) 1 ... p p L L L λ λ λ = - -- , 0 1 1 1 1 ( ) ... q q L L L η η η η + + - = -- , 1 1 ( ) 1 ... p p L L L π π π = - -- , 0 1 1 1 1 ( ) ... q q L L L ϕ ϕ ϕ ϕ + + - = -- .At least
Two important properties of the speed of adjustment coefficients are worth mentioning:

First, 1 α measures the speed that the natural logarithm of the SMC of an individual equity market adjusts to the equilibrium path. This, in turn, is determined by the natural logarithm of the SMC of the equity block. In this case, the equity block appears to be the force of attraction to the individual equity market. Second, the speed of adjustment parameter will take an absolute value between zero and one; a value close to zero indicates a tendency for the system to fail to correct the disequilibrium to its long-run equilibrium, and a value close to one indicates a tendency for the system to narrow the distance (in the current period) from its long-run equilibrium path. Similarly, 2 α captures the speed that the natural logarithm of the SMC of the equity block corrects towards the long-run equilibrium path (which is determined by thenatural logarithm of the SMC of the individual equity market). In this latter case, the individual equity market acts as the attractor. By observing which of the absolute ECTs from Equation 2, 1 α and 2 α , has the larger value, we can identify whether the individual equity market or the respective equity block is acting as the attractor to the underlying long-run equilibrium path.

Error-Correction and Granger-Causality

The error-correction model formulation also provides a means of investigating the short-run causal impact between the growth rate of the SMC of the individual stock market and the respective equity block, and vice versa. [START_REF] Granger | Investigating causal relations by econometric models and crossspectral methods[END_REF] maintained that long-run equilibrium is a concern for cointegration, while short-run forecastability is the concern of = . The chosen, optimal number of lags for p and q are based on AIC, following the sequential procedure outlined by Hsiao (1979a, b). This procedure requires the addition of q lags to the error correction model, once the number of p lags, which minimizes the AIC, has been chosen.

IV. RESULTS AND DISCUSSION

Results

The results of the unit root tests using the ADF and PP tests are reported in Table 2. The usual information based rule, namely the AIC, is used to determine the optimal lag length 1 .

[Insert Table 2 here]

Results presented in Table 2 suggest that the natural logarithm transformed weekly SMC variable is not stationary in its level form. These series appear to be stationary for all countries in the Asia Pacific region after taking the first difference (growth rate in SMC). The same is true for the EMB and AMB.

[Insert Table 3, 4, 5 and 6 here]

The results of the Engle-Granger two-step cointegration test, presented in Table 3, reveal the existence of cointegration relationships between the individual equity markets against the two equity blocks. The adequacy of the cointegration model used this study is confirmed by 1 For a detailed discussion of the guidelines for determining the optimal lags for inclusion in the unit root tests, refer to [START_REF] Ng | Unit root tests in ARMA models with data-dependent methods for the selection of the truncation lag[END_REF]. 3). The results presented in the last columns of Tables 4 and5 show the pair-wise estimated coefficients of the speed of adjustment of individual stock markets against the long-run equilibrium path (as determined by the respective equity block, and vice versa). The adequacy of the error correction models is confirmed by the negative and statistically significant ECT coefficients, which are presented as the estimated speed of adjustment coefficients in the last columns in Tables 4 and5. From the results presented in Panel A of Table 5, it is also clear that, with the exception of China, the speed of adjustment estimates of all individual equity markets in the EMB are statistically significant at the 1 percent level. For China, the natural logarithm of SMC is correcting towards the equilibrium long-run path (which is determined by the EMB) but there is no evidence of the natural logarithm of SMC of EMB correcting towards the equilibrium long-run path determined by China. This is clear as the speed of adjustment estimate 2 α is not statistically significant. All of the estimates for the speed of adjustment pairs (shown in Panel B, Table 5) are statistically significant at 1 percent for the AMB. It appears that the two equity blocks are also adjusting to the long-run equilibrium path (results are significant at the 1 percent; see Panel C, Table 4).

Comparing the relative sizes of the absolute ECTs, we generate a list of attractor markets (shown in second column, Table 6.); in particular, Korea, Hong Kong SAR and Singapore for EMB and China, Malaysia, Hong Kong SAR, Australia, Singapore and New Zealand for AMB.

As indicated above, the results from this test only satisfy the first criterionfor identifying the leader. It is clear that the natural logarithm of SMC of the equity blocks also needs to correct The results from a Wald test of jointly testing for all lagged independent variables are reported in Tables 4 and5. The direction of causality is summarized in column 3 of Table 6.

Allowing for bi-directional causality, the SMC growth rate in Indonesia appears to be causing (significant at the 1 percent level) the growth in the SMC of the EMB in the Granger sense (see Panel A of Table 4). In addition, the results suggest that the SMC growth rate of Hong Kong SAR Granger-cause the growth in the EMB (see Panel B, Table 4). By comparing the results for the EMB and AMB, the SMC growth rate of EMB appears to be Granger-causing the growth in SMC in AMB (see Panel C of Table 4). The results also indicate (at the 1 percent level of significance) that the SMC growth rates of all emerging equity markets, with the exception of Korea, are Granger causing the growth in the AMB (see Panel A, Table 5). In addition, with the exception of Japan and New Zealand, the growth rate of SMC of the individual advanced equity markets are Granger causing the growth in the AMB (see Panel B of Table 5).

When the two leadership conditions are jointly considered (i.e. equity market must be an attractor and must Granger-cause the growth in the SMC of the respective equity block),

Hong Kong SAR appears to be the overall leader in the Asia Pacific region, as it fulfills both conditions in both equity blocks. China, Malaysia, Hong Kong SAR, Australia and Singapore are all identified as possible potential leadersforthe AMB. However, Malaysia may be eliminated from this list, since the relative absolute values of its speed of adjustment derived from the pair-wise error correction model are close. If only uni-directional causality is allowed, then only China and Hong Kong SAR emerge as the potential leaders for the AMB (see last column, Table 6). We have explored the financial integration dynamics in the Asia Pacific region using SMC. As indicated above, SMC is used as a proxy for a host of financial performance measures related to the respective equity markets (such as stock market activity, level of credit and economic growth). It is clear from our findings that the size of the respective equity markets helps to identify the potential leading equity market in the region. Identifying this leader has several implications. First, to provide financial stability in terms of policy coordination during a financial crisis [START_REF] Click | Stock market integration in ASEAN after the Asian financial crisis[END_REF], is vital to identify the leader to ensure that coordinated policy implementations can be executed. Further, concerted and coordinated efforts to remove trade and financial barriers among member countries can be achieved by a strong equity market leading the way. This includes the removal of qualitative barriers, as well as capital controls, legislative control over deposits and many other non-tariff barriers on financial services. This will enable a general reduction in the cost of equity and allow financial asset portfolio diversification to yield its maximum benefit in terms of risk reduction [START_REF] Levy | International diversification of investment portfolios[END_REF]. Subsequently, this is likely to attract further equity inflow into the region and can increase the competitiveness of the region for equity inflows [START_REF] Freeman | A regional platform for trading Southeast Asia equities: viable option or lofty "red herring?[END_REF]. Here, we have proposed the use of SMC as a means of identifying the market which should play the leading role in this process.

Implications of Study

V. CONCLUSION

We have argued that the size of a particular equity market plays an important role in deciding the status of a leader within a region and this study tests for financial integration in the Asia Pacific region, using the Engle-Granger two-step approach on the SMC growth rate.

Our results show that the size of equity markets, measured by their SMC growth rates, matter in determining potential leaders within the Asia Pacific region. Such countries can take an important role in spearheading the region into a full-fledged and integrated capital market block. Our results suggest Hong Kong SAR has the potential totake a leading role in Figures in parentheses under the independent variables signify the number of lags p and q which minimizes the AIC.

3.

The F-values in column 3 denotes the Wald test of restricted model where all lagged independent terms are equal to zero under the null hypothesis. The p-values are in parentheses.

4.

The speed of adjustment coefficients are reported along with their respective p-values. Figures in parentheses under the independent variables are signifies the number of lags p and q which minimizes the AIC.

3.

The F-values in column 3 denotes the Wald test of restricted model where all lagged independent terms are equal to zero under the null hypothesis. The p-values are in parentheses.

4.

The speed of adjustment coefficients are reported along with their respective p-values. If uni-directional causality is taken, only China and Hong Kong SAR will appear to be the leaders for AMB and Hong Kong SAR will appear as the overall leader in the Asia Pacific region.

3.

Malaysia is ruled out as the estimated relative absolute size in terms of speed of adjustment coefficient derived from the corresponding error correction models are relatively close.

  results of the ADF test on the residuals on each equation in Equation 1(as presented in Table

  towards the natural logarithm of SMC of the individual equity market for it to provide the leadership role. Our results clearly show that Hong Kong SAR and Singapore act as the collective leaders of this Asia Pacific region, as the natural logarithm of SMC of the two equity blocks are correcting towards the natural logarithm of SMC of Hong Kong SAR and Singapore.

  of financial integration in this region.However, whether or not Hong Kong SAR takes up this challenge remains to be seen.

  one of the speed of adjustments coefficients, 1

	F o r
	P
	e
	e r
	R
	e
	v i e
	w
	α or
	2 α , is significantly different from zero and 1 1 t ε -and 2 1 t ε -are the error-correction terms
	(ECT) in the model. The formulation in Equation 2 above allows us to estimate the
	corresponding ECT coefficients, which indicate the strength and speed of adjustment

towards long-run equilibrium. These speed of adjustment values measure the proportion of last period's equilibrium error that is corrected by the narrowing of the distance of the

Table 1 :

 1 Summary Statistics. The critical values of the ADF and PP tests are based on MacKinnon (1996) one-sided p-value. 3. Figures in parentheses under the estimated values of ADF signify the estimated values of the corresponding PP test.

	TABLES

Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

Table 3 :

 3 Evidence of Cointegrations between SMCs.

	Panel A

Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

Page 20 of 27 Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

	Submitted Manuscript
	F o r P e e r R e v i e w
	20

Table 4 :

 4 Estimates of Error Correction Models against Emerging Market Block.

	Dependent Variable	Independent Variable	Wald F-test	Speed of Adjustment
			(p-value)	Coefficient
				(p-value)
		Panel A: Individual Emerging Equity Markets against Emerging Market Block
	China	EMB	19.70069***	-0.779117***
		(2, 6)	(0.0000)	(0.0000)
	EMB	China	6.679414**	-0.251885
		(5, 2)	(0.0105)	(0.1504)
	Indonesia	EMB	6.443682**	-0.64234***
		(2, 1)	(0.0119)	(0.0000)
	EMB	Indonesia	9.116705***	-0.485543***
		(5, 2)	(0.0029)	(0.0008)
	Korea	EMB	5.149842**	-0.363091**
		(4, 1)	(0.0243)	(0.0236)
	EMB	Korea	0.115936	-0.485083***
		(5, 1)	(0.7338)	(0.0003)
	Malaysia	EMB	11.25897***	-0.843909***
		(4, 4)	(0.0009)	(0.0000)
	EMB	Malaysia	4.515803**	-0.337252**
		(5, 1)	(0.0348)	(0.0129)
	Philippines	EMB	15.05381***	-0.772915***
		(2, 3)	(0.0001)	(0.0000)
	EMB	Philippines	4.52804**	-0.481801***
		(3, 2)	(0.0345)	(0.0001)
	Taiwan	EMB	36.05928***	-0.61523***

Page 21 of 27 Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

			Submitted Manuscript
		(1, 4)	(0.0000)	(0.0000)
	EMB	Taiwan	0.290822	-0.538728***
		(3, 2)	(0.5903)	(0.0004)
	Thailand	EMB	8.879683***	-0.706711***
		(2, 2)	(0.0032)	(0.0000)
	EMB	Thailand	1.856584	-0.576348***
	Japan EMB Hong Kong SAR EMB Australia EMB Singapore	Panel B: Individual Advanced Equity Markets against Emerging Market Block EMB (2, 3) 19.37817*** (0.0000) -0.643777*** (0.0000) Japan (3, 1) 2.459042 (0.1184) -0.521199*** (0.0000) EMB (4, 4) 9.327231*** (0.0026) -0.597776*** (0.0025) Hong Kong SAR (3, 3) 9.229452*** (0.0027) -0.815902*** (0.0000) EMB (3, 3) 21.14276*** (0.0000) -0.84493*** (0.0000) Australia (3, 1) 2.058858 (0.1528) -0.618561*** (0.0000) EMB (4, 6) 32.93215*** (0.0000) -0.766225*** (0.0000) F o r P e e r R e v i e w (3, 2) (0.1745) (0.0000)
	EMB	Singapore	4.30954**	-0.788452***
		(3, 2)	(0.0392)	(0.0000)
	New Zealand	EMB	5.641265**	-0.810908***
		(1, 1)	(0.0184)	(0.0000)
	EMB	New Zealand	0.402935	-0.649744***
		(2, 1)	(0.5263)	(0.0000)
			21

Page 22 of 27 Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

				Submitted Manuscript
			Panel C: Advanced Markets Block against Emerging Markets Block
		AMB	EMB	20.6137***	-0.683884***
			(4, 3)	(0.0000)	(0.0001)
		EMB	AMB	4.302481**	-0.618691***
	Notes: 1. 2.	(3, 2) ***denotes significance at 1 percent; **denotes significance at 5 percent; *denotes significance at 10 percent. (0.0393) (0.0000) F o r P e e r R e v i e w
				22

Page 23 of 27 Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

	Submitted Manuscript
	F o r P e e r R e v i e w
	23

Table 5 :

 5 Estimates of the Error Correction Models against Advanced Market Block.

	Dependent Variable	Independent Variable	Wald F-test	Speed of Adjustment Coefficient
			(p-value)	(p-value)
		Panel A: Individual Emerging Equity Markets against Advanced Market Block
	China	AMB	0.096184	-0.563683***
		(2, 1)	(0.7568)	(0.0000)
	AMB	China	12.29548***	-0.733785***
		(2, 3)	(0.0006)	(0.0000)
	Indonesia	AMB	14.08945***	-0.87125***
		(2, 4)	(0.0002)	(0.0000)
	AMB	Indonesia	16.13188***	-0.716338***
		(3, 2)	(0.0001)	(0.0000)
	Korea	AMB	13.84236***	-0.737018***
		(3, 2)	(0.0003)	(0.0000)
	AMB	Korea	3.773704*	-0.407259**
		(4, 1)	(0.0534)	(0.0105)
	Malaysia	AMB	5.495756**	-0.728974***
		(3, 2)	(0.0200)	(0.0000)
	AMB	Malaysia	17.29416***	-0.755547***
		(3, 3)	(0.0000)	(0.0000)
	Philippines	AMB	1.541935	-0.729709***
		(2, 1)	(0.2157)	(0.0000)
	AMB	Philippines	23.98597***	-0.719533***
		(3, 3)	(0.0000)	(0.0000)
	Taiwan	AMB	13.26778***	-0.801936***
		(1, 2)	(0.0003)	(0.0000)
	AMB	Taiwan	9.762198***	-0.687157***
		(3, 1)	(0.002)	(0.0000)
	Thailand	AMB	10.0047***	-0.84583***
		(2, 2)	(0.0018)	(0.0000)
	AMB	Thailand	7.210975***	-0.817329***
		(2, 2)	(0.0078)	(0.0000)

Page 24 of 27 Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

		Submitted Manuscript
	Notes: 1.	F o r P e e r R e v i e w
		24

***denotes significance at 1 percent; **denotes significance at 5 percent; *denotes significance at 10 percent. 2.

Page 25 of 27 Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK Submitted Manuscript F o r P e e r R e v i e w 25Table 6 :

 6 Panel B: Individual Advanced Equity Markets against Advanced Market Block Leaders for Emerging and Advanced Market Blocks at 1 percent level of significance. The leading equity markets selected are jointly based on a 1 percent level of significance from the Wald test and it being an attractor in the pairwise error correction model in Table4 and 5.2.

				Submitted Manuscript
	Japan Equity Market/Block	AMB Attractor	3.098978* Causality	-0.709438** Leading Equity Market
			(4, 2)	(0.0799)	(0.0295)
		AMB	Japan	0.71199	-0.167401
			(4, 1)	(0.3998)	(0.5740)
		Hong Kong SAR	AMB	2.705466	-0.545825***
	Notes: 1.	AMB Australia AMB Singapore AMB New Zealand AMB	(3, 2) Hong Kong SAR (4, 3) AMB (4, 2) Australia (3, 3) AMB (2, 4) Singapore (4, 2) AMB (2, 1) New Zealand (2, 2) F o r P e e r R e v i e w (0.1015) 21.72249*** (0.0000) 15.201*** (0.0001) 7.741249*** (0.0059) 18.3439*** (0.0000) 9.944836*** (0.0019) 8.544757*** (0.0039) 6.432093** (0.0119)	(0.0004) -0.877174*** (0.0000) -0.704868*** (0.0001) -0.931003*** (0.0000) -0.646834*** (0.0000) -0.714413*** (0.0000) -0.751229*** (0.0000) -0.798965*** (0.0000)
				27

Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK

Page 28 of 27 Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK Submitted Manuscript

			Hong Kong → AMB
	Australia and AMB	Australia	Bi-directional	Yes
			Australia ↔ AMB
	Singapore and AMB	Singapore	Bi-directional	Yes
			Singapore ↔ AMB
	New Zealand and AMB	New Zealand	Uni-directional	No
			AMB→ New Zealand

Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK Submitted Manuscript

ACKNOWLEDGEMENTS

The authors would like to thank Jean-Yves Pitarakis, Jan Podivinsky and TaufiqChoudhury of University of Southampton for helpful comments and suggests. Panel A: Individual Equity Emerging Markets against Emerging Markets Block Developed and EMB EMB Uni-directional EMB→ Developed No China and EMB EMB Uni-directional EMB→ China No Indonesia and EMB EMB Uni-directional Indonesia → EMB No Korea and EMB Korea No causality No Malaysia and EMB EMB Uni-directional EMB→ Malaysia No Philippines and EMB EMB Uni-directional EMB→ Philippines No Taiwan and EMB EMB Uni-directional EMB→ Taiwan No Thailand and EMB EMB Uni-directional EMB→ Thailand No Japan and EMB EMB Uni-directional EMB→ Japan No Hong Kong SAR and EMB Hong Kong SAR Bi-directional Hong Kong ↔ EMB Yes

Editorial Office, Dept of Economics, Warwick University, Coventry CV4 7AL, UK Submitted Manuscript