Benedikt Bollig
email: bollig@lsv.ens-cachan.fr

Aiswarya Cyriac
email: cyriac@lsv.ens-cachan.fr

Paul Gastin
email: gastin@lsv.ens-cachan.fr

Marc Zeitoun Lsv

Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking ⋆

We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and that, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.

Introduction

We are concerned with the analysis of computer programs and systems that consist of several components sharing an access to resources such as variables or channels. Any component itself might be built of several modules that can be called recursively resulting in complex infinite-state systems. The analysis of such programs, which consist of a fixed number of recursive threads communicating with one another, is particularly challenging, due to the intrinsically high complexity of interaction between its components. All the more, it is important to provide tools and algorithms that support the design of correct programs, or verify if a given program corresponds to a specification.

It is widely acknowledged that linear-time temporal logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] is a yardstick among the specification languages. It combines high expressiveness (equivalence to first-order logic [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF]) with a reasonable complexity of decision problems such as satisfiability and model checking. LTL has originally been considered for finite-state sequential programs. As real programs are often concurrent or rely on recursive procedures, LTL has been extended in two directions.

First, asynchronous finite-state programs (asynchronous automata) [START_REF] Zielonka | Notes on finite asynchronous automata[END_REF] are a formal model of shared-memory systems and properly generalize finite-state sequential programs. Their executions are no longer sequential (i.e., totally ordered) but can be naturally modeled as graphs or partial orders. In the literature, these structures are known as Mazurkiewicz traces. They look back on a long list of now classic results that smoothly extend the purely sequential setting (e.g., expressive equivalence to first-order logic) [START_REF] Diekert | The Book of Traces[END_REF][START_REF] Diekert | Pure future local temporal logics are expressively complete for Mazurkiewicz traces[END_REF].

Second, in an influential paper, Alur and Madhusudan extend the finite-state sequential model to visibly pushdown automata (VPA) [START_REF] Alur | Adding nesting structure to words[END_REF]. VPA are a flexible model for recursive programs, where subroutines can be called and executed while the current thread is suspended. The execution of a VPA is still totally ordered. However, it comes with some extra information that relates a subroutine call with the corresponding return position, which gives rise to the notion of nested words [START_REF] Alur | Adding nesting structure to words[END_REF]. Alur et al. recently defined versions of LTL towards this infinitestate setting [START_REF] Alur | A temporal logic of nested calls and returns[END_REF][START_REF] Alur | Firstorder and temporal logics for nested words[END_REF] that can be considered as canonical counterparts of the classical logic introduced by Pnueli.

To model programs that involve both recursion and concurrency, one needs to mix both views. Most approaches to modeling concurrent recursive programs, however, reduce concurrency to interleaving and neglect a behavioral semantics that preserves independencies between program events [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF][START_REF] La Torre | A robust class of context-sensitive languages[END_REF][START_REF] La Torre | Context-bounded analysis of concurrent queue systems[END_REF][START_REF] Atig | Global Model Checking of Ordered Multi-Pushdown Systems[END_REF]. A first model for concurrent recursive programs with partial-order semantics was considered in [START_REF] Bollig | Realizability of concurrent recursive programs[END_REF]. Executions of their concurrent VPA equip Mazurkiewicz traces with multiple nesting relations. Temporal logics have not been considered, though, and there is for now no canonical merge of the two existing approaches. It must be noted that satisfiability is undecidable when considering multiple nesting relations, even for simple logics. Yet, it becomes decidable if we restrict to system behaviors that can be executed within a bounded number of phase switches, a notion introduced in [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]. A phase switch consists of a transfer of control from one process to another. This allows for the discovery of many errors, since they typically manifest themselves after a few phase switches [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF].

In this paper, we present linear-time temporal logics for concurrent recursive programs. A temporal logic is parametrized by a finite set of modalities that are definable in monadic second-order logic (cf. [START_REF] Gastin | Satisfiability and model checking for MSO-definable temporal logics are in PSPACE[END_REF]). In addition, it provides path expressions similar to those from PDL [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] or XPath [START_REF] Libkin | Logics for Unranked Trees: An Overview[END_REF], which are orthogonal to the modalities. This general framework captures temporal logics considered in [START_REF] Alur | A temporal logic of nested calls and returns[END_REF][START_REF] Alur | Firstorder and temporal logics for nested words[END_REF][START_REF] Dax | Alternation elimination for automata over nested words[END_REF] when we restrict to one process, and it captures those considered in [START_REF] Diekert | Pure future local temporal logics are expressively complete for Mazurkiewicz traces[END_REF][START_REF] Gastin | Satisfiability and model checking for MSO-definable temporal logics are in PSPACE[END_REF][START_REF] Gastin | Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces[END_REF] when we go without recursion. Our decision procedures for the (bounded phase) satisfiability problem are optimal in all these special cases, but provide a unifying proof. They also apply to other structures such as ranked and unranked trees. We then use our logics for model checking. To do so, we provide a system model whose behavioral semantics preserves concurrency (unlike the models from [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF][START_REF] Atig | Global Model Checking of Ordered Multi-Pushdown Systems[END_REF][START_REF] La Torre | A robust class of context-sensitive languages[END_REF]). The complexity upper bounds from satisfiability are preserved.

Summarizing, we provide a first framework to specify linear-time properties of concurrent recursive programs appropriately over partial orders.

Outline In Section 2, we introduce some basic notions such as graphs and trees, and we define nested traces, which serve as our model of program executions. Section 3 provides a range of temporal logics over nested traces. In Section 4, we state and solve their satisfiability problem. Section 5 addresses model checking.

Graphs, Nested Traces, and Trees

To model the behavior of distributed systems, we consider labeled graphs, each representing one single execution. A node of a graph is an event that can be observed during an execution. Its labeling reveals its type (e.g., procedure call, return, or internal) or some processes that are involved in its execution. Edges reflect causal dependencies: an edge (u, v) from node u to node v implies that u happens before v. A labeling of (u, v) may provide information about the kind of causality between u and v (e.g., successive events on some process).

Accordingly, we consider a signature, which is a pair S = (Σ, Γ ) consisting of a finite set Σ of node labelings and a finite set Γ of edge labelings. Throughout the paper, we assume |Σ| ≥ 1 and |Γ | ≥ 2. An S-graph is a structure G = (V, λ, ν) where V is a non-empty set of countably many nodes, λ : V → 2 Σ is the nodelabeling function, and ν : (V × V ) → 2 Γ is the edge-labeling function, with the intuitive understanding that there is an edge between u and v iff ν(u, v) = ∅.

For σ ∈ Σ, V σ := {u ∈ V | σ ∈ λ(u)} denotes the set of nodes that are labeled with σ. Moreover, for γ ∈ Γ , E γ := {(u, v) ∈ V × V | γ ∈ ν(u, v)}
denotes the set of edges with labeling γ. Then, E := γ∈Γ E γ is the set of all the edges. We require that the transitive closure E + of E is a well-founded (strict) partial order on V . We write ≺ G or simply ≺ for E + , and we write G or for E * . Next, we consider concrete classes of S-graphs.

Nested Traces

To model executions of concurrent recursive programs that communicate via shared variables, we introduce graphs with multiple nesting relations. We fix non-empty finite sets Proc and Act, and let Type = {call, ret, int}. Then, Σ = Proc ∪ Act ∪ Type is the set of node labelings. Its component Type indicates whether an event is a procedure call, a return, or an internal action. A nesting edge connects a procedure call with the corresponding return, and will be labeled by cr ∈ Γ . In addition, we use succ p ∈ Γ to label those edges that link successive events of process p ∈ Proc. Thus, Γ = {succ p | p ∈ Proc} ∪ {cr}. We obtain the signature S = (Σ, Γ ). Formally, a nested (Mazurkiewicz) trace over Proc and Act is an S-graph G = (V, λ, ν) such that the following hold:

T1 V = V call ⊎ V ret ⊎ V int = a∈Act V a = p∈Proc V p
T2 for all processes p, q ∈ Proc with p = q, we have

V p ∩ V q ⊆ V int T3 for all p ∈ Proc, E succ p is the direct successor relation of a total order on V p T4 E cr ⊆ (V call × V ret ) ∩ p∈Proc (V p × V p ) T5 for all (u, v), (u ′ , v ′ ) ∈ E cr , we have u = u ′ iff v = v ′ T6 for all p ∈ Proc and u ∈ V call ∩ V p and v ′ ∈ V ret ∩ V p , if u ≺ v ′ then either there exists v v ′ with (u, v) ∈ E cr or there exists u ′ u with (u ′ , v ′ ) ∈ E cr
Intuitively, each event has exactly one type and one action and belongs to at least one process (T1), synchronizing events are always internal (T2), along any process the events are totally ordered (T3), a nesting edge is always between a call and a return of the same process (T4), and cr-edges restricted to any process are well nested (T5 and T6). Note that we may have unmatched calls or returns. For u ∈ V , we let Proc(u) = λ(u) ∩ Proc. When |Proc| = 1, then a nested trace is a nested word in the classical sense [START_REF] Alur | Adding nesting structure to words[END_REF]. The set of nested traces over Proc and Act is denoted by Traces(Proc, Act). Figure 1 depicts a nested trace over Proc = {p, q} and Act = {c, r, sv }. Action c denotes a call, r a return, and sv reveals some synchronization via a shared variable. Node labelings from Proc are given by the gray-shaded regions, i.e., sv -events involve both p and q. Edge labelings succ p and succ q are abbreviated by p and q, resp.

We introduce a restricted class of nested traces over Proc and Act . It is parametrized by an (existential) upper bound k ≥ 1 on the number of phases that a trace needs to be executed. In each phase, return events belong to one dedicated process. Let us first introduce the notion of linearization. A linearization of a nested trace G = (V, λ, ν) is any structure (V, λ, ≤) such that ≤ is a total order extending . Fig. 2 depicts a linearization of the nested trace from Fig. 1. We identify isomorphic structures so that a linearization can be considered as a word over 2 Σ . Note that, for every word w ∈ (2 Σ ) * , there is at most one (up to isomorphism) nested trace G such that w is a linearization of G [START_REF] Diekert | The Book of Traces[END_REF].

For k ≥ 1, a word w ∈ (2 Σ ) * is a k-phase word if it can be written as

w 1 • • • w k
where, for all i ∈ {1, . . . , k}, there is p ∈ Proc such that for each letter a of w i we have ret ∈ a implies p ∈ a. A nested trace is called a k-phase nested trace if at least one of its linearizations is a k-phase word. The set of k-phase nested traces over Proc and Act is denoted by Traces k (Proc, Act). We denote by Lin k (G) the set of linearizations of nested trace G that are k-phase words. In particular, G is a k-phase nested trace iff Lin k (G) = ∅. The nested trace from Fig. 1 is a 2-phase trace: its linearization from Fig. 2 schedules returns of q before all returns of p.

Ranked Trees Let S = (Σ, Γ ). An S-tree is an S-graph t = (V, λ, ν). We require that there is a "root" u 0 ∈ V such that for all u, v, v ′ ∈ V and γ, γ ′ ∈ Γ :

