Mamadou Moustapha Kanté
email: mamadou.kante@isima.fr

Eun Jung Kim

O-Joung Kwon
email: ojoungkwon@gmail.com

Christophe Paul
email: christophe.paul@lirmm.fr

© Mamadou

Moustapha Kanté

An FPT Algorithm and a Polynomial Kernel for Linear Rankwidth-1 Vertex Deletion

Keywords: 1998 ACM Subject Classification F.2.2 Computation on Discrete Structures, G.2.1 Combinatorics Algorithms, G.2.2 Graph Agorithms Keywords and phrases (linear) rankwidth, distance-hereditary graphs, thread graphs, parameterized complexity, kernelization Digital Object Identifier 10.4230/LIPIcs.IPEC.2015

Linear rankwidth is a linearized variant of rankwidth, introduced by Oum and Seymour [Approximating clique-width and branch-width. J. Combin. Theory Ser. B, 96(4):514-528, 2006.], and it is similar to pathwidth, which is the linearized variant of treewidth. Motivated from the results on graph modification problems into graphs of bounded treewidth or pathwidth, we investigate a graph modification problem into the class of graphs having linear rankwidth at most one, called the Linear Rankwidth-1 Vertex Deletion (shortly, LRW1-Vertex Deletion). In this problem, given an n-vertex graph G and a positive integer k, we want to decide whether there is a set of at most k vertices whose removal turns G into a graph of linear rankwidth at most one and if one exists, find such a vertex set. While the meta-theorem of Courcelle, Makowsky, and Rotics implies that LRW1-Vertex Deletion can be solved in time f (k) • n 3 for some function f , it is not clear whether this problem allows a runtime with a modest exponential function. We establish that LRW1-Vertex Deletion can be solved in time 8 k • n O(1) . The major obstacle to this end is how to handle a long induced cycle as an obstruction. To fix this issue, we define the necklace graphs and investigate their structural properties. We also show that the LRW1-Vertex Deletion has a polynomial kernel.

Introduction

In a parameterized problem, we are given an instance (x, k), where k is a secondary measurement, called as the parameter. The central question in parameterized complexity is whether a parameterized problem admits an algorithm with runtime f (k) • |x| O (1) , equivalently an FPT algorithm, where f is a function depending on the parameter k alone, and |x| is the input size. As we study a parameterized problem when its unparameterized decision version is NP-hard, the function f is super-polynomial in general. A parameterized problem admitting such an algorithm is said to be fixed-parameter tractable, or FPT in short. For many natural parameterized problems, the function f is overwhelming [START_REF] Frick | The complexity of first-order and monadic second-order logic revisited[END_REF] or even non-explicit [START_REF] Robertson | Graph minors. XX. Wagner's conjecture[END_REF], especially when the algorithm is indicated by a meta-theorem. Therefore, a lot of research effort focus on designing an FPT algorithm with affordable super-exponential part in the runtime. We are especially interested in solving a parameterized problem in single-exponential time, that is, in time c k • n O (1) for some constant c.

A powerful technique to handle parameterized problems is the kernelization algorithm. A kernelization algorithm takes an instance (x, k) and outputs an instance (x , k ) in time polynomial in |x| + k satisfying that (1) (x, k) is a Yes-instance if and only if (x , k ) is a Yes-instance, (2) k ≤ k, and |x | ≤ g(k) for some function g. The reduced instance is called a kernel and the function g is called the size of the kernel. A parameterized problem is said to admit a polynomial kernel if there is a kernelization algorithm that reduces the input instance into an instance with size bounded by a polynomial function g(k) in k.

Many natural graph problems can be expressed as a graph modification problem. Generally, given an input graph G and a fixed set O of elementary operations and a graph property Π, the objective is to transform G into a graph H ∈ Π by applying at most k operations from O. Vertex deletion, edge deletion/addition or contraction are examples of such elementary operations.

The graph property Π having treewidth or pathwidth at most w has received in-depth attention as many problems become tractable on graphs of small treewidth. The celebrated Courcelle's theorem [START_REF] Courcelle | The Monadic Second-Order Theory of Graphs. I. Recognizable Sets of Finite graphs[END_REF] implies that every graph property expressible in monadic second order logic of the second type (MSO 2 ) can be verified in time f (w) • n, when the input n-vertex graph has treewidth at most w. Furthermore, having small treewidth frequently facilitates the design of a dynamic programming algorithm whose runtime is much faster than that of the all-round algorithm from the Courcelle's meta-theorem. Therefore, it is reasonable to measure how close an instance is from "an island of tractability within an ocean of intractable problems" [START_REF] Gaspers | The Multivariate Algorithmic Revolution and Beyond -Essays Dedicated to Michael R. Fellows on the Occasion of His 60th Birthday[END_REF].

In the context of treewidth, the deletion problems for the special cases of w = 0 and w = 1 correspond to the well-known Vertex Cover and Feedback Vertex Set problems respectively. More generally, for any fixed w, the corresponding graph modification problem Treewidth-w Vertex Deletion can be solved in time f (w, k) • n implied by Graph Minor Theory [START_REF] Robertson | Graph minors. XX. Wagner's conjecture[END_REF] and Courcelle's meta-theorem [START_REF] Courcelle | The Monadic Second-Order Theory of Graphs. I. Recognizable Sets of Finite graphs[END_REF]. As the function f subsumed in the meta theorem is gigantic, it is natural to ask whether the exponential function in the runtime can be rendered realistic. Recent endeavor pursuing this question culminated in establishing that for any fixed w, the Treewidth-w Vertex Deletion is single-exponential fixed parameter tractable with the deletion number k as the parameter [START_REF] Fedor | Planar f-deletion: Approximation, kernelization and optimal FPT algorithms[END_REF][START_REF] Jung | Linear kernels and single-exponential algorithms via protrusion decompositions[END_REF].

As for pathwidth, Pathwidth-1 Vertex Deletion was first studied by Philip, Raman, Villanger [START_REF] Philip | A quartic kernel for pathwidth-one vertex deletion[END_REF], and later Cygan, Pilipczuk, Pilipczuk, Wojtaszczyk [START_REF] Cygan | An improved fpt algorithm and a quadratic kernel for pathwidth one vertex deletion[END_REF] showed that Pathwidth-1 Vertex Deletion can be solved in time 4.65 k • n O (1) and it admits a quadratic kernel. Using the general method developed for Treewidth-w Vertex Deletion [START_REF] Fedor | Planar f-deletion: Approximation, kernelization and optimal FPT algorithms[END_REF][START_REF] Jung | Linear kernels and single-exponential algorithms via protrusion decompositions[END_REF], the Pathwidth-w Vertex Deletion problem admits a single exponential FPT algorithm.

Linear rankwidth.

Rankwidth was introduced by Oum and Seymour [START_REF] Oum | Approximating clique-width and branch-width[END_REF] for efficiently approximating clique-width. Linear rankwidth is a linearized variation of rankwidth like

I P E C ' 1 5
Parameterized Complexity of Linear Rankwidth-1 Vertex Deletion pathwidth is the linearized variant of treewidth. While treewidth and pathwidth are small only on sparse graphs, dense graphs may have small rankwidth or linear rankwidth. For instance, complete graphs, complete bipartite graphs, and threshold graphs [START_REF] Chvátal | Studies in integer programming, chapter Aggregation of inequalities in integer programming[END_REF] have linear rankwidth at most one even though all of them have unbounded treewidth. Rankwidth and linear rankwidth have been intensively studied to generalize the known results for treewidth and pathwidth [START_REF] Adler | Linear rank-width of distance-hereditary graphs[END_REF][START_REF] Courcelle | Graph operations characterizing rankwidth[END_REF][START_REF] Ganian | On parse trees and myhill-nerode-type tools for handling graphs of bounded rank-width[END_REF][START_REF] Oum | Rank-width and vertex-minors[END_REF][START_REF] Oum | Approximating clique-width and branch-width[END_REF].

Ganian [START_REF] Ganian | Thread graphs, linear rank-width and their algorithmic applications[END_REF] pointed out that some NP-hard problems, such as computing pathwidth, can be solved in polynomial time on graphs of linear rankwidth at most 1. Generally, the meta-theorem by Courcelle, Makowsky, Rotics [START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF] states that for every graph property Π expressible in monadic second order logic of the first type (MSO 1 ) and fixed k, there is a cubic-time algorithm for testing whether a graph of rankwidth at most k has property Π. As rankwidth is always less than or equal to linear rankwidth, those problems are tractable on graphs of bounded linear rankwidth as well.

In the same context, it is natural to ask whether there is an FPT algorithm for (Linear) Rankwidth-w Vertex Deletion, that is, a problem asking whether for a given graph G and a positive integer k, G contains a vertex subset of size at most k whose deletion makes G a graph of (linear) rankwidth at most w. It is only known that for fixed w, both problems are FPT from the meta-theorem on graphs of bounded rankwidth [START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF] and the fact that one vertex deletion can decrease rankwidth or linear rankwidth by at most one. We discuss it in more detail in the last section. However, as the function of k obtained from the meta-theorem is enormous, it is interesting to know whether there is a single-exponential FPT algorithm for both problems, like Treewidth-w Vertex Deletion. Also, to the best of our knowledge, there was no known previous result whether (Linear) Rankwidth-w Vertex Deletion admits a polynomial kernel for any integer w.

