Nicolas Amat

Silvano Dal

Didier Le Botlan

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

Keywords: Petri nets, Quantifier elimination, Reachability problems

We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net. Our projection is defined as a variable elimination procedure for linear integer arithmetic tailored to the specific kind of constraints we handle. It has linear complexity, is guaranteed to return a sound property, and makes use of a simple condition to detect when the result is exact. Experimental results show that our approach works well in practice and that it can be useful even when there is only a limited amount of reductions.

Introduction

We describe a method to accelerate the verification of reachability properties in Petri nets by taking advantage of structural reductions [START_REF] Berthelot | Transformations and Decompositions of Nets[END_REF]. We focus on the verification of generalized properties, that can be expressed using a Boolean combination of linear constraints between places, such as (2 p 0 + p 1 = 5) ∧ (p 1 ⩾ p 2 ) for example. This class of formulas corresponds to the reachability queries used in the Model Checking Contest (MCC) [ABC + 19], a competition of Petri net verification tools that we use as a benchmark.

In essence, net reductions are a class of transformations that can simplify an initial net, (N 1 , m 1 ), into another, residual net (N 2 , m 2 ), while preserving a given class of properties. This technique has become a conventional optimization integrated into several model-checking tools [BLBDZ18, BDJ + 19, TM21]. A contribution of our paper is a procedure to transform a property F 1 , about the net N 1 , into a property F 2 about the reduced net N 2 , while preserving the verdict. We have implemented this procedure into a new tool, called Octant [START_REF] Amat | Octant (version 1.0): projection of Petri net reachability properties[END_REF], that can act as a pre-processor allowing any model-checker to transparently benefit from our optimization. Something that was not possible in our previous works. In practice, it means that we can use our approach as a front-end to accelerate any model-checking tool that supports generalized reachability properties, without modifying them.

Our approach relies on a notion, called polyhedral reduction [ABD21, ABD22, ADZLB21, BLBDZ19], that describes a linear dependence relation, E, between the reachable markings of a net and those of its reduced version. This equivalence, denoted (N 1 , m 1 ) ≡ E (N 2 , m 2 ), preserves enough information in E so that we can rebuild the state space of N 1 knowing only the one of N 2 . An interesting application of this relation is the following reachability conservation theorem [START_REF] Amat | On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets[END_REF]: assume we have (N 1 , m 1 ) ≡ E (N 2 , m 2 ), then property F is reachable in N 1 if and only if E ∧ F is reachable in N 2 . This property is interesting since it means that we can apply more aggressive reduction techniques than, say, slicing [Rak12, LOST17, KKG18], cone of influence [CJGK + 18], or other methods [START_REF] Ganty | From many places to few: Automatic abstraction refinement for Petri nets[END_REF][START_REF] Kang | Abstraction-based incremental inductive coverability for Petri nets[END_REF] that seek to remove or gather together places that are not relevant to the property we want to check. We do not share this restriction in our approach, since we reduce nets beforehand and can therefore reduce places that occur in the initial property. We could argue that approaches similar to slicing only simplify a model with respect to a formula, whereas, with our method, we simplify the model as much as possible and then simplify formulas as needed. This is more efficient when we need to check several properties on the same model and, in any case, nothing prevents us from applying slicing techniques on the result of our projection.

However, there is a complication, arising from the fact that the formula E ∧ F may include variables (places) that no longer occur in the reduced net N 2 , and therefore act as existentially quantified variables. This can complicate some symbolic verification techniques, such as k-induction [START_REF] Sheeran | Checking Safety Properties Using Induction and a SAT-Solver[END_REF], and impede the use of explicit, enumerative approaches. Indeed, in the latter case, it means that we need to solve an integer linear problem for each new state, instead of just evaluating a closed formula. To overcome this problem, we propose a new method for projecting the formula E ∧ F into an equivalent one, F ′ , that only refers to the places of N 2 . We define our projection as a procedure for quantifier elimination in Presburger Arithmetic (PA) that is tailored to the specific kind of constraints we handle in E. Whereas quantifier elimination has an exponential complexity in general for existential formulas, our construction has linear complexity and can only decrease the size of a formula. It also always terminates and returns a result that is guaranteed to be sound; meaning it under-approximates the set of reachable models and, therefore, a witness of F ′ in N 2 necessarily corresponds to a witness of F in N 1 . Additionally, our approach includes a simple condition on F that is enough to detect when our result is exact, meaning that if F ′ is unreachable in N 2 , then F is unreachable in N 1 . We show in Sect. 6 that our projection is complete for 80% of the formulas used in the MCC.

Outline and Contributions. We start by giving some technical background about Petri nets and the notion of polyhedral abstraction in Sect. 2, then describe how to use this equivalence to accelerate the verification of reachability properties (Th. 3.1 in Sect. 3). We also use this section to motivate our need to find methods to eliminate (or project) variables in a linear integer system. We define our fast projection method in Sect. 4, which is based on a dedicated graph structure, called Token Flow Graph (TFG), capturing the particular form of constraints occurring with polyhedral reductions. We prove the correctness of this method in Sect. 5. Our method has been implemented, and we report on the results of our experiments in Sect. 6. We give quantitative evidence about several natural questions raised by our approach. We start by proving the effectiveness of our optimization on both k-induction and random walk. Then, we show that our method can be transparently added as a preprocessing step to off-the-shelf verification tools. This is achieved by testing our approach with the three best-performing tools that participated in the reachability category of the MCC-ITS-Tools [START_REF] Thierry-Mieg | Symbolic Model-Checking Using ITS-Tools[END_REF] (or ITS for short); LoLA [START_REF] Wolf | Petri Net Model Checking with LoLA 2[END_REF]; and TAPAAL [DJJ + 12]-which are already optimized for the type of models and formulas used in our benchmark. Our results show that reductions are effective on a large set of queries and that their benefits do not overlap with other existing optimizations, an observation that was already made in [ABD22, BDJ + 19]. We also prove that our procedure often computes an exact projection and compares favorably well with the variable elimination methods implemented in isl [START_REF] Verdoolaege | isl: An integer set library for the polyhedral model[END_REF] and Redlog [START_REF] Dolzmann | Redlog: Computer algebra meets computer logic[END_REF]. This supports our claim that we are able to solve non-trivial quantifier elimination problems.

Petri Nets and Polyhedral Abstraction

Most of our results involve non-negative integer solutions to constraints expressed in Presburger Arithmetic, the first-order theory of the integers with addition [START_REF] Haase | A survival guide to Presburger arithmetic[END_REF]. We focus on the quantifier-free fragment of PA, meaning Boolean combinations (using ∧, ∨ and ¬) of atomic propositions of the form α ∼ β, where ∼ is one of =, ⩽ or ⩾, and α, β are linear expressions with coefficients in Z. Without loss of generality, we can consider only formulas in disjunctive normal form (DNF), with linear predicates of the form ( k i x i )+b ⩾ 0. We deliberately do not add a divisibility operator k | α, which requires that k evenly divides α, since it can already be expressed with linear predicates, though at the cost of an extra existentially quantified variable. This fragment corresponds to the set of reachability formulas supported by many model-checkers for Petri nets, such as [ABB + 16, BRV04, DJJ + 12, TM15, Wol18].

We use N V to denote the space of mappings over V = {x 1 , . . . , x n }, meaning total mappings from V to N. We say that a mapping m in N V is a model of a quantifier-free formula F if the variables of F , denoted fv(F ), are included in V and the closed formula F {m} (the substitution of m in F ) is true. We denote this relation m |= F .

F {m} ≜ F {x 1 ← m(x 1 )} . . . {x n ← m(x n )} (1)
We say that a Presburger formula is consistent when it has at least one model. We can use this notion to extend the definition of models in the case where F is over-specified; i.e. it has a larger support than m.

If m ′ ∈ N U with U ⊆ fv(F ), we write m ′ |= F when F {m ′ } is consistent.
Petri Nets and Reachability Formulas. A Petri net N is a tuple (P, T, Pre, Post) where P = {p 1 , . . . , p n } is an ordered set of places, T = {t 1 , . . . , t k } is a finite set of transitions (disjoint from P ), and Pre : T → N P and Post : T → N P are the pre-and post-condition functions (also called the flow functions of N ).

A state m of a net, also called a marking, is a mapping of N P . A marked net (N, m 0 ) is a pair composed of a net and its initial marking m 0 . We extend the comparison (=, ⩾) and arithmetic operations (-, +) to their point-wise equivalent. With our notations, a transition t ∈ T is said enabled

m ′ = m -Pre(t) + Post(t).
When the identity of the transition is unimportant, we simply write this relation m -→ m ′ . More generally, a marking m ′ is reachable from m in N , denoted m -→ ⋆ m ′ if there is a (possibly empty) sequence of transitions such that m -→ • • • -→ m ′ . We denote R(N, m 0 ) the set of markings reachable from m 0 in N .

We are interested in the verification of properties over the reachable markings of a marked net (N, m 0 ), with a set of places P . Given a formula F with variables in P , we say that F is reachable if there exists at least one reachable marking, m ∈ R(N, m 0 ), such that m |= F . We call such marking a witness of F . Likewise, F is said to be an invariant when all the reachable markings of (N, m 0 ) are models of F . This corresponds to the two classes of queries found in our benchmark: EF F , which is true only if F is reachable; and AG F , which is true when F is an invariant, with the classic relationship that AG F ≡ ¬ (EF ¬F ).

Examples of properties we can express in this way include: checking if some transition can possibly be enabled, checking if there is a deadlock, checking whether some linear invariant between places is always true, etc.

We use a standard graphical notation for nets where places are depicted with circles and transitions with squares. We give an example in Fig. 1, where net M 1 depicts the SmallOperatingSystem model, borrowed from the MCC benchmark [START_REF] Kordon | Model SmallOperatingSystem, Model Checking Contest benchmark[END_REF]. This net abstracts the lifecycle of a task in a simplified operating system handling several memory segments (place p 0 ), disk controller units (p 4 ), and cores (p 6 ). The initial marking of the net gives the number of resources available (e.g., there are 8 192 available memory segments in our example).