(i) (u 0 , u) ∈ E * , and (v, u), (v ′ , u) ∈ E implies v = v ′ (ii) (u, v), (u, v ′ ) ∈ E γ implies v = v ′ , and (u, v) ∈ E γ ∩ E γ ′ implies γ = γ ′
The tree structure is enforced by (i), and (ii) ensures that every node has at most one γ-successor and edges have a unique label from Γ , which can be seen as a set of directions. Thus, Γ = {left, right} yields binary trees. The set of all S-trees is denoted Trees(S).

Ordered Unranked Trees Each node in an ordered unranked tree can have a potentially unbounded number of children, and the children of any node are totally ordered. Formally it is an S-graph t = (V, λ, ν) over S = (Σ, Γ ) where

Γ = {child, next}. Again, there is a "root" u 0 ∈ V such that for all u, v, v ′ ∈ V : (i) (u 0 , u) ∈ E * and (u 0 , u) / ∈ E next (ii) (v, u), (v ′ , u) ∈ E child implies v = v ′ , and (v, u), (v ′ , u) ∈ E next implies v = v ′ (iii) (u, v), (u, v ′ ) ∈ E next implies v = v ′ and (u, v) ∈ E γ ∩ E γ ′ implies γ = γ ′ (iv) (u, v) ∈ E child implies that there exists v 0 ∈ V such that (u, v 0 ) ∈ E child and, (u, v ′ ) ∈ E child if and only if (v 0 , v ′ ) ∈ E * next .
The set of all ordered unranked trees over S is denoted o.u.Trees(S).

Temporal Logic

In this section, let S = (Σ, Γ ) be any signature. We study temporal logics whose modalities are defined in the monadic second-order (MSO) logic over S-graphs, which we recall in the following. We use x, y, . . . to denote first-order variables which vary over nodes of the graphs, and X, Y, . . . to denote second-order variables which vary over sets of nodes. The syntax of MSO(S) is given by the grammar ϕ ::

= σ(x) | γ(x, y) | x = y | x ∈ X | ¬ϕ | ϕ ∨ ϕ | ∃xϕ |
∃Xϕ where σ ranges over Σ, γ ranges over Γ , x and y are first-order variables, and X is a second-order variable. We use ≺, the transitive closure of the relations induced by Γ , freely as it can be expressed in MSO(S). For an S-graph G = (V, λ, ν) and a formula ϕ(x 1 , . . . , x n , X 1 , . . . , X m ) with free variables in {x 1 , . . . , x n , X 1 , . . . , X m }, we write G |= ϕ(u 1 , . . . , u n , U 1 , . . . , U m ) if ϕ is evaluated to true when interpreting the variables by u 1 , . . . , u n ∈ V and U 1 , . . . , U m ⊆ V , respectively.

We will use MSO formulas to define modalities of a temporal logic. For m ∈ N = {0, 1, 2, . . .}, we call ϕ ∈ MSO(S) an m-ary modality if its free variables consist of m set variables X 1 , . . . , X m and one first-order variable x.

A temporal logic over S is given by a triple L = (M, arity, [[-]]) including a finite set M of modality names, a mapping arity : M → N, and a mapping

[[-]] : M → MSO(S) such that, for M ∈ M with arity(M ) = m, [[M ]
] is an m-ary modality. Its syntax, i.e., the set of formulas ϕ ∈ Form(L) is given by

ϕ ::= σ | ¬ϕ | ϕ ∨ ϕ | M (ϕ, . . . , ϕ arity(M) ) | ∃π π ::= ?ϕ | γ | γ -1 | π ∪ π | π ∩ π | π • π | π * [[σ]] G := V σ [[¬ϕ]] G := V \ [[ϕ]] G [[ϕ 1 ∨ ϕ 2 ]] G := [[ϕ 1 ]] G ∪ [[ϕ 2 ]] G [[M (ϕ 1 , . . . , ϕ m )]] G := {u ∈ V | G |= [[M ]](u, [[ϕ 1 ]] G , . . . , [[ϕ m ]] G )} [[∃π]] G := {u ∈ V | there is v ∈ V such that (u, v) ∈ [[π]] G } [[?ϕ]] G := {(u, u) | u ∈ [[ϕ]] G } [[γ]] G := E γ [[γ -1 ]] G := E -1 γ [[π ⊗ τ ]] G := [[π]] G ⊗ [[τ ]] G [[π * ]] G := [[π]] * G Fig. 3. Semantics of temporal logic
where σ ranges over Σ, M ranges over M, and γ ranges over Γ . We call ϕ a node formula and π a path formula (or path expression). Their semantics wrt. an S-graph G = (V, λ, ν) is defined inductively: for subformulas ϕ, we obtain a set

[[ϕ]] G ⊆ V , containing the nodes of G that satisfy ϕ. Accordingly, [[π]] G ⊆ V × V
is the set of pairs of nodes linked with a path defined by π. Then, ∃π is the set of nodes that admit a path following π. Formally, [[-]] G is given in Fig. 3 where

⊗ ∈ {∪, ∩, •} (• denotes the product of two relations). We may write G, u |= ϕ if u ∈ [[ϕ]] G and G, u, v |= π if (u, v) ∈ [[π]] G . We also use π + := π • π * .
An intersection free temporal logic over S is defined as expected: path expressions do not contain subformulas of the form π 1 ∩π 2 . Moreover, a path-expression free temporal logic does not contain formulas of the form ∃π.

Remark 1. We can easily include π -1 also in our syntax but it is redundant:

(?ϕ) -1 = ?ϕ, (π -1 ) -1 = π, (π 1 ∪ π 2 ) -1 = π -1 1 ∪ π -1 2 , (π 1 ∩ π 2 ) -1 = π -1 1 ∩ π -1 2 , (π 1 • π 2 ) -1 = π -1 2 • π -1 1 and (π * ) -1 = (π -1 ) * Example 2.
We consider the path-expression free temporal logic CTL over (Σ, Γ ) (interpreted over (Σ, Γ )-trees) [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF]. The modalities are M = {EX, EG, EU} with EX and EG being unary and EU being binary. Node formula EX ϕ holds at a node if there is a child satisfying ϕ. Thus,

[[EX]](x, X) = ∃y (x ≺• y ∧ y ∈ X)
where x ≺• y := γ∈Γ γ(x, y). Formula EG ϕ means that there is an infinite path starting from the current node where ϕ always holds. Formula ϕ EU ψ means that there is a path starting from the current node satisfying ϕ until ψ :

[[EG]](x, X) = ∃Y (Y ⊆ X ∧ x ∈ Y ∧ ∀z (z ∈ Y → ∃z ′ (z ′ ∈ Y ∧ z ≺• z ′ ))) [[EU]](x, X 1 , X 2 ) = ∃z (x z ∧ z ∈ X 2 ∧ ∀y (x y ≺ z → y ∈ X 1 ))
Example 3. Our approach captures various logics over unranked trees (see [START_REF] Libkin | Logics for Unranked Trees: An Overview[END_REF] for an overview). E.g., the intersection free temporal logic L - 0 with no modalities over ordered unranked trees is precisely regular XPath [START_REF] Calvanese | An Automata-Theoretic Approach to Regular XPath[END_REF].

Example 4. We give a property over nested traces using a path expression: ϕ = ¬∃(cr ∩ (?q • ( γ∈Γ γ) + • ?(call ∧ p) • ( γ∈Γ γ) + )) means that process p is not allowed to call a new procedure when it is in the scope of an active procedure call from q. The first call node along q in Fig. 1 does not satisfy this property due to the second call of p.

Example 5. We now present a path-expression free temporal logic over nested traces, NTrLTL = (M, arity, [[-]]). The unary modalities are given by {X cr , Y cr } ∪ {X p , Y p | p ∈ Proc}. Intuitively, X p ϕ means that ϕ holds at the next p-position and X cr claims that we are at a call position and ϕ holds at the corresponding return position. The dual past modalities are Y p and Y cr . Formally, the semantics of the future modalities is given by

[[X p ]](x, X) = ∃y (p(y) ∧ x ≺ y ∧ y ∈ X ∧ ∀z (p(z) ∧ x ≺ z → y z)) [[X cr ]](x, X) = ∃y (cr(x, y) ∧ y ∈ X)
The binary modalities consist of {EU, ES, AU, AS, EU a , ES a , EU s , ES s } and {U p , S p , U a p , S a p , U s p , S s p | p ∈ Proc}. Formula ϕ EU ψ means that in the graph G there is a path not using cr-edges from the current node satisfying ϕ until ψ, whereas ϕ AU ψ means that in the partial order G there is a future node satisfying ψ, and ϕ should hold on all nodes in between. Formally, the semantics is given by

[[AU]](x, X 1 , X 2 ) = ∃z (x z ∧ z ∈ X 2 ∧ ∀y (x y ≺ z → z ∈ X 1 )) [[EU]](x, X 1 , X 2 ) = ∃z∃Y (z ∈ X 2 ∧ Y ⊆ X 1 ∧ ∀y (y ∈ Y ∨ y = z) → (y = x ∨ ∃y ′ (y ′ ∈ Y ∧ q∈Proc succ q (y ′ , y))))
A summary path in G is a path that may freely use cr-edges. Formally, the semantics [

[EU s ]](x, X 1 , X 2 ) is defined as ∃z∃Y (z ∈ X 2 ∧ Y ⊆ X 1 ∧ ∀y (y ∈ Y ∨ y = z) → (y = x ∨ ∃y ′ (y ′ ∈ Y ∧ (cr(y ′ , y) ∨ q∈Proc succ q (y ′ , y)))))
An abstract path in G is a path which does not take a succ q -edge from a call node or to a return node. Restricting to abstract paths we obtain the modality

EU a whose semantics [[EU a ]](x, X 1 , X 2 ) is defined as ∃z∃Y (z ∈ X 2 ∧ Y ⊆ X 1 ∧ ∀y (y ∈ Y ∨ y = z) → (y = x ∨ ∃y ′ (y ′ ∈ Y ∧ (cr(y ′ , y) ∨ (¬call(y ′ ) ∧ ¬ret(y) ∧ q∈Proc succ q (y ′ , y))))))
Modalities U p , U s p and U a p are obtained from EU, EU s and EU a by restricting to paths on process p. The semantics is obtained easily by adding the constraint p(x) and replacing q∈Proc succ q by succ p in the formulas above. For instance, the formula ⊤ U a p q says that in the abstract future (that is, in the scope of the current procedure call and with the same stack contents) of process p, there is a synchronizing action with process q.

Modalities AS, ES, ES s , ES a , S p , S s p , and S a p are the past-time counterparts of the above future modalities.

Note that this example captures various logics defined in [START_REF] Alur | Firstorder and temporal logics for nested words[END_REF] for the case |Proc| = 1. For example, when we choose {X cr , Y cr , X p , Y p , EU s , ES s } to be our modalities (where p is the only process in Proc), our logic is precisely NWTL.