Our contributions. In this paper, we show that the Linear Rankwidth-1 Vertex Deletion problem admits a single-exponential FPT algorithm and a polynomial kernel. This is a first step towards a goal of investigating whether (Linear) Rankwidth-w Vertex Deletion is single-exponential FPT or has a polynomial kernel. We note that several graph classes with a certain path-like structure have been studied for parameterized vertex deleting problems. Such classes include graphs of pathwidth 1, proper interval graphs [START_REF] Fedor | A polynomial kernel for proper interval vertex deletion[END_REF]25], unit interval graphs [24,[START_REF] Cao | Unit interval editing is fixed-parameter tractable[END_REF], and interval graphs [START_REF] Cao | Interval deletion is fixed-parameter tractable[END_REF]. A common approach in the previous work is to use the characterization of the structures obtained after removing small obstructions. We also characterize graphs excluding small obstructions for graphs of linear rankwidth at most 1 to develop an FPT algorithm and a polynomial kernel.

The main ingredient is to investigate a new class of graphs, called necklace graphs, which are close to graphs of linear rankwidth at most 1. To define this class, we use the induced subgraph obstructions for graphs of linear rankwidth at most 1, which are listed in Figures 1

house gem domino hole 1 Figure 1
The induced subgraph obstructions for distance-hereditary graphs.

α 1 α 2 α 3 α 4 α 5 α 6 β 1 β 2 β 3 β 4 γ 1 γ 2 γ 3 γ 4 1 Figure 2
The distance-hereditary induced subgraph obstructions for thread graphs.

and 2 [START_REF] Adler | Obstructions for linear rankwidth at most 1[END_REF]. Briefly speaking, necklace graphs, when viewed locally, are graphs of linear rankwidth at most 1, but they may have a long induced cycle. We show that every connected graph having no obstructions of size at most 8 is a necklace graph, and we can easily find a minimum deleting set on a connected necklace graph. In our FPT algorithm, we first use a simple branching algorithm to remove the obstructions of size at most 8 with the time complexity 8 k • n O (1) . Since a final instance does not have obstructions of size at most 8, it is a disjoint union of thread graph and necklace graphs, and we compare the remaining budget with the sum of minimum deleting set over all necklace components to decide whether it is a Yes-instance.

To obtain a polynomial kernel, we start with packing obstructions of size at most 8 using the Sunflower lemma, and taking a minimum deleting set on the remaining necklace graph. The union of two sets will have size bounded by a polynomial in k, and its removal makes an input graph into a graph of linear rankwidth at most 1. Graphs of linear rankwidth at most 1 can be seen as graphs obtained by connecting certain blocks, called thread blocks, like a path (Theorem 2.1). The main difficulty for reducing the remaining part is to shrink a large thread block. Even though there is a simple pattern of constructions on thread blocks, it is not at all obvious how to find an irrelevant vertex in a sufficiently large thread block regarding all individual small obstructions. We can resolve this issue using the set obtained by the Sunflower lemma, which has the nice property that any minimum deleting set for the small obstructions in G is contained in the prescribed set. Using this, we will show how to find another obstruction from the long induced cycle containing a potential irrelevant vertex. We remark that a similar idea was used by Fomin, Saurabh, and Villanger [START_REF] Fedor | A polynomial kernel for proper interval vertex deletion[END_REF] to obtain a polynomial kernel for the Proper Interval Vertex Deletion problem.

Preliminaries

In this paper, all graphs are finite and undirected, if not mentioned otherwise. For a graph G, we denote by V (G) and E(G) the vertex set and the edge set of G, respectively, if they are not specified. Let G = (V, E) be a graph. Let N G (x) denote the neighborhood of a vertex x ∈ V . For S ⊆ V , G[S] denotes the subgraph of G induced on S and we denote by

G \ S := G[V \ S]. For W ⊆ E, we denote by G \ W := (V, E \ W ). For short we write G \ x instead of G \ {x} for x ∈ V ∪ E. A vertex v of G is called a pendant vertex if |N G (x)| = 1.
An edge e of a connected graph G is called a cut-edge if G \ e is disconnected. The length of a path is defined as the number of edges in the path. For n ≥ 3, we denote by C n the cycle with n vertices. For a set F of graphs, a graph G is F-free if G has no induced subgraph isomorphic to a graph in F.

A (linear) ordering on a finite set S is a bijective mapping σ : S → {1, . . . , |S|}, and we write x < σ y if σ(x) < σ(y), and σ -1 as the inverse bijective mapping. For an X × Y -matrix M and X ⊆ X, Y ⊆ Y , let M [X , Y ] be the submatrix of M whose rows and columns are indexed by X and Y , respectively.

Linear rankwidth and thread graphs. The adjacency matrix of a graph G = (V, E), which is a (0, 1)-matrix over the binary field, will be denoted by A G . The width of a linear ordering

σ of V in G is max 1≤i≤|V | rank(A G [{σ -1 (1), . . . , σ -1 (i)}, V \ {σ -1 (1), . . . , σ -1 (i)}])
, where the rank is computed over the binary field. The linear rankwidth of a graph G is defined as the minimum width over all linear orderings of V .

Graphs of linear rankwidth at most one are called thread graphs by Ganian [START_REF] Ganian | Thread graphs, linear rank-width and their algorithmic applications[END_REF], and each connected thread graph consists of a sequence of thread blocks. We follow the definition of thread blocks given by Adler, Farley, and Proskurowski [START_REF] Adler | Obstructions for linear rankwidth at most 1[END_REF], and develop a more convenient way to create a thread graph, which is useful to define necklace graphs.

A triple B(x, y) = (G, σ, ), where x and y are two vertices of the graph G = (V, E), σ is a ordering on V , and is a function from V to {{L}, {R}, {L, R}}, is a thread block if:

1. (x) = {R} and (y) = {L}, 2. for v, w ∈ V with v < σ w, vw ∈ E(G) if and only if R ∈ (v) and L ∈ (w), 3. (σ -1 (2)) = {L} if σ -1 (2) = y.
See Figure 3 for an example. The aim of the third condition is to guarantee a unique decomposition of thread graphs into thread blocks. For a digraph D = (V D , A D ), a set of thread blocks {B(x, y) = (G xy , σ xy , xy ) | xy ∈ A D } is said to be mergeable with D if for any two arcs A connected graph G is a thread graph if G is an one vertex graph or G = P B P for some directed path P , called the underlying path, and some set of thread blocks B P mergeable with P . A graph is a thread graph if each of its connected components is a thread graph.

x 1 y 1 , x 2 y 2 of A D , V (G x1y1 ) ∩ V (G x2y2 ) = {x 1 , y 1 } ∩ {x 2 , y 2 }.
The induced subgraph obstructions for graphs of linear rankwidth at most 1 consist of the set of induced subgraph obstructions for graphs of rankwidth at most 1 (equivalently, distance-hereditary graphs) [START_REF] Bandelt | Distance-hereditary graphs[END_REF], which are a house, a gem, a domino, and induced cycles of length at least 5 in Figure 1, and the set of 14 induced subgraph obstructions for linear rankwidth at most 1 that are graphs of rankwidth 1, depicted in Figure 2. For convenience, we define that Ω U is the set of 14 graphs in Figure 2, It is known that one can recognize a graph of linear rankwidth 1 in polynomial time using split decompositions of graphs [START_REF] Bui-Xuan | A note on graphs of linear rank-width 1[END_REF][START_REF] Adler | Linear rank-width of distance-hereditary graphs[END_REF], and easily decompose a connected thread graph into thread blocks.

Ω T := {house, gem, domino} ∪ {C k | k ≥ 5} ∪ Ω U ,

Theorem 2.2 ([4, 2]

). Let G be a graph on with n vertices and m edges. Then in time O(n + m), we can test whether G is a thread graph, and if G is a thread graph, then we can decompose each connected component into a sequence of thread blocks in the same time.

In the remaining part, we frequently use the term 'thread graphs' for graphs of linear rankwidth at most 1. For a graph G and S ⊆ V , S is called a LRW1-deletion set if G \ S is a thread graph.

Necklace graphs. We generalize the construction of thread graphs from directed paths to directed cycles. A connected graph G is called a necklace graph if G = C B C for some directed cycle C, called the underlying cycle, and some set of thread blocks B C mergeable with C. Our FPT algorithm and the construction of a polynomial kernel relies on the following characterization of Ω N -free graphs.

Theorem 2.3. A connected Ω N -free graph is either a connected thread graph or a necklace graph whose underlying cycle has length at least 9.

Let us sketch the proof of Theorem 2.3, which constructs the underlying cycle and a set of thread blocks as follows. Let G = (V, E) be a connected Ω N -free graph and suppose that G is not a thread graph. Since G is Ω N -free and it is not a thread graph, by Theorem 2.1, G has an induced subgraph isomorphic to C k for some k ≥ 9. We prove by induction on |V | that if C is a shortest cycle among induced cycles of length at least 9 in G, then G is a necklace graph whose underlying cycle is C.

Let C := v 1 v 2 • • • v k v 1

3

An FPT algorithm for LRW1-Vertex Deletion

Our FPT algorithm is a branching algorithm that reduces an input instance to a Ω N -free graph. As each graph of Ω N has size at most 8, the announced complexity follows. It remains to prove that given a Ω N -free graph, a minimum vertex deletion set for LRW1-Vertex Deletion can be found in polynomial time. In fact, we prove that such a set has size at most one per necklace component and identifying such a vertex requires polynomial time.

Using the following proposition, we can find a minimum LRW1-deletion set of a Ω N -free graph in polynomial time. To prove it, we use the following lemma.

Lemma 3.2. Let G be a connected necklace graph with the underlying cycle

C of length at least 4. For each v ∈ V (C), G \ v is a thread graph.
Proof of Proposition 3.1. Let k be the minimum size of a LRW1-deletion set of G. We remark that each connected component of G is either a thread graph or a necklace graph by Theorem 2.3. For each component H of G, we test whether H is a thread graph or not in time O(|V (H)| + |E(H)|) using Theorem 2.2. Note that we should remove at least one vertex for each necklace component of G, and moreover, by Lemma 3.2, it is enough to remove exactly one vertex for each component. Thus, k is the number of its necklace components.

To identify such a vertex in each necklace component, it is sufficient to find a vertex on the underlying cycle by Lemma 3.2. Let H be a necklace component and C be the underlying cycle of H. Observe that for v ∈ V (H) \ V (C), H \ v is still a connected necklace graph with the same underlying cycle, because we can adjust the ordering of the thread block containing v into an ordering without v with the restricted labeling. We first test whether H has a cut vertex, and if it has a cut vertex w, then w ∈ V (C). Otherwise, we search a vertex cut of size 2. Since every necklace graph whose underlying cycle has length at least 4 contains a vertex cut of size 2, we can find it, say {v, w}. Then one of the two vertices should be contained in C. We test whether H \ v or H \ w is a thread graph or not. If H \ v is a thread graph, then v ∈ V (C), and otherwise, w ∈ V (C). Since finding a cut vertex or a vertex cut of size two can be done in linear time, we are done with the time complexity.

Proof of Theorem 1.1. Let (G, k) be an instance of the LRW1-Vertex Deletion problem. First find an induced subgraph of G isomorphic to a graph in Ω N and branch by removing one of the vertices in the subgraph. Because the maximum size of graphs in Ω N is 8, we can find such a vertex subset in time O(n 8 ) if exists. After the branching algorithm, we transform the given instance (G, k) into at most 8 k sub-instances (G , k ) such that each sub-instance consists of a Ω N -free graph G and a remaining budget k . Clearly, (G, k) is a Yes-instance if and only if one of sub-instances (G , k ) is a Yes-instance.

Let (G , k ) be a sub-instance obtained from the branching algorithm. Since G is Ω N -free, by Theorem 2.3, each connected component of G is either a thread graph or a necklace graph with the underlying cycle of length at least 9. By Proposition 3.1, we can compute a minimum LRW1-deletion set of G in time O(|V (G | + |E(G )|), and decide whether (G , k ) is a Yes-instance. By checking all sub-instances, we can decide whether (G, k) is a Yesinstance in time 8 k • O(n + m) where m is the number of edges of G. We conclude that the LRW1-Vertex Deletion problem can be solved in time 8 k • O(n 8 ).

4

A polynomial kernel for LRW1-Vertex Deletion

We use the Sunflower lemma for packing obstructions of small size. It consists in finding a subset T of the input graph G = (V, E) whose removal turns G into a thread graph with the property that for every set S ⊆ V of size at most k, the following are equivalent (Lemma 4.2): S is a minimal vertex set such that G \ S has no obstructions in Ω N . S is a minimal vertex set such that G[T ] \ S has no obstructions in Ω N . From this property, if we choose a minimal LRW1-deletion set S in the input graph, then the vertices of S \ T should be used to remove at least one long induced cycle. This property is essentially used to find an irrelevant vertex in a large thread block. Moreover, with this set, we can preprocess the instance so that there is no obstruction containing exactly one vertex of T . This would be used to bound the length of the sequence of thread blocks in each connected component, and the number of non-trivial components.

Let (G = (V, E), k) be an instance of LRW1-Vertex Deletion. We start with an easy reduction rule.

Reduction Rule 1.

If G has a component that is a thread graph, then we remove it from G.

Packing small obstructions

Let F be a family of subsets over a set U . A subset U ⊆ U is called a hitting set of F if for every set F ∈ F, F ∩ U = ∅. For a graph G and a family of graphs F, a set S ⊆ V (G) is also called a hitting set for F if for every induced subgraph H of G that is isomorphic to a graph in F, V (H) ∩ S = ∅. The following lemma can be obtained from the Sunflower lemma. From now on, we assume that G is reduced under Reduction Rules 1 and2

. A vertex v of G is called irrelevant if (G, k) is a Yes-instance if and only if (G \ v, k) is a Yes-instance.

Bounding the size of components of G \ T

The goal is to shrink G \ T while preserving the solutions. For convenience, let µ(k) := 8 • 8!(k + 1) 8 + k. We first show that if a thread block in G \ T is large, then we can always find an irrelevant vertex in there. We mainly use the following lemma. Proof of Proposition 4.4. Suppose that G \ T contains a thread block of size at least (k + 2)(µ(k) + 2) 2 + 1. We can find such a thread block in polynomial time using Theorem 2.2. Let B := B(x, y) = (B, σ, ) be a thread block of size at least (k + 2)(µ(k) + 2) 2 + 1. For convenience, let σ be the ordering obtained from σ by removing the end vertices x and y.

In the following procedure, we mark some vertices of B in order to find an irrelevant vertex in B. We set Z := ∅. (1) For each v of T , choose the first k + 2 vertices z of σ that are neighbors of v with R ∈ (z), and choose the last k + 2 vertices z of σ that are neighbors of v with L ∈ (z), and add them to Z. (2) For each pair of two vertices v, v in T , choose k + 2 common neighbors of v and v in B, and add them to Z. (3) Choose the first k + 2 vertices z of σ with R ∈ (z), and choose the last k + 2 vertices z of σ with L ∈ (z), and add them to Z. In each case, If there are at most k + 1 such vertices, then we add all of them to Z. Then

|Z| ≤ |T |(2k + 4) + |T | 2 (k + 2) + (2k + 4) ≤ (k + 2)(µ(k) + 2) 2 -2. Since |V (B)| ≥ (k + 2)(µ(k) + 2) 2 + 1, there exists a vertex w in V (B) \ Z \ {x, y}. We claim that w is an irrelevant vertex. If (G, k) is a Yes-instance, then (G \ w, k) is clealry a Yes-instance.
Suppose that (G \ w, k) is a Yes-instance and let X ⊆ V (G) \ {w} such that |X| ≤ k and G \ (X ∪ {w}) is a thread graph. We may assume that G \ X is not a thread graph. So, G \ X must have an obstruction in Ω T that contains the vertex w. Let X ⊆ X ∪ {w} be a minimal hitting set for Ω N in G. From the property of the set T , X is a minimal hitting set for Ω N in G[T ], which implies that X ⊆ T . Thus G \ X must have an induced cycle of length at least 9 that contains w. Let C be an induced cycle of length at least 9 containing w in G \ X.

We will find an induced subgraph of G \ (X ∪ {w}) that is isomorphic to a graph in Ω N using Lemma 4.5, which leads a contradiction. Let v 1 , v 2 , w, v 3 , v 4 be the consecutive vertices on C. To apply Lemma 4.5, we will find two vertices that are adjacent to v 2 and v 3 .

Parameterized Complexity of Linear Rankwidth-1 Vertex Deletion

Let us now piece everything together and analyze the kernel size. Proof. Let (G = (V, E), k) be an instance of LRW1-Vertex Deletion. By Reduction Rule 1, we may safely assume that G has no components that are thread graphs. Let T ⊂ V be a vertex subset satisfying Lemma 4.2, and we preprocess using Reduction Rule 2.

By Lemma 4.3, we may assume that for every vertex subset S ⊆ V such that G[S] is a graph of {β 1 , β 2 , β 3 , β 4 }, |S ∩ T | ≥ 2. Combining Proposition 4.4 and Lemma 4.6, we can assume that every connected component of G\T has size at most (k+2)(µ(k)+2) 2 •19(6µ(k)+1) (otherwise the instance can be reduced in polynomial time). Note that for each connected component H of G \ T , there exists a vertex in H that has a neighbor in T , otherwise, H is a component of G that is a thread graph. Therefore, by Lemma 4.7, we can assume that the number of non-trivial components of G \ T is at most 2µ(k) and the number of isolated vertices in G \ T is at most µ(k) 2 (k + 2). It follows that

|T | + |V \ T | ≤ µ(k) + 2µ(k) • 19(6µ(k) + 1) • (k + 2)(µ(k) + 2) 2 + µ(k) 2 • (k + 2) = O(k • µ(k) 4 ) = O(k 33 ).

Concluding remarks

We consider the problem Linear rankwidth-w Vertex Deletion when w = 1. A next step is to investigate the problem for bigger w, or for any fixed w. A closely related problem is Rankwidth-w Vertex Deletion, which asks whether G has a vertex subset of size at most k such that G \ S has rankwidth at most w. This problem is fixed-parameter tractable for the following reason. Note that any Yes-instance has rankwidth at most w + k.

Having bounded rankwith can be characterized by a finite list of forbidden vertex-minors [START_REF] Oum | Rank-width and vertex-minors[END_REF].

From [START_REF] Courcelle | Vertex-minors, monadic second-order logic, and a conjecture by Seese[END_REF], having a vertex-minor can be expressed in C 2 MSO, i.e., monadic second order logic without edge set quantification where we can express the parity of |X| for a vertex set X. Fixed-parameter tractability follows as a consequence of Courcelle, Makowsky, Rotics [START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF]. This result can be turned into a constructive algorithm as [START_REF] Oum | Rank-width and vertex-minors[END_REF] provides an explicit upper bound on the size of vertex-minor obstructions for rankwidth k. However, the exponential blow-up in the runtime is huge with respect to both w and k. It is a challenging question whether a reasonable dependency on k can be achieved. A single-exponential time would be ideal, which was achievable for its treewidth counterpart. A first realistic goal is to consider the case when w = 1, i.e. the Distance-Hereditary Vertex Deletion. We leave it as an open question whether this problem can be solved in time c k • n O (1) time for some constant c.

Linear Rankwidth- 1 Theorem 1 . 1 .Theorem 1 . 2 .

 11112 Vertex Deletion (LRW1-Vertex Deletion) Input : A graph G, a positive integer k Parameter : k Question : Does G have a vertex subset S of size at most k whose removal makes G a graph of linear rankwidth at most one? For fixed k and a given graph G with n vertices, the LRW1-Vertex Deletion problem can be solved in 8 k • n O(1) time. The LRW1-Vertex Deletion problem has a polynomial kernel.

Figure 3

 3 Figure 3 An example of a thread block.

  For a digraph D = (V D , A D ) and a mergeable set of thread blocks B D = {B(x, y) = (G xy , σ xy , xy ) | xy ∈ A D }, G = D B D is the graph with the vertex set V = xy∈A D V (G xy ) and the edge set E = xy∈A D E(G xy ).

  be a shortest cycle among induced cycles of length at least 9 in G and for convenience, let v k+1 := v 1 and v k+2 := v 2 . We regard C as a directed cycle where for each 1≤ j ≤ k, v j v j+1 is an arc. If G = C,then we are done because C itself is a necklace graph with the underlying cycle C. We may assume that |V | > |V (C)|, and choose a vertex v ∈ V \ V (C) such that G \ v is I P E C ' 1 5 connected. Clearly, G \ v is again Ω N -free graph, and C is a shortest cycle among induced cycles of length at least 9 in G \ v. By the induction hypothesis, there exists some set of thread blocks B C mergeable with C such that G \ v = C B C . The rest of the proof consists in showing that G = C B C for some set of thread blocks B C mergeable with C.

Proposition 3 . 1 .

 31 Let G be a Ω N -free graph with n vertices and m edges. We can compute the minimum size of a LRW1-deletion set of G in time O(n + m), and find such a set S in the same time.

Lemma 4 . 1 (Lemma 4 . 2 .Lemma 4 . 3 .

 414243 [START_REF] Fedor | A polynomial kernel for proper interval vertex deletion[END_REF]). Let F be a family of sets of size at most d over a set U , and let k be a positive integer. Then in time O(|F|(k + |F|)), we can find a nonempty set F ⊆ F such that 1. for every U ⊆ U of size at most k, U is a minimal hitting set of F if and only if U is a minimal hitting set of F , and2. |F | ≤ d!(k + 1) d .Using Proposition 3.1 and Lemma 4.1, we identify a subset T of vertices of G of polynomial size in k that allows us to forget about small obstructions in G. Let (G = (V, E), k) be an instance of LRW1-Vertex Deletion. There is a polynomial time algorithm that either concludes that (G, k) is a No-instance or finds a non-empty set T ⊆ V such that 1. G \ T is a thread graph, 2. for every set S ⊆ V of size at most k, S is a minimal hitting set for Ω N in G if and only if it is a minimal hitting set for Ω N contained in G[T ], and3. |T | ≤ 8 • 8!(k + 1) 8 + k.Let us fix a subset T of V obtained by Lemma 4.2. We preprocess using the following reduction rule.Reduction Rule 2. Let U ⊆ T such that for every u ∈ U , there exists an induced subgraphH of G isomorphic to a graph in Ω N with V (H) ∩ T = {u}. If |U | > k, then (G, k) is a No-instance; otherwise, remove U fromG and reduce k by |U |, and use T \ U instead of T .It can be done in polynomial time because we only need to look at obstructions of Ω N in G. Reduction Rule 2 is safe.

Proposition 4 . 4 .

 44 If G \ T contains a thread block (G xy , σ xy , xy ) of size at least (k + 2)(µ(k) + 2) 2 + 1, then we can find an irrelevant vertex in G xy in polynomial time.

Lemma 4 . 5 .

 45 Let G be a graph and letv 1 v 2 v 3 v 4 v 5 be an induced path of length 4 in G. If two distinct vertices w 1 , w 2 in V (G) \ {v 1 , v 2 , . . . , v 5 } have the neighbors v 2 and v 4 in G, then G \ v 3 contains an induced subgraph isomorphic to a graph in Ω N .

Theorem 4 . 8 .

 48 The LRW1-Vertex Deletion problem has a kernel of size O(k 33 ).

  andΩ N := {house, gem, domino, C 5 , C 6 , C 7 , C 8 } ∪ Ω U .

Theorem 2.1

([16, 1]

). Let G be a graph. The following are equivalent. G has linear rankwidth at most 1. G is a thread graph. G has no induced subgraph isomorphic to a graph in Ω T .

I P E C ' 1 5

René van Bevern, Christian Komusiewicz, Hannes Moser, and Rolf Niedermeier. Measuring indifference: unit interval vertex deletion. In International Workshop on Graph Theoretic Concepts in Computer Science -WG, volume 6410 of Lecture Notes in Computer Science, pages 232-243, 2010.

Pim van't Hof and Yngve Villanger. Proper interval vertex deletion. Algorithmica, 65(4):845-867, 2013.

Supported by ERC Starting Grant PARAMTIGHT (No. 280152). † Supported by the "Chercheur d'avenir -Languedoc-Roussillon" project KERNEL

We choose two vertices of them that are not in X. In case when L ∈ (w) and v 3 < σ w, we use the last k + 2 vertices z of σ that are neighbors of v 2 with L ∈ (z) to identify two vertices similarly.

(Case Neither

happen. Thus, both of v 2 and v 3 appear either before w in σ or after w in σ. By the symmetry, we may assume that v 2 and v 3 appear before w in σ. So, R ∈ (v 2 ), R ∈ (v 3 ), and L ∈ (w). Since Z contains the last k + 2 vertices z of σ with L ∈ (z), there exist two vertices w 1 , w 2 from those k + 2 vertices that are not in X and C.

In all cases, G \ (X ∪ {w}) has an induced subgraph isomorphic to a graph in Ω N by Lemma 4.5. It contradicts to the assumption that X ∪ {w} is a LRW1-deletion set of G. Therefore, G \ X is a thread graph, and we conclude that (G, k) is a Yes-instance.

We show that if a vertex v in T has neighbors on 7 distinct blocks, then we can find a subgraph H isomorphic to one of {β 1 , β 2 , β 3 , β 4 } such that V (H) ∩ T = {v}. However, there is no obstruction in Ω N containing exactly one vertex from T by Reduction Rule 2. Thus, if a component of G \ T has many thread blocks, then we can identify a sequence of consecutive thread blocks not touched by any obstruction in Ω N . This allows us to contract one of these "safe" thread blocks, say B(x, y), to a vertex v such that N G\T (v) = (N G\T (x) ∪ N G\T (y)) \ B(x, y).

Kernel size

We bound the number of connected components using the following lemma.


Alexey Bakhirkin

Thomas Ferrère

Thomas A Henzinger

Dejan Ničković

The First-Order Logic of Signals

Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain.

I. INTRODUCTION

Cyber-physical systems (CPS) are networks of computational and physical elements that interact with their environment via sensors and actuators. CPS applications are today everywhere around us, deeply impacting our society. Medical devices that enable adaptive therapy based on the continuous measurement of patients' parameters, smart buildings that optimize heating strategy to the users' habits, and industrial plants that collaborate to minimize production costs are just a few examples of CPS applications. The inherent complexity of CPS and the intricate interactions with their physical environment makes their verification a challenging task.

Property-based monitoring is a light-weight verification technique that combines formal specifications with the analysis of individual system behaviors. It is a pragmatic, yet rigorous approach to reason about complex systems. Central to the property-based monitoring approach is the specification language that allows to precisely describe the intended system behaviors. Signal temporal logic (STL) [START_REF] Maler | Monitoring temporal properties of continuous signals[END_REF] is a specification formalism for expressing real-time temporal properties of real-valued signals. It extends linear-time temporal logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] with linear inequalities over signal values and with real-time bounds associated to temporal operators [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF]. The This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by the EU ICT COST Action IC1402 (ARVI), and by the European Research Council under the European Union's Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement nr. 306595 "STATOR". monitoring of STL enjoys an efficient procedure [START_REF] Maler | Monitoring temporal properties of continuous signals[END_REF], with time complexity linear in the size of the signals. Several research directions around STL have been explored in the recent years: the extension of the language with quantitative semantics and robust monitoring [START_REF] Fainekos | Robustness of temporal logic specifications for continuous-time signals[END_REF]- [START_REF] Donzé | Efficient robust monitoring for STL[END_REF], parameter estimation [START_REF] Asarin | Parametric identification of temporal properties[END_REF]- [START_REF] Bakhirkin | Efficient parametric identification for STL[END_REF], specification mining [START_REF] Bartocci | Data-driven statistical learning of temporal logic properties[END_REF]- [START_REF] Kong | Temporal logics for learning and detection of anomalous behavior[END_REF] and diagnosis [START_REF] Ferrère | Trace diagnostics using temporal implicants[END_REF]. STL specifications were used to analyze complex systems in the automotive, biomedical, robotics, analog system design and education application domains (see the survey [START_REF] Bartocci | Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications[END_REF] for more details).

The success of STL in recent years is mainly due to the simple monitoring procedures and the ability to capture many asynchronous sequential behaviors of real-valued signals observed in control applications. The bounded stabilization requirement is a typical example of a temporal specification than can be naturally expressed in STL. Given a Boolean signal b and a real-valued signal f , the bounded stabilization requirement is formulated as follows: "Whenever the control signal b is on its rising edge, the absolute value of f must go inside the interval [4.5, 5.5] within 10 time units and continuously remain within that same interval for at least 8 time units". This informal requirement, illustrated in Figure 1, is expressed as the following STL specification. Nevertheless, the expressiveness of STL has some limitations. For instance, the bounded stabilization property requires apriori knowledge of thresholds and timing bounds. In reallife applications, these bounds may not be known in advance and may even change dynamically during system execution. A more general formulation of the bounded stabilization property requires the signal f to stabilize around some value of r, which can vary during the execution of the system as shown in Figure 2. This more general specification cannot be expressed in STL. Intuitively, the general bounded stabilization requirement could be formulated in STL extended with quantification over the threshold value as follows. When introducing variable time parameters, temporal logic operators become unnecessary because the quantification over time implicit in temporal operators is then made explicit in syntax. In particular, by using first-order quantification, the modality 1 [s,s] , where s is a free variable, can express all other forms of temporal operators.

0(↑b

Motivated by the lack of a clean specification language that is sufficiently expressive to capture rich temporal properties, we propose signal first-order logic (SFO) as a powerful declarative formalism for expressing real-valued signal requirements. SFO combines first-order logic with linear real arithmetic and uninterpreted unary function symbols, which represent realvalued signals over time. The syntax of SFO allows quantification over time and value variables. This constitutes a general semantic framework with a syntax that can be used to directly specify rich temporal requirements and that provides a clean theoretical basis from which other specification formalisms can be derived. Quantified signal temporal logic (QSTL) is one such formalism, which, as we will demonstrate, is equally expressive as SFO.

SFO is an expressive formalism with undecidable satisfiability. In contrast, we show that the membership problem for SFO relative to piecewise-linear signals is decidable in time that is doubly exponential in the number of quantifiers and function symbols appearing in the specification, which is typically small in practice. A problem related to membership is known as monitoring. The monitoring problem takes as input a signal trace w and a formula ϕ with one free (time) variable and asks for the Boolean signal u such that u(t) = 1 iff ϕ is satisfied by w at time t. We propose an efficient monitoring algorithm based on a polyhedral representation of the set of free variables interpretations that satisfy a formula for a given input signal. We then define a class of bounded-response SFO specifications, over which we show that our algorithm performs in time linear in the length of the input signal. Informally, a bounded-response property ϕ can be associated with a horizon h such that the satisfaction of ϕ[t] by a trace w does not depend on values of w at any t with |t -t| > h. Finally, we illustrate the expressiveness of SFO specifications on a case study from the micro-electronics application domain.

II. EXAMPLES

In this section, we introduce SFO with several examples. We first formulate the bounded stabilization property from Section I by using the SFO syntax, and then introduce control

↑ b[t] ≡ b(t) = 1 ∧ ∃c ∈ (0, ∞) : ∀c ∈ (0, c) : b(t -c ) = 0
We now express the bounded stabilization property in SFO as follows.

ϕ 1 ≡ ↑ b[t] → ∃r : ∃c ∈ [0, 10] : ∀d ∈ [0, 8] : |f (t + c + d) -r| ≤ 0.5
Example 2 (Control). Consider the following property.

ϕ 2 ≡ ∀r : (∀c ∈ [0, 10] : |f (t + c) -r| ≤ 1) → (∀d ∈ [5, 10] : |g(t + d) -r| ≤ 2)
Formula ϕ 2 requires that if f is stable (stays within 1.0 of some value r for 10 time units), then g stabilizes around the same value (stays within 2.0 of r within 5 time units).

Example 3 (Rise time). Consider the following property.

ϕ 3 ≡ ∀c ∈ (0, 10) : f (t) = 1 ∧ f (t + c) = 2 ∧ ∀c ∈ (0, c) : 1 < f (t + c ) < 2 → ∃d ∈ (0, 10) : 9c ≤ 10d ≤ 11c ∧ ∃e ∈ (0, 20) :   ∀e ∈ (0, e) : g(t + e ) < 1 ∧ g(t + e ) = 1 ∧ g(t + e + d) = 2 ∧ ∀d ∈ (0, d) : 1 < g(t + e + d ) < 2  
Formula ϕ 3 expresses the fact that if signal f has a positive edge (from 1.0 to 2.0 in less than 10 time units) then signal g subsequently (in less than 20 time units) has a positive edge whose rise time is within 10% of that of f .

III. SIGNAL FIRST-ORDER LOGIC

In this section we define signal first-order logic (SFO), and study the decidability of its satisfiability and membership problems.

A. Definitions

A time domain T is a non-singular interval of R, and a (realvalued) signal is a function T → R. Let F = {f 1 , f 2 , . . .} be a set of function symbols. We call Boolean a signal with value in {0, 1}. A trace w is an interpretation of functions symbols f ∈ F as signals, denoted f w . Let X = {x 1 , x 2 , . . .} be a set of variables. A valuation v is an interpretation of variables x ∈ X as real numbers, denoted x v .

Signal first-order logic is obtained from variables in X and the signature f 1 , f 2 , . . . , Z, -, +, < where f 1 , f 2 , . . . ∈ F are uninterpreted unary function symbols, Z are integer constants, and -, +, < are the usual arithmetic binary functions and order relation. For practical purposes, we partition the set of variables X into T ∪R where t ∈ T are called time variables and r ∈ R are called value variables.

Definition 4 (SFO syntax). Terms τ and ρ of SFO are given by the grammar

τ ::= t | n | τ 1 -τ 2 | τ 1 + τ 2 ρ ::= r | f (τ ) | n | ρ 1 -ρ 2 | ρ 1 + ρ 2
where n ∈ Z, r ∈ R, and t ∈ T . A term θ is either a time term τ or a value term ρ as above.

Formulas ϕ of SFO are given by the grammar

ϕ ::= θ 1 < θ 2 | ¬ϕ | ϕ 1 ∨ ϕ 2 | ∃r : ϕ | ∃t ∈ I : ϕ
where n ∈ Z, θ 1 , θ 2 are terms, and I are real intervals with bounds in Z ∪ {±∞}.

We use standard abbreviations such as ϕ 1 →ϕ 2 ≡ ¬ϕ 1 ∨ϕ 2 , ϕ 1 ∧ ϕ 2 ≡ ¬(¬ϕ 1 ∨ ¬ϕ 2 ), and ∀r : ϕ ≡ ¬∃r : ¬ϕ. We also write ∀t ∈ I : ϕ as a shorthand for ¬∃t ∈ I : ¬ϕ. Definition 5 (SFO semantics). The value of a term θ over a trace w and valuation v, denoted θ w,v , extends the interpretation of function symbols and variables given by w inductively as follows:

n w,v = n for all n ∈ Z, θ 1 -θ 2 w,v = θ 1 w,v -θ 2 w,v and θ 1 + θ 2 w,v = θ 1 w,v + θ 2 w,v .
The satisfaction of a formula ϕ over a trace w and valuation v, denoted (w, v) |= ϕ, is inductively defined by letting (w, v) |= θ 1 < θ 2 iff θ 1 w,v < θ 2 w,v , (w, v) |= ∃r : ϕ iff (w, v[r ← a]) |= ϕ for some a ∈ R, similarly for quantification over time variables, and as expected for Boolean connectives.

We can also consider variants of SFO extented to:

• non-linear arithmetic, with formulas over the signature f 1 , f 2 , . . . , Z, -, +, ×, < ;

or restricted to:

• difference logic, with formulas over f 1 , f 2 , . . . , +Z, < ;

• linear order, with formulas over f 1 , f 2 , . . . , < . Here by +Z we denote the set of functions t → t + n for all n ∈ Z.

The proposed syntax of SFO may appear overly restrictive as compared to arbitrary formulas over the signature f, g, . . . , Z, -, +, < for f, g, . . . ∈ F . Two natural restrictions are enforced; we show that neither are essential.

1) The nesting of uninterpreted function symbols is disallowed. We did not encounter examples of properties of real-valued signals requiring such a nesting. Remark that nesting of function symbols can be eliminated by change of variable: any atomic formula of the form γ[f (τ )] can be rewritten as ∃r : r = f (τ ) ∧ γ[r] and applying this rewrite repeatedly will yield terms without nested function symbols.

2) Quantification over time variables is according to the form ∃t ∈ I : ϕ. This is a natural way of expressing many temporal properties. Enforcing this particular form is obviously not a restriction since taking I = (-∞, +∞) is allowed.

We sometimes use variable bounds in quantification over time, as in formula ∀c ∈ (0, c) : ϕ. Such bounds can also be eliminated and replaced by integers when the corresponding free variables are themselves bounded. In our example, assuming c is bounded by (0, 1), the formula can be rewritten as ∀c ∈ (0, 1) : 0 < c < c ∧ ϕ. The general motivation for restricting the quantification over time to a fixed or variable interval is to obtain an efficient monitoring algorithm. The bounds on time variables can be used to limit the scope of the resulting operations over signals to a neighborhood of each linear segment, as we shown in Section IV-C.

Notice that time and value variables are not fully separated since they can be compared in formulas θ 1 < θ 2 where θ 1 and θ 2 feature both types of variables. If this was undesirable one could enforce that θ 1 and θ 2 are of the same type. Comparing times with signal values is necessary in order to constrain derivatives of signals.

B. Satisfiability

We show that the satisfiability of SFO is undecidable. Theorem 6. The satisfiability of SFO is undecidable in general, and remains undecidable 1) over piecewise-linear or piecewise-constant signals;