We chose this model since it is one of the few examples in our benchmark that fits on one page. This is not to say that the example is simple. Net M 1 has about 10 17 reachable states, which means that it is out of reach of enumerative methods, and only one symbolic tool in the MCC is able to generate its whole state space1 [KBG + 22]. For comparison, the reduced net M 2 has about 10 10 states.

Polyhedral Abstraction. We recently defined an equivalence relation that describes linear dependencies between the markings of two different nets, N 1 and N 2 [START_REF] Amat | A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking[END_REF]. In the following, we reserve F for formulas about a single net and use E to refer to relations. Assume m is a mapping of N V . We can associate m to the linear predicate m, which is a formula with a unique model m.

m

≜ {x = m(x) | x ∈ V } (2)
By extension, we say that m is a (partial) solution of E if the system E ∧ m is consistent. In some sense, we use m as a substitution, since the formulas E{m} and E ∧ m have the same models. Given two mappings m 1 ∈ N V1 and m 2 ∈ N V2 , we say that m 1 and m 2 are compatible when they have equal values on their shared domain:

m 1 (x) = m 2 (x) for all x in V 1 ∩ V 2
. This is a necessary and sufficient condition for the system m 1 ∧ m 2 to be consistent. Finally, we say that m 1 and m 2 are related up-to E, denoted

m 1 ≡ E m 2 , when E ∧ m 1 ∧ m 2 is consistent. m 1 ≡ E m 2 ⇔ ∃m ∈ N V . m |= E ∧ m 1 ∧ m 2 (3)
This relation defines an equivalence between markings of two different nets (≡ E ⊆ N P1 × N P2 ) and, by extension, can be used to define an equivalence between nets themselves, that we call polyhedral equivalence.

Definition 2.1 (E-equivalence). We say that (N 1 , m 1 ) is E-equivalent to (N 2 , m 2 ), denoted (N 1 , m 1 ) ≡ E (N 2 , m 2 ), if and only if:

(A1) E ∧ m is consistent for all markings m in R(N 1 , m 1 ) or R(N 2 , m 2 );
(A2) initial markings are compatible: m 1 ≡ E m 2 ;

(A3) assume m ′ 1 , m ′ 2 are markings of N 1 , N 2 , such that m ′ 1 ≡ E m ′ 2 , then m ′ 1 is reachable iff m ′ 2 is reachable: m ′ 1 ∈ R(N 1 , m 1 ) ⇐⇒ m ′ 2 ∈ R(N 2 , m 2 )
. By definition, given the equivalence (N 1 , m 1 ) ≡ E (N 2 , m 2 ), every marking m ′ 2 reachable in N 2 can be associated to a subset of markings in N 1 , defined from the solutions to E ∧ m ′ 2 (by condition (A1) and (A3)). In practice, this gives a partition of the reachable markings of (N 1 , m 1 ) into "convex sets"-hence the name polyhedral abstraction-each associated with a reachable marking in N 2 . This approach is particularly useful when the state space of N 2 is very small compared to the one of N 1 .

We can prove that the two marked nets in our running example satisfy M 1 ≡ E M 2 , for the relation E defined in Fig. 1. Net M 2 is obtained automatically from M 1 by applying a set of reduction rules, iteratively, and in a compositional way. This process relies on the reduction system defined in [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF][START_REF] Amat | A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking[END_REF]. As a result, we manage to remove five places: p 1 , p 5 , p 6 , p 7 , p 8 , and only add a new one, a 2 . The "reduction system" (E) also contains an extra variable, a 1 , that does not occur in any of the nets. It corresponds to a place that was introduced and then removed in different reduction steps.

Polyhedral abstractions are not necessarily derived from reductions, but reductions provide a way to automatically find interesting instances of abstractions. Also, the equation systems obtained using structural reductions exhibit a specific structure, that we exploit in Sect. 4.

Combining Polyhedral Abstraction with Reachability

We can define a counterpart to our notion of polyhedral abstraction which relates to reachability formulas. We show that this equivalence can be used to speed up the verification of properties by checking formulas on a reduced net instead of the initial one (see Th. 3.1 and its corollary, below). In the following, we assume that we have two marked nets such that (N 1 , m 1 ) ≡ E (N 2 , m 2 ). Our goal is to define a relation F 1 ≡ E F 2 , between reachability formulas, such that F 1 and F 2 have the same truth values on equivalent models, with respect to E.

Definition 3.1 (Equivalence between formulas). Assume F 1 , F 2 are reachable formulas with respective sets of variables, V 1 and V 2 , in the support of E. We say that formula

F 2 implies F 1 up-to E, denoted F 2 ⊑ E F 1 , if for every marking m ′ 2 ∈ N V2 such that m ′ 2 |= E ∧ F 2 there exists at least one marking m ′ 1 ∈ N V1 such that m ′ 1 ≡ E m ′ 2 and m ′ 1 |= E ∧ F 1 . F 2 ⊑ E F 1 iff ∀m ′ 2 . (m ′ 2 |= E ∧ F 2 ) ⇒ ∃m ′ 1 . (m ′ 1 ≡ E m ′ 2 ∧ m ′ 1 |= E ∧ F 1 ) (4) We say that F 1 and F 2 are equivalent, denoted F 1 ≡ E F 2 , when both F 1 ⊑ E F 2 and F 2 ⊑ E F 1 .
This notion is interesting when F 1 , F 2 are reachability formulas on the nets N 1 , respectively N 2 . Indeed, we prove that when

F 2 ⊑ E F 1 , it is enough to find a witness of F 2 in N 2 to prove that F 1 is reachable in N 1 . Theorem 3.1 (Finding Witnesses). Assume (N 1 , m 1 ) ≡ E (N 2 , m 2 ) and F 2 ⊑ E F 1 , and take a marking m ′ 2 reachable in (N 2 , m 2 ) such that m ′ 2 |= F 2 . Then there exists m ′ 1 ∈ R(N 1 , m 1 ) such that m ′ 1 ≡ E m ′ 2 and m ′ 1 |= F 1 . Proof. Assume we have m ′ 2 reachable in N 2 such that m ′ 2 |= F 2 . By property (A1) of E-equivalence (Def. 2.1), formula E ∧ m ′ 2 is consistent, which gives m ′ 2 |= E ∧ F 2 . By definition of the E-implication F 2 ⊑ E F 1 , we get a marking m ′ 1 such that m ′ 1 |= F 1 and m ′ 1 ≡ E m ′ 2 . We conclude that m ′ 1 is reachable in N 1 thanks to property (A3). Hence, when F 2 ⊑ E F 1 holds, F 2 reachable in N 2 implies that F 1 is reachable in N 1 .
We can derive stronger results when F 1 and F 2 are equivalent.

Corollary 3.1.1. Assume (N 1 , m 1 ) ≡ E (N 2 , m 2 ) and F 1 ≡ E F 2 , with fv(F i ) ⊆ P i for all i ∈ 1..2, then: (CEX) property F 1 is reachable in N 1 if and only if F 2 is reachable in N 2 ; and (INV) F 1 is an invariant on N 1 if and only if F 2 is an invariant on N 2 .
Theorem 3.1 means that we can check the reachability (or invariance) of a formula on the net N 1 by checking instead the reachability of another formula (F 2 ) on N 2 . But it does not indicate how to compute a good candidate for F 2 . By Definition 3.1, a natural choice is to select F 2 ≜ E ∧F 1 . We can actually do a bit better. It is enough to choose a formula F 2 that has the same (integer points) solution as E ∧ F 1 over the places of N 2 . More formally, let A ≜ fv(E) \ P 2 be the set of "additional variables" from E; variables occurring in E which are not places of the reduced net N 2 . Then if F 2 has the same integer solutions over N P2 than the Presburger formula ∃A. (E ∧ F 1 ), we have F 1 ≡ E F 2 . We say in this case that F 2 is the projection of E ∧ F 1 on the set P 2 , by eliminating the variables in A.

In the next section, we show how to compute a candidate projection formula without resorting to a classical, complete variable elimination procedure on E ∧ F 1 . This eliminates a potential source of complexity blow-up.