In the next section we show that satisfiability problem of any MSO-definable temporal logic L over any of the structures defined in Section 2 (that is, kphase nested traces, ranked trees, and unranked trees) is decidable in 2EXPTIME. Moreover, if L is intersection free, then it is decidable in EXPTIME. Question: Are there t ∈ Trees(S) and node u of t such that t, u |= ϕ ? Theorem 7 ( [START_REF] Göller | PDL with intersection and converse: satisfiability and infinite-state model checking[END_REF][START_REF] Lange | 2-ExpTime lower bounds for Propositional Dynamic Logics with Intersection[END_REF][START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF][START_REF] Vardi | The taming of converse: Reasoning about two-way computations[END_REF]). Let L 0 be the temporal logic over S with M = ∅. The problem Tree-Sat(L 0 ) is 2EXPTIME-complete [START_REF] Göller | PDL with intersection and converse: satisfiability and infinite-state model checking[END_REF][START_REF] Lange | 2-ExpTime lower bounds for Propositional Dynamic Logics with Intersection[END_REF]. For the intersection free fragment L - 0 , the problem Tree-Sat(L - 0 ) is EXPTIME-complete [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF][START_REF] Vardi | The taming of converse: Reasoning about two-way computations[END_REF]. We will extend these results to logics L and L -including MSO modalities. For this, we need the notion of an alternating 2-way tree automaton.

Alternating 2-way Tree Automata An alternating 2-way tree automaton (A2A) over S = (Σ, Γ ) of index r ∈ N is a tuple A = (Q, δ, q 0 , Acc) where Q is a finite set of states, q 0 ∈ Q is the initial state, Acc : Q → N is a parity acceptance condition with r = max(Acc(Q)), and

δ : Q × 2 Σ × 2 D → B + (D × Q)
is the transition function where D = Γ ∪ {stay, up} and B + (D × Q) is the set of positive boolean formulas over D × Q. We only give an intuition of the semantics of A2A and refer to [START_REF] Vardi | The taming of converse: Reasoning about two-way computations[END_REF][START_REF] Göller | PDL with intersection and converse: satisfiability and infinite-state model checking[END_REF] for details. An A2A walks in an S-tree t = (V, λ, ν). A configuration is a set of "threads" (q, u) where q ∈ Q and u ∈ V is the current node. For every thread (q, u), we have to choose some model {(d 1 , q 1 ), . . . , (d n , q n )} of δ(q, λ(u), D ′ ) where D ′ is the set of directions available at u. Then, we replace (q, u) with n new threads (q i , u i ) for 1 ≤ i ≤ n where u i is obtained from u by following direction d i (if d i = stay, then u i = u). The parity acceptance condition has to be applied to all infinite paths when we consider the run as a tree, threads (q i , u i ) being the children of (q, u). For u ∈ V , a run over (t, u) is a run that starts in the single configuration (q 0 , u). The semantics [[A]] t contains all nodes u of t such that there is an accepting run of A over (t, u).

Theorem 8 ([23]

). Given an A2A A of index r with n states, one can check in time exponential in n • r if there is a tree t such that

[[A]] t = ∅.
The main ingredient of the proof of Theorem 7 is the construction of an A2A from a given formula, whose existence is given by the following lemma.

Lemma 9 ([14]

). Consider the temporal logic L 0 over S with M = ∅. For every formula ϕ ∈ Form(L 0 ), we can construct an A2A B ϕ over S of exponential size such that, for all S-trees t, we have

[[ϕ]] t = [[B ϕ ]] t . Moreover, if ϕ ∈ Form(L - 0 ) is intersection free, then B ϕ is of polynomial size.
Using Theorem 8 and Lemma 9, we can extend Theorem 7: Theorem 10. Let L be a temporal logic over S. The problem Tree-Sat(L) is 2EXPTIME-complete. For the intersection free fragment L -, Tree-Sat(L -) is

EXPTIME-complete.
Proof. The lower bounds follow from Theorem 7. We show the upper bounds. Let ϕ be any L formula. Let Subf(ϕ) denote the set of subformulas of ϕ and let top(ξ) denote the topmost symbol of ξ ∈ Subf(ϕ) which could be ∃ or a modality M ∈ M ∪ Σ ∪ {¬, ∨}: below, we treat atomic propositions σ ∈ Σ, negation ¬, and disjunction ∨ as modalities of arities 0, 1, and 2 resp.

For each modality M ∈ M ∪ Σ ∪ {¬, ∨} of arity m, we define an MSO(S) formula ψ M with free variables X 0 , . . . , X m by

ψ M (X 0 , X 1 , . . . , X m ) := ∀x (x ∈ X 0 ←→ [[M ]](x, X 1 , . . . , X m )) .
Let S m = (Σ ∪ {X 0 , . . . , X m }, Γ ) so that the node labeling encodes the valuations of the free set variables as usual. By Rabin's theorem, there is a nondeterministic (N1A) tree automaton A M recognizing all S m -trees satisfying ψ M . Note that A M for M ∈ Σ ∪ {¬, ∨} has only one state.

Let ∃π(ξ 1 , . . . , ξ m ) ∈ Subf(ϕ) where ξ 1 , . . . , ξ m are the node formulas checked in path π. Replacing ξ 1 , . . . , ξ m by set variables X 1 , . . . , X m (or new predicates) we will construct using Lemma 9 an A2A A ∃π accepting all S m -trees satisfying the "formula"

ψ ∃π (X 0 , X 1 , . . . , X m ) := ∀x (x ∈ X 0 ←→ ∃π(X 1 , . . . , X m )) .
By Lemma 9, we can construct automata B 1 and B 2 for ∃π(X 1 , . . . , X m ) and ¬∃π(X 1 , . . . , X m ), resp., which are L 0 formulas. Let ι 1 and ι 2 be the initial states of B 1 and B 2 . The automaton A ∃π includes the disjoint union of B 1 and B 2 plus a new initial state ι (with even priority in the acceptance condition) and, for σ ⊆ Σ ∪ {X 0 , . . . , X m } and D ′ ⊆ D, the transition

δ(ι, σ, D ′ ) = γ∈D ′ (γ, ι) ∧ (stay, ι 1 ) if X 0 ∈ σ (stay, ι 2 ) otherwise.
By Lemma 9, the size of A ∃π is exponential (resp. polynomial) in the size of π(X 1 , . . . , X m ) (resp. if this path expression is intersection free). The final automaton A runs over S ϕ -trees t where S ϕ = (Σ ∪ Subf(ϕ), Γ ), i.e., the node labeling includes the (guessed) truth values for Subf(ϕ). To check that these guesses are correct, A runs an automaton A ξ for each ξ ∈ Subf(ϕ).

For each ξ 0 = M (ξ 1 , . . . , ξ m ) ∈ Subf(ϕ) with M ∈ M ∪ Σ ∪ {¬, ∨}, we define an automaton A ξ0 over S ϕ -trees by taking a copy of A M which reads a label σ ⊆ Σ ∪ Subf(ϕ) of t as if it was σ ∩ (Σ ∪ {ξ 0 , . . . , ξ m }) with ξ i further replaced by X i . Similarly, for each ξ 0 = ∃π(ξ 1 , . . . , ξ m ) ∈ Subf(ϕ), we define an automaton A ξ0 over S ϕ -trees by taking a copy of A ∃π which reads a label σ ⊆ Σ ∪ Subf(ϕ) of t as above.

Finally, A is the disjoint union of all A ξ for ξ ∈ Subf(ϕ) together with a new initial state ι which starts all the automata A ξ with the initial transitions δ(ι, σ, D ′ ) = ξ∈Subf(ϕ) (stay, ι ξ ) for all D ′ ⊆ D. We can check that an S ϕ -tree t = (V, λ, ν) is accepted by A iff its projection t ′ = (V, λ ′ , ν) on Σ is an S-tree and for each node u ∈ V we have λ(u)\Σ = {ξ ∈ Subf(ϕ) | t ′ , u |= ξ}. Therefore, satisfiability of ϕ over S-trees is reduced to emptiness of the conjunction of A with a two state automaton checking that ϕ ∈ λ(u) for some node u of the tree.

The size of A is at most exponential (resp. polynomial) in the size of ϕ. Indeed, each A ξ with top(ξ) = ∃ is of constant size since the MSO modalities are fixed and not part of the input. If ξ = ∃π(ξ 1 , . . . , ξ m ) then the size of A ξ is exponential in |π(X 1 , . . . , X m )| (note that ξ i is replaced by X i so that its size does not influence the size of A ξ ). Moreover, if π is intersection free then the size of A ξ is polynomial in |π(X 1 , . . . , X m )|. We deduce from Theorem 8 the 2EXPTIME upper bound for Tree-Sat(L) and the EXPTIME upper bound for Tree-Sat(L -), the intersection free case.

⊓ ⊔ Remark 11. Satisfiability for the path-expression free logic CTL considered in Example 2 is known to be EXPTIME-complete [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF]. The above procedure gives an EXPTIME procedure for the satisfiability checking meeting the lower bound.

From Ordered Unranked Trees to Binary Trees We recall that an ordered unranked tree can be encoded as a binary tree by removing the edges (u, v) ∈ E child whenever v is not a first-child. Note that E child can be retrieved from the binary encoding by the path expression child • next * . Hence any path expression over ordered unranked trees can be converted to a path expression over binary trees (with only a linear blowup in the size), and any MSO(S)formula over ordered unranked trees can be translated to an MSO(S)-formula over binary trees. Thus, Theorem 10 holds for ordered unranked trees as well: The 2EXPTIME lower bound follows from [START_REF] Lange | 2-ExpTime lower bounds for Propositional Dynamic Logics with Intersection[END_REF]. The EXPTIME lower bound is inherited from regular XPath [START_REF] Calvanese | An Automata-Theoretic Approach to Regular XPath[END_REF] (cf. Example 3).

From Nested Traces to Trees Now, we turn to nested traces and we will reduce the satisfiability problems for formulas over nested traces to the satisfiability problems over trees. More precisely, we will transform a given temporal logic over nested traces into some temporal logic over tree encodings of nested traces that "simulates" the original logic. This will allow us to solve the following problem, which is parametrized by Proc, Act, k ≥ 1, and a temporal logic L over the induced signature: The proof of Theorem 15 will be developed in the following. In order to exploit Theorem 10, we interpret a k-phase nested trace G = (V, λ, ν) in a (binary) S ′tree (where S ′ := (Σ ⊎ {1, . . . , k}, {left, right})) using the encoding from [START_REF] La Torre | A robust class of context-sensitive languages[END_REF], extended to infinite trees. Actually, [START_REF] La Torre | A robust class of context-sensitive languages[END_REF] does not consider nested traces but k-phase words. Therefore, we will use linearizations of nested traces. Let w = (V, λ, ≤) ∈ Lin k (G). By ⋖, we denote the direct successor relation of ≤. Suppose that V = {u 0 , u 1 , u 2 , . . .} and that u 0 ⋖ u 1 ⋖ u 2 ⋖ . . . is the corresponding total order. For 0 ≤ i < |V |, we let phase w (u i ) = min{j ∈ {1, . . . , k} | λ(u 0 ) . . . λ(u i ) is a j-phase word}. Intuitively, this provides a "tight" factorization of w. We associate with w the S ′ -tree t w k = (V, λ ′ , ν ′ ) where the node labeling is given by λ ′ (u i ) = λ(u i ) ∪ {phase w (u i )} and the sets of edges are defined by