2) over a fixed, bounded or unbounded time domain;

3) restricted to linear order; 4) restricted to difference logic over Boolean signals.

Proof. In general, we can proceed by reduction to the halting of two-counter machines, a well-known undecidable problem [START_REF] Minsky | Computation: finite and infinite machines[END_REF]. The run of a two-counter machine can be encoded using functions f 1 , f 2 whose value at integer times is directly that of counters, and a function f 3 holding the instruction number. Then every instruction of a given two-counter machine can be encoded as an SFO formula. For instance, an instruction i incrementing counter 1 is written ∀t ∈ [0, +∞) :

f 3 (t) = i → f 1 (t + 1) = f 1 (t) + 1 ∧ f 3 (t + 1) = i + 1.
The state of the machine can be maintained at integer times, definable via some signal

f 0 satisfying f 0 (0) = 0 ∧ ∀t ∈ [0, +∞) : f 0 (t) = 0 → f 0 (t + 1) = 0 ∧ ∀c ∈ (0, 1) : f 0 (t + c) = 0.
This does not pose any difficulty. We now show that the undecidability still holds under the various restrictions. 1) We can use the same reduction as in the general case. Since nothing is required of f 1 , f 2 , and f 3 between integer times the formula is satisfiable over restricted models iff it is satisfiable over unrestricted models. 2) We can modify the previous reduction by maintaining the state of the two-counter machine not at integer times but at times of the form c + id for i ∈ N, given an initial time c ∈ (-∞, +∞) and a period d ∈ (0, 1). For instance, incrementing the counter 1 in instruction i is