We can use Fourier-Motzkin elimination (FM) as a point of reference. Given a system of linear inequalities S, with variables in V , we denote FM A (S) the system obtained by FM elimination of variables in A from S. (We do not describe the construction of FM A (S) here, since there exists many good references [START_REF] Imbert | Fourier's elimination: Which to choose?[END_REF][START_REF] Monniaux | Quantifier elimination by lazy model enumeration[END_REF] on the subject.) Borrowing an intuition popularized by Pugh in its Omega test [START_REF] Pugh | The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis[END_REF], we can define two distinct notions of "shadows" cast by the projection of S. On the one hand, we have the real shadow, relative to A, which are the integer points (in N V \A ) solutions of FM A (S). On the other hand, the integer shadow of S is the set of markings m ′ with an integer point antecedent in S. We need the latter to check a query on N 1 . A main source of complexity is that the (real) shadow is only exact on rational points and may contain strictly more models than the integer shadow. Moreover, while the real shadow of a convex region will always be convex, it may not be the case with the integer shadow. Like with the real shadow, the set of equations computed with our fast projection will always be convex. Unlike FM, our procedure will compute an under-approximation of the integer shadow, not an over-approximation. Also, we never rearrange or create more inequalities than the one contained in S; but instead rely on variable substitution.

We illustrate the concepts introduced in this section on our running example, with the reduction system from Fig. 1. With our notations, we try to eliminate variables in A ≜ {a 1 , p 1 , p 5 , p 6 , p 7 , p 8 } and keep only those in P 2 ≜ {a 2 , p 0 , p 2 , p 3 , p 4 }.

Take the formula G 1 ≜ (p 5 + p 6 ⩽ p 8 ). Using substitutions from constraints in E, namely the fact that (a 2 = p 7 + p 8 + p 5 ) and (p 6 = p 0 + p 2 + p 3 + p 5 + p 7 ), we can remove occurrences of a 1 , p 1 , p 6 , p 8 from E ∧ G 1 , leaving the resulting equation (3 p 5 + 2 p 7 + p 0 + p 2 + p 3 ⩽ a 2 ) ∧ (a 2 = p 5 + p 7 + p 8 ), that still refers to p 5 and p 7 . We observe that non-trivial coefficients (like 3 p 5 ) can naturally occur during this process, even though all the coefficients are either 1 or -1 in the initial constraints. We can remove the remaining variables to obtain an exact projection of G 1 using our fast projection method, described below. The result is the formula

G 2 ≜ (p 0 + p 2 + p 3 ⩽ a 2 ).
Another example is H 1 ≜ (p 6 = p 8 ). We can prove that the integer shadow of E ∧H 1 , after projecting the variables in A, are the solutions to the PA formula (a 2p 0p 2p 3 ≡ 0 mod 2) ∧ (a 2 ⩾ p 0 + p 2 + p 3 ). This set is not convex, since (a 2 = 0 ∧ p 0 = p 1 = p 2 = p 3 = 0) and (a 2 = 2 ∧ p 0 = p 1 = p 2 = p 3 = 0) are in the integer shadow, but not (a 2 = 1 ∧ p 0 = p 1 = p 2 = p 3 = 0) for instance. Our fast projection method will compute the formula H 2 ≜ (a 2 + p 0 + p 2 + p 3 = 0) and flag it as an under-approximation.

# R |-p1 = p4 + 4096 # R |-p6 = p0 + p2 + p3 + p5 + p7 # A |-a1 = p7 + p8 # A |-a2 = a1 + p5

Projecting Formulas Using Token Flow Graphs

We describe a formula projection procedure that is tailored to the specific kind of constraints occurring in polyhedral reductions. The example in Fig. 1 is representative of the "shape" of reduction systems: it mostly contains equalities of the form x = x i , over a sparse set of variables, but may also include some inequalities; and it can have a very large number of literals (often proportional to the size of the initial net). Another interesting feature is the absence of cyclic dependencies, which underlines a hierarchical relationship between variables.

We can find a more precise and formal description of these constraints in [START_REF] Amat | Accelerating the Computation of Dead and Concurrent Places using Reductions[END_REF], with the definition of a Token Flow Graph (TFG). Basically, a TFG for a reduction system E is a directed acyclic graph (DAG) with one vertex for each variable occurring in E. We consider two kinds of arcs, redundancy (→•) and agglomeration (•→), that correspond to two main classes of reduction rules.

Arcs for redundancy equations, q →• p, correspond to equations of the form p = q + r + . . . , expressing that the marking of place p can be reconstructed from the marking of q, r, . . . In this case, we say that place p is removed by arc q →• p, because the marking of q may influence the marking of p, but not necessarily the other way round.

Arcs for agglomeration equations, a •→ p, represent equations of the form a = p + q + . . . , generated when we agglomerate several places into a new one. In this case, we expect that if we can reach a marking with k tokens in a, then we can certainly reach a marking with k 1 tokens in p, and k 2 tokens in q, . . . such that k = k 1 + k 2 + . . . . Hence, the possible markings of p and q can be reconstructed from the markings of a. In this case, it is p, q, . . . which are removed. We also say that node a is inserted ; it does not exist in N 1 but may appear as a new place in N 2 unless it is removed by a subsequent reduction. We can have more than two places in an agglomeration, see the rules in [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF].

A TFG can also include nodes for constants, used to express invariant statements on the markings of the form p + q = k. To this end, we assume that we have a family of disjoint sets K(n) for each n in N, such that the "valuation" of a node v ∈ K(n) is always n. We use K to denote the set of all constants. Definition 4.1 (Token Flow Graph). A TFG with set of places P is a directed graph (P, S, R • , A • ) such that:

• V = P ∪ S is a set of vertices (or nodes) with S ⊂ K a finite set of constants, • R • ∈ V × V is a set of redundancy arcs, v →• v ′ , • A • ∈ V × V is a set of agglomeration arcs, v •→ v ′ , disjoint from R.
The main source of complexity in this approach arises from the need to manage interdependencies between A • and R • arcs, that is situations where redundancies and agglomerations are combined. This is not something that can be easily achieved by looking only at the equations in E and thus motivates the need for a specific data structure.

We define several notations that will be useful in the following. We use the notation v → v ′ when we have

(v →• v ′ ) or (v •→ v ′ ). We say that a node v is a root if it is not the target of an arc. A sequence of nodes (v 1 , . . . , v n ) in V n is a path if for all 1 ⩽ i < n we have v i → v i+1 . We use the notation v → ⋆ v ′ when there is a path from v to v ′ in the graph, or when v = v ′ . We write v •→ X when X is the largest subset {v 1 , . . . , v k } of V such that X ̸ = ∅ and v •→ v i for all i ∈ 1..k.
And similarly with reductions, X →• v. Finally, the notation ↓v denotes the set of successors of v, that is:

↓v ≜ {v ′ ∈ V \ {v} | v → ⋆ v ′ }.
We extend it to a set of variables X with ↓X = x∈X ↓x.

We display an example of TFG in Fig. 2 (right), which corresponds to the reduction equations generated on our running example, where annotations R and A indicate if an equation is a redundancy or an agglomeration. TFGs were initially defined in [ADZLB21, ADLB22] to efficiently compute the set of concurrent places in a net, that is all pairs of places that can be marked simultaneously in some reachable marking. We reuse this concept here to project reachability formulas.

High Literal Factor. The projection procedure, described next, applies to cubes only, meaning a conjunction of literals i∈1..n α i . Given a formula F 1 , assumed in DNF, we can apply the projection procedure to each of its cubes, separately. Then the projection of F 1 is the disjunction of the projected cubes. We assume from now on that F 1 is a cube formula.

We assume that every literal is in normal form, α i ≜ ( pj ∈B k i j p j ) + b i ⩾ 0, where the k i j 's and b i are in Z. In the following, we denote α i (q) the coefficient associated with variable q in α i . We also use max X α i and min X α i for the maximal (resp. minimal) coefficient associated with variables in X ⊆ B .

α i = p∈B α i (p) p + b i and max X α i = max {α i (p) | p ∈ X}
We define the Highest Literal Factor (HLF) of a set of variables X with respect to a set of normalized literals (α i ) i∈I . In the simplest case, the HLF of X with respect to a single literal, α, is the subset of variables in X with the highest coefficients in α. Then, the HLF of X with respect to a set of literals is the (possibly empty) intersection of the HLFs of X with respect to each literal. When non-empty, it means that at least one variable in X always has the highest coefficient, and we say then that the whole set X is polarized with respect to the literals (α i ).

HLF X (α i ) = {p ∈ X | α i (p) = max X α i } HLF X (α i ) i∈I = i∈I HLF X (α i )
Definition 4.2 (Polarized Set of Constraints). A set of variables X ⊆ fv(C ) is said polarized with respect to a set of normalized literals C when HLF X (C ) ̸ = ∅.

We prove in the next section that our procedure is exact when the variables we eliminate are polarized. While this condition seems very restrictive, we observe that it is often true with the queries used in our experiments.

Example. Let us illustrate our approach with two examples. Assume we want to eliminate an agglomeration a •→ {q, r}, meaning that we have the condition a = q + r and that both q and r must disappear. We consider two examples of systems, each with only two literals, and with free variables {p, q}.

3 p + 2 q -1 r 0 2 p + 1 q + 1 r -5 0 3 p + 2 q -r 0 -p + q + 2 r -5 0 3 p + 2 a 0 2 p + 1 a -5 0 3 p -a 0 -p + a -5 0
In the left example, the set {q, r} is polarized with respect to the initial system (top), with the highest literal factor being q. So we replace q with a in both literals and eliminate r. Uninvolved variables (the singleton {p} in this case) are left unchanged. We can prove that both systems, before and after substitution, are equivalent. For instance, every solution in the resulting system can be associated with a solution of the initial one by taking q = a and r = 0.

The initial system on the right (top) is non-polarized: the HLF relative to {q, r} is {q} for the first literal (+2 q versus -r) and {r} in the second (+q versus 2 r). So we substitute a to the variable with the lowest literal factor, in each literal, and remove the other variable (r in the first literal and q in the second). This is sound because we take into account the worst case in each case. But this is not complete, because we may be too pessimistic. For instance, the resulting system has no solution for p = 2; because it entails a ⩽ 6 and a ⩾ 7. But p = 2, q = 3, r = 2 is a model of the initial system.

Next, we give a formal description of our projection procedure as a sequence of formula rewriting steps and prove that the result is exact (we have F 2 ≡ E F 1 ) when all the reduction steps corresponding to an agglomeration are on polarized variables.

Formal Procedure and Proof of Correctness

In all the results of this section, we assume that N 1 and N 2 are two nets, with respective sets of places P 1 , P 2 and initial markings m 1 , m 2 , such that (N 1 , m 1 ) ≡ E (N 2 , m 2 ). Given a formula F 1 with support on N 1 , we describe a procedure to project formula E ∧ F 1 into a new formula, F 2 , with support on N 2 . Our projection will always lead to a sound formula, meaning F 2 ⊑ E F 1 . It is also able in many cases (see some statistics in Sect. 6) to result in an exact formula, such that F 2 ≡ E F 1 .

Constraints on TFGs. To ensure that a TFG preserves the semantics of the system E we must introduce a set of constraints on it. A well-formed TFG G built from E is a graph with one node for every variable and constant occurring in E, such that we can find one set of arcs, either X →• v or v •→ X, for every equation of the form v = vi∈X v i in E. We deal with inequalities by adding slack variables. We also impose additional constraints which reflect that the same place cannot be removed more than once. Note that the places of N 2 are exactly the root of G (if we forget about constants).

Definition 5.1 (Well-formed TFG). A TFG G = (P, S, R • , A • ) for the equivalence statement (N 1 , m 1 ) ≡ E (N 2 , m 2 ) is well-formed when the following constraints are met, with P 1 , P 2 the set of places in N 1 , N 2 :

(T1) nodes in S are roots: if v ∈ S then v is a root of G;
(T2) nodes can be removed only once: it is not possible to have v •→ w and v ′ → w with v ̸ = v ′ , or to have both v →• w and v •→ w;

(T3) G contains all and only the equations in

E: we have v •→ X or X →• v if and only if the equation v = vi∈X v i is in E;
(T4) G is acyclic and roots in P \ S are exactly the set P 2 .

Given a relation (N 1 , m 1 ) ≡ E (N 2 , m 2 ), the well-formedness conditions are enough to ensure the unicity of a TFG (up-to the choice of constant nodes) when we set each equation to be either in A or in R. In this case, we denote the graph T(E). In practice, we use the tool Reduce [START_REF]Tina Toolbox[END_REF] to generate the reduction system E. Formula Rewriting. We assume given a relation (N 1 , m 1 ) ≡ E (N 2 , m 2 ), and its associated well-formed TFG written T(E). We consider that F 1 is a cube of n literals, F 1 ≜ i∈1..n α 0 i . Our algorithm rewrites each α 0 i by applying iteratively an elimination step, described next, according to the constraints expressed in T(E). The final result is a conjunction F 2 = i∈1..n β i , where each literal β i has support in N 2 . Rewriting can only replace a variable with a group of other variables that are its predecessors in the TFG, which ensures termination in polynomial time (in the size of E). Although the result has the same number of literals, it usually contains many redundancies and trivial constant comparisons, so that, after simplification, F 2 can actually be much smaller than F 1 .

A reduction step (to be applied repeatedly) takes as input the current set of literals, C = (α i ) i∈1..n , and modifies it. To ease the presentation, we also keep track of a set of variables, B such that i∈1..n fv(α i ) ⊆ B .

An elimination step is a reduction written (B , C ) → (B ′ , C ′ ) where C = (α i ) i∈1..n and B ′ ⊊ B , defined as one of the three cases below (one for redundancy, and two for agglomerations, depending on whether the removed variables are polarized or not). We assume that literals are in normal form and that X is a set of variables {x 1 , . . . , x k }. Note the precondition ↓X ∩ B = ∅ on all rules, which forces them to be applied bottom-up on the TFG (remember it is a DAG). We gave a short example of how to apply rules (AGP) and (AGD) at the end of the previous section. (RED) In this case we have X →• p and B ′ = B \ {p}, with X = {x 1 , . . . , x k }.

We can extend m ′ into the unique valuation (AGP) In this case we have a •→ X with X = {x 1 , . . . , x k }, polarized relative to C , and B ′ = B \X. We consider x j in X the variable in HLF X (C ) that was chosen in the reduction; meaning that C ′ is a conjunction of literals of the form α{x l ← 0} l̸ =j {x j ← a}, with α a literal of C . Given m ′ a model of C ′ , we define m the unique marking on N B such that m(x j ) = m(a), m(x l ) = 0 for all l ̸ = j, and

m of N B such that m(p) = m ′ (x 1 ) + • • • + m ′ (x k ) and m(v) = m ′ (v) for all other nodes v in B \ {p}. Since p = x 1 + • • • + x k is
m(v) = m ′ (v) for all other variables v in B \ X.
From Lemma 2 of [ADZLB21] (the "token propagation" property of TFGs), we know that any distribution of m(a) tokens, in place a, over the

(x i ) i∈1..k , is also a model of E.
Which means that m |= E ( * ). Note that the token propagation Lemma does not imply that the value of m(v), for the nodes "below X" (v in ↓X), is unchanged. This is not problematic, since the side condition ↓X ∩ B = ∅ ensures that these nodes are not in B , and therefore cannot influence the value of α{m}.

Consider a literal α in C . Since m ′ |= C ′ , we have that α{x l ← 0} l̸ =j {x j ← a}{m ′ } SAT, which is exactly α{m}, since ↓X ∩ B = ∅, as needed ( * * ).

(AGD) In this case we have a •→ X with X = {x 1 , . . . , x k }, non-polarized relative to C , and B ′ = B \ X. We know that m ′ |= E, therefore there is a marking m of N B that extends m ′ such that m ≡ E m ′ ( * ).

Consider a literal α in C . By definition of (AGD), we have an associated

literal α ′ ≜ α{x l ← 0} l̸ =j {x j ← a} in C ′ such that α(x j ) = min X α i . Since the coefficient of x j is minimal, we have that i∈1..k α(x i ) m(x i ) ⩾ α(x j ) i∈1..k m(x i ) = α(x j ) m ′ (a), and therefore v∈B α(v) m(v) ⩾ v∈B ′ α ′ (v) m ′ (v).
The result follows from the fact that α{m} SAT ( * * ). Now we prove that our quantifier elimination step, for the (RED) and (AGP) cases, leads to a complete projection, that is any solution of the initial formula corresponds to a projected solution in the projected formula.

Lemma 5.3 (Completeness). If (B , C ) → (B ′ , C ′ ) is a (RED) or (AGP) re- duction then C ⊑ E C ′ .
Proof. Take a marking m of N B such that m |= E ∧ C . We want to show that there exists a valuation m ′ of N B ′ such that m ≡ E m ′ ( * ) and m ′ |= C ′ ( * * ). This is enough to prove m ′ |= E ∧C ′ . We have two different cases, corresponding to the rules (RED) and (AGP).

(RED) In this case we have X →• p with X = {x 1 , . . . , x k } and B ′ = B \ {p}.

We define m ′ as the (unique) projection of m on B ′ . Since m |= E we have that m ′ ≡ E m ( * ).

Also, literals in

C ′ are of the form α ′ ≜ α{p ← x 1 + • • • + x k } where α is a literal of C . Since m(p) = i∈1..k m(x i )
and m is a model of α, it is also the case that m ′ is a model of α ′ ( * * ).

(AGP) In this case we have a •→ X with X = {x 1 , . . . , x k } and B ′ = B \ X.

We define m ′ as the (unique) projection of m on B ′ , by taking m ′ (a) = i∈1..k m(x i ). Since m |= E we have that m ′ ≡ E m ( * ). We consider x j in X the variable in HLF X (C ) that was chosen in the reduction; meaning that C ′ is a conjunction of literals of the form

α{x l ← 0} l̸ =j {x j ← a}, with α a literal of C . Since i∈1..k α(x i ) m(x i ) ⩽ α(x j ) i∈1..k m(x i ) = α(x j ) m ′ (a), we have m ′ is a model of α ′ ( * * ).
The final step of our proof relies on a progress property, meaning there is always a reduction step to apply except when all the literals have their support on the reduced net, N 2 . This property relies on relation → * , which is the transitive closure of →. Together with Th. 5.1, the progress theorem ensures the existence of a sequence (P, C ) → * (P 2 , C ′ ), such that C ≡ E C ′ (or C ′ ⊑ E C if we have at least one non-polarized agglomeration). In this context, P is the set of all variables occurring in the TFG of E, and therefore it contains P 1 ∪ P 2 .

Theorem 5.4 (Progress). Assume (P, F 1 ) → * (B , C ) then either B ⊆ P 2 , the set of places of N 2 , or there is an elimination step (B , C ) → (B ′ , C ′ ) such that fv(C ′ ) ⊆ B ′ and the places removed from B have no successors in B ′ : for all places p in B \ B ′ , we have ↓p ∩ B = ∅.

Proof. Assume we have (P, F 1 ) → * (B , C ) and B ⊈ P 2 .

By condition (T4) in Def. 5.1, we know that P 2 are roots in the TFG T(E). We consider the set of nodes in B \ P 2 , which corresponds to nodes in B with at least one parent. Also, by condition (T4), we know that T(E) is acyclic, then there are nodes in B \ P 2 that have no successors in B . We call this set L.

Hence, L ≜ {v | v ∈ B \ P 2 ∧ ↓v ∩ B = ∅}.
Take a node p in L. We have two possible cases. If there is a set X such that X →• p, we can apply the (RED) elimination rule. Otherwise, there exists a node a and a set X ⊆ L (by condition (T2)) such that a •→ X with p ∈ X. In this case, apply rule (AGP) or (AGD), depending on whether the agglomeration is polarized or not.

Remark. We have designed the rule (AGD) to obtain at least F 2 ⊑ E F 1 when the procedure is not complete (instead of F 2 ≡ E F 1 ), which is useful for finding witnesses (see Th. 3.1). Alternatively, we could propose a variant rule, say (AGD'), which chooses the variable x j having the highest coefficient in α i , that is α i (x j ) = max X α i . This variant guarantees a dual result, that is F 1 ⊑ E F 2 . In this case, if F 2 is not reachable then F 1 is not reachable, which is useful to prove invariants.

Experimental Results

Data-Availability Statement. We have implemented our fast quantifier elimination procedure in a new, open-source tool called Octant [START_REF] Amat | Octant (version 1.0): projection of Petri net reachability properties[END_REF], available on GitHub. All the tools, scripts and benchmarks used in our experiments are part of our artifact [START_REF] Amat | Artifact for VMCAI 2024 Paper "Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability[END_REF].

We use an extensive, and independently managed, set of models and formulas collected from the 2022 edition of the Model Checking Contest (MCC) [KBG + 22]. The benchmark is built from a collection of 128 models. Most models are parametrized and can have several instances. This amounts to about 1 400 different instances of Petri nets whose size varies widely, from 9 to 50 000 places, and from 7 to 200 000 transitions. This collection provides a large number of examples with various structural and behavioral characteristics, covering a large variety of use cases. Each year, the MCC organizers randomly generate 16 reachability formulas for each instance. The pair of a Petri instance and a formula is a query; which means we have more than 22 000 queries overall.

We do not compute reductions ourselves but rely on the tool Reduce, part of the latest public release of Tina [START_REF]Tina Toolbox[END_REF]. We define the reduction ratio (r p ) of an instance as the ratio (p initp red )/p init between the number of places before (p init ) and after (p red ) reduction. We only consider instances with a ratio, r p , between 1% and 100% (meaning the net is fully reduced ), which still leaves about 17 000 queries, so about 77% of the whole benchmark. More information about the distribution of reductions can be found in [START_REF] Amat | A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking[END_REF][START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF], where we show that almost half the instances (48%) can be reduced by a factor of 25% or more.

The size of the reduction system, E, is proportional to the number of places that can be removed. To give a rough idea, the mean number of variables in E is 1 375, with a median value of 114 and a maximum of about 62 000. The number of literals is also rather substantial: a mean of 869 literals (62% of agglomerations and 38% of redundancies), with a median of 27 and a maximum of about 38 000.

We report on the results obtained on two main categories of experiments: first with model-checking, to evaluate if our approach is effective in practice, using real tools; then to assess the precision and performance of our fast quantifier elimination procedure.

Model-Checking. We start by showing the effectiveness of our approach on both k-induction and random walk. This is achieved by comparing the computation time, with and without reductions, on a model-checker that provides a "reference" implementation of these techniques. (Without any other optimizations that could interfere with our experiments.) It is interesting to test the results of our optimization separately on these two techniques. Indeed, each technique is adapted to a different category of queries: properties that can be decided by finding a witness, meaning true EF formulas or false AG ones, can Figure 4: k-induction w/wo reductions.

often be checked more efficiently using a random exploration of the state space.

On the other hand, symbolic verification methods are required when we want to check invariants. We display our results using the two "cactus plots" in Figs. 3 and4. We distinguish between two categories of instances, depending on their reduction ratio. We use dashed lines for models with a low or moderate reduction ratio (value of r p less than 50%) and solid lines for models that can be reduced by more than half. The first category amounts to roughly 10 700 queries (62% of our benchmark), while the second category contains about 6 000 queries. The most interesting conclusion we can draw from these results is the fact that our approach is beneficial even when there is only a limited amount of reductions.

Our experiments were performed with a maximal timeout of 180 s and integrated the projection time into the total execution time. The "vertical asymptote" that we observe in these plots is a good indication that we cannot expect further gains, without projection, for timeout values above 60s. Hence, our choice of timeout value does not have an overriding effect. We observe moderate performance gains with random exploration (with ×1.06 more computed queries on low-reduction instances and ×1.19 otherwise) and good results with k-induction (respectively ×1.94 and ×2.33).

We obtain better results if we focus on queries that take more than 1 s on the original formula, which indicates that reductions are most effective on "difficult problems" (there is not much to gain on instances that are already easy to solve). With random walk, for instance, the gain becomes ×1.48 for low-reduction instances and ×1.93 otherwise. The same observation is true with k-induction, with performance gains of ×3.78 and ×3.51 respectively.

Model-Checking under Real Conditions. We also tested our approach by transparently adding polyhedral reductions as a front-end to three different model-checkers: TAPAAL [DJJ + 12], ITS [START_REF] Thierry-Mieg | Symbolic Model-Checking Using ITS-Tools[END_REF], and LoLA [START_REF] Wolf | Petri Net Model Checking with LoLA 2[END_REF], that implement portfolios of verification techniques. All three tools regularly compete in the MCC (on the same set of queries that we use for our benchmark), TAPAAL and ITS share the top two places in the reachability category of the 2022 and 2023 editions. We ran each tool on our set of complete projections, which amounts to almost 100 000 runs (one run for each tool, once on both the original and the projected query). We obtained a 100% reliability result, meaning that all tools gave compatible results on all the queries; and therefore also compatible results on the original and the projected formulas.

A large part of the queries can be computed by all the tools in less than 100 ms and can be considered as easy. These queries are useful for testing reliability but can skew the interpretation of results when comparing performances. This is why we decided to focus our results on a set of 809 challenging queries, that we define as queries for which either TAPAAL or ITS, or both, are not able to compute a result before projection. The 809 challenging queries (4% of queries) are well distributed, since they cover 209 different instances (14% of all instances), themselves covering 43 different models (33% of the models).

We display the results obtained on the challenging queries, for a timeout of 180 s, in Table 5. We provide the number of computed queries before and after projection, together with the mean and median speed-up (the ratio between the computation time with and without projection). The "Exclusive" column reports, for each tool, the number of queries that can only be computed using the projected formula. Note that we may sometimes time out with the projected query, but obtain a result without. This can be explained by cases where the size of the formula blows up during the transformation into DNF.

We observe substantial performance gains with our approach and can solve about half of the challenging queries. For instance, we are able to compute ×1.6 more challenging queries with TAPAAL using projections than without. (We display more precise results on TAPAAL, the winner of the MCC 2022 edition, in Fig. 6.) We were also able to compute 62 queries, using projections, that no tool was able to solve during the last MCC (where each tool has 3600 s to answer 16 queries on a given model instance). All these results show that polyhedral reductions are effective on a large set of queries and that their benefits do not significantly overlap with other existing optimizations, an observation that was already made, independently, in [START_REF] Amat | A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking[END_REF] and [BDJ + 19].

The approach implemented in Octant was partially included in the version of our model-checker, called SMPT [START_REF] Amat | SMPT: A Testbed for Reachability Methods in Generalized Petri Nets[END_REF], that participated in the MCC 2023 edition. We mainly left aside the handling of under-approximated queries, when the formula projection is not complete. While SMPT placed third in the reachability category, the proportion of queries it was able to solve raised by 5.5% between 2022 (without the use of Octant) and 2023, to reach a ratio of 93.6% of all queries solved with our tool. A 5% gain is a substantial result, taking into account that the best-performing tools are within 1% of each other; the ratios for ITS and TAPAAL in 2023 are respectively 94.6% and 94.3%.

Performance of Fast Elimination. Our last set of experiments is concerned with the accuracy and performance of our quantifier elimination procedure. We decided to compare our approach with Redlog [DS97] and isl [Ver10] (we give more details on these two tools in Sect. 7).

We display our results in the cactus plot of Fig. 7, where we compare the number of projections we can compute given a fixed timeout. We observe a significant performance gap. For instance, with a timeout of 60 s, we are able to compute 16 653 projections, out of 16 976 queries (98%), compared to 9 407 (55%) with isl or 4 915 (29%) with Redlog. So an increase of ×1.77 over the better of the two tools. This provides more empirical evidence that the class of linear systems we manage is not trivial, or at least does not correspond to an easy case for the classical procedure implemented in Redlog and isl. We also have good results concerning the precision of our approach, since we observe that about 80% of the projections are complete. Furthermore, projections are inexpensive. For instance, the computation time is less than 1 s for 96% of the formulas. We also obtained a median reduction ratio (computed as for the number of places) of 0.2 for the number of cubes and their respective number of literals.

Discussion and Related Works

We proposed a quantifier elimination procedure that can take benefit of polyhedral reductions and can be used, transparently, as a pre-processing step of existing model-checkers. The main characteristic of our approach is to rely on a graph structure, called Token Flow Graph, that encodes the specific shape of our reduction equations.

The idea of using linear equations to keep track of the effects of structural reductions originates from [START_REF] Berthomieu | Petri net reductions for counting markings[END_REF][START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF], as a method for counting the number of reachable markings. We extended this approach to Bounded Model Checking (BMC) in [START_REF] Amat | A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking[END_REF] where we defined our polyhedral abstraction equivalence, ≡ E , and in [START_REF] Amat | Automated Polyhedral Abstraction Proving[END_REF] where we proposed a procedure to automatically prove when such abstractions are correct. The idea to extend this relation to formulas is new (see Def. 3.1). In this paper, we broaden our approach to a larger set of verification methods; most particularly k-induction, which is useful to prove invariants, and simulation (or random walk ), which is useful for finding counter-examples. We introduced the notion of a Token Flow Graph (TFG) in [START_REF] Amat | Accelerating the Computation of Dead and Concurrent Places using Reductions[END_REF], as a new method to compute the concurrent places of a net; meaning all pairs of places that can be marked simultaneously. We find a new use for TFGs here, as the backbone of our variable elimination algorithm, and show that we can efficiently eliminate variables in systems of the form E ∧ F , for an arbitrary F .

We formulated our method as a variable elimination procedure for a restricted class of linear systems. There exist some well-known classes of linear systems where variable elimination has a low complexity. A celebrated example is given by the link between unimodular matrices and integral polyhedra [START_REF] Hoffman | Integral boundary points of convex polyhedra[END_REF], which is related to many examples found in abstract domains used in program verification, such as systems of differences [START_REF] Aspvall | A polynomial time algorithm for solving systems of linear inequalities with two variables per inequality[END_REF] or octagon [START_REF] Miné | The octagon abstract domain[END_REF][START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. To the best of our knowledge, none of the known classes correspond to what we define using TFGs. There is also a rich literature about quantifier elimination in Presburger arithmetic, such as Cooper's algorithm [START_REF] David | Theorem proving in arithmetic without multiplication[END_REF][START_REF] Haase | A survival guide to Presburger arithmetic[END_REF] or the Omega test [START_REF] Pugh | The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis[END_REF] for instance, and how to implement it efficiently [HLL92, LS07, Mon10]. These algorithms have been implemented in several tools, using many different approaches: automata-based, e.g. TaPAS [START_REF] Leroux | TaPAS: the Talence Presburger arithmetic suite[END_REF]; inside computer algebra systems, like with Redlog [DS97]; or in program analysis tools, like isl [START_REF] Verdoolaege | isl: An integer set library for the polyhedral model[END_REF], part of the Barvinok toolbox. Another solution would have been to retrieve "projected formulas" directly from SMT solvers for linear arithmetic, which often use quantifier elimination internally. Unfortunately, this feature is not available, even though some partial solutions have been proposed recently [BDHP]. All the exact methods that we tested have proved impractical in our case. This was to be expected. Quantifier elimination can be very complex, with an exponential time complexity in the worst case (for existential formulas as we target); it can generate very large formulas; and it is highly sensitive to the number of variables, when our problem often involves several hundreds and sometimes thousands of variables. Also, quantifier elimination often requires the use of a divisibility operator (also called stride format in [START_REF] Pugh | The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis[END_REF]), which is not part of the logic fragment that we target.

Another set of related works is concerned with polyhedral techniques [START_REF] Feautrier | Polyhedron Model[END_REF], used in program analysis. For instance, our approach obviously shares similarities with works that try to derive linear equalities between variables of a program [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], and polyhedral abstractions are very close in spirit to the notion of linear dependence between vectors of integers (markings in our case) computed in compiler optimizations. Another indication of this close relationship is the fact that isl, the numerical library that we use to compare our performances, was developed to support polyhedral compilation. We need to investigate this relationship further and see if our approach could find an application with program verification. From a more theoretical viewpoint, we are also looking into ways to improve the precision of our projection in the cases where we find non-polarized sets of constraints.

Figure 2 :

 2 Figure 2: Equations from our example in Fig. 1 and the associated TFG.

(

  RED) If X →• p and ↓p ∩ B = ∅ then (B , C ) → (B ′ , C ′ ) holds, where B ′ = B \ {p} and C ′ is the set of literals α ′ i obtained by normalizing the linear constraint α i {p ← x 1 + • • • + x k }.That is, we substitute p is enough to prove m |= E, we only need to check two properties: first that m ≡ E m ′ ( * ), then that m |= α for every literal α in C ( * * ).

Figure 3 :

 3 Figure 3: Random walk w/wo reductions.Figure4: k-induction w/wo reductions.

Figure 5 :

 5 Figure 5: Impact of projections on the challenging queries.

Figure 6 :

 6 Figure 6: TAPAAL w/wo polyhedral reductions.

Figure 7 :

 7 Figure 7: Redlog vs isl vs Fast elimination.

  Figure 1: An example of Petri net, M 1 (left), and one of its polyhedral abstractions, M 2 (right), with E ≜ (p 1 = p 4 +4096)∧(p 6 = p 0 +p 2 +p 3 +p 5 +p 7 )∧(a 1 = p 7 + p 8 ) ∧ (a 2 = a 1 + p 5 ). Colors are used to emphasize places that are either removed or added. at marking m when m ⩾ Pre(t). A marking m ′ is reachable from a marking m by firing transition t, denoted m

	p 0	p 1			p 0
	t 0	8192	t 1		8192	t 0	t 1
	p 2				p 3	p 2		p 3
		p 4					p 4
	t 2	4096	t 3	≡ E		t 2	4096	t 3
	p 5
	t 4	8192	p 6	t 5	p 7	t 4	a 2
	t 6
	1	p 8		t 7
	m; and (2)				t -→ m ′ , if: (1) transition t is enabled at

  an equation of E (condition (T3)) we obtain that m ′ ≡ E m and therefore also m |= E ( * ). We now prove that m |= C . The literals in C ′ are of the form ασ with σ the substitution {p ← x 1 + • • • + x k } and α in C . Remember that, with our notations (e.g. Equation (1) in page 3), we have m |= α if and only if α{m} SAT (is satisfiable). By hypothesis, m ′ |= ασ. Hence, ασ{m ′ } SAT, which is equivalent to α{m} SAT, and therefore m |= α ( * * ), as required.

It is Tedd, part of the Tina toolbox, which also uses polyhedral reductions.

with xi∈X x i in C , which is the meaning of the redundancy equation (constraint (T3) in Def. 5.1).

(AGP) If a •→ X with ↓X ∩ B = ∅, a ∈ B , and X polarized with respect to C . Then (B , C ) → (B ′ , C ′ ) holds, where B ′ = B \ X, and, by taking x j ∈ HLF X (C ), we define C ′ as the set of literals α ′ i obtained by normalizing the linear constraint α i {x l ← 0} l̸ =j {x j ← a}. That is, we eliminate the variables x l , different from x j , from C and replace x j with a; where x j is a variable of X that always have the highest coefficient in each literal (among the ones of X).

(AGD) If a •→ X with ↓X ∩ B = ∅, a ∈ B , and X is not polarized with respect to C . Then (B , C ) → (B ′ , C ′ ) holds, where B ′ = B \ X and C ′ is the set of literals α ′ i obtained by normalizing the linear constraint α i {x l ← 0} l̸ =j {x j ← a} such that α i (x j ) = min X α i . Meaning we eliminate the variables x l different from x j from α i and replace x j with a, where x j is a variable with the smallest coefficient in α i (among the ones of X). Note that the chosen variable x j is not necessarily the same in every literal of C .

Our goal is to preserve the semantics of formulas at each reduction step, in the sense of the relations ⊑ E and ≡ E . In the following, we use C to represent both a set of literals (α i ) i∈I and the cube formula i∈I α i . We can prove that the elimination steps corresponding to the redundancy (RED) and polarized agglomeration (AGP) cases preserve the semantics of the formula C . On the other hand, a non-polarized agglomeration step (AGD) may lose some markings.

Proof of the Algorithm. We prove the main result of the paper, namely that fast quantifier elimination preserves the integer solutions of a system when we only have polarized agglomerations. To this end, we need to prove two theorems. First, Theorem 5.1, which entails the soundness of one step of elimination. It also entails completeness for rules (RED) and (AGP). Second, we prove a progress property (Th. 5.4 below), which guarantees that we can apply elimination steps until we reach a set of literals C ′ with support on the reduced net N 2 .

We prove Th. 5.1 in two steps. We start by proving that elimination steps are sound, meaning that the integer solutions of C ′ are also solutions of C (upto E). Then we prove that elimination is also complete for rules (RED) and (AGP). In the following, we use C to represent both a set of literals (α i ) i∈I and the cube formula i∈I α i .

Proof. Take a valuation m ′ of N B ′ such that m ′ |= E ∧ C ′ . We want to show that there exists a marking m of N B such that m ≡ E m ′ satisfying E ∧ C .

We have three possible cases, corresponding to rule (RED), (AGP) or (AGD). In each case, we provide a marking m built from m ′ . Since m ≡ E m ′


Jessica Bainton
email: jessica.bainton@sickkids.ca--

Felicia Trachtenberg

Brian Mccrindle

Ke Wang

Richard Boruta

Cheryl Brosig

Erica D'andrea Egerson

Johanna Sood

Tammy Calderon

Doman

Jessica Bainton1

Felicia Trachtenberg2

Brian W Mccrindle1

Ke Wang2

Richard Boruta3

Cheryl L Brosig4

Andrea D'

Erica Egerson5

Johanna Sood6

Tammy Calderon7

Katrina Doman8

Amanda Golub9

Karen Graham10

Michelle Haas11

Bergen Hamstra12

Donna Lindauer13

Frances Sylvester14

Lisa Woodard15

Kathleen A Young-Borkowski16

Mussatto17

stress disorder in parents whose infants have single ventricle heart disease

Keywords: Norwood, CHD, post-traumatic stress disorder, parent, stress, coping

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Materials and methods:

A large longitudinal multi-centre cohort study evaluated 215 mothers and fathers for symptoms of post-traumatic stress disorder at three timepoints, including post-Norwood, post-Stage II, and a final study timepoint when the child reached approximately 16 months of age, using the self-report questionnaire Impact of Event Scale-Revised.

Results:

The prevalence of probable post-traumatic stress disorder post-Norwood surgery was 50% of mothers and 39% of fathers, decreasing to 27% of mothers and 24% of fathers by final follow-up. Intrusive symptoms such as flashbacks and nightmares and hyperarousal symptoms such as poor concentration, irritability, and sudden physical symptoms of racing heart and difficulty breathing were particularly elevated in parents. Higher levels of anxiety, reduced coping, and decreased satisfaction with parenting were significantly associated with symptoms of post-traumatic stress disorder in parents. Demographic and clinical variables such as parent education, pre-natal diagnosis, medical complications, and length of hospital stay(s) were not significantly associated with symptoms of post-traumatic stress disorder.

Discussion:

Parents whose infants underwent staged palliation for single ventricle heart disease often reported symptoms of post-traumatic stress disorder. Symptoms persisted over time and routine screening might help identify parents at-risk and prompt referral to appropriate supports.

Parents of infants with CHD have an elevated risk for mental health problems including anxiety disorders, depression, and post-traumatic stress disorder particularly in the weeks and months following heart surgery.1 For infants who undergo a staged surgical palliation for hypoplastic left heart syndrome and associated single ventricle anomalies, parents can experience a range of stressors that could be considered traumatic events. These stressors include receipt of the infant's diagnosis, complex open-heart surgeries, intensive care stays and long-term hospitalization, unexpected complications, and general uncertainty about the infant's survival and quality of life.2,3,4,5 Prevalence over time of post-traumatic stress disorder in mothers and fathers whose children have single ventricle heart disease and undergo multiple surgeries is not well described.

Post-traumatic stress disorder may develop in response to trauma.6 Criteria for diagnosis outlined in the Diagnostic and Statistical Manual of Mental Disorders include intrusive memories, avoidance, changes in physical and emotional reactions, and negative changes in thinking and mood.6 Symptoms must be present for at least 30 days and can include emotional numbing, difficulty concentrating, an altered sense of time and place, detachment from self and others, flashbacks, nightmares, difficulty sleeping, and sudden intense fear accompanied by distressing physical symptoms (e.g., racing heart, shortness of breath).6 A formal diagnosis involves a lengthy structured interview with a trained healthcare professional, but shorter self-report screening tools such as the Impact of Event Scale -Revised are frequently used to identify individuals with probable post-traumatic stress disorder.7

In the Family Adaptation study, an ancillary study to the Pediatric Heart Network Single Ventricle Reconstruction Trial,8 it was reported that parents' perception of their well-being was worse if parents experience increased symptoms of post-traumatic stress disorder.2 Therefore, we sought to further evaluate the prevalence of symptoms of post-traumatic stress disorder in both mothers and fathers of infants with critical CHD who underwent staged surgical palliation. We also investigated potential associations of demographic, clinical, stress, and coping variables with symptoms of post-traumatic stress disorder.

Materials and methods

Design of the study

The Family Adaptation study was ancillary to the multi-institutional Pediatric Heart Network Single Ventricle Reconstruction Trial, both previously described.2,8 The Family Adaptation study investigated parents' perceptions of family function, quality of life, and well-being after their infant underwent the Norwood procedure.2 The study theoretical framework was based on the Resiliency Model of Family Adaptation.9 Parents completed 13 self-reported questionnaires at three timepoints. The first assessment was post-Norwood surgery, at approximately 8 weeks of infant age. The second assessment was post-Stage II surgery, at approximately 6 months of infant age. The final follow-up assessment took place at a study visit at end of trial when the child was approximately 16 months of age.

Participants

Parents from 9 of the 15 Single Ventricle Reconstruction Trial (SVR) centres and parents from two additional centres, whose infants underwent staged surgical palliation for hypoplastic left or hypoplastic right heart syndrome, participated in the study. Both mothers and fathers of the same infant were eligible to participate. Parents not fluent in English were excluded. Parents whose infant died or required heart transplantation were excluded from participation, and parents were automatically withdrawn from the survey study if infant death or heart transplantation occurred during the study. Data obtained prior to infant death or heart transplantation were included in the analysis. Each centre's Institutional Review Board reviewed and approved the study. Parents provided informed consent to participate.

Measures

Questionnaires were organised into booklets and each participant was invited to complete one booklet per timepoint. Questionnaires took approximately 40minutes to complete. All questionnaires are described in detail in Supplementary Table S1.

The Impact of Event Scale -Revised was used to measure symptoms of post-traumatic stress disorder in parents.8 The 22-item self-report screening questionnaire corresponds to DSM-IV symptoms of post-traumatic stress disorder in 3 subdomains as follows: intrusion (e.g., symptoms include flashbacks, nightmares, difficulty sleeping); avoidance (e.g., symptoms include emotional numbing, altered sense of time and place, detached from self and others); and hyperarousal (e.g., symptoms include reduced concentration, irritability, and sudden onset of physical symptoms like a racing heart and trouble breathing). Data for this study were collected prior to the release of the DSM-V; however, screening tools based on DSM-IV are still widely used and reported. The questionnaire's psychometric properties have been previously established.10 Eight questions evaluated intrusion, eight evaluated avoidance, and six evaluated hyperarousal. Parents answered the questions with respect to their infant's diagnosis and ongoing clinical course. They rated each question on a 5-point Likert scale ranging from 0, "not at all" to 4, "extremely". The highest possible total score is 88, with subdomain highest scores of 32 for intrusion, 32 for avoidance, and 24 for hyperarousal. The total score provides a continuum of risk, including no risk (0-23), possible posttraumatic stress disorder [START_REF] Bradley | Low rates of PTSD in men attending childbirth: a preliminary study[END_REF][START_REF] Ayers | Symptoms of post-traumatic stress disorder in couples after birth: association with the couple's relationship and parentbaby bond[END_REF][START_REF] Aftyka | Post-traumatic stress disorder in parents of children hospitalized in the neonatal intensive care unit (NICU): medical and demographic risk factors[END_REF][START_REF] Aftyka | Risk factors for the development of post-traumatic stress disorder and coping strategies in mothers and fathers following infant hospitalization in the neonatal intensive care unit[END_REF][START_REF] Ionio | Premature birth: complexities and difficulties in building the mother-child relationship[END_REF][START_REF] Youngblut | Comparison of mothers and grandmothers physical and mental health and functioning within 6 months after child NICU/PICU death[END_REF][START_REF] Cacciatore | A parent's tears: primary results from the traumatic experiences and resiliency study[END_REF][START_REF] Helfricht | Surgery-related posttraumatic stress disorder in parents of children undergoing cardiopulmonary bypass surgery: a prospective cohort study[END_REF][START_REF] Helfricht | Psychometric evaluation and validation of the german version of the acute stress disorder scale across two distinct trauma populations[END_REF], and probable post-traumatic stress disorder (> 33).11,12,13 Seven additional questionnaires were used to address the study aims including: Family Information Form (demographic variables); Life Stress Inventory (total burden of stressful life events); 14 State-Trait Anxiety Index (measure of transient (state) and sustained (trait) anxiety); 15 Pediatric Inventory for Parents (level of stress and appraisal of stress in parents of child with serious or chronic disease); 16 Coping Health Inventory for Parents (measures family integration and social support of parents of child with serious or chronic disease); 9 Family Inventory of Resources for Management (measures resources that impact parent selfesteem, communication, financial well-being and social support); 9 and Inventory of Parent's Experiences (measures social support network and satisfaction with parenting).17 For stress questionnaires (2, 3, and 4), lower scores reflected lower stress and for coping questionnaires (5, 6, and 7) higher scores reflected better coping.

Statistical analysis

All analyses were conducted using SAS v9.4 (SAS Institute Inc., Cary, NC, United States of America), with p-values < 0.05 representing statistical significance. Change in post-traumatic stress disorder scores over time and comparison of mothers to fathers were assessed via repeated measures regression modelling on study timepoint (as a categorical variable) and parent (mother versus father). Multi-variable, backwards stepwise repeated measures regression was used to model the relationships between post-traumatic stress disorder symptoms and other variables of interest, separated into demographic and clinical variables and stress and coping variables. Data from both parents were included when available, specifying infant as a repeated variable within the mixed model regression. All data from the same infant over time were correlated (compound symmetric variance structure). All variables with a p-value < 0.2 in bivariable modelling were included in the initial multi-variable model, and backwards selection performed. The State-Trait Anxiety state anxiety scores were included in bivariable modelling but not included in multi-variable modelling. The State-Trait Anxiety trait anxiety scores were included in both bivariable and multi-variable modelling.

Prior to model building, independent variables were investigated for substantial associations, defined as an absolute Pearson correlation > 0.5 for continuous variables, p < 0.05 on Pearson chi-square test for categorical variables, or p < 0.05 on ANOVA for the association between a continuous and a categorical variable. No substantial associations were found among the demographic and clinical variables for the total score; a small number were found for subdomains and the variable more significantly associated with outcome on bivariable modelling was chosen to proceed to multi-variable modelling, as noted in table footnotes. Some stress and coping variables had strong correlations (Supplementary Table S8), but all except trait anxiety scores were included in multi-variable modelling as these variables are designed to measure different concepts in our conceptual framework.9 After arriving at multivariable models for demographic/clinical variables and stress/coping variables separately, but including effects of parent and timepoint in both, all significant variables were included together in a final backwards stepwise repeated measures regression analysis to arrive at the final, combined parsimonious model. The R2 for models (typically defined as the amount of variance in outcome explained) was calculated for these repeated measures models using the method of Jaeger et al. [START_REF] Jaeger | An R2 statistic for fixed effects in the generalized linear mixed model[END_REF]

Results

Participant demographic information

Participants included 215 parents (143 mothers and 72 fathers) representing 146 infants (Fig 1). Demographic characteristics of parent and infants are presented in Table 1. Most infants (92%) had hypoplastic left heart syndrome, with 8% having hypoplastic right heart syndrome. Infants underwent staged surgical palliation with first surgery being the Norwood procedure in all cases. Most infants (73%) were diagnosed with CHD pre-natally. Ten percent of infants had a genetic syndrome, while 23% of infants had a nonsyndromic abnormality.

Complete Impact of Event Scale -Revised data were available for 133 parents of infants post-Norwood, 107 parents post-Stage II, and 76 parents at final follow-up (Fig 1). For the participants also in SVR, timepoint 1 occurred 53 ± 113 days after Norwood surgery, timepoint 2 occurred 56 ± 129 days after Stage II surgery or before Stage II (n = 3), and timepoint 3 occurred 348 ± 168 days after Stage II surgery. Fourteen parents at timepoint 3 representing nine children completed assessments 2-29 days after their child's Fontan procedure. Children post-Fontan procedure were 20-32 months old versus the average age of 16 months old at final follow-up. The number of participants who became ineligible over the course of the study due to infant death or heart transplantation was 22 parents. Data obtained prior to infant death or heart transplantation were included in the analysis.

Impact of Event Scale -Revised scores over time in mothers and fathers

Total parent scores on the Impact of Event Scale -Revised were highest post-Norwood and lowest at final follow-up, for both mothers and fathers (Fig 2 ; p < 0.001 for time). Each of the three subdomain scores also decreased over time (p = 0.009 for time for intrusion, p = 0.03 for time for avoidance, p < 0.001 for time for hyperarousal). Total scores were significantly lower for fathers compared to mothers across all timepoints (p < 0.001 for parent; no significant interaction with time).

Median Impact of Event Scale -Revised total scores for mothers were 33 (IQR 21, 45) post-Norwood, 31 (IQR 18, 41) post-Stage II, and 22 (IQR 18, 41) at final follow-up, while median scores for fathers were 23 (IQR 14, 37) post-Norwood, 26 post-Stage II (IQR 11,[START_REF] Shalev | stress disorder. N Engl J Med Marmar CPost-traumatic. Post-Traumatic stress disorder[END_REF], and 20 (IQR 11, 31) at final follow-up. Subdomain scores for intrusion were significantly lower for fathers than for mothers (p < 0.001 for parent) with a decrease over time only in mothers (p = 0.006 for the interaction). No difference between mothers and fathers was observed in the avoidance subdomain (p = 0.57 for parent), but fathers reported fewer hyperarousal symptoms compared to mothers (p < 0.001 for parent).

Prevalence of post-traumatic stress disorder in parents

The prevalence of probable post-traumatic stress disorder (total Impact of Event Scale -Revised > 33) was higher in mothers compared to fathers and decreased over time for both (Fig 3). The prevalence of probable post-traumatic stress disorder in mothers was 50% post-Norwood, 47% post-Stage II, and 27% at final follow-up, compared to 39%, 36%, and 24% of fathers, respectively. The percentage of mothers with possible post-traumatic stress disorder (total Impact of Event Scale -Revised score of 24-32) was 19% post-Norwood, 16% post-Stage II, and 19% at final follow-up, compared to 11%, 17% and 14% of fathers, respectively. There were only 28 parents (20 mothers, 8 fathers) who participated at all three timepoints. Of these 28 parents, 25% had probable post-traumatic stress disorder at all three timepoints (5 mothers, 2 fathers), another 14% had possible post-traumatic stress disorder at all three timepoints (2 mothers, 2 fathers), and 29% had no risk for post-traumatic stress disorder at all three timepoints (5 mothers, 3 fathers). The sample size was too small for statistical testing and data are not reported for parents whose scores changed over time.

Factors associated with symptoms of post-traumatic stress disorder: Bivariable modelling

In the bivariable modelling, the only demographic variable significantly associated with symptoms of post-traumatic stress disorder was parent age (Table 2), with older parents reporting less symptoms of post-traumatic stress disorder (p = 0.04, R2 = 0.02). Stress variables had much stronger associations with symptoms of post-traumatic stress disorder compared to demographic variables (Table 2, Supplementary Tables S2-S4) and had higher R2 (up to 0.52 for the total Impact of Event Scale -Revised score). Higher scores of stress variables (indicating increased stress and anxiety) in the Inventory of Life Changes, State-Trait Anxiety Index, or Pediatric Inventory for Parents were significantly associated with symptoms of post-traumatic stress disorder, while lower scores of coping variables (indicating reduced coping and social support) in the Inventory of Parents Experiences or Family Inventory of Resources for Management were significantly associated with symptoms of posttraumatic stress disorder.

Factors associated with symptoms of post-traumatic stress disorder: Multi-variable modelling

In the multi-variable modelling, mothers (versus fathers) and earlier study timepoints (post-Norwood and post-Stage II) were significantly associated with more symptoms of posttraumatic stress disorder and more strongly associated with post-traumatic stress disorder than any of the demographic or clinical variables (Table 3, Supplementary Tables S5 andS7, R2 = 0.16-0.20). An increased number of complications during the interstage period was the only demographic variable significantly associated with increased symptoms of avoidance (R2 = 0.07) (Supplementary Table S6).

Stress variables were significantly associated with symptoms of post-traumatic stress disorder both the total and subdomain Impact of Event Scale -Revised scores. In the multi-variable modelling, higher scores in the trait anxiety score of the State-Trait Anxiety Index indicating one's tendency towards becoming anxious along with higher scores in the Pediatric Inventory for Parents indicating more frequent and more difficulty with events parents of children with serious illness experience were both significantly associated variables of symptoms of posttraumatic stress disorder (total Impact of Event Scale -Revised score, R2 = 0.65). Higher scores in state anxiety scores of the State-Trait Anxiety Index indicating transient situational anxiety bring the proportion of variance to 71% (data not shown, total Impact of Event Scale -Revised score, R2 to 0.71). Trait anxiety scores versus state anxiety scores were included in the final model because trait anxiety scores are less subject to fluctuation with change in number and degree of stressful circumstances and trait anxiety scores are strongly correlated with state anxiety scores (Supplementary Table S8). Higher scores on stress scales indicating more stress and anxiety were also significantly associated variables for increased symptoms of intrusion, avoidance, and hyperarousal (Supplementary Tables S5-S7).

Coping variables were significantly associated with symptoms of avoidance and hyperarousal. Lower scores on the Family Inventory of Resources for Management, which indicated less resources to support parent self-esteem, communication, financial well-being, and social support, were significantly associated with increased symptoms of avoidance (Supplementary Table S6). Lower scores on the Inventory of Parent Experiences, signalling less social support, and reduced satisfaction with parenting were significantly associated variables for increased symptoms of hyperarousal (Supplementary Table S7).

Discussion

Symptoms of post-traumatic stress disorder are prevalent and persistent in both mothers and fathers of infants with single ventricle CHD after surgical palliation. Symptoms of posttraumatic stress disorder (total Impact of Event Scale -Revised score) are significantly associated with increased parent anxiety as well as the frequency and parent's appraisal of the degree of difficulty of events they face while caring for a child with serious illness. Reduced coping and decreased satisfaction with parenting were significantly associated with two of the subdomains (avoidance and hyperarousal) of symptoms of post-traumatic stress.

In this study, as many as 50% of mothers and 39% of fathersmet the criteria for probable posttraumatic stress disorder. This is considerably higher than prevalence seen in the general population, wherein the lifetime prevalence is 8% and the 12-month prevalence is 4%. [START_REF] Bromet | Trauma and posttraumatic stress disorder: Global perspectives from the WHO World Mental Health Surveys[END_REF] The disorder is associated with younger age, female gender, unemployment, single marital status, lower education, and reduced income in the general population.6,19 The prevalence of posttraumatic stress disorder in healthy post-partum mothers, with no pre-existing mental health conditions, is 5%-13%.20,21,22,23 Symptoms steadily decline around 6 weeks postpartum in healthy mothers.20 Data on post-traumatic stress disorder in healthy fathers in the postpartum period are very limited although one report found no significant symptoms across the three subdomains while another reported 5% of fathers had symptoms of post-traumatic stress disorder.24,25 Higher prevalence (19-24% of mothers and 13% of fathers) of post-traumatic stress disorder is observed in parents of preterm infants and infants with fetal abnormality. [START_REF] Aftyka | Post-traumatic stress disorder in parents of children hospitalized in the neonatal intensive care unit (NICU): medical and demographic risk factors[END_REF][START_REF] Aftyka | Risk factors for the development of post-traumatic stress disorder and coping strategies in mothers and fathers following infant hospitalization in the neonatal intensive care unit[END_REF][START_REF] Ionio | Premature birth: complexities and difficulties in building the mother-child relationship[END_REF] The prevalence of post-traumatic stress disorder in parents of children with single ventricle CHD post-Norwood and post-Stage II palliation is comparable to that seen in bereaved mothers (42-69% of bereaved mothers). [START_REF] Youngblut | Comparison of mothers and grandmothers physical and mental health and functioning within 6 months after child NICU/PICU death[END_REF][START_REF] Cacciatore | A parent's tears: primary results from the traumatic experiences and resiliency study[END_REF] Of parents of children who require bypass surgery for mild to severe CHD, 25% of parents met criteria for post-traumatic stress disorder 1-month post-surgery and 15% of mothers and 10% of fathers still met criteria for post-traumatic stress disorder at 6 months postsurgery.31,32 Data on parents further out from their child's surgery are lacking, but in a single centre study with 29 parents (16 mothers, 13 fathers) of children with hypoplastic left heart syndrome who were interviewed one time when their child was age 1-18 years old, 88% of mothers interviewed had symptoms of post-traumatic stress disorder and 66% of fathers had symptoms of post-traumatic stress disorder.3,33,34 It is not clear if parent's symptoms of post-traumatic stress disorder fully resolve or whether post-traumatic stress disorder symptoms remain prevalent months to years after their child's surgery for single ventricle CHD. Continued research is needed.

Post-traumatic stress disorder has a high level of comorbidity with other mood disorders, anxiety disorders, disruptive behaviour disorders, chronic physical conditions, and addictions.6,35 Poorer parent mental health including higher parent stress and anxiety has been found to be associated with poorer neurodevelopmental outcomes in children with CHD.36 Parental post-traumatic stress symptoms severity is associated with overprotective parenting as well as emotional and behavioural problems in children who have CHD.5 Parental post-traumatic stress is also associated with an increase in unplanned hospital visits in the first few months of their infant's life.37 Family-based psychosocial interventions that empower parents as caregivers and advocates for their children with CHD could reduce the impact of parent mental health problems and improve child outcomes.38,39,40 Effective treatments provided early on for post-traumatic stress disorder such as cognitive-behavioural therapy have been tested in many settings showing effective results. [START_REF] Sijbrandij | Treatment of acute posttraumatic stress disorder with brief cognitive behavioral therapy: a randomized controlled trial[END_REF] Our results demonstrate that mothers and fathers could benefit from early identification through screening for anxiety during hospitalization with continued monitoring for development of symptoms of post-traumatic stress especially symptoms that persist longer than 30 days after cardiac surgery as persistence of symptoms is part of criteria for diagnosis.

It is important to consider the reality that single ventricle CHD carries the highest morbidity of any form of CHD with a significant risk of death or heart transplantation.42 All single ventricle CHD children require additional cardiac surgeries, catheter procedures, and a significant number will have complications including pacemaker placement, thrombotic events, stroke, seizure, protein-losing enteropathy, and plastic bronchitis. [START_REF] Newburger | Transplant-free survival and interventions at 6 years in the SVR trial[END_REF] Complications can occur at any point in the child's life and their parents likely repeatedly experience trauma over time as their child requires further palliation that necessitates intensive care support, lengthy hospitalizations, and uncertain futures.42 Screening for symptoms of posttraumatic stress disorder should be on-going pre-operatively through hospitalization and again postoperatively. Early identification, appropriate resource allocation to those parents who are deemed at-risk, empathic communication, and consistency in care could help support parents.2,4,43

Our study showed that demographic and clinical (medical or surgical) factors such as prenatal diagnosis, complications, and length of hospital stay did not identify which parents were at greater risk to develop post-traumatic stress disorder symptoms, a finding supported by other studies.44,45 Measures of anxiety have been associated with elevated post-traumatic stress disorder symptoms in parents of children with CHD.45,46 Like our findings, Turgoose et al. did not find significant demographic or clinical factors that predict post-traumatic stress disorder in parents of children with CHD (any type) undergoing bypass. [START_REF] Turgoose | Prevalence of traumatic psychological stress reactions in children and parents following paediatric surgery: a systematic review and metaanalysis[END_REF] Parents need support and education to help them adapt to the stress and challenge of raising a child with critical CHD.47,48 Healthcare professionals are in a unique position to have a positive influence on how parents adapt to stressors by recognising symptoms in parents and referring parents to appropriate resources.

Study participant withdrawal was a limitation of this study which prevented analysis of paired parent dyads. There were too few parents with longitudinal data to address the question of change in probable post-traumatic stress disorder between timepoints per parent. The most common reason for participant withdrawal from the study was parent stress. Parents who were struggling the most may not have participated at some timepoints or may never have consented at all. It is also a possibility that survey fatigue due to the time commitment required to complete the questionnaires contributed to attrition rates. The Family Adaptation study was designed to capture the elements of a complex psychosocial process and surveys were selected based on the framework of stress appraisal, coping, and adaptation; however, all surveys contributed to the framework and allowed thorough analysis of findings. This study relied on self-report measures and the Impact of Event Scale -Revised is a screening tool versus formal diagnostic tool for post-traumatic stress disorder. The high prevalence of probable post-traumatic syndrome disorder on screening does suggest that future studies should consider a formal diagnosis through clinical standard diagnostic interview to better understand the true prevalence in this vulnerable parent population. Attention to parent mental health and overall well-being during uncertain and stressful times is important. These results suggest more help is needed for parents, and screening and intervention might be beneficial.

Acknowledgements.

We would like to acknowledge the NIH/NHLBI Pediatric Heart Network Family Adaptation parent participants for all data in this manuscript.

Financial support.

This study was supported by grants (HL135680, HL135685, HL135683, HL135689, HL135646, HL135665, HL135678, HL135682, HL135666, HL135691, HL068270) from the NHLBI, NIH. The authors are solely responsible for the design and conduct of this study, all study analyses, the drafting and editing of the paper, and its final contents. The views expressed in this manuscript are those of the authors and do not necessarily represent the views of the National Heart, Lung, and Blood Institute; the National Institutes of Health; or the U.S. Department of Health and Human Services.

Conflicts of interest.

None.

Ethical standards.

The authors assert that all procedures contributing to this work comply with the ethical standards of the relevant national guidelines on human experimentation Department of Health and Human Services Code of Federal Regulations (45 CFR 46)