E ′ right = E cr and E ′ left = ⋖ \ {(u, v) ∈ ⋖ | there is u ′ such that (u ′ , v) ∈ E cr }.
That is, the tree encoding is obtained from the linearization by adding the cr-edges as right children and removing the superfluous linear edges to return nodes having a matching call. Figure 4 depicts the tree t w 2 for the linearization w that was illustrated in Fig. 2. The edges removed from the linearization are shown in dotted lines. The newly added edges are labelled right. All -nodes are phase 1 and the -nodes are phase 2.

By Trees k (Proc, Act), we denote the set {t w k | w ∈ Lin k (G) for some G ∈ Traces k (Proc, Act)} of valid tree encodings. The following was proved in [START_REF] La Torre | A robust class of context-sensitive languages[END_REF] for finite structures, and extends easily to infinite structures.

Lemma 16 ([16]

). There is a formula TreeEnc k ∈ MSO(S ′ ) defining the set Trees k (Proc, Act). Also, there is less k (x, y) ∈ MSO(S ′ ) such that for all k-phase words w = (V, λ, ≤) and all u, v ∈ V , we have u < v in w iff t w k |= less k (u, v). Lemma 16 will be used to reduce nested-trace modalities to tree modalities in the proof of Theorem 15. We also need to deal with path expressions, which motivates the following lemma: Lemma 17. There exists a path expression succ ≤k over S ′ such that, for all kphase linearizations w = (V, λ, ≤), we have

[[succ ≤k ]] t w k = {(u, v) ∈ V 2 | u ⋖ v}.
In other words, succ ≤k encodes the successor relation ⋖ of ≤ in the tree encoding t w k of w. Moreover, the length of succ ≤k is exponential in k.

Fig. 5. A 3-phase linearization and the corresponding tree encoding. Nodes in phase 1 are denoted , those in phase 2 are denoted and the nodes in phase 3 are denoted ♦. There are two stacks. The call return edges corresponding to stack 1 are shown above the line and those corresponding to stack 2 are shown below the line. Note that these edges are uniquely determined by the linearization. The dotted edges in the tree are the missing edges from the linearization. The sequence of nodes from the linearization is recovered by traversing the left-edges whenever possible, and the dotted edges otherwise. The label on the dotted edge says which case it corresponds to, in the path expressions succm-1,m and succm,m.

Proof. We give the path expression inductively by case analysis. The different cases are illustrated in Figure 5. In the next paragraph we make a few observations which will ease the understanding of the path expressions.

-The phase numbers are monotonically non-decreasing in the linearization.

Recall that the tree encoding is obtained from the linearization by adding the cr-edges as right children and removing the superfluous linear edges to return nodes having a matching call. Hence the phase numbers are monotonically non-decreasing in any path from the root to any node. -The left-successor of the tree always corresponds to a successor in the linearization.

-If a node has a right-child, then it is a call node, and the right-child is its corresponding return. -If u < v in the linearization, then there is a path from node u to node v in the tree which does not visit any node that comes after node v in the linearization. This can be proved by induction on v (with the total order ≤).

-If u ⋖ v in the linearization and node v is not the left-successor of node u, then node v is a return node which is attached to its call node. -The first node of any phase greater than 1 is always a return. Moreover it will be attached as a right-child if it is a matched return and as a left-child otherwise.

We inductively define a path expression succ ≤m for the successor relation of the linearization restricted to the nodes with phase at most m. That is,

[[succ ≤m ]] t w k = {(u, v) ∈ V 2 | u ⋖ v, phase w (u) ≤ m, phase w (v) ≤ m}. It will be of the form succ ≤m = succ ≤m-1 ∪ succ m-1,m (a) ∪ succ m,m (b)
where cases (a) and (b) are specified below and illustrated in Figures 4 and5. The base case will be succ ≤1 = succ 1,1 .

(a) We will consider the case when u is the last node in phase m -1 and v is the first node in phase m. If v is a pending return (that is, it does not have a matching call), we have the path expression ?(m -1) • left • ?m. If v is a matched return, then v is the return of the most recent call with a return in phase m. For example situations, we refer to the edges labelled (1) in Figures 4 and5. This can be reached by the path expression prev-call-ret m which goes back to the most recent call which has a return in phase m, and then moves to that return.

prev-call-ret m = (?¬∃(right

• ?m) • succ ≤m-1 -1 ) * • right • ?m
Note that these two cases are mutually exclusive. That is, if a phase starts with a pending return, it is not possible to have a matched return in the same phase with the corresponding call belonging to a smaller phase. Hence we get the path expression from u to v in this case as:

succ m-1,m = ?(m -1) • left • ?m ∪ ?(m -1 ∧ ¬∃succ ≤m-1 ) • prev-call-ret m (1)
(b) If two successive nodes u and v in the linearization are in the same phase m and are connected in the tree by a path where each node is in phase m, then either (i) we can reach v from u by taking a left edge, or (ii) v is a return appended to the latest pending call which is also in the phase m and has a return in phase m. In that case, we can reach v by moving up the tree along nodes in phase m until we find the first "pending call" and then taking the right edge to node v. For example situations of case (ii), please refer to the edges labelled (2) in Figures 4 and5. Note that, while moving up the tree, if we move from a right child to its parent, we are at a call node which cannot be a right child. Hence it is not possible to take right -1 twice in succession. Assume finally that the successive nodes u and v are in the same phase m, but there is no path from u to v visiting only nodes of phase m. This case arises when v is a return whose corresponding call is in a different phase. Now we can move up the tree from u until we see the first node, call it w, belonging to a smaller phase. Clearly w is a call node with its return w ′ in phase m. Since w ′ and v are return nodes in the same phase, the corresponding call of v will be before w, and in fact it will be the most recent call before w with its return in phase m. Moving from the parent of w to v is abstracted by the path expression prev-call-ret m . Examples are edges labelled (3) in Figures 4 and5.

The path expression succ m,m is given by:

succ m,m = (?m • left • ?m) ∪ ?(m ∧ ¬∃left) • [(right -1 ∪ ?(¬∃(right • ?m)) • left -1 • ?m] * • [right • ?m ∪ (2) right -1 • ?(¬m) • left -1 • prev-call-ret m ] (3)
Note that right -1 • left -1 allows us to skip call nodes which were previously matched.

All nodes in phase 1 will be connected in the tree, hence we get the basis for the induction, succ ≤1 := succ 1,1 which simplifies to:

left • ?1 ∪ ?(1 ∧ ¬∃left) • [(right -1 ∪ ?¬∃(right • ?1)) • left -1 ] * • right • ?1
Note that the length of the path expression succ ≤m is exponential in m.

⊓ ⊔

We are now ready to prove Theorem 15. where less k is the formula from Lemma 16. Note that these transformations of the semantics of the modalities only depends on L and on k (which are not part of the input) and not on the formula for which we want to check satisfiability.

Proof (of

The translation T from formulas over L to "equivalent" formulas over L ′ is defined inductively for node formulas by

T (σ) = σ T (M (ϕ 1 , . . . , ϕ ℓ )) = M (T (ϕ 1 ), . . . , T (ϕ ℓ )) T (¬ϕ) = ¬T (ϕ) T (∃π) = ∃T (π) T (ϕ 1 ∨ ϕ 2 ) = T (ϕ 1 ) ∨ T (ϕ 2 )
and for path formulas by

T (?ϕ) = ?T (ϕ) T (π 1 ∪ π 2 ) = T (π 1 ) ∪ T (π 2 ) T (cr) = right T (π 1 ∩ π 2 ) = T (π 1 ) ∩ T (π 2 ) T (cr -1 ) = right -1 T (π 1 • π 2 ) = T (π 1 ) • T (π 2 ) T (succ p ) = ?p • succ ≤k • (?¬p • succ ≤k ) * • ?p T (π * ) = T (π) * T (succ -1 p ) = ?p • succ -1 ≤k • (?¬p • succ -1 ≤k ) * • ?p
where succ ≤k is defined in Lemma 17. Note that the transformation T (π) of a path formula π is linear in |π| since k is not part of the input. Now we check inductively that the translation T is correct. Let G = (V, λ, ν) ∈ Traces k (Proc, Act), let w = (V, λ, ≤) be a k-phase linearization of G and let t w k = (V, λ ′ , ν ′ ) be the tree encoding of w. We have to show that [

[ϕ]] G = [[T (ϕ)]] t w k for each node formula ϕ and [[π]] G = [[T (π)]] t w k for each path formula π. By definition of t w k we have immediately [[cr]] G = E cr = E right = [[right]] t w k .
The case succ p is more interesting. We have (u, v) ∈ [[succ p ]] G iff u is on process p and v is the first node (wrt. the ordering < of w) which is on process p. By Lemma 17, this is described by the formula T (succ p ) interpreted on the tree encoding t w k . The cases cr -1 and succ -1 p are similar and the remaining cases for path formulas are obtained directly by induction.

We turn now to node formulas. Again by definition of t w k we have immediately

[[σ]] G = {u ∈ V | σ ∈ λ(u)} = {u ∈ V | σ ∈ λ ′ (u)} = [[σ]] t w k for each σ ∈ Σ. The cases ¬ϕ, ϕ 1 ∨ ϕ 2 ,
and ∃π follow directly by induction. It remains to deal with a modality M of arity ℓ. We prove by induction on the MSO formula [[M ]] that for all U 1 , . . . , U ℓ ⊆ V and all nodes u ∈ V , we have G

|= [[M ]](u, U 1 , . . . , U ℓ ) iff t w k |= [[M ]] ′ (u, U 1
, . . . , U ℓ ). Among the atomic subformulas, the only non trivial case is for succ p (x, y) and it follows from Lemma 16 and the definition of succ p (x, y) given above. The non atomic cases follow directly by induction.

Finally, a formula ϕ ∈ Form(L) is satisfiable over k-phase nested traces iff the formula Enc ∧ T (ϕ) ∈ Form(L ′ ) is satisfiable over S ′ -trees. Using Theorem 10 we get the upper bounds stated in Theorem 15. The lower bound for the intersection free fragment is proved in the following proposition.

⊓ ⊔ Proposition 18. Let Proc and Act be non-empty finite sets inducing S, let k ≥ 1, and let L -be an intersection free temporal logic over S. The problem Nested-Trace-Sat(L -, k) is EXPTIME-hard.

Proof. We show a reduction from the EXPTIME complete logic NWTL [START_REF] Alur | Firstorder and temporal logics for nested words[END_REF] to the temporal logic L - 0 with no modalities and only one process p. The modalities are X, Y, X cr , Y cr , U s and S s which are the same as EX, EY, X cr , Y cr , EU s and ES s of the temporal logic NTrLTL defined in Example 5 when |Proc| = 1. Below we give its semantics through path expressions. This also evinces the translation of an NWTL formula ϕ into an equivalent L - 0 -formula ϕ (by induction).

X ϕ = ∃(succ p • ϕ) Y ϕ = ∃(succ -1 p • ϕ) X cr ϕ = ∃(cr • ϕ) ϕ U s ψ = ∃((?ϕ • (succ p ∪ cr)) * • ?ψ) Y cr ϕ = ∃(cr -1 • ϕ) ϕ S s ψ = ∃((?ϕ • (succ -1 p ∪ cr -1 )) * • ?ψ) ⊓ ⊔ Remark 19.
If k is given as part of the input, the above method for modalities does not work: the new semantics [[M ]] ′ over trees depend on k and are no more fixed and independent of the input. However, if we consider the fragment L 0 with no MSO modalities, we get a 3EXPTIME procedure even if k is part of the input since the length of the path expression T (π) is linear in |π| and exponential in k.

Moreover, for the intersection free fragment L - 0 , we get a 2EXPTIME procedure.

Model Checking

Our approach extends to model checking. We can define a model of concurrent recursive programs, called concurrent recursive Kripke structures (CRK), that generates nested traces. It is similar to the concurrent visibly pushdown automata from [START_REF] Bollig | Realizability of concurrent recursive programs[END_REF]. Let S = P ⊆Proc S P . For s ∈ S and p ∈ Proc, we let s p be the p-th component of s (if it exists). A run of a CRK K is an S ′ -graph G = (V, λ, ν) where S ′ = (Σ ⊎ p∈Proc S p , Γ ) with Σ = Proc ∪ Act ∪ Type and Γ = {cr} ∪ {succ p | p ∈ Proc}, and the following conditions hold:

-The graph G without the labeling from p∈Proc S p is a nested trace. That is nt(G) := (V, λ ′ , ν) where λ ′ (u) = λ(u) ∩ Σ is a nested trace over Proc and Act.

-Every node u is labeled with one, and only one, state from S p for each process p ∈ Proc(u). This state is denoted ρ(u) p . The label of a node u does not contain any state from S p if p / ∈ Proc(u). That is, for p ∈ Proc and all u ∈ V ,

λ(u) ∩ S p = {ρ(u) p } if p ∈ λ(u) ∅ otherwise.
This defines a mapping ρ : V → S by ρ(u) = (ρ(u) p ) p∈Proc(u) . -Let us determine another mapping ρ -: V → S as follows: for u ∈ V , we let ρ -(u) = (ρ -(u) p ) p∈Proc(u) where ρ -(u) p = ρ(u ′ ) p if (u ′ , u) ∈ E succ p , and ρ -(u) p = ι p if there is no u ′ such that (u ′ , u) ∈ E succ p . The following hold, for every u, u ′ ∈ V and a ∈ Act:

• (ρ -(u), a, ρ(u)) ∈ ∆ call if u ∈ V call ∩ V a • (ρ -(u), a, ρ(u)) ∈ ∆ 1 ret if u ∈ V ret ∩ V a
and there is no v with (v, u) ∈ E cr • (ρ(u ′ ), ρ -(u), a, ρ(u)) ∈ ∆ 2 ret if u ∈ V ret ∩ V a and (u ′ , u) ∈ E cr • (ρ -(u), a, ρ(u))

∈ ∆ int if u ∈ V int ∩ V a
We are only interested in maximal runs. We say that a run G of a CRK K is maximal if G is not a strict prefix of another run of K. The language L(K) of K is the set {nt(G) | G is a maximal run of K}. By L k (K), we denote its restriction L(K) ∩ Traces k (Proc, Act) to k-phase nested traces.

Let Proc and Act be non-empty finite sets inducing signature S, let k ≥ 1, and let L be a temporal logic over S. We are interested in the following decision problem. Note that the sizes of Max and Trans are linear in the size of the CRK K. Moreover, a nested trace decorated with states satisfies MaxRun iff it defines a maximal run of the CRK K. Thus, K |= k ϕ iff the formula MaxRun ∧ ¬ EN ϕ is not satisfiable by a (state-labeled) k-phase nested trace. This concludes the reduction. ⊓ ⊔

Fig. 1 .Fig. 2 .

 12 Fig. 1. A nested trace over Proc = {p, q} and Act = {c, r, sv }

4

  Satisfiability: From Trees to Nested Traces Consider any signature S = (Σ, Γ ) and temporal logic L over S. The following decision problem is well known. Problem 6. Tree-Sat(L): Instance: ϕ ∈ Form(L)

Problem 12 .Theorem 13 .

 1213 O-U-Tree-Sat(L): Instance: ϕ ∈ Form(L) Question: Are there t ∈ o.u.Trees(S) and node u of t such that t, u |= ϕ ? The problem O-U-Tree-Sat(L) is 2EXPTIME-complete. For the intersection free fragment L -, O-U-Tree-Sat(L -) is EXPTIME-complete.

Problem 14 .Fig. 4 .

 144 Fig. 4. The tree encoding of a 2-phase linearization

  Theorem 15). Let S = (Σ, Γ ) be the signature induced by Proc and Act, and let L = (M, arity, [[-]]) be the considered temporal logic over nested traces. For S ′ = (Σ ⊎ {1, . . . , k}, {left, right}), we define a new temporal logic L ′ = (M ′ , arity ′ , [[-]] ′ ) over S ′ -trees and give an inductive, linear-time computable translation T of formulas over L to "equivalent" formulas over L ′ . By "equivalent", we mean that for all G ∈ Traces k (Proc, Act) and all k-phase linearizations w of G, we have[[ϕ]] G = [[T (ϕ)]] t w k for each node formula ϕ over L and [[π]] G = [[T (π)]] t wk for each path formula π over L.We set M ′ = M ∪ {Enc} where Enc is a new modality with arity ′ (Enc) = 0 that characterizes valid tree encodings: the semantics [[Enc]] ′ is given by the formula TreeEnc k from Lemma 16. We also change the semantics of the modalities from M: for each M ∈ M, the new semantics [[M ]] ′ ∈ MSO(S ′ ) is obtained from [[M ]] ∈ MSO(S) by replacing each occurrence of cr(x, y) by right(x, y) and each occurrence of succ p (x, y) by succ p (x, y) := p(x) ∧ less k (x, y) ∧ p(y) ∧ ¬∃z (less k (x, z) ∧ p(z) ∧ less k (z, y))

Definition 20 .

 20 A concurrent recursive Kripke structure (CRK) over finite sets Proc and Act is a tuple K = ((S p ) p∈Proc , ∆, ι). The S p are disjont finite sets of local states (S p containing the local states of process p). Given a set P ⊆ Proc, we let S P := p∈P S p . The tuple ι ∈ S Proc is a global initial state. Finally, ∆ provides the transitions, which are divided into four sets:∆ = (∆ call , ∆ 1 ret , ∆ 2 ret , ∆ int ) where -∆ call ⊆ p∈Proc (S p × Act × S p ), -∆ 1 ret ⊆ p∈Proc (S p × Act × S p ),-∆ 2 ret ⊆ p∈Proc (S p × S p × Act × S p ), and -∆ int ⊆ P ⊆Proc (S P × Act × S P ).

Problem 21 .Theorem 22 .

 2122 Model-Checking(L, k):Instance: CRK K and ϕ ∈ Form(L) Question: Do we have K |= k ϕ, i.e., for all G ∈ L k (K), is there a node u of G such that G, u |= ϕ ?We show the following result: The problem Model-Checking(L, k) is in 2EXPTIME. For the intersection free fragment L -, Model-Checking(L -, k) in EXPTIME.

, and DIGITEO LoCoReP.

Proof. We will reduce the model-checking problem to the satisfiability problem by encoding maximal runs of a CRK K with a formula MaxRun. For this, we enrich L to L ′ with the additional unary modality EN (there exists a node) whose semantics is defined by [[EN]](x, X) = ∃y (y ∈ X). Now we will describe the maximal runs of the CRK K by the formula MaxRun = Val ∧ Max ∧ ¬ EN ¬Trans. Here, Val says that the labeling by states is valid. That is, no node is labelled by two states of the same process, and a node is labeled p iff it is labeled by some state from S p .

Formula Max says that the maximal nodes of the nested run do not enable any transition. Formula Trans says that the labeling of the current node and its predecessors comply with the transition relations.

For s ∈ S we let ∆ int (s) = {(a, s ′ ) ∈ Act × S | (s, a, s ′ ) ∈ ∆ int } and we define similarly ∆ call (s), ∆ ret (s), and ∆ ret (s 1 , s 2 ). In the following, for all s ∈ S and p ∈ Proc, let "s p = ι p " be a shorthand for true (⊤) if s p = ι p and false (⊥) otherwise. Then, we define

Then, we define Trans = Trans call ∨ Trans 1 ret ∨ Trans 2 ret ∨ Trans int .


Heather Jebbari

Ian Simms
email: ian.simms@hpa.org.uk

Stefano Conti

Andrea Marongiu

Gwenda Hughes

Helen Ward

Cassandra Powers

Daniel Rh Thomas

Barry Evans

Variations in the epidemiology of primary, secondary and early latent syphilis, England and Wales: 1999 to 2008

Keywords: Infectious syphilis, epidemiology, stage of infection, England & Wales

Key messages

• Over the last ten years the infectious syphilis epidemic has remained 'young', with a high proportion of primary and secondary cases.

• The increase in primary syphilis as a proportion of early syphilis indicates that infection is detected and managed at an earlier stage of infection.

• Sustained, intensive, targeted efforts to interrupt further transmission need to be maintained and intensified.

• Locally-based interventions that penetrate sexual networks identified through partner notification and surveillance initiatives will likely be the most effective method of controlling infection.

Introduction

In England and Wales the resurgence of infectious syphilis started in 1997 with an outbreak amongst heterosexual men and women in Bristol. Since then diagnoses made at genitourinary medicine (GUM) clinics have risen from 285 in 1997 to 3265 cases in 2008. [START_REF]STI Table 1 Country 2008[END_REF][START_REF] Simms | The re-emergence of Syphilis in the United Kingdom: the new epidemic phases[END_REF] This dramatic change in incidence has been focused on major urban areas, particularly London and Manchester, but outbreaks have been seen throughout England and Wales, and there are striking similarities within outbreaks seen in Europe, North America and Australia. [START_REF] Simms | The re-emergence of Syphilis in the United Kingdom: the new epidemic phases[END_REF] The epidemic has been influenced by developments in the HIV epidemic and behavioural change in men who have sex with men (MSM) and has been characterised by a rapid increase in diagnoses made in MSM, and a high proportion of HIV coinfections. An outbreak amongst heterosexuals, including young people, has developed alongside the larger MSM epidemic.

The natural history of syphilis suggests that an early epidemic dominated by primary and secondary infection would be expected to develop into an epidemic predominantly composed of early latent infections. 3,[START_REF] Simms | International Encyclopedia of Public Health[END_REF] Each phase presents a different public health challenge. Here we investigate the factors that are associated with variations in the stage of diagnosed infections over the past ten years and consider the implications of these findings in terms of public health intervention.

Methods

Data sources

Two data sources were used: diagnoses made in GUM clinics reported on form KC60, and information collected through National Enhanced Syphilis Surveillance (NESS) which was also undertaken only within GUM clinics. Both methodologies have been previously described and discussed in detail. [START_REF]The UK Collaborative Group for HIV and STI surveillance. Testing times. HIV and Sexually Transmitted Infections in the United Kngdom: 2007[END_REF] In brief the KC60 was an aggregate mandatory return, the number of cases is recorded by gender and male sexual orientation for primary, secondary and early latent syphilis a . Age group was also recorded but only for primary and secondary infection. NESS is a voluntary reporting system based on the collection of disaggregate (patient level) data including: gender, age, ethnic background, sexual orientation, stage of infection, HIV status, geographic area where the infection was likely to have been acquired and connections with social and sexual networks.

Definitions

Definitions of early latent syphilis vary between countries. The definitions used for primary, secondary and early latent infection within the UK are given in the guidelines published by the British Association for Sexual Health and HIV (BASHH www.bashh.org). The BASHH guidelines define early latent syphilis as "Treponema pallidum infection diagnosed on serological testing with no symptoms or signs within the first two years of infection: this is early latent syphilis and beyond that late latent syphilis". In the KC60 return, primary and secondary infections were recorded under a single combined category (A1, A2) and early latent (A3) was recorded separately. In contrast, under the NESS collection system primary (A1), secondary (A2) and early latent (A3) are recorded separately.

Data completeness & representativeness

The NESS dataset is a subset of the KC60 dataset. KC60 data are shown as a reference point for the NESS data, although only the patient level NESS dataset was used in the subsequent detailed analysis. Completeness of reporting varies over time and by Strategic Health Authority (SHA): reporting from the North West and North East SHAs was close to 100%. NESS began in 1999 in the North West, while Wales and most other English regions followed from 2003, the East of England and East Midlands regions submitting data for the first time in 2007. Coding accuracy varies between the two datasets. [START_REF] Menon-Johansson | Surveillance of an infectious syphilis outbreak in south London, UK: a comparison of reporting systems[END_REF] For example the patient management software used in some clinics automatically defaults male sexuality to 'heterosexual', leading to the incorrect assignment of some patients to this category. Regional variation in diagnoses reported through NESS was the area of most concern in terms of selection bias. To investigate this in more detail SHA of diagnosing GUM clinic was included in the statistical model.

Statistical analysis

Statistical analysis was only undertaken on NESS data. The relationship between stage of infection and selected explanatory variables was investigated by using multinomial (also known as multi-categorical logistic) regression modelling (details given in Annex). [START_REF] Fahrmeir | Multivariate Statistical Modelling Based on Generalized Linear Models[END_REF] The probability of presenting with syphilis at each stage of infection was estimated by year and for different patient characteristics from the model using maximum likelihood.

Predicted probabilities were plotted to investigate infection dynamics over time. These figures are shown in the main text and Annex.

Results

Between 1999 and 2008, annual cases of infectious syphilis reported through the KC60 system rose from 415 to 3265, an increase in incidence from 0.79 per 100,000 (denominator = total population) 5.99/100,000. A cumulative total of 22 156 diagnoses were made over the period. For the same period, NESS reports were received for 12 021 cases, 54% of the KC60 total. The NESS and KC60 datasets were compared in terms of the outcome variable, stage of infection, and an overview of the proportions recorded in each dataset indicate that there was a good general level of qualitative agreement (Figure 1). This suggests that overall NESS gave a consistent representation of the distribution of diagnoses over time. The analysis was undertaken on those patients for whom complete information were available. After exclusion of cases with missing values 11 838 were used for the statistical analysis (Table 1). The majority (73%, 8656/11 838) of cases were seen in MSM compared to 16% (1938/11 838) in heterosexual men and 10% in heterosexual women (1244/11 838). Most cases were seen in patients of White ethnic background (9491/11 594 or 82%), whereas Black and Asian groups accounted for 10% (1126/11 594) and 6% (656/11 594) respectively. Primary syphilis was reported in 43% (4698/10 997) of cases, secondary in 33% (3677/10 997) and early latent in 24% (2622/10 997). Of the 233 patients identified through antenatal screening 97% were women and 141 (61%) were diagnosed with early latent syphilis. MSM reported a median of 2 (interquartile range 1 to 5) sexual partners in the 3 months prior to diagnosis, whereas the median number reported by heterosexual men and women was 1 (IQR 1 to 2). Just over a third of syphilis patients (3087/7870 or 39%) thought that they had been infected through oral sex, 92% of whom (2847/3087) were MSM.

Results of the multinomial regression model are summarised in Tables 2 and3. Each estimated regression coefficient provides a measure of increased (if positive) or decreased (if negative) likelihood of presenting with either primary or secondary syphilis, relative to early latent. For example, an HIV positive individual would be expected to have a 1.62=exp{0.48} higher odds ratio of presenting primary syphilis infection (as opposed to early latent) compared to an HIV negative patient.

Patients who attended because they had symptoms of infection were significantly more likely to present with primary infection relative to early latent infection (p<0.001) (Table 2).

Patients brought in through partner notification (p=0.051), who were HIV positive (p=0.052) and who were UK-born (p=0.064) were also more likely to present with primary infection, although this was of borderline significance. In contrast, patients who were Asian (p=0.039), or those who had contacted sexual partners through saunas (p=0.001), bars (p<0.01) and the internet (p=0.01), had untraceable partners (p=0.029) and had acquired infection in Manchester (p=0.043) were significantly less likely to present with primary infection relative to early latent infection.

The pattern was similar when secondary and early latent infection were compared (Table 3). Patients who attended because they had symptoms of infection (p<0.001), had been identified through partner notification (p=0.022), were HIV positive (p<0.001) and were UKborn (p=0.045) were significantly more likely to present with secondary infection relative to early latent infection (Table 3). Patients who had contacted sexual partners through saunas (p=0.005), bars (p=0.002) and the internet (p=0.005) were significantly less likely to present with secondary infection relative to early latent infection.

There was no significant association between stage of infection at presentation and the health region reporting the data, suggesting that inconsistent regional reporting is unlikely to have influenced the main findings (Tables 2 and3).

In general, the proportion of diagnosed cases of primary infection increased over time, whereas the proportion of secondary cases fell (Figure 2 and Annex Figures 1 to 5). For all the variables studied, the proportion of primary cases had exceeded that of secondary cases by 2004. The proportion of early latent cases remained relatively stable over time and was lower than that of primary and secondary infection. MSM were more likely to present with primary infection whereas heterosexual men were more likely to present with secondary infection (Figure 2). Women were most likely to present with primary infection but a relatively high and increasing proportion presented with early latent infection (Figure 2). The relative proportion of the stages of infection varied substantially depending on the reasons for attending clinical care, a higher proportion of early latent cases being seen in those attending for routine clinical care (Annex Figure 4). The proportion of primary cases seen in patients who acquired their infection in Brighton exceeded that of secondary cases at least three years before this was observed for those infected in London, Manchester and other parts of the UK (Annex Figure 5).

Discussion

Over the last ten years the epidemic of infectious syphilis has remained 'young', with a high proportion of primary and secondary cases. The decline in diagnoses of secondary infection and the increase in diagnoses of primary infection indicate that infection is being detected and managed at an earlier stage of infection through increased disease awareness, better case ascertainment and increased access to GUM services. However, in the early 2000s waiting times to access GUM services increased substantially, caused by large increases in attendance at already overstretched clinical services and this is likely to have contributed to an increase in the duration of infectiousness. [START_REF] Simms | The re-emergence of Syphilis in the United Kingdom: the new epidemic phases[END_REF] The problem was recognized by the Department of Health (England) and the proportion of people contacting GUM services seen within 48 hours now approaches 100%.

The consistent level of early latent cases, although low, indicates that primary and secondary infections are going undiagnosed but it is not possible to predict the number of undetected cases present in the population. Undiagnosed cases have a number of public health implications. Some infections will be resolved through indirect antimicrobial treatment but of those that progress to tertiary syphilis, around a third are likely to develop clinical manifestations of late syphilis which may be seen in clinical settings such as neurology and cardiology over future decades. The high proportion of syphilis diagnoses in MSM that are co-infected with HIV reflects the close relationship between the epidemics. Syphilis infection is known to facilitate HIV transmission, and consequently may be contributing to increased HIV incidence. This highlights recommendations that MSM should have an annual sexual health screen, including testing for HIV where not already diagnosed, supported by improved laboratory turnaround times for the diagnosis of syphilis. 8,9 MSM also need to be aware that syphilis can be transmitted through oral sex.

There is also an increased risk of congenital syphilis in reproductive age women.

Congenital syphilis can be prevented through first trimester screening supported by treatment and partner notification. This control method is cost-effective but highly dependent on well structured healthcare pathways. In 2007 95% of pregnant women were screened for syphilis in England, although uptake varied from 82% to 98% between regions. 10 This level of screening is slightly higher than that for HIV screening (93% nationally, range: 85% to 97%) despite there being no national target for syphilis screening in pregnancy. Over the period studied, this important public health intervention identified 22% of infections seen amongst women. The cases of congenital syphilis that have emerged reflect failures of both the antenatal screening and adult syphilis intervention strategies. 11,12 The dominant profile of the epidemic is one of White, MSM aged 25 to 34, many of whom are co-infected with HIV and over a third believed that they had acquired infection through oral sex. This risk profile has been observed consistently since the re-emergence of infectious syphilis over a decade ago. [START_REF]STI Table 1 Country 2008[END_REF] The associations between primary and secondary infection and social networks within saunas, bars and the internet reflects risk taking amongst MSM accessing both traditional 'sexual marketplaces' and internet chat rooms. The easy acquisition of sexual partners via the internet has joined previously isolated networks, and reduced the time taken for epidemics to evolve.

Infections amongst heterosexuals have also increased with the East Midlands region seeing a high proportion (54%) of heterosexual cases. The profile of these cases is more diverse than those seen in MSM. In the early stages of the epidemic, heterosexual outbreaks were generally isolated and linked, for example, to travel abroad. [START_REF]STI Table 1 Country 2008[END_REF] More recently heterosexual infections have been acquired through local sexual networks within the UK, sex work, and in some cases amongst students and young people aged less than 20. 13,14 In England and Wales, GUM clinics offer free, open access services that are widely advertised but some of those at risk of infection find accessing services difficult. For example, outbreak investigations showed that some young people diagnosed with syphilis were marginalised in society in terms of socio-economic circumstance. 15 They were not registered with health services and did not attend services when they experienced issues with their health. Increased risk of infection amongst patients of Asian ethnicity may reflect infection acquired abroad, but it may also be caused by barriers to accessing sexual health services that deter patients from seeking clinical advice. 16 These observations highlight the importance that all young people should be able to access comprehensive sexual health services for testing, treatment and management.

The main potential limitation of the study is the use of voluntary NESS dataset. The NESS dataset includes around 60% of the diagnoses recorded in the KC60 dataset and consequently it may not be representative of the overall pattern of diagnoses. High regional variation is a feature of the epidemic, but analysis of the NESS dataset showed that the presence of region as a factor in the analysis did not have a significant effect on the model, indicating that the enhanced data-set was not geographically biased.

Over the past decade diagnoses of infectious syphilis have increased in Western Europe and the US but few countries collect detailed information by stage of infection. In the US in 2008 primary and secondary infection accounted for 52% of diagnoses of early syphilis whereas early latent accounted for 48%. 17 In contrast, 24% of diagnoses of early syphilis made in England and Wales were early latent. However, comparisons are difficult to make given variations in the quality of surveillance data, sexual behaviour, access to clinical services and treatment, and the different case definitions used for early latent syphilis. For example, the definition used in the US includes latent cases seen within the previous 12 months, a shorter period than the 24 months used in the UK definition. and surveillance initiatives will likely be the most effective method of controlling infection. no baseline is shown for partner notification because it is a discrete variable. Interpretation: each estimated regression coefficient provides a measure of increased (if positive) or decreased (if negative) likelihood of presenting with secondary, relative to early latent infection. For example, an HIV positive individual would be expected to have a 1.62=exp{0.48} higher odds ratio of presenting primary syphilis infection (as opposed to early latent) compared to an HIV negative patient.

Word count = 2588

Figure 1

Comparison of proportion of primary, secondary and early latent infection reported to the KC60 and NESS: 1999 to 2008 Figure 2 Probability of infection with syphilis by stage of infection, gender and male sexual orientation (model estimates): 1999 to 2008

Annex

Methods

Multinomial regression modelling is a extension to standard logistic regression allowing for three or more levels (say J) to be used for the categorical response variable. [START_REF]STI Table 1 Country 2008[END_REF] A multinomial model was fitted with the R package VGAM to obtain maximum likelihood estimates. [START_REF] Simms | The re-emergence of Syphilis in the United Kingdom: the new epidemic phases[END_REF] In its most basic form, a multinomial model pairs each response category j=1,...,J-1 with an arbitrary baseline level (J). Accordingly the J-1 relative risks RR 1J , RR 2J ,..., RR (J-1)J , induced by the ensuing set of pairwise contrasts, are modelled to be log-linearly related to a set of selected predictors. Here primary, secondary and early latent syphilis are considered (J=3), and so the model simultaneously estimates underlying log-odds ratios through the use of iterative re-weighted least squares.

Early latent infection was used as the baseline and the log-odds ratios were simultaneously modelled for each non-baseline stage of infection (primary and secondary) relative to the baseline. Parameter estimates from each regression equation were interpreted as in standard logistic regression.

Various multinomial models were fitted to the NESS data-set, each including a different set of explanatory variables and network of interactions. A stepwise search strategy was carried out to identify within the set of available predictors (and interactions) those significantly influencing the likelihood of syphilis infection at its various stages. Candidate multinomial models were derived from the full model with no interaction terms through both forward selection and backward elimination, whereby a predictor/interaction at a time is respectively included or excluded from the pool of explanatory variables. A number of 'core' predictors identified by the authors were also consistently retained within the analysis. Sparsely populated categories were merged to ensure robust

Figures

Figure A1

Probability

  The re-establishment of syphilis as an endemic infection reflects a failure of control strategies. Partner notification, which is central to the detection of the infection, has been of limited use to control efforts due to the high proportion of anonymous partners seen in MSM. Other forms of control include a combination of interventions such as the promotion of early diagnosis and treatment through measures, such as facilitating access to sexual health services, antenatal screening, diagnosis and treatment and promoting behavioural changes such as increased condom use and reducing the number of sexual partners. As the syphilis epidemic continues to develop, sustained, intensive and targeted efforts to interrupt further transmission need to be maintained and intensified. Locally-based interventions that penetrate sexual networks identified through local partner notification

  Figure A1Probability of infection with syphilis by stage of infection, gender and HIV status (model estimates): 1999 to 2008 Figure A2 Probability of infection with syphilis by stage of infection and age group (model estimates): 1999 to 2008 Figure A3 Probability of infection with syphilis by ethnicity and UK birth status (model estimates): 1999 to 2008 Figure A4 Probability of infection with syphilis by stage of infection and reason for attendance at GUM services (model estimates): 1999 to 2008 Figure A5 Probability of infection with syphilis by stage of infection and likely geographic region of acquisition (model estimates): 1999 to 2008

Table & figuresTable 1 Absolute (relative) frequencies of syphilis diagnoses reported through NESS by gender and male sexual orientation: 1999 to 2008

 &1

		Yorkshire &
		The Humber	22 (1.14)	8 (0.64)	67 (0.77)	97 (0.83)
		Not available	387 (19.97)	187 (15.03)	1251 (14.45) 1825 (15.42)
	Year	1999	5 (0.26)	10 (0.80)	32 (0.37)	47 (0.39)
		2000	7 (0.36)	5 (0.40)	74 (0.85)	86 (0.73)
		2001	62 (3.20)	44 (3.54)	355 (4.10)	461 (3.89)
	Parameter*	2002	Male 147 (7.59)	Female 79 (6.35)	Men having sex 643 (7.43)	Total 869 (7.34)
		2003	heterosexual 242 (12.49)	heterosexual n (%) 144 (11.58)	with men 808 (9.33) 1194 (10.09) n (%)
		2004	n (%) 278 (14.34)	197 (15.84)	n (%) 1091 (12.60) 1566 (13.23)
	Total	2005	258 (13.31)	167 (13.42)	11 838 1170 (13.52) 1595 (13.47)
		2006	1938 (16.37) 372 (15.20)	1244 (10.51) 226 (18.17)	8656 (73.12) 1397 (16.14) 1995 (16.85) (100.00)
	Stage of infection Primary 2007	916 (47.27) 303 (15.63)	409 (32.88) 188 (15.11)	3373 (38.97) 4698 (39.68) 1568 (18.11) 2059 (17.40)
		Secondary 2008	414 (21.36) 231 (11.92)	246 (19.77) 153 (12.30)	3017 (34.85) 3677 (31.07) 1309 (15.12) 1693 (14.30)
		Early latent	419 (21.62)	417 (33.952)	1786 (20.63) 2622 (22.15) 273
		Not available Not available	189 (9.75 33 (1.70)	172 (13.83) 31 (2.49)	480 (5.55) 20 (2.41)	841 (7.10) (2.31)
	Whether born in the
	UK	UK born	707 (36.48)	469 (37.70)	1736 (20.06) 2912 (24.59)
		Non-UK born	1065 (54.95)	682 (54.82)	6143 (70.97) 7890 (66.65)
		Not available	166 (8.57)	93 (7.48)	777 (8.98) 1036 (8.75)
	Ethnicity	White	1056 (54.49)	720 (57.88)	7715 (89.13) 9491 (80.17)
		Black	499 (25.75)	341 (27.41)	286 (3.30) 1126 (9.52)
		Asian	268 (13.83)	111 (8.92)	277 (3.20)	656 (5.54)
		Other
		ethnicity	61 (3.15)	45 (3.62)	215 (2.48)	321 (2.72)
		Not available	54 (2.79)	27 (2.17)	163 (1.88)	244 (2.07)
	Reason for
	attending clinical	Routine
	services	screen	361 (18.63)	314 (25.24)	2275 (26.28) 2950 (24.92)
		Symptoms	1058 (54.59)	259 (20.82)	4283 (49.48) 5600 (47.31)
		Campaign	14 (0.72)	3 (0.24)	21 (0.24)	38 (0.33)
		Contact
		tracing	200 (10.32)	191 (15.35)	722 (8.34) 1113 (9.40)
		Antenatal
		screening	7 (0.36)	276 (22.19)	1 (0.01)	284 (2.40)
		Other	163 (8.41)	136 (10.93)	641 (7.41)	940 (7.94)
		Not available	135 (6.97)	65 (5.23)	713 (8.24)	(7.71)
	HIV status	HIV positive	110 (5.68)	54 (4.34)	3071 (35.48) 3235 (27.33)
		HIV negative	1350 (69.66)	923 (74.20)	4393 (50.75) 6666 (56.31)
		Not available	478 (24.66)	267 (21.46)	1192 (13.77) 1937(16.37)
	Infection acquired
	through oral sex	Yes	192 (9.91)	48 (3.86)	2847 (32.89) 3087 (26.08)
		No	1095 (56.50)	735 (59.08)	2953 (34.12) 4783 (40.41)
		Not available	651 (33.59)	461 (37.06)	2856 (32.99) 3968 (33.52)
	Location	London	551 (28.43)	297 (23.87)	2903 (33.54) 3751 (31.68)
		Brighton	20 (1.03)	14 (1.13)	437 (5.05)	471 (3.98)
		Manchester	66 (3.41)	37 (2.97)	1018 (11.76) 1121 (9.47)
		Elsewhere in
		UK	586 (30.24)	420 (33.76)	1828 (21.12) 2834 (23.94)
		Overseas	320 (16.51)	208 (16.72)	682 (7.88) 1210 (10.22)
		Not available	395 (20.38)	268 (21.54)	1788 (20.66) 2451 (20.70)
	Commercial sex
	worker	Yes	11 (0.57)	111 (8.92)	92 (1.06)	214 (1.81)
		No	1534 (79.15)	873 (70.18)	6947 (80.26) 9354 (79.01)
		Not available	393 (20.28)	260 (20.90)	1617 (18.68) 2270 (19.18)
	Social network	Sauna	26 (1.34)	8 (0.64)	1064 (12.29) 1098 (9.28)
		Bar	180 (9.29)	50 (4.02)	1265 (14.61) 1495 (12.63)
		Internet	9 (0.46)	5 (0.40)	535 (6.18)	549 (4.64)
		Not available	1723 (88.91	1181 (94.94)	5792 (66.91) 8696 (73.46)
	Age	≤15	2 (0.10)	10 (0.80)	2 (0.02)	14 (0.12)
		16 to 19	51 (2.63)	128 (10.29)	170 (1.96)	349 (2.95)
		20 to 24	220 (11.35)	283 (22.75)	920 (10.63) 1423 (12.02)
		25 to 34	611 (31.53)	466 (37.46)	2710 (31.31) 3787 (31.99)
		35 to 44	542 (27.97)	209 (16.80)	3022 (34.91) 3773 (31.88)
		45+	459 (23.68)	114 (9.16)	1562 (18.05) 2135 (18.03)
		Not available	53 (2.73)	34 (2.73)	270 (3.12)	357 (3.02)
	Strategic Health
	Authority	East Midlands	208 (10.73)	165 (13.26)	197 (2.28)	570 (4.81)
		East of
		England	21 (1.08)	14 (1.13)	43 (0.50)	78 (0.66)
		London	557 (28.74)	345 (27.73)	2888 (33.36) 3790 (32.02)
		North East	111 (5.73)	58 (4.66)	483 (5.58)	652 (5.51)
		North West	295 (15.22)	211 (16.96)	2315 (26.74) 2821 (23.83)
		South Central	65 (3.35)	34 (2.73)	198 (2.29)	297 (2.51)
		South East
		Coast	39 (2.01)	30 (2.41)	516 (5.96)	585 (4.94)
		South West	89 (4.59)	71 (5.71)	442 (5.11)	602 (5.08)
		West Midlands	144 (7.43)	121 (9.73)	256 (2.96)	521 (4.40)

Table 2

 2 Comparison of primary with early latent infection: estimates and confidence intervals for multinomial regression modelling* UK-born HIV negative male, aged 16 to 19, who attended GUM services in the East Midlands for a routine STI screen, likely to have acquired syphilis in London but unlikely to have acquired infection through oral sex, not a commercial sex worker and with no stated social/sexual networks. † no baseline is shown for partner notification because it is a discrete variable. Interpretation: each estimated regression coefficient provides a measure of increased (if positive) or decreased (if negative) likelihood of presenting with primary, relative to early latent infection. For example, an HIV positive individual would be expected to have a

	Parameter		Estimate	Standard Error (95% CI)	p-value
	Intercept		-12.36	142.88 (-292.66 to 267.93)	0.466
	Strategic Health Authority	East Midlands (baseline*)
			East of England	12.49	306.01 (-587.83 to 612.82)	0.484
			London	0.04	1.13 (-2.18 to 2.26)	0.486
			North West	0.65	1.04 (-1.38 to 2.68)	0.266
			South Central	10.99	215.44 (-411.65 to 466.64)	0.480
			South East Coast	-0.20	1.27 (-2.69 to 2.29)	0.437
			South West	0.62	1.12 (-1.58 to 2.81)	0.291
			West Midlands	0.26	1.18 (-2.05 to 2.56)	0.413
			Yorkshire & The Humber	10.68	290.09 (-558.41 to 579.76)	0.485
	Gender		Male (baseline*)
			Female	0.85	1.29 (-1.68 to 3.37)	0.255
	Whether born in the UK	UK-born (baseline*)
			Non UK-born	0.56	0.37 (-0.16 to 1.29)	0.064
	Ethnicity	White
			Black	-0.06	0.94 (-1.92 to 1.79)	0.473
			Asian	-1.20	0.68 (-2.53 to 0.14)	0.039
			Other ethnicity	0.02	0.92 (-1.79 to 1.82)	0.493
	Sexual orientation	Heterosexual (baseline*)
			Men who have sex with
			men	0.31	0.66 (-0.97 to 1.60)	0.317
	Reason for attending	Routine STI screen
	clinical services	(baseline*)
			Symptoms	2.34	0.31 (1.74 to 2.94)	<0.001
			Campaign	0.26	1.56 (-2.79 to 3.31)	0.433
			Partner notification	0.77	0.47 (-0.15 to 1.70)	0.051
			Antenatal screening	-14.78	717.42 (-1422.19 to 1392.64)	0.492
			Other	-0.32	0.42 (-1.14 to 0.50)	0.224
	HIV serostatus	HIV negative (baseline*)
			HIV positive	0.48	0.30 (-0.10 to 1.06)	0.052
	Infection acquired through
	oral sex		No (baseline*)
			Yes	0.12	0.29 (-0.46 to 0.69)	0.346
	Partner notification †	Traceable	-0.01	0.04 (-0.08 to 0.06)	0.399
			Untraceable	-0.02	0.01 (-0.03 to 0.00)	0.029
	Location	London (baseline*)
			Brighton	-0.76	0.75 (-2.23 to 0.70)	0.153
			Manchester	-0.97	0.56 (-2.08 to 0.14)	0.043
			Elsewhere UK	0.36	0.56 (-0.74 to 1.46)	0.259
			Overseas	-0.55	0.50 (-1.52 to 0.42)	0.134
	Commercial sex worker	No (baseline*)
			Yes	0.32	0.76 (-1.17 to 1.80)	0.337
	Social network	None (baseline*)
			Sauna	-0.95	0.31 (-1.56 to -0.34)	0.001
			Bar	-1.02	0.30 (-1.61 to -0.44)	<0.001
			Internet	-1.01	0.31 (-1.61 to -0.41)	0.001
	Age		16 to 19 (baseline*)
			20 to 24	-1.24	1.23 (-3.66 to 1.17)	0.157
			25 to 34	-1.15	1.21 (-3.52 to 1.23)	0.172
			35 to 44	-0.92	1.23 (-3.32 to 1.49)	0.227
			45+	-1.02	1.23 (-3.44 to 1.40)	0.204
	Time		Year	0.01	0.07 (-0.13 to 0.15)	0.462
	*	baseline individual: white heterosexual,

Table 3

 3 Comparison of secondary with early latent infection: estimates and confidence intervals for multinomial regression modelling*

	Parameter		Estimate	Standard Error (95% CI)	p-value
	Intercept		175.39	142.23 (-103.63 to 454.41)	0.109
	Strategic Health	East Midlands
	Authority	(baseline*)
		East of England	13.80	306.01 (-586.52 to 614.13)	0.482
		London	1.42	1.29 (-1.11 to 3.94)	0.136
		North West	1.32	1.20 (-1.04 to 3.68)	0.136
		South Central	11.52	215.44 (-411.13 to 434.16)	0.479
		South East Coast	0.37	1.42 (-2.41 to 3.15)	0.397
		South West	1.53	1.27 (-097 to 4.03)	0.115
		West Midlands	0.37	1.37 (-2.32 to 3.06)	0.393
		Yorkshire & The Humber	11.19	290.09 (-557.90 to 580.28)	0.485
	Gender	Male (baseline*)
		Female	-0.74	1.60 (-3.88 to 2.39)	0.321
	Whether born in the UK	UK-born (baseline*)
		Non UK-born	0.61	0.36 (-0.10 to 1.32)	0.045
	Ethnicity	White (baseline)
		Black	0.60	0.94 (-1.24 to 2.44)	0.261
		Asian	-0.77	0.66 (-2.06 to 0.52)	0.12
		Other ethnicity	-0.40	0.90 (-2.17 to 1.38)	0.33
	Sexual orientation	Heterosexual (baseline*)
		Men who have sex with men	0.37	0.67 (-0.95 to 1.69)	0.292
	Reason for attending	Routine STI screen
	clinical services	(baseline*)
		Symptoms	2.32	0.31 (1.71 to 2.92)	<0.001
		Campaign	-11.76	342.18 (-683.04 to 659.52)	0.486
		Partner notification	0.96	0.48 (0.02 to 1.90)	0.022
		Antenatal screening	-12.26	717.42 (-1419.67 to 1395.16)	0.493
		Other	0.33	0.39 (-0.43 to 1.10)	0.197
	HIV serostatus	HIV negative (baseline*)
		HIV positive	0.97	0.29 (0.40 to 1.54)	<0.001
	Infection acquired
	through oral sex	No (baseline*)
		Yes	-0.16	0.29 (-0.73 to 0.41)	0.29
	Partner notification	Traceable	0.00	0.03 (-0.05 to 0.06)	0.438
		Untraceable	0.00	0.01 (-0.01 to 0.01)	0.441
	Location	London (baseline*)
		Brighton	-0.46	0.74 (-1.91 to -0.99)	0.268
		Manchester	-0.18	0.57 (-1.31 to 0.94)	0.374
		Elsewhere UK	0.85	0.57 (-0.27 to 1.96)	0.068
		Overseas	-0.37	0.48 (-1.32 to 0.58)	0.223
	Commercial sex worker	No (baseline*)
		Yes	-1.43	0.95 (-3.29 to 0.44)	0.067
	Social network	None (baseline*)
		Sauna	-0.78	0.30 (-1.38 to -0.19)	0.005
		Bar	-0.86	0.29 (-1.43 to -0.28)_	0.002
		Internet	-0.76	1.30 (-1.34 to -0.18)	0.005
	Age	16 to 19 (baseline*)
		20 to 24	-1.30	0.27 (-3.86 to 1.25)	0.158
		25 to 34	-0.72	1.27 (-3.22 to 1.77)	0.285
		35 to 44	-0.76	1.29 (-3.29 to 1.77)	0.278
		45+	-0.89	1.30 (-3.44 to 1.65)	0.245
	Time	Year	-0.09	0.07 (-0.23 to 0.05)	0.108

* baseline individual: white heterosexual, UK-born HIV negative male, aged 16 to 19, who attended GUM services in the East Midlands for a routine STI screen, likely to have acquired syphilis in London but unlikely to have acquired infection through oral sex, not a commercial sex worker and with no stated social/sexual networks. †

* Partner notification is not shown because it is a discrete variable.

1.62=exp{0.48} higher odds ratio of presenting primary syphilis infection (as opposed to early latent) compared to an HIV negative patient.

Acknowledgements

We would like to thank GUM clinicians for reporting cases of infectious syphilis through the enhanced surveillance systems operated by the HPA Regional Epidemiology Units and HPA Centre for Infections, and Dr Marion Lyons for providing surveillance data for Wales.

Competing interests

None

Copyright licence

The Corresponding Author has the right to grant on behalf of all authors and does grant on behalf of all authors, an exclusive licence (or non-exclusive for government employees) on a worldwide basis to the BMJ Publishing Group Ltd, and its Licensees to permit this article (if accepted) to be published in Sexually Transmitted Infections and any other BMJPGL products and to exploit all subsidiary rights, as set out in our licence.

Footnote a

The KC60 statistical return was replaced by the Genitourinary Medicine Clinic

Activity Dataset as at 1 st April 2009.

estimation of the underlying infection rates. The model offering the best compromise between goodness of fit and model complexity, as measured by the AIC statistic, was ultimately used for drawing predictions over time. 3 Interaction terms were excluded because they did not increase the predictive power of the model. Alternative models encoding more structured time trends were also considered. Although a quadratic pattern was tested, it produced a model that had no appreciable difference in terms of overall accuracy-complexity balance, as indicated by corresponding AIC statistics (1382.045 from a linear time trend, 1383.154 from quadratic time trend).

Maximum likelihood estimates of regression coefficients were computed with corresponding standard errors, 95% confidence intervals (CI) and p-values. Some nonsignificant variables were retained within the model to preserve its robustness and facilitate the interpretation of its predictions. Baseline variables were arbitrarily taken as a white heterosexual, UK-born HIV negative male, who attended GUM services for routine STI screen within the East Midlands NHS SHA, was likely to have acquired syphilis in London although unlikely through oral sex, was not a commercial sex worker and had no stated social/sexual networks.