now written ∀t ∈ [c, +∞) : f 3 (t) = i → f 1 (t + d) = f 1 (t) + 1 ∧ f 3 (t + d) = i + 1.
The main formula is prefixed by existential quantification over c and d. 3) We introduce function symbols g, h that we use to mark the beginning of time slots where the state of the counter machine is encoded. We require ∃t ∈ (-∞, +∞) :

g(t) = h(t) ∧ ∀t ∈ (-∞, +∞) : g(t) = h(t) → ∃t ∈ (t, +∞) : g(t ) = h(t ) ∧ ∀t ∈ (t, t ) : g(t ) = h(t ).
This ensures the existence of a monotone, infinitely countable sequence of times t 0 , t 1 , . . . where g and h are equal at t i and differ in between t i and t i+1 for all i. We then encode machine configurations between t i and t i+1 as follows. Signals f 1 , f 2 do not hold the value of counters or instruction numbers, but assume a sequence of unique values. As an example, to increment a counter, we require the existence of a unique value that is in the next time slot but not in the previous one, and symmetrically for decrementing. 4) We proceed by reduction to the satisfiability of metric temporal logic [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF], which is undecidable in dense time [START_REF] Alur | The benefits of relaxing punctuality[END_REF]. Propositions p of metric temporal logic translate as atomic formulas f p (t) = 1 for some time variable t. The temporal operator until, denoted ϕ U I ψ with timing interval I, can be defined as ∃c ∈ I :

ϕ[t + c] ∧ ∀c ∈ (0, c) : ψ[t + c ]
where ϕ and ψ are formulas with one free time variable.

C. Membership

We show that by contrast to the satisfiability problem, the simpler membership problem for SFO is decidable.

Theorem 7. The membership problem of SFO relative to piecewise-linear traces is decidable.

Proof. Let w be a piecewise-linear trace and ϕ a closed formula. We reduce the membership of w in the language of ϕ to the satisfiability of first-order linear arithmetic. Formulas W i translating signals f i w can be constructed with size

|W i | = O(|w|). They guarantee W i [a, b] iff f i w (a) = b for all a ∈ T, b ∈ R. Then we replace every term ρ[f i (τ )] by ∃x : ρ[x] ∧ W i [τ, x]
recursively until all function symbols are eliminated. We obtain a formula of linear real arithmetic, i.e. without function symbols. The satisfiability of linear real arithmetic formulas is decidable by quantifier elimination.

Fischer and Rabin showed that the complexity of satisfiability of linear real arithmetic is at least exponential time for nondeterministic computations [START_REF] Fischer | Super-exponential complexity of presburger arithmetic[END_REF]. The input to the membership problem is given as a formula and a trace, and while the complexity relative to the formula size is subject to this lower bound, the complexity relative to the size of the trace is not. In particular, we show that the reduction of Theorem 7 yields an algorithm that for a fixed formula decides the membership problem relative to piecewise-linear traces in polynomial time. The quantifier elimination problem in linear real arithmetic produced by this reduction can be solved by the method of Ferrante and Rackoff [START_REF] Ferrante | A decision procedure for the first order theory of real addition with order[END_REF], or its improvement by Loos and Weispfenning [START_REF] Loos | Applying linear quantifier elimination[END_REF], both proceeding by virtual substitution. Such a method eliminates each existential quantifier ∃x in some subformula ∃x : F [x] in two steps that we briefly recall.

In the first step, terms featuring variable x are put in the form x < θ or θ < x where θ is a term not featuring x. Note that this may create rational coefficients, we temporarily allow them. Such terms θ form a set Θ.

In the second step, the subformula ∃x : F [x] is replaced by a finite disjunction γ∈Γ F [x γ] over a set of terms Γ. Ferrante and Rackoff take Γ = { θ1+θ2 2 | θ 1 , θ 2 ∈ Θ} ∪ {±∞}, while Loos and Weispfenning take Γ = {θ, θ ± | θ ∈ Θ} for some infinitesimal . The substitution is virtual because such terms are not proper, but one can define atomic formulas equivalent to their substitution, for example y 3 < z + is equivalent to y < 3z. The process is repeated for each quantifier.

By applying the method of [START_REF] Ferrante | A decision procedure for the first order theory of real addition with order[END_REF] or [START_REF] Loos | Applying linear quantifier elimination[END_REF], eliminating k quantifiers from a linear real arithmetic formula of size m can be done in time

m 2 O(k)
. We thus obtain the following:

Theorem 8. The membership problem of an SFO formula ϕ relative to a piecewise-linear trace w is computable in time k+l) where k is the number of quantifiers in ϕ, l is the number of occurrences of function symbols in ϕ, m is the length of ϕ, and n is the length of w.

(m + n) 2 O(
Proof. We translate the SFO formula ϕ into a quantified formula F of linear real arithmetic, using the procedure of Theorem 7. Formula F has size O(m + nl) and k + l quantifiers. Eliminating all quantifiers from F can be done in time

(m + n) 2 O(k+l)
, and deciding the validity of the resulting ground formula can be done in linear time.

The cylindric algebraic decomposition method of Collins [START_REF] Collins | Quantifier elimination for real closed fields by cylindrical algebraic decompostion[END_REF], although much more involved, has time complexity with the same bounds so that Theorem 8 also extends to SFO with non-linear arithmetic and piecewise-polynomial signals. In the case of difference logic, the quantifier elimination problem can be decided in exponential time by a similar method [START_REF] Koubarakis | Complexity results for first-order theories of temporal constraints[END_REF], so that the membership problem of SFO restricted to difference logic over piecewise-constant signals is decidable in exponential time.

We first remark that the (doubly) exponential complexity comes solely from the number of function symbols and quantifiers, which is expected to be small in practice. The complexity relative to trace size still appears prohibitive of practical applications that involve long traces. We will show in Section IV that for a fairly large class of formulas, the complexity relative to the trace size can be reduced to linear time.

D. Signal Second-Order Logic

Let us call signal second-order logic (SSO) the extension of SFO with quantifiers over uninterpreted function symbols. We briefly survey the theoretical properties of this extension. Since SSO contains SFO, its satisfiability problem is evidently not decidable. We show that indeed even its membership problem is not decidable.

Theorem 9. The membership problem of SSO relative to piecewise-linear traces is undecidable.

Proof. For any closed SFO formula ϕ whose uninterpreted function symbols are f 1 , . . . , f n , the membership in ∃f 1 ∃f 2 . . . ∃f n : ϕ is equivalent to the satisfiability of ϕ. By Theorem 6, the satisfiability of an arbitrary SFO formula ϕ is undecidable.

IV. MONITORING

In this section, we study the monitoring problem for SFO, defined as follows. We call temporal a formula ϕ with exactly one free variable t, of type time, and such that t appears with coefficient 0 or 1 in every term τ argument of a function symbol.

Definition 10. The satisfaction signal of formula ϕ relative to trace w is the Boolean signal denoted w ϕ such that w ϕ (t) = 1 iff (w, t) |= ϕ for all t ∈ T.

We restrict our attention to piecewise-linear traces over a bounded time domain. The satisfaction signal of some formula ϕ relative to such a trace w is a piecewise-constant Boolean signal, and can be represented as a finite union of intervals over which the formula is true.

Definition 11. The monitoring problem is the task of computing, given a temporal formula ϕ and a signal w, the satisfaction signal of ϕ relative to w.

The monitoring problem provides a slight generalization of the membership problem. It is particularly relevant when seen as an online computation problem, where the satisfaction signal should be produced along with the trace. It is also relevant as an offline computation problem, when used for testing. The time at which the formula is true and false provides valuable information for the debugging of simulation traces. Such information is explicitly computed for monitoring, but not strictly required for membership.

A. Polyhedral Representation

The interpretation of every term and every formula can be represented as a set of convex polyhedra. Our monitoring procedure of piecewise-linear signals for SFO over linear real arithmetic is based on this principle. Below, we give a high-level polyhedral characterization of operations over SFO terms and formula and later we give the corresponding concrete algorithms. We denote convex polyhedra as a set of linear equalities and inequalities, and use operations , , complement, and eliminate denoting the union, intersection, complement, and projection of polyhedra or sets of polyhedra. Their implementation is presented in full details in Section IV-B.

Functions We assume that the interpretation of every function f is given as a set of (convex) polyhedra P f with two free variables: t f denoting time and v f denoting the value of f at the given time point.

Terms In general, the interpretation of a term can be seen as a function from the values of its free variables to a real value. Thus a term θ (as in Definition 4) can be represented as a set of convex polyhedra P θ , with variables corresponding to free variables of the term and one extra variable v θ that corresponds to the value of the term. Polyhedron P θ and variable v θ can be defined by induction over the term structure as follows.

• For θ ≡ τ , P θ = {v = τ }, v θ = v , where τ is a time term as in Definition 4, i.e., a linear constraint over time variables, and v is a fresh variable. • For θ ≡ r, P θ = {v = r}, v θ = v , where r is a value variable, and v is a fresh variable. • For θ ≡ n, P θ = {v = n}, v θ = v , where n ∈ Z and v is a fresh variable.

• For θ ≡ f (τ ), P θ = P f [t f → τ, v f → v ], v θ = v ,
where τ is a linear expression as in Definition 4, v is a fresh variable, and denotes intersection of sets of polyhedra.

• For θ ≡ θ 1 ± θ 2 , P θ = eliminate(v θ1 , v θ2 , {v = v θ1 ± v θ2 } P θ1 P θ2 )
, where v is a fresh variable, and eliminate denotes the elimination of the given variables from the set of polyhedra.

Formulas Similarly, the interpretation of a formula ϕ can be seen as a function from the values of its free variables to a Boolean value and thus can represented as a set of polyhedra P ϕ , with variables corresponding to free variables of the formula. P ϕ can be defined by induction over the formula structure as follows.

• For ϕ ≡ θ 1 < θ 2 , P ϕ = eliminate(v θ1 , v θ2 , {v θ1 < v θ2 } P θ1 P θ2 ), where eliminate(V, P) denotes the elimination of variables V in the polyhedral set P. • For ϕ ≡ ¬ϕ , P ϕ = complement(P ϕ ), where complement takes the complement of a polyhedral set. • For ϕ ≡ ϕ 1 ∨ ϕ 2 , P ϕ = P ϕ1 P ϕ2 , where stands for the union of two sets of polyhedra. • For ϕ ≡ ∃r : ϕ , P ϕ = eliminate(r, P ϕ ).

• For ϕ ≡ ∃t ∈ I : ϕ , P ϕ = eliminate(t, {t ∈ I} P ϕ ).

B. Monitoring Algorithm

In this section we present a monitoring algorithm for SFO.

The key idea behind this algorithm is that for a temporal formula ϕ, its free time variable t is often the most significant dimension in the following sense: for a fixed value of t the interpretation of ϕ as a non-convex polyhedron has few convex parts. We internally represent every convex polyhedron P in the form {t ∈ I} Q, where I is an interval with bounds in Z ∪ {±∞}. We use interval I to order polyhedra along the time axis according to sup(I), which enables to rule out many empty intersections of polyhedra.

Representing the interpretations An interpreted function f that corresponds to an input signal is assumed to be piecewiselinear, have bounded domain and finite variability and thus can be represented as a list of polyhedra that are disjoint and ordered by time t f ; each polyhedron represents the value of the function on a separate bounded interval of time.

For every term and every formula, we represent its interpretation as a list ordered by the upper bound on variable t, the free variable of the top-level formula. We make sure that every operation on lists of polyhedra (union, intersection, complement) preserves this ordering. Operations on polyhedra used as subroutines in our algorithm all admit efficient implementations based the double description method, see [START_REF] Bagnara | Not necessarily closed convex polyhedra and the double description method[END_REF].

Terms Algorithm 1 implements the function term that builds a list of polyhedra representing the term θ (as in Definition 4). The function returns a pair of values: list of polyhedra and the variable denoting the value. The extra argument P dom is a set of constraints on bound time variables that was collected when traversing the formula.

Algorithm 1 Creating a list of polyhedra for a term.

function term(θ, P dom ) if θ ≡ τ then v ← fresh variable return {v = τ }, v else if θ ≡ r then v ← fresh variable return {v = r}, v else if θ ≡ n then v ← fresh variable return {v = n} P dom , v else if θ ≡ f (τ ) then v ← fresh variable return P f [t f → τ, v f → v ] P dom , v else if θ ≡ θ 1 ± θ 2 then P 1 , v 1 ← term(θ 1 , P dom ) P 2 , v 2 ← term(θ 2 , P dom ) v ← fresh variable return eliminate(v 1 , v 2 , {v = v 1 ± v 2 } P 1 P 2 ), v end end
We note that when constructing the list of polyhedra for f (τ ), the term τ is a linear expression over time variables, and thus substitution of t f with τ is a valid polyhedral operation. Since t can only appear positively in τ , the resulting list will naturally be sorted by the upper bound on variable t. Formulas Fig. 2 shows the function formula that builds a list of polyhedra representing the formula ϕ. Again, θ ranges over the terms as in Definition 4. The extra argument P dom is again a set of constraints on bound variables that was collected when traversing the formula. For the top-level formula, we pass { } as the P dom argument.

Variable elimination

The operation eliminate traverses the given list of polyhedra and eliminates from every polyhedron the given set of variables, which is a standard polyhedral operation. The projection operation leaves the time-ordering of polyhedra unaffected. Union The operation denotes the union of two lists of polyhedra. When the input lists are ordered, we can merge them into a new list that is also ordered. This is a standard algorithm on ordered lists, which preforms in linear-time.

Intersection The operation denotes the intersection, and we use the same symbol to denote one of the three operations:

• The intersection of two convex polyhedra.

• The intersection of a polyhedron and a list, which can be implemented with pairwise intersection. This intersection operation preserves the time-ordering of polyhedra. • The intersection of two lists of polyhedra, which can be implemented efficiently by exploiting the time ordering and the fact that two polyhedra, whose time projections do not intersect, themselves do not intersect.

Complement In general, a list of polyhedra can be complemented by following De Morgan's laws. For sets of polyhedra representing formulas, we can make the procedure more efficient by following the intuition that the projections of polyhedra on the main time variable t are in most cases bounded and every projection intersects only a small number of projections of "nearby" polyhedra. The function complement in Algorithm 3 implements this intuition. It starts with P being the list of polyhedra to complement and C being a singleton containing the "universal" polyhedron that only restricts t to the time domain. In every step, the function takes the first polyhedron P in the list P which is presented in the form P = {t ∈ I} Q and partitions C according to I. with {t ∈ I} is done similarly, and by the same intuition we usually only need to scan a few elements in the neighborhood of interval I. The result of this intersection, denoted S, is expected to contain few elements. Then Q is subtracted from S. Taking the union of the two parts is done using the merge subroutine previously discussed. We are done processing P and we remove it from the list P.

C. Bounded-Response Formulas

We now define a fragment of SFO that we call boundedresponse. In the following section, we show that for the bounded-response fragment of SFO and bounded-variability traces, Algorithm 2 has time complexity linear in the trace length.

Definition 12 (Bounded-Response SFO). We call boundedresponse the fragment of SFO in which all intervals I in subformulas of the form ∃t : t ∈ I are such that inf I = -∞ and sup I = +∞.

One may argue that the bounded-response restriction is too strong. We observe that properties involving unbounded time can still be expressed. In the context of monitoring, this still allows for one unbounded time variable. This fragment is thus sufficient to monitor safety properties in which bad prefixes can be identified by a segment of the input of bounded duration, a very common situation in practice.

D. Complexity

In this section, we characterize the complexity of our algorithm, first in the general case, and then we identify a fragment of SFO for which the complexity is reduced to lineartime relative to the trace length.

Theorem 13. Algorithm 2 operates in time 2 (m+n) 2 O(k+l)
where k is the number of quantifiers in ϕ, l is the number of occurrences of function symbols in ϕ, m is the length of ϕ, and n is the length of w.

Proof. For any union of polyhedra P, we denote by #(P) the number of unique linear constraints that appear (possibly repeated) in P. We show that for any formula ϕ and trace w, if P is a polyhedral representation of ϕ w , then

#(P ) ≤ (m + n) 2 O(k+l)
, where k, l, m, n are as in the statement of Theorem 7. One can see that #(P) = nl when ϕ is atomic, #(complement(P)) = #(P), and #(P 1 P 2 ) ≤ #(P 1 ) + #(P 2 ). The projection operation is such that #(eliminate(x, P)) ≤ #(P) 2 . Thus the bound holds by induction on the formula structure. Now any set of convex polyhedra P has at most 2 #(P) elements, each with at most #(P) constraints. Algorithm 2 ensures that convex polyhedra are not duplicated, since it removes every convex polyhedron that is already covered by another convex polyhedron. Observe that every subroutine of Algorithm 2 has running time polynomial in the size of their combined input and output. This gives us the bound as desired.

In the general case the complexity of monitoring is related to that of the membership problem. One notable difference is that the membership problem is a decision procedure, and its output has constant size. When using a quantifier elimination procedure, it is best not to enforce disjunctive normal form [START_REF] Ferrante | A decision procedure for the first order theory of real addition with order[END_REF]. Since the formula is closed, the result will be a ground formula that can easily be decided without using such a special form. By contrast the output of the monitoring can grow fast with the size of the signal. When using a quantifier elimination procedure, we must at least in the last step use a disjunctive normal form, since the required format of the output is a union of intervals. Algorithm 2 indeed enforces a disjunctive normal form at every step of the quantifier elimination, as with Fourier-Motzkin elimination. We note that the complexity of such a procedure is not worse than virtual substitution method when the output is required to be in disjunction normal form, see also [START_REF] Monniaux | A quantifier elimination algorithm for linear real arithmetic[END_REF].

Let us now consider the bounded-response fragment of SFO. We call horizon of a bounded-response formula the sum of the absolute value of all its time constants. We call variability of a piecewise-linear signal w relative to some bounded-response formula ϕ the maximum number of linear segments in w during any time period as long as the horizon of ϕ. Theorem 14. Algorithm 2 operates in time n2 (m+j) 2 O(k+l) over the class of bounded-response formulas, where j is the variability of w relative to ϕ, k is the number of quantifiers in ϕ, l is the number of occurrences of function symbols in ϕ, m is the length of ϕ, and n is the length of w.

Proof. Let h be the horizon of formula ϕ, and (t, t ) be an interval over which signal w is linear. It follows from the definition variability that the size of the restriction of w to the time interval [t -2h, t + 2h] is at most 5h. Similarly as in the proof of Theorem 13, we have that if P is a polyhedral representation of the set

S t,t = {(t , v) | t -h ≤ t ≤ t + h and (t , v) ∈ ϕ w }, then the number of unique constraints in P is (m + h) 2 O(k+l)
. This is because the part of the signal that can influence the set S t is contained in [t -2h, t + 2h]. The set ϕ w is covered by the S t,t obtained from all t, t chosen as endpoints of linear pieces of w. Thus the polyhedral representation of ϕ w has size n2 (m+h) 2 O(k+l)

. Subroutines of Algorithm 2 have running time at most proportional to the size of their input multiplied by maximum the number of polytopes that overlap in time. Indeed the only superlinear operation is that of complement. For bounded-response formulas, the set of polyhedra that overlap in time is

2 (m+h) 2 O(k+l)
. This gives us the desired computation time upper bound.

Remark that following a similar argument, one could obtain an online monitoring algorithm with matching complexity for bounded-response SFO.

V. QUANTIFIED SIGNAL TEMPORAL LOGIC

In this section we define quantified signal temporal logic (QSTL), which extends STL [START_REF] Maler | Monitoring temporal properties of continuous signals[END_REF] with first order quantification, and study its relation with SFO.

Terms of type time and value of QSTL are given by the grammar:

τ ::= t | n | τ 1 -τ 2 | τ 1 + τ 2 ρ ::= r | f | x | n | ρ 1 -ρ 2 | ρ 1 + ρ 2
where n ∈ Z, t ∈ T , r ∈ R, and f ∈ F . Formulas of QSTL are given by the grammar:

ϕ ::= θ 1 < θ 2 | ¬ϕ | ϕ 1 ∨ ϕ 2 | ∃x : ϕ | ϕ 1 U ϕ 2 | 1 [τ1,τ2] ϕ | ϕ 1 S ϕ 2 | Q [τ1,τ2] ϕ
where x ∈ X and τ 1 , τ 2 , θ 1 , and θ 2 are QSTL terms, such that τ 1 and τ 2 are of type time.

In our SFO framework, the temporal modalities of QSTL are seen as syntactic sugar that may be applied to SFO temporal formulas. Let us assume a distinguished time variable t, standing for the absolute time. Atomic formulas θ 1 < θ 2 are defined as θ 1 (t) < θ 2 (t), where for some term θ, writing θ(t) means applying the argument t to all function symbols in θ. Operator until, denoted U, is defined by letting

ϕ U ψ ≡ ∃c ∈ (0, +∞) : ϕ[t + c] ∧ ∀d ∈ (0, c) : ψ[t + d]
for all temporal formulas ϕ and ψ. The definition of operator since S is symmetrical. Operator eventually, denoted 1 [τ1,τ2] for time terms τ 1 , τ 2 , is defined by letting

1 [τ1,τ2] ϕ ≡ ∃c : 0 ≤ τ 1 ≤ c ≤ τ 2 ∧ ϕ[t + c]
for all temporal formulas ϕ. The definition of operator once, denoted Q [τ1,τ2] , is symmetrical. One can also define operator always, denoted 0 [τ1,τ2] , by letting 0 [τ1,τ2] ϕ ≡ ¬ 1 [τ1,τ2] ¬ϕ, and operator historically, denoted `[τ1,τ2] , by letting `[τ1,τ2] ϕ ≡ ¬ Q [τ1,τ2] ¬ϕ.

It is easy to see that every SFO formula can be written in QSTL form, so that QSTL is complete for SFO. This is because the modality ∃r : 1 [t,t] f (t) = r allows to access the value r of function f at any time t explicitly. In more details, putting an SFO formula in QSTL form is a two-stage process. The first stage recursively moves signals outside of inequalities by rewriting a formula ϕ into formula ϕ defined as follows:

γ[f (τ )] ≡ ∃t ∈ (-∞, +∞) : ∃r : r = f (t) ∧ t = τ ∧ γ[r] ¬ϕ ≡ ¬ϕ ϕ 1 ∨ ϕ 2 ≡ ϕ 1 ∨ ϕ 2 ∃x : ϕ ≡ ∃x : ϕ
The second stage consists in replacing every subformulas r = f (t) by 1 [t,t] f = r. We have removed all arguments of function symbols and thus obtain a QSTL formula. Since this formula has no nested temporal operators, it is equivalent at time zero to the original SFO formula.

VI. CASE STUDY

We present in this section the DDR2 memory interface case study. DDR2 memory interface acts as a bus between the memory and other components and exhibits communication of digital data implemented at the analog level of abstraction. In DDR2, the data access is controlled by a single-ended or differential strobe signal, which acts as an asynchronous clock. In the remainder of this section, we consider the single-ended data strobe DDR2-400 memory interface.

We focus more specifically on the alignment property between data signal DS and data signal strobe DQS. The alignment between the two signals is defined with respect to their respective crossings of thresholds defined in Table I. In the remainder of the section, we refer to different thresholds by their identifier. Threshold name Threshold id Value (V)

V DDQ V 1 1.800 V IH(AC) min V 2 1.250 V IH(DC) min V 3 1.025 V REF(DC) V 4 0.900 V IL(DC) max V 5 0.775 V IL(AC) max V 6 0.650
More specifically, the proper alignment between DS and DQS is determined by two values, the setup time tDS and hold time tDH. The setup and hold times of DS and DQS are checked both on their falling and rising edges of the strobe signal. We focus on the setup time tDS at the falling edge of DQS, the other three cases are symmetric. We illustrate this property with the timing diagram shown in Figure 3.

Informally, we can express the setup time alignment property at the falling edge of DQS as follows: Whenever DQS is on its falling edge, the distance from the previous falling edge in DS is at least tDS time. The falling edge of DQS (DS) is characterized by DQS (DS) crossing V 3 (V 6 ) from above. In order to express the above requirement in SFO, we first define the falling edge operator ↓(s, c)[t], which holds at t iff signal f crosses the threshold c from above. We formalize this operators as follows:

↓(f, c)[t] ≡ f (t) = c ∧ ∃d ∈ (0, +∞) : ∀d ∈ (0, d) : f (t + d ) < c
It is now straightforward to define the alignment requirement as the following SFO ψ[t] formula:

ψ[t] ≡ ↓(DQS, V 3 )[t] → `[0,t DS] ¬ ↓(DS, V 6 )[t]
We note that falling edges of a signal f below threshold c can also be captured in pure STL by letting ↓(f, c) ≡ (f = c) ∧ (f < c) U . As a consequence, the alignment requirement does not seem to need the power of SFO. In fact, the above STL specification relies on the assumption that tDS is a constant value. In reality, this is not the case. The setup time tDS varies dynamically according to the slew rates (slopes) of DS and DQS. According to the DDR2 standard, the setup time tDS is the sum of a constant base term tDS(base) and a variable correction term ∆tDS = tDS -tDS(base)

where tDS(base) equals to 150ps for single-ended DDR2-400 and the correction term ∆tDS is a value that depends directly on slew rates ssr DS and ssr DQS measured in DS and DQS. The setup slew rate ssr s of a falling signal s being defined as

ssr s = V 2 -V 4 ∆TF s
where ∆TF s is the time that the signal s spends between V 4 and V 2 (see Figure 3). The exact computation of ∆tDS = δ(∆TF DQS , ∆TF DS ) is done by interpolating the values from the look-up table depicted in Table II. To summarize, checking the setup time for DQS and DS requires dynamically measuring their nominal slew rates via ∆TF DQS and ∆TF DS and adapting accordingly the setup time bound tDS. This specification is clearly beyond the expressiveness of STL.

In the remainder of this section, we will demonstrate the formalization of the full alignment property in SFO. We We first define two auxiliary operators We are now ready to express the alignment requirement ψ [t] is SFO as follows:

ψ [t] ≡ ↓(DQS, V 3 )[t] → ∃∆TF DQS , ∆TF DS : V6,V4 ∆TFDS (DS)[t] ∧ 2 V6,V4 ∆TFDQS (DQS)[t]∧ tDS = δ(∆TF DQS , ∆TF DS ) ∧ `[0,t DS] ¬ ↓(DS, V 6 )[t]
The specification states that whenever DS is on its falling edge, there exist timing parameters ∆TF DQS and ∆TF DS such that (1) ∆TF DQS is the duration that DQS spends in the region [V 6 , V 4 ] used to measure its slew rate, (2) ∆TF DS is the duration that DS spends in the region [V 6 , V 4 ] used to measure its slew rate, (3) tDS is the setup time as a function of ∆TF DQS and ∆TF DS , and (4) the previous falling edge of DS is at least tDS time away.

VII. CONCLUSION

We introduced signal first-order logic (SFO) for the purpose of specifying and monitoring properties of real-valued signal. On the specification side, we show that this logic is equivalent in expressive power as signal temporal logic extended with quantifiers (QSTL). We believe that SFO provides a clear and general framework for studying the specification of real-valued temporal behaviors. On the monitoring side, the algorithm that we propose works recursively on the SFO formula structure, and computes the satisfaction set (or validity domain) of the formula at every time point. The monitoring of SFO is hard, and part of it is due to the lack of temporal structure of the formula. The hardness of this problem is indeed already present for monadic first-order logic. The simpler membership problem of SFO is at least nondeterministic exponential time relative to the formula size. We identify the fragment of bounded-response formulas, for which our monitoring algorithm terminates in linear-time relative to the trace length.

The problem of monitoring SFO or QSTL can be related to the parametric identification of STL. In the latter problem, the objective is to find the set of (tightest) parameter values such that the STL formula is satisfied. Variables in parametric signal temporal logic (PSTL) [START_REF] Asarin | Parametric identification of temporal properties[END_REF] can be seen as free variables in QSTL. We also remark that QSTL semantically contains STL* [START_REF] Brim | STL*: Extending signal temporal logic with signal-value freezing operator[END_REF], which supplements STL by freeze quantifiers [START_REF] Alur | A really temporal logic[END_REF]. The monitoring algorithm of [START_REF] Brim | STL*: Extending signal temporal logic with signal-value freezing operator[END_REF] proceeds by representing the satisfaction set using several time dimensions: the reference time, and the time at which values are frozen. On the other hand, our algorithm represents the satisfaction set relative to value dimensions.

In the future, we plan to implement our monitoring algorithm and assess its performance. We will also investigate the adaptation of our SFO monitoring algorithm to the problem of pattern matching. The problem of pattern matching over Boolean and real-valued signals is studied in [START_REF] Ulus | Timed pattern matching[END_REF] and in [START_REF] Bakhirkin | On the quantitative semantics of regular expressions over real-valued signals[END_REF], respectively. Both work consider timed regular expressions of [START_REF] Asarin | Timed regular expressions[END_REF] as a specification language. A star-free variant of such expressions could readily be encoded in SFO. The problem of finding an adequate counterpart in logic to the Kleene closure remains open.

Fig. 1 .

 1 Fig. 1. Bounded stabilization with fixed threshold r = 5.

0Fig. 2 .

 2 Fig. 2. Bounded stabilization without fixed threshold r.

  and rise time specifications. Function symbols f, g range over real-valued signals and b ranges over Boolean signals. Value variable r and time variables c, c , d, d , e, e and t range over the reals. Example 1 (Bounded stabilization). Before formulating the main stabilization formula, we define what is a rising edge ↑ b of a Boolean signal b at time t.

Fig. 3 .

 3 Fig. 3. Data DS and data strobe DQS alignment with tDS setup and tDH hold time on the falling edge.

  c,c d (f )[t] and 2 c,c d (f )[t] as the shorthands c,c d (f )[t] ≡ ∃e ∈ (0, ∞) :     ∀e ∈ (0, e) : f (t -e ) < c ∧ f (t -e) = c ∧ ∀e ∈ (e, e + d) : c < f (t -e ) < c ∧ f (t -e -d) = c e) : f (t + e ) < c ∧ f (t + e) = c∧ ∀e ∈ (e, e + d) : c < f (t + e ) < c ∧ f (t + e + d) = c )[t] (2 c,c d (f )) holds at time t iff the previous (next) duration that f spends in the region defined by the interval [c, c ] has the duration d.

  Algorithm 2 Creating a list of polyhedra for a formula.function formula(ϕ, P dom ) if ϕ ≡ θ 1 < θ 2 then P, v ← term(θ 1 -θ 2 , P dom ) return eliminate(v, P {v < 0}) else if ϕ ≡ ¬ϕ then P ← formula(ϕ , P dom ) return P dom complement(P) else if ϕ ≡ ϕ 1 ∨ ϕ 2 then P 1 ← formula(ϕ 1 , P dom ) P 2 ← formula(ϕ 2 , P dom )

	return P 1 P 2
	else if ϕ ≡ ∃r : ϕ then
	P ← formula(ϕ , P dom )
	return eliminate(r, P)
	else if ϕ ≡ ∃s ∈ I : ϕ then
	P ← formula(ϕ , P dom {s ∈ I})
	return eliminate(s, P)
	end
	end

  Complementation over a list of polyhedra. The operation subtract between a list of polyhedra and a single polyhedron denotes straightforward intersection with complement following De Morgan's laws. Morgan's laws. Since C is ordered by t and polyhedra are often bounded in t, subtracting {t ∈ I} from C can usually be done by scanning only a few elements of C. Intersecting C

	function complement(P)
	C ← {t ∈ T}
	while P = ∅ do
	pick P ∈ P
	{t ∈ I} Q ← P
	S ← C {t ∈ I}
	C ← subtract(C, {t ∈ I}) subtract(S, Q)
	P ← P \ P
	end
	return C
	end

Polyhedron P is subtracted from C, by subtracting {t ∈ I} on one hand, subtracting Q from the intersection of C with {t ∈ I} on the other hand, and then taking the union of the two. Subtraction (denoted by subtract) can be done by a straightforward intersection with complement, following De Algorithm 3

TABLE II FRAGMENT

 II OF THE LOOK-UP TABLE USED TO COMPUTE THE CORRECTION TERM ∆tDS AS A FUNCTION OF ssr DQS AND ssr DS .

				DQS slew rate (V /ns)
			2	1.5	1	0.9	0.8
		2	188	146 63	-	-
		1.5	167	125 42	43	-
	DS slew rate (V /ns)	1	125	83	0	-2	-13
		0.9	-	69	-14 -13	-27
		0.8	-	-	-31 -30	-44

ACKNOWLEDGMENTS

We thank Eugene Asarin and Oded Maler for their helpful comments.