Hans L Bodlaender
email: h.l.bodlaender@uu.nl

P O Box

089

Hans L Marijke

P O Bodlaender

Box

Probabilistic Inference and Monadic Second Order Logic

This paper combines two classic results from two di↵erent fields: the result by Lauritzen and Spiegelhalter [21] that the probabilistic inference problem on probabilistic networks can be solved in linear time on networks with a moralization of bounded treewidth, and the result by Courcelle [10] that problems that can be formulated in counting monadic second order logic can be solved in linear time on graphs of bounded treewidth. It is shown that, given a probabilistic network whose moralization has bounded treewidth and a property P of the network and the values of the variables that can be formulated in counting monadic second order logic, one can determine in linear time the probability that P holds.

Introduction

This paper combines two classic results from two di↵erent fields from computer science: the result by Lauritzen and Spiegelhalter [START_REF] Lauritzen | Local computations with probabilities on graphical structures and their application to expert systems[END_REF] that the probabilistic inference problem can be solved in linear time for probabilistic network whose moral graph has treewidth bounded by some constant, and the result by Courcelle [START_REF] Courcelle | The monadic second-order logic of graphs I: Recognizable sets of finite graphs[END_REF] that problems that can be formulated in counting monadic second order logic can be solved in linear time on graphs of bounded treewidth.

Probabilistic networks (also called Bayesian networks or belief networks) are the underlying technology of several modern decision support systems. See for more background, e.g., [START_REF] Jensen | Bayesian Networks and Decision Graphs[END_REF][START_REF] Pearl | Probablistic Reasoning in Intelligent Systems: Networks of Plausible Inference[END_REF]. A probabilistic network consists of a directed acyclic graph, and for each vertex in the graph a table of conditional probabilities. Each vertex in the graph represents a statistical variable, which can assume one of a fixed number of values; the table for a vertex gives the probability distribution for the values for that vertex, conditional on the values of the parents of the vertex.

Probabilistic networks are a topic of intense study. A central problem for probabilistic networks is the inference problem. One of the most commonly used algorithm to solve this problem is the clique tree propagation algorithm of Lauritzen and Spiegelhalter [START_REF] Lauritzen | Local computations with probabilities on graphical structures and their application to expert systems[END_REF]. It consists of the following steps: first the moral graph or moralization is formed from the probabilistic network. (See Section 2 for the definition of moral graph.) To this moral graph, edges are added such that a triangulated (or chordal) graph is formed. To a triangulated graph G, one can associate a clique tree: a tree with every tree node associated to a unique maximal clique in G, with the additional property that for each node of the graph, the cliques to which it belong form a connected subtree of the tree. The clique tree can be used to solve the inference problem, with the time exponential in the sizes of the cliques, but linear when these sizes are bounded by a constant. An alternative way of describing the algorithm of [START_REF] Lauritzen | Local computations with probabilities on graphical structures and their application to expert systems[END_REF] is by means of tree decompositions. Doing so, we have an algorithm for the probabilistic inference problem that is linear in the number of variables, but exponential in the width of the tree decomposition, in other words: the problem is linear time solvable when the moral graph has its treewidth bounded by a constant.

There are many other problems with the property that they are intractable (e.g., NP-hard) for general graphs, but become linear time solvable on graphs with bounded treewidth. A very powerful characterization of a class of such problems is by [START_REF] Courcelle | The monadic second-order logic of graphs I: Recognizable sets of finite graphs[END_REF] by the notion of Monadic Second Order Logic, or extensions of this notion. In this paper, we use the notion of Counting Monadic Second Order Logicand the notion of regularity. The result of Courcelle has been extended a number of times (e.g., [START_REF] Arnborg | Easy problems for tree-decomposable graphs[END_REF][START_REF] Borie | Automatic generation of lineartime algorithms from predicate calculus descriptions of problems on recursively constructed graph families[END_REF][START_REF] Courcelle | Monadic second-order evaluations on treedecomposable graphs[END_REF], see also [START_REF] Borie | Solving problems on recursively constructed graphs[END_REF].)

In this paper, we show that the results by Lauritzen and Spiegelhalter and by Courcelle can be combined. Suppose we have a probabilistic network whose moral graph has bounded treewidth. We can state some property of the network and of the values of the variables. Our result shows that if the property can be formulated in a language called (Counting) Monadic Second Order Logic, then we can compute the probability that it holds in linear time; i.e., to compute such a probability is fixed parameter tractable when parameterized by treewidth. (The result can also be seen as a variant of results shown by Courcelle and Mosbah [START_REF] Courcelle | Monadic second-order evaluations on treedecomposable graphs[END_REF].) Examples of such CMSOL properties are: do the variables that are true form a connected subgraph of the network, does no directed path in the network have all its variables alternatingly true and false along the path, are there an odd number of variables true, is the subgraph of the network induced by the false variables 3-colorable? It includes many properties that are NP-hard to check for arbitrary networks.

In Section 2, we give some preliminary results and definitions, including a hypergraph model that can be used instead of moral graphs. In Section 3, we sketch the proof of the main result. Some variants, extensions, and applications are discussed in Section 4. Some conclusions are given in Section 5.

Preliminaries

Probabilistic networks and the inference problem

To ease descriptions, we assume all variables in the probabilistic networks that are dealt with to be binary (boolean). Notations in the paper sometimes follow conventions from algorithmic graph theory, and sometimes follow conventions from probabilistic networks theory.

For a set S, a configuration on S is a function S ! {true, false}. We denote the set of all configurations on S as C(S). A configuration on a set S is often denoted as x S ; when S is a single vertex v, we write x v for x {v} . x ; denotes the unique configuration on the empty domain.

For sets S and S' and configurations x S 2 C(S) and x S 0 2 C(S 0 ), we say that x S agrees with x S 0 , notated x S ⇠ x S 0 , if for all v 2 S \ S 0 : x S (v) = x S 0 (v). Given a configuration x S 2 C(S) and a subset S 0 ✓ S, we write x S (S 0 ) for the configuration on S 0 that is a restriction of x S to the smaller domain: x S (S 0 ) 2 C(S 0 ) with x S (S 0 ) ⇠ x S . Given a directed graph G = (V, A) with a vertex v 2 V , par(v) denotes the set of vertices that have an arc to v: par

(v) = {w 2 V | 9(w, v) 2 A}. par(v) is called the set of parents of v.
Let G = (V, A) be a directed graph. The moral graphof G is the undirected graph, obtained by adding an edge between each pair of di↵erent vertices that are parents of the same vertex, and then dropping all directions of arcs, i.e., the graph (V, {{v, w} | (v, w) 2 A _ (w, v) 2 A _ 9x 2 V : v, w 2 par(x)}. (The process of obtaining the moral graph of a directed graph is called moralization. The term, frequently used in probabilistic network research, comes from the notion to 'marry the parents'.)

A probabilistic network is a pair (G, ), with G = (V, A) a directed acyclic graph, and  a set of functions, as follows. For each v 2 V , we have a function

 v : C({v}) ⇥ C(par(v)) ! [0, 1].
 v is meant to describe the conditional probability distribution for v, here conditional on the values of the parents of v, i.e., for configurations

x v , x par(v) ,  v (x v , x par(v) ) should give the value P r(x v |x par(v)
). G and  together define a joint probability distribution on the set of probabilistic variables V in the following way.

A

full configuration of a probabilistic network (G, ), G = (V, A) is a config- uration x V 2 C
V on the set V of all vertices in G. For each full configuration, define the probability of the configuration as the product of the conditional probabilities over all vertices, as follows. Assume

x V 2 C(V ). Pr(x V ) = Y v2V  v (x V ({v}), x V (par(v))) (1)
Throughout this paper, we write x V as the stochastic variable, that selects one full configuration with the distribution as given by (1) for the considered probabilistic network (G, ).

For each configuration, its probability now is the sum of the probabilities of all full configurations that agree with it. Assume

x W 2 C(W ), W ✓ V . Pr(x W ) = X x V 2C(V ), x V ⇠x W Pr(x V ) (2)
In applications of probabilistic networks, one generally desires to know the probability that a variable has a certain value, conditional to given values for some other variables. For instance, in a network, modeling a medical application, one may want to know if a patient has a certain disease, given some symptoms.

The given values of variables are called the observations. The set of observed variables is denoted by O, and the observed configuration is denoted x O . The probabilistic inference problem is to compute the conditional probability Pr(

x v | x O ), for a variable v 2 V and x v 2 C(v)
, or, more generally, the probability distribution for each variable, conditional to x O . To compute Pr(

x v | x O ), we can use that Pr(x v | x O ) = Pr(x v ^xO )/Pr(x O ).
Computational model In the paper, we assume all computations with values of probabilities can be done in constant time. In a practical setting, one could work with standard rounded representations of real numbers. To be precise, we should assume each conditional probability in  is given as a fraction of two integers. Analysis of the algorithms show that each value remains a fraction of two integers, both expressible with a polynomial number of bits; the algorithms we give involve a linear number of operations with such integers, while each such operation involves a polynomial number of bit operations. The details are not given here.

A mixed hypergraph model

Instead of using the more standard method of using a moralization of a probabilistic network, we instead associate with each probabilistic network a mixed hypergraph.

A mixed hypergraph is a pair H = (V, E, A), with V a finite set of vertices, and E a finite set of hyperedges, and A a set of arcs; each hyperedge e ✓ V is a non-empty subset of the vertices; an arc is an ordered pair of distinct vertices.

To a directed acyclic graph G = (V, A), we associate a mixed hypergraph H = (V, E, A) in the following way. H has the same vertices and arcs as G.

For each vertex v 2 V , we take a hyperedge consisting of v and its parents:

E = {{v} [ par(v) | v 2 V }.
H is the mixed hypergraph associated with G. The following lemma shows there is a one-to-one correspondence between the vertices and the hyperedges.

Lemma 1. Let G = (V, A) be a directed acyclic graph. If v, w 2 V , v 6 = w, then {v} [ par(v) 6 = {w} [ par(w).
Besides the hypergraph model of the directed acyclic graph, we also define a set of functions  e : C(e) ! [0, 1], one for each hyperedge e 2 E; these reflect the conditional probability functions  v . Consider an edge e = {v}[par(v). Let for each configuration on e, x e 2 C(e):

 e (x e ) =  v (x e ({v}), x e (par(v))) (3)
We introduce one more notation. Let x S 2 C(S) be a configuration. Let e be a hyperedge with e ✓ S. Then we write (x S , e) = (x e ) for the configuration x e , obtained by restricting the function x S to domain e. We now can rephrase Equation 1 in terms of the  e functions. The next (well known) proposition follows directly from the definitions. See also [START_REF] Van Der Gaag | Probability-Based Models for Plausible Reasoning[END_REF].

Proposition 1. Let (G = (V, A), ) be a probabilistic network. For each full configuration x V 2 C(V ): Pr(x V ) = Y e2A  e (x V )

Monadic Second Order Logic

The Monadic Second Order Logic language (MSOL) allows us to express properties of (mixed hyper)graphs. The language has the following constructs:

-Quantification over vertices, (hyper)edges, arcs: 9v 2 V , 9e 2 E, 8v 2 V , 8e 2 E, 8a 2 A, -Quantification over sets of vertices, sets of (hyper)edges, sets of arcs:

9W ✓ V , 9F ✓ E, 8W ✓ V , 8F ✓ E, . . . -Membership tests: v 2 W , e 2 F . -Identity tests: v = w, e = f .
-Adjacency tests: v 2 e, {v, w} 2 E, {v, w} 2 F , v is tail (head) of a, . . . -Logic operations: _, ^, ), ¬, . . . MSOL is a powerful language. Many graph properties can be expressed in it. E.g, Borie et al. [START_REF] Borie | Automatic generation of lineartime algorithms from predicate calculus descriptions of problems on recursively constructed graph families[END_REF] show how many graph properties can be expressed in MSOL. For example, the following property expresses that directed graph G = (V, A) is acyclic:

8W ✓ V : 9v 2 W : ¬9w 2 W : (v, w) 2 A
Extensions of MSOL can include the following language constructs:

- To these, we add one more construct, for the case that G is a probabilistic network.

-Value tests for vertices:

x v = true, x v = false. (Or: x v , ¬x v .
) Call the resulting language CMSOL with value tests. For example, one can write the property that an even number of variables is true as follows:

9W : (8v : v 2 W $ x v ) ^(|W | mod 2)
= 0 Given a property in CMSOL with value tests, we are interested in the probability that this property holds for a given probabilistic network.

Treewidth, terminal hypergraphs, and parse trees

The notion of treewidth was introduced by Robertson and Seymour in [START_REF] Robertson | Graph minors. II. Algorithmic aspects of treewidth[END_REF]. There are several equivalent notions known, e.g., the treewidth of a graph is exactly one larger than the minimum over all chordal supergraphs of the maximum clique size; and graphs of treewidth at most k are also known as partial k-trees. See [START_REF] Bodlaender | A partial k-arboretum of graphs with bounded treewidth[END_REF] for an overview. The definition here is given in terms of mixed hypergraphs.

Definition 1. A tree decomposition of a mixed hypergraph H = (V, E, A) is a pair ({X i | i 2 I}, T = (I, F )) with {X i | i 2 I}
a collection of subsets of vertices (called bags), and T a tree, such that

- S i2I X i = V .
-For each hyperedge e 2 E and each arc (v, w) 2 A: there exists an i 2 I with e ✓ X i , or {v, w} ✓ X i , respectively. -For all vertices v 2 V : the set of nodes {i 2

I | v 2 X i } is connected in T . The width of tree decomposition ({X i | i 2 I}, T = (I, F )) is max i2I |X i | 1.
The treewidth of a graph G is the minimum width over all possible tree decompositions of G.

Instead of using tree decompositions, we use an equivalent framework, where we use an 'algebra' on terminal mixed hypergraphs. A k-terminal mixed hypergraph is a 4-tuple G = (V, E, A, (x 1 , . . . , x k )) with V a finite set of vertices, E ✓ P(V ) a set of hyper edges, A ✓ V ⇥ V a set of arcs, and (x 1 , . . . , x k ) 2 V k an ordered set of k vertices from V , called the terminals. A terminal mixed hypergraph is a k-terminal mixed hypergraph for some k 0.

We define the following operations on terminal mixed hypergraphs.

-

((V, E, A, (x 1 , . . . , x k )), (V 0 , A 0 , E 0 , (x 1 , . . . , x k ))) = (V [V 0 , E[E 0 , A[A 0 , (x 1 , . . . , x k )), with V \ V 0 = {x 1 , . . . , x k }. Let O k be the set of operations, containing for all k 0 , `, 1  ` k 0  k, the operations CreateHyperedge k 0 , CreateArc k 0 , DropTerminal k 0 ,`, AddTerminal k 0 , Join k 0 .
Lemma 2. Let (G = (V, A), ) be a probabilistic network, let H be the moral graph of G, and let H 0 = (V, E 0 , A) be the associated mixed hypergraph of G.

The following statements are equivalent.

1. H has treewidth at most k 1.

2. H is subgraph of a triangulated graph with maximum clique size k.

3. H 0 has treewidth at most k 1.

4. The 0-terminal mixed hypergraph (V, E 0 , A, ;) can be constructed using the operations from O k . This can be shown using proofs and techniques from [START_REF] Wimer | Linear Algorithms on k-Terminal Graphs[END_REF], see also [START_REF] Bodlaender | A partial k-arboretum of graphs with bounded treewidth[END_REF]. Note that the notion is a minor twist on the well known notion of nice tree decompositions, see e.g., [START_REF] Bodlaender | A partial k-arboretum of graphs with bounded treewidth[END_REF][START_REF] Kloks | Computations and Approximations[END_REF].

If we have a method to construct a terminal mixed hypergraph with operations from O k , we can express this in a parse tree. Each node of such a tree is labeled with one operation from O k . To each tree node i, we associate a terminal mixed hypergraph

G i = (V i , E i , A i , (x i 1 , . . . , x i k 0 )
; the terminal mixed hypergraph associated to the node is the graph obtained by applying its operation to the terminal mixed hypergraphs associated with its children. We assume that the root r of the parse tree is a 0-terminal mixed hypergraph, otherwise, use some DropTerminal operations at the top of the tree.

If G r = (V r , E r , A r , ;), (V r , E r , A r )
is the mixed terminal hypergraph represented by the parse tree. It is well known (see e.g., [START_REF] Bodlaender | The pathwidth and treewidth of cographs[END_REF]) that if W is a clique in G, then a tree decomposition of G has a bag that contains all vertices in W . .Note that for each vertex v, v [ par(v) forms a clique in the moral graph and thus, for each tree decomposition of the moral graph, there is a bag that contains v [ par(v).

Regular properties and finite state tree automata

Many of the linear time algorithms on graphs of bounded treewidth can be expressed as a finite state tree automaton, a generalization of the classic finite state automaton. Such an automaton can be written as a 4-tuple (S, S A , t, 2), with S a finite set of states, S A ✓ S a set of accepting states, 2 a special symbol, and t a state transition function:

t : (S [ {2}) ⇥ (S [ {2}) ⇥ O k ! S.
The automaton works on a binary tree with nodes labeled with elements from O k (and in particular: on a parse tree), in the following way. Each element i of the tree is associated a state s(i) with s(i) = t(s L , s R , o(i)), with s L (s R ) the state s(j) of the left (right) child j of i, s(i) = 2 if i has no left (right) child, and o(i) the operation from O k with which i is labeled. Note that these states can be computed in bottom-up order (e.g., in postorder) in the tree. We say an automaton accepts the labeled tree, if the state of the root belongs to the set S A .

A property P of graphs (or, of mixed hypergraphs) is regular, if for each k, there is a finite state tree automaton M k , such that for each G: P (G) holds, if and only if M k accepts all parse trees of G with operations from O k , if and only if M k accepts at least one such parse tree. Courcelle's theorem can be stated as follows.

Di↵erent models

Possibly, the results can also be applied to di↵erent probabilistic models, whose structure can be modeled by hypergraphs. See e.g. [START_REF] Daskalakis | Computing pure Nash equilibria in graphical games via Markov random fields[END_REF].

Conclusions

Examples The results in this paper can be applied to a large number of problems, as many graph properties can be formulated in CMSOL. See e.g., [START_REF] Borie | Automatic generation of lineartime algorithms from predicate calculus descriptions of problems on recursively constructed graph families[END_REF] for many examples of CMSOL graph properties. Some examples are:

-'Suggested causality': for two variables x and y: what is the probability that

x and y hold and there is a path from x to y of variables that all are true? -Independence: what is the probability that no true variables are adjacent? -In graphical games: some vertices represent an agent. Agents have states, which are modeled by a probabilistic network. For a collection of pairs of agents F , we ask: what is the probability that no two pair in F of agents have the same state? Or: can we partition the agents into three (or any other constant) number of groups, such that adjacent agents with the same state belong to a di↵erent group?

Time and space considerations

The time and space used by the algorithm of Theorem 3 is approximately the product of the time, respectively the space, of the Lauritzen Spiegelhalter algorithm and the number of states of the tree automaton. In some cases this number of states is large, in particular, when the property whose probability is to be computed is NP-hard when the treewidth is not bounded. In some other cases, the number of states can be reasonably small. For instance, when P is the property that an even number of variables has the value true, then a machine with only two states su ces. So, while in some cases, the algorithm implied by Theorem 3 is not practical, in other cases, we get algorithms that are su ciently e cient.

It is also often possible to use some optimizations that decrease the running time. For instance, many machines will have a state s r that will never lead to an accepting state later. Here, we can see that we do not need to compute values of the form Q i (c, s r ) for any node i and any configuration c. (For notation, see the proof of Theorem 3.) More Myhill-Nerode type optimizations (compare [START_REF] Fellows | An analogue of the Myhill-Nerode theorem and its use in computing finite-basis characterizations[END_REF]) are also possible. For instance, computing the probability that there is at most one true variable needs tables with `+ 3 entries per node in the parse tree, `the treewidth.

Finally, in practical cases, one can try to design more e cient algorithms by hand. The situation can resemble the experiences with the use of Courcelle's theorem: Consider some practical problem P , which can be formulated in monadic second order logic. Courcelle's theorem directly tells us that the problem can be solved in linear time for graphs of bounded treewidth. However, a direct use of the machinery behind the proof of Courcelle's theorem would most probably give an algorithm that is too slow in practice, due to large hidden constants in the O-notation. However, in most cases, algorithms that are tailor made for problem P will have much better constant factors, and may be practical for small values of treewidth (see e.g. [START_REF] Koster | Solving partial constraint satisfaction problems with tree decomposition[END_REF]. )

A direct application of Courcelle's theorem may also yield an automaton that is too large to e↵ectively build.A recent technique by Courcelle and Durand [START_REF] Courcelle | Fly-automata, their properties and applications[END_REF] helps to (partially) overcome such problems. It is interesting to investigate if the techniques from [START_REF] Courcelle | Fly-automata, their properties and applications[END_REF] can give practical improvements for implementations of Theorem 3.

If a tree decomposition of bounded width is not given with the input, it is possible to find one in linear time (assuming the width bound is a constant): run the algorithm of [START_REF] Bodlaender | A linear time algorithm for finding tree-decompositions of small treewidth[END_REF] on the undirected graph, obtained by dropping directions of edges and replacing hyperedges by a clique. Unfortunately, this algorithm is not practical, even for small values of the treewidth. However, there are good heuristics that often perform very well, see [START_REF] Bodlaender | Treewidth computations I. Upper bounds[END_REF][START_REF] Bodlaender | Treewidth computations II. Lower bounds[END_REF] for overviews.

Final conclusions In this paper, we have shown that two famous results from di↵erent fields of computer science can be combined: the algorithm for probabilistic inference by Lauritzen and Spiegelhalter, and the result by Courcelle that problems in CMSOL can be solved in linear time when the treewidth of the graph is bounded. The formalism chosen in this paper to present the results may depart from what is sometimes usual; a description in other formalisms (tree decompositions or clique trees) is also possible, but seems to require more clumsy details.

The result allows us to compute the probability of several properties of the network and the values of the variables in linear time. For some properties, the constant factor hidden in the 'O' may yield it impractical, but for other properties, one can expect that the resulting algorithm is indeed su ciently e cient.

An interesting question is whether other problems that were studied for probabilistic networks have a similar CMSOL variant. Other interesting theoretical questions include:

-Is Inference on probabilistic networks with moral graphs of bounded treewidth solvable in logspace? (Compare [START_REF] Elberfeld | Logspace versions of the theorems of Bodlaender and Courcelle[END_REF].) -Inference is #P -hard [START_REF] Roth | On the hardness of approximate reasoning[END_REF]. What complexities have computing the probabilities of CMSOL properties on general probabilistic networks (i.e., without bounds on treewidth)? -Are there other graph problems for which a variant of Theorem 3 holds? One possible direction may be to look at optimization problems, e.g., with the finite integer index property [START_REF] Bodlaender | Reduction algorithms for graphs of small treewidth[END_REF]. Also, when we allow polynomial running time instead of linear, it is to be expected that a larger class of problems can be handled.

For fixed constants c 1 , c 2 :

 12 |W | mod c 1 = c 2 , |F | mod c 1 = c 2 . MSOL with these constructs, for all fixed c 1 and c 2 is called Counting MSOL, or CMSOL. -If the vertices, edges, or arcs of G are labeled with a bounded number of di↵erent labels, L the labeling function, we have label tests: L(v) = c, L(e) = e.

  , and adds a new terminal vertex. Hyperedges and arcs are not a↵ected. So, (V, E, A, (x 1 , . . . , x Has two k-terminal mixed hypergraphs as argument. Yields the k-terminal mixed hypergraph obtained by taking the union of the arguments and then identifying the corresponding terminals. So, Join k

CreateHyperedge k (). Has no arguments. Yields a k-terminal hypergraph with k vertices and one hyperedge, containing all vertices: ({v 1 , . . . , v k }, {{v 1 , . . . , v k }}, ;, (v 1 , . . . , v k )). -CreateArc(). As CreateHyperedge, but creates a directed arc: ({v 1 , v 2 }, ;, {(v 1 , v 2 )}, (v 1 , v 2 )). -DropTerminal k,`( G). Has a k-terminal mixed hypergraph as argument, and turns the `th terminal into a non-terminal: (V, E, A, (x 1 , . . . , x k )) maps to (V, E, A, (x 1 , . . . , x ` 1 , x `+1 , . . . , x k )). -AddTerminal k (G). Has a (k 1)-terminal mixed hypergraph as argumentk 1 )) maps to (V [ {x k }, E, A, (x 1 , . . . , x k )). -Join k (G, H).

Acknowledgement

I thank the referees for several very helpful comments, and colleagues from the Decision Support Systems and the Algorithmic Systems groups at the Depart-ment of Information and Computing Science of Utrecht University for useful discussions.

Theorem 1. [START_REF] Courcelle | The monadic second-order logic of graphs I: Recognizable sets of finite graphs[END_REF] A graph property in CMSOL is regular.

Courcelle conjectured that all regular properties belong to CMSOL; for some special cases, the conjecture has been shown by Kabanets [17] and Kaller [START_REF] Kaller | Definability equals recognizability of partial 3-trees and k-connected partial k-trees[END_REF]. Regularity implies that for each k, there is a linear time algorithm that, given a (mixed hyper)graph G of treewidth at most k, decides if the property holds for G or not: the parse tree with operations in O k can be constructed in linear time, and then the automaton M is run in linear time on the parse tree; decide 'yes', if M ends in an accepting state.

We need to look at a minor variant of Theorem 1 for graph expressions with one free vertex set variable, i.e., properties of the form P (G, W ), G = (V, E, A) a mixed hyper graph, W ✓ V a set of vertices. Our finite state tree automaton gets as input a labeled tree, and for each node in the tree that gives a new vertex (i.e., one that is not used by any node that is a descendant in the tree) whether this vertex belongs to the vertex set we denote by W . The state transition function gets a fourth argument, that is empty, except for the AddTerminal, CreateArc, and CreateHyperedge k 0 operations, where it gets a series of 1, 2, or k 0 booleans telling whether the new vertices belong to set W or not. Theorem 2. [START_REF] Courcelle | The monadic second-order logic of graphs I: Recognizable sets of finite graphs[END_REF] Let P be an expression in CMSOL with free set variable W . Then P is regular.

We write as shorthand notation: {x

, the set of variables with value true in configuration x V . For a probabilistic network (G, ) and (regular) property P with free vertex set variable W , we can ask for the probability that P (G, x V } holds. Examples of such properties are given in the introduction. We can write:

with x W V the full configuration with {x V } = W . This generalizes (2).

Main results

The main result of this paper is given now. It shows that we can combine the results of Courcelle (Theorem 2) and [START_REF] Lauritzen | Local computations with probabilities on graphical structures and their application to expert systems[END_REF]. Note that the treewidth of the moral graph of G is at least the treewidth of G.

Theorem 3. Let P be a property of (mixed hyper)graphs with one free vertex set variable. Suppose P is regular. For each constant k, there is a linear time algorithm that, when given a probabilistic network (G, ) with the treewidth of the moral graph of G at most k, computes the probability of P (G, {x V }}. Proof. Let k be fixed. Assume we have the finite state tree automaton M = (S, S A , t, 2) for P and O k+1 . We first build in linear time a parse tree T with operations in O k+1 for the hypergraph associated with (G, ). Then, we compute for each node in T a table called Q i . These tables can be computed in bottom up order in the tree. Given the table of the root node, the requested value can be computed.

For each node i in T , we denote its associated terminal graph

, and write X i = {x i 1 , . . . , x i ki }. Q i maps each pair (x Xi , s) to a real value in the interval [0, 1], with x Xi a configuration on X i , and s 2 S a state, such that

where we sum over all configurations x Vi on V i that agree with x Xi and that have the property that when we run machine M on the subtree with root i with

Claim. Let i be a node in the parse tree. Given tables Q j for all children j of i, we can compute the table Q i in O(1) time. Proof. i is labeled with some operation from O k+1 . For each type of operation, we must show the claim separately. We consider two more interesting cases, and omit the others here.

Join Suppose i is labeled Join k 0 and has children j 1 and j 2 .

For each configuration x Xi and state s:

where the sum is taken over all pairs (s 1 , s 2 ) with t(s 1 , s 2 ,Join k 0 ) = s. There are O(1) such pairs, and thus each of the O(1) values Q i (x Xi , s) can be computed in O(1) time.

AddTerminal Suppose j is the child of node i, i is labeled AddTerminal 0 k , with z the added new vertex. Consider a configuration x Xi and a state s. We look at the case that z has value true in x Xi , the other case is similar. Now, one can show

where x Xi {z} is the restriction of x Xi to domain X i {z}, and the sum is taken over all s 0 2 S with t(s, 2,AddTerminal 0 k ) = s. This implies that Q i can be computed in O(1) time, given Q j . Claim. Let r be the root of the parse tree of G.

Proof. G r has 0 terminals, so there is a unique configuration x Xr = x ; . Pr(P (G, {x

where the sum is taken over all configurations x V on V = V r where P (G, {x V }) holds. Each such configuration trivially agrees with x ; . As M is the finite state tree automaton for P , these configurations are exactly those where M accepts when W = {x V }. So, the sum equals

where the second sum is taken over the configurations x V on V that have M end in state s when W is as above. This equals P s2S A Q r (x ; , s). So, working bottom-up in the parse tree, we can compute in linear time all tables Q i , and then compute the requested answer in O(1) time using the table of the root of the parse tree.

Extensions

We briefly mention a few extensions of the result.

Non-binary variables

While most results were described in terms of binary variables, the same results hold when variables are non-binary but can attain a number of values bounded by some constant.

Conditional probabilities

Suppose we want to compute the probability that property P holds, conditional to the observations x O . The value can be computed with the same method. We use that Pr(P (G, x V )|x O ) = Pr(P (G, x V ) ^xO )/ Pr(x O ) and that regularity and CMSOL are closed under conjunction, and compute Pr(P (G, x V ) ^xO ) and Pr(x O ) separately.

Di↵erent types of edges

To the mixed hypergraph model, we can add additional edges and arcs that are not part of the probabilistic network, but can be used in CMSOL queries on the network. Assuming that we work with bounded width tree decompositions that also fulfill the property that for each of the di↵erent types of edges there are bags that contain the endpoints, we can also answer compute the probability of CMSOL queries on properties about the graph formed by these additional edges in linear time.


Petr Jančar

Prateek Karandikar

Philippe Schnoebelen

Unidirectional Channel Systems Can Be Tested

Introduction

Channel systems are a family of computational models where several, usually finitestate, agents communicate via usually unbounded fifo communication channels [START_REF] Brand | On communicating finite-state machines[END_REF]. These models are well-suited to the formal specification and algorithmic analysis of asynchronous communication protocols [START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using QDDs[END_REF][START_REF] Bouajjani | Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations[END_REF][START_REF] Atig | On the reachability analysis of acyclic networks of pushdown systems[END_REF][START_REF] Muscholl | Analysis of communicating automata[END_REF]. They are sometimes called queue automata when there is only one agent using the channels as fifo memory buffers.

A particularly interesting class of channel systems are the lossy channel systems, "LCS" for short, popularized by Abdulla, Bouajjani, Jonsson, Finkel, et al. [START_REF] Cécé | Unreliable channels are easier to verify than perfect channels[END_REF][START_REF] Abdulla | Verifying programs with unreliable channels[END_REF][START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF]. Lossy channels are unreliable and can lose messages nondeterministically and without any notification. A bit surprisingly, this makes lossy systems easier to analyse: safety, inevitability and several more properties are decidable for this model [START_REF] Cécé | Unreliable channels are easier to verify than perfect channels[END_REF][START_REF] Abdulla | Verifying programs with unreliable channels[END_REF][START_REF] Abdulla | Verification of probabilistic systems with faulty communication[END_REF][START_REF] Baier | On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems[END_REF][START_REF] Baier | Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties[END_REF] while they are undecidable when channels are reliable.

It should be stressed that LCS's have also been very useful outside the field of communicating systems and distributed computing. During the last decade, they have been used to show the decidability, or (more often) the hardness, of problems on Timed Automata, Metric Temporal Logic, modal logics, etc. [START_REF] Abdulla | Decidability and complexity results for timed automata via channel machines[END_REF][START_REF] Ouaknine | On metric temporal logic and faulty Turing machines[END_REF][START_REF] Kurucz | Combining modal logics[END_REF][START_REF] Konev | Dynamic topological logics over spaces with continuous functions[END_REF][START_REF] Lasota | Alternating timed automata[END_REF]. With other unreliable computational models, lossy channel systems are now an important tool for the complexity analysis of algorithms that rely on well-quasi-ordering theory [START_REF] Schmitz | Multiply-recursive upper bounds with Higman's lemma[END_REF][START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF][START_REF] Haddad | The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets[END_REF].

Unidirectional channel systems, "UCS" for short, are a variant of LCS's where a Sender process communicates to a Receiver process via one reliable and one lossy channel. Fig. 1 gives an example. The presence of one reliable channel put UCS's beyond plain LCS's. On the other hand, the unidirectionality (there is no channel from Receiver to Sender) is a limitation that LCS's do not share.

UCS's were first studied by Chambart and Schnoebelen who considered mixed channel systems (i.e., communicating systems using both reliable and lossy channels in arbitrary combinations) and showed how to reduce safety and reachability problems for arbitrary network topologies to reachability problems on either queue automata (undecidable), or LCS's (decidable), or the previously unidentified UCS's [START_REF] Chambart | Mixing lossy and perfect fifo channels[END_REF].

The reachability problem for UCS's is quite challenging: it was proved decidable by reformulating it more abstractly as PEP, aka the Regular Post Embedding Problem, which is easier to analyze [START_REF] Chambart | Post Embedding Problem is not primitive recursive, with applications to channel systems[END_REF][START_REF] Chambart | The ω-Regular Post Embedding Problem[END_REF][START_REF] Chambart | Pumping and counting on the regular Post embedding problem[END_REF]. We want to stress that, while PEP is a natural variant of Post's Correspondence Problem, it was only identified through questions on UCS's. Recently, PEP has proved useful in other areas, starting with Graph Logics [START_REF] Barceló | Graph logics with rational relations and the generalized intersection problem[END_REF].

Testing channel contents. Basic channel machines are not allowed to inspect the contents of the channels. However, it is natural to enrich the basic setup with tests (conditions on channel contents) as in, e.g., Fig. 1 where some sender's actions depend on (the parity of) the number of messages currently in r. Adding tests goes smoothly and painlessly for LCS's where the main decidability results extend directly with almost unchanged algorithms [10, sect. 3.3]. Adding even simple tests to UCS's is a completely different story, as we discovered. One meets two obstacles when trying to extend the approach that worked for UCS's:

1. The "reformulation" of UCS reachability as a Post Embedding Problem is a nontrivial reduction that reorders the events in a UCS run, relying on the independence (in a concurrency-theoretical sense) of sendings wrt readings. Tests on channel contents introduce global dependencies that are not reflected in PEP problems. 2. One is then led to consider extensions of PEP where said dependencies can be reflected, raising a new question: how to show the decidability of these extensions?

Our contribution. We extend UCS's with the possibility of testing channel contents with simple regular predicates. This makes reachability undecidable even with restricted sets of simple tests. Our main result is that reachability remains decidable when only emptiness and non-emptiness tests are allowed. The proof goes through a series of reductions that leave us with UCS's extended by only emptiness tests on a single side of a single channel (called "Z l 1 tests"). This minimal extension can then be reformulated as PEP partial codir , or "PEP with partial codirectness", a nontrivial extension of PEP that was recently proved decidable [START_REF] Karandikar | Cutting through regular Post embedding problems[END_REF].

Outline of the paper. Unidirectional channel systems with tests are defined in Section 2. Section 3 shows how undecidability creeps in when regular tests are allowed. Section 4 presents protocols for simulating (non-)emptiness in UCST's with only emptiness tests by Sender, thus reducing UCST to UCST[Z 1 ]. Section 5 proves decidability for UCST[Z l 1 ] by reducing to PEP partial codir . This is then leveraged in section 6 to account for the whole of UCST[Z 1 ]. Finally, Section 7 proves that (non-)emptiness tests strictly enrich the basic UCS model.

Unidirectional Channel Systems

Structure. Formally, a UCST (for Unidirectional Channel System with Tests) is a tuple

S = (Ch, M, Q 1 , ∆ 1 , Q 2 , ∆ 2 )
, where M is a finite alphabet of messages, Q 1 , Q 2 are disjoint finite sets of states of Sender and Receiver, respectively, and ∆ 1 , ∆ 2 are finite sets of rules of Sender and Receiver, respectively. Ch = {r, l} is a fixed set of channel (names), r being reliable and l unreliable, so called "lossy".

A rule δ ∈ ∆ i is a tuple (q, c, α, q ) ∈ Q i × Ch × Act × Q i
where the set of actions Act contains tests R (checking whether the contents of c ∈ Ch belongs to R, a regular language) and communications w (sending a sequence of messages to c in the case of Sender's actions, reading it for Receiver's) and is thus given by Act

def = Reg(M) ∪ M * .
We write q R:c -→ q for a rule where the action is a test on c, and q c!w -→ q (resp., q c?w -→ q ) when the action is a communication by Sender (resp., by Receiver).

In graphical representations like Fig. 1, Sender and Receiver are depicted as two disjoint directed graphs, where states appear as nodes and where rules q α -→ q appear as edges from q to q with action and channel name labeling the edge. We may omit the label, or just use , for trivial tests, R = M * , or empty communications, w = ε.

Remark 2.1 (On separating tests from communications). Our definition requires that an action is a test or a communication. It does not allow performing both atomically inside a single step (but they can be chained using intermediary states). This choice, which is no real loss of generality, lets us focus on simulating tests by other constructs (or other tests) without having to account for accompanying communications.

Operational Semantics. The behaviour of S is defined via an operational semantics defined along standard lines.

A configuration of S = (Ch, M, Q 1 , ∆ 1 , Q 2 , ∆ 2 ) is a tuple C ∈ Conf S def = Q 1 × Q 2 × M * × M * . In C = (q 1 , q 2 ,
u, v), q 1 and q 2 are the current states of, respectively, Sender and Receiver, while u and v are the current contents of, respectively, r and l.

Rules give rise to transitions in the expected way. We start with so-called "reliable" steps where the effect of a rule is deterministic. Formally, given two configurations C = (q 1 , q 2 , u, v), C = (q 1 , q 2 , u , v ) and a rule δ = (q, c, α, q ), there is a reliable step denoted C δ -→ rel C if, and only if, the following four conditions are satisfied: states: q = q 1 and q = q 1 and q 2 = q 2 (for Sender rules), or q = q 2 and q = q 2 and q 1 = q 1 (for Receiver rules); tests: if δ is a test rule q R:c -→ q , then c = r and u ∈ R, or c = l and v ∈ R, and furthermore u = u and v = v; writes: if δ is a writing rule q c!w -→ q , then c = r and u = uw and v = v, or c = l and u = u and v = vw; reads: if δ is a reading rule q c?w -→ q , then c = r and u = wu and v = v, or c = l and u = u and v = wv . Now to unreliable, aka lossy, steps denoted C δ -→ los C . As is standard, a lossy step is defined as a combination of message losses (where the contents of l may be replaced with a subword) with a reliable step. For v 1 , v 2 ∈ M * , we write v 1 v 2 when v 1 is a subword of v 2 , i.e., a (scattered) subsequence. In particular, ε v 2 and v 2 v 2 for any v 2 . This is extended to configurations and we write C D when C = (q 1 , q 2 , u, v) and D = (q 1 , q 2 , u, v ) with v v . 4 We now define:

C δ - → los C def ⇔ ∃D, D : C D ∧ D δ - → rel D ∧ D C . (1)
In other words, a lossy step is a reliable step sandwiched between arbitrary message losses on l. In particular, reliable steps are a special case of lossy steps. In the rest of this paper, we consider reachability via lossy steps, and often write simply C δ -→ C without a "los" subscript. (When we refer to reliable steps and runs, we always use "rel" subscript.) Remark 2.2 (On reliable steps). As is usual with lossy channel systems, the reliable semantics plays a key role even though the object of our study is reachability via unreliable steps. First -→ rel is a normative yardstick from which the unreliable semantics depart: -→ los is defined as a modification of -→ rel . Then many hardness results on lossy systems are proved with reductions where a lossy system simulates in some way the reliable (and Turing-powerful) behaviour.

A run from C 0 to C n is a sequence of chained steps C 0

δ 1 - → C 1 δ 2 - → C 2 • • • δ n - → C n , abbre- viated as C 0 * - → C n (or C 0 + - → C n
when we rule out zero-length runs).

Definition 2.3. The Reachability Problem is the question, given a UCST S and some states p in ,

p fi ∈ Q 1 , q in , q fi ∈ Q 2 , whether S has a (lossy) run C in = (p in , q in , ε, ε) * - → C fi = (p fi , q fi , ε, ε).
The Extended Reachability Problem asks, further given regular languages U,V,U ,V ⊆ M * , whether there exist u ∈ U, v ∈ V , u ∈ U , and v ∈ V such that S has a (lossy) run

(p in , q in , u, v) * - → (p fi , q fi , u , v ).
In the following we only consider reachability problems with empty channels in C in and C fi since this is technically convenient. There is no loss of generality: Lemma 2.4. The extended reachability problem many-one reduces to the reachability problem.

Roughly speaking, we can transform an instance of the extended reachability problem to an "empty-channel" instance by letting Sender start with generating some u ∈ U, v ∈ V into the channels, and by letting Receiver read some u ∈ U , v ∈ V in the end.

The two problems are thus equivalent. Moreover, the reduction does not need to introduce any new tests, and the equivalence thus also holds for UCST's with restricted sets of tests which we will consider.

Testing channels and the undecidability of reachability

Despite their similarities, UCS's and LCS's (lossy channel systems) behave differently. The algorithms deciding reachability for LCS's can easily accommodate regular (or even more expressive) tests [START_REF] Baier | On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems[END_REF]Sect. 3.3]. By contrast, this section gives several versions of the following result: Theorem 3.1. Reachability is undecidable for UCST.

Simulating queue automata

We now show how even simple tests lead to undecidability. The main technique we use is to simulate queue automata which are a Turing-powerful model already with a single reliable channel.

UCS's already have a reliable channel but Sender (or Receiver) cannot both read and write from/to it. If Sender could somehow read from the head of r as well as write to its tail, it would be as powerful as a queue automaton. Now, with regular tests on channels, there exists a simple protocol making Receiver act as a proxy for Sender and implement read actions on its behalf.

Described informally, the protocol is the following5 :

1. Channel l is initially empty. 2. In order to "read" from r, Sender checks and records whether the length of the contents of r is odd or even, using a regular test on r. 3. It then sends on l the message, say a, that it wants to read. 4. It checks that (equivalently, waits until) the parity of the contents of r has changed, and on detecting this change, concludes that the read was successful. 5. Receiver waits in its initial q proxy (or q p ) state and tries to read from l. When it reads a message a from l, it understands it as an request telling it to read a from r on behalf of Sender. Once it has performed this read on r, it returns to q proxy and waits for the next instruction. 6. l is now empty and the simulation of a read by Sender is concluded.

If no messages are lost on l, the protocol allows Sender to read on r. If a message is lost on l, the protocol deadlocks. Also, Sender deadlocks if it attempts to read a message that is not at the head of r (it has to guess correctly). We note that these deadlocks do not make the simulation incorrect since we are only concerned with reachability. We further observe that in Fig. 1 only the sender uses tests, and only r is submitted to tests. We denote such restricted uses of tests by qualifying test sets like T with a subscript 1 (for Sender) or 2 (for Receiver), and/or by a superscript r or l. We can now state the following stronger form of Theorem 3.1:

Restricted sets of tests

Theorem 3.2. Reachability is undecidable for UCST[P r 1 ].
In the rest of this paper, we single out other simple test sets by letting:

Z def = {ε}, N def = M + , H a def = a.M * , H def = {H x | x ∈ M}.
In 1 by using two copies of the message alphabet, say using different colors. It alternates strictly between the two colors when writing on r. This requires an extra bit of memory, encoded in local states. Then the parity of the length of r contents can be tested by looking at the first message, using H r 1 tests, and comparing with the color of the last written message. (This assumes that r is never completely emptied, otherwise deadlocks will occur, but this is no loss of generality.) [START_REF] Atig | On the reachability analysis of acyclic networks of pushdown systems[END_REF] Simulating UCST[Z Z Z, , , N N N] by using Sender's emptiness tests only This section describes two simulations that, put together, entail Theorem 4.1.

Remark. The simulations are tailored to the reachability problem. They may not preserve, e.g., termination or deadlock-freedom.

Reducing UCST

[Z Z Z, , , N N N] to UCST[Z Z Z 1 1 1 , , , N N N 1 1 1 ]
We now explain how to eliminate Z and N tests by Receiver. W.l.o.g. we assume that x in c!x and c?x is always one symbol (x ∈ M), and we use two special new messages, "z" and "n", with which Sender will signal to Receiver about the status, empty or not, of the channels.

Formally, for S ∈UCST[Z, N], where S = ({r, l}, M,

Q 1 , ∆ 1 , Q 2 , ∆ 2 )
, we construct S arising from S as follows (see Fig. -→ p ; every receiver rule q Z:c -→ q testing emptiness of c is replaced by q c?z -→ q ; every receiver rule q N:c -→ q testing non-emptiness of c is replaced by q c?n

-→ q . q q ′ q ′′ Z : c N : c ′ p p ′ c!a S r l a ⇒ q q ′ q ′′ c?z c ′ ?n p p ′ p θ p 1 c p 2 c p 1 c ′ p 2 c ′ Z : c c!z Z : c ⊤ c!a c!n S ′
- → p θ c!n -→ p θ c!n -→ • • • c!n -→ p θ c!x
-→ p where the padding loop is used k o times; any Receiver's step q N:c -→ q is replaced by q c?n -→ q . Any original Receiver's step q Z:c -→ q , when Sender is in state p, is replaced with the sequence of steps corresponding to p Z:c

-→ p 1 c c!z -→ p 2 c , q c?z -→ q , p 2 c Z:c -→ p.
The inserted n's (and z's) are never lost; other message losses are the same as originally.

The "⇐" direction. Suppose a run C in * -→ los C fi of S . It is convenient to consider the run as a sequence of fine-grained steps, i.e., C in

δ 1 - → C 1 δ 2 - → C 2 δ 3 - → • • •C n-1 δ n - → C fi ,
where each step is either a reliable step C i-1 δ i -→ rel C i or the loss of a single message. The idea is to repeatedly switch two consecutive steps conveniently so that the validity of the obtained (fine-grained) runs is kept, with the aim to achieve a "straight run" which can be easily translated to a run C in * -→ los C fi of S. Imagine first that we give the priority to Sender's (reliable) steps: whenever some (current) δ i is a Receiver's step or a loss and δ i+1 is a Sender's step then we switch the steps if the result is still a valid run. It is easy to observe that the writing steps in the resulting run (in which no above switches are possible) are only in the segments corresponding to p -

→ p θ c!n -→ p θ c!n -→ • • • c!n -→ p θ c!x
-→ p (uninterrupted by Receiver or message losses). Regarding the steps corresponding to testing loops, we get segments p Z:c

-→ p 1 c c!z
-→ q or a loss of z. There is a final issue: we arrange that the finally achieved run is also "head-lossy", i.e. any loss-step loses the first message (the head) of l; thus we never have only n's in l when Sender tests the non-emptiness of l. It is then straightforward to translate the finally achieved run of S to the corresponding run of S.

Reducing UCST[Z

Z Z 1 1 1 , , , N N N 1 1 1 ] to UCST[Z Z Z 1 1 1 ]
When there are no receiver tests, N 1 tests can be eliminated by a buffering technique on Sender's side. With any S ∈UCST[Z 1 , N 1 ] we associate a derived system S as follows:

For each channel c ∈ Ch, S uses an auxiliary 1-place buffer between Sender and the channel c. In any S configuration, a buffer is empty (containing no messages) or full (containing a single message). Now the sender does not write to the channels, it can only directly write to the auxiliary buffers, and it may only write to a buffer when it is empty, making it full. Buffers may be nondeterministically flushed at any time, transferring their contents to the actual channel (in a potentially lossy way for l). Finally, the buffers are not actual extra peripherals, rather they are encoded in the finite control of Sender, which also simulates the lossy behavior of writing to channel l. Within this setup, an N c

1 test translates to "c's auxiliary buffer is full", and a Z c 1 test translates to "c's buffer is empty and c is empty".

Finally, S ∈UCST[Z 1 ] simulates S without any need of N 1 tests, as stated by the following lemma.

Reachability for UCST[Z Z Z l 1 1 1 ] via Post's Embedding Problem

This section develops a many-one reduction from the reachability problem for UCST[Z l 1 ] to PEP partial codir , a generalization of Post's Embedding Problem.

Definition 5.1 (Post embedding with partial codirectness [START_REF] Karandikar | Cutting through regular Post embedding problems[END_REF]). PEP partial codir is the question, given two finite alphabets Σ, Γ, two morphisms u, v : Σ * → Γ * , and two regular languages R, R ∈ Reg(Σ), whether there is σ ∈ R (called a solution) such that u(σ) v(σ), and such that furthermore u(σ ) v(σ ) for all suffixes σ of σ that belong to R . 6 The above definition uses the same subword relation, " ", that captures message losses. PEP partial codir can be compared with Post's Correspondence Problem, where the question is whether there exists σ ∈ Σ + such that u(σ) = v(σ).

Since PEP partial codir is decidable [START_REF] Karandikar | Cutting through regular Post embedding problems[END_REF], we deduce:

Corollary 5.2. Reachability is decidable for UCST[Z l 1 ].
The reduction from UCST[Z l 1 ] to PEP partial codir extends an earlier reduction from UCS to PEP [START_REF] Chambart | The ω-Regular Post Embedding Problem[END_REF]. Here the presence of Z l 1 tests creates new difficulties. We fix an instance S = ({r, l}, M,

Q 1 , ∆ 1 , Q 2 , ∆ 2 ), C in = (p in , q in , ε, ε), C fi = (p fi , q fi , ε, ε) of the reachability problem for UCST[Z l 1 ]. (We again assume x ∈ M in each c!x, c?x.) We construct a PEP partial codir instance P = (Σ, Γ, u, v, R, R ) intended to express the existence of a run from C in to C fi .
We first put Σ def = ∆ 1 ∪ ∆ 2 and Γ def = M so that words σ ∈ Σ * are sequences of UCST rules and their images u(σ), v(σ) ∈ Γ * are sequences of messages. With any δ ∈ Σ, we associate write_r(δ) defined by write_r(δ) = x if δ is a sender rule of the form . r!x -→ ., and write_r(δ) = ε in all other cases. This is extended to sequences with write_r(δ

1 • • • δ n ) = write_r(δ 1 ) • • • write_r(δ n ).
In a similar way we define write_l(σ) ∈ M * , the sequence written to l by the sequence σ, and read_r(σ) and read_l(σ), the sequences read by σ from r and l, respectively. We define E r ∈ Reg(Σ)

where E r def = E 1 ∪ E 2 and E 1 def ={δ ∈ Σ | write_r(δ) = read_r(δ) = ε} , E 2 def ={δ 1 • δ 2 ∈ Σ 2 | write_r(δ 1 ) = read_r(δ 2 ) = ε} .
In other words, E 1 gathers the rules that do not write to or read from r, and E 2 contains all pairs of sender/receiver rules that write/read a same letter to/from r.

Let now P 1 ⊆ ∆ * 1 be the set of all sequences of sender rules of the form

p in = p 0 .. - → p 1 .. - → p 2 • • • ..
-→ p n = p fi , i.e., sequences which take the sender state from p in to p fi . 7 Similarly, let P 2 ⊆ ∆ * 2 be the set of all sequences of receiver rules which take the receiver component from q in to q fi . Since P 1 and P 2 are defined by finite state systems, they are regular languages. We write P 1 P 2 to denote the set of all interleavings (shuffles) of 6 This problem is actually called PEP partial codir in [START_REF] Karandikar | Cutting through regular Post embedding problems[END_REF]. 7 I.e., all paths from p in to p fi in the directed graph of the sender, seeing rules as directed edges.

a word in P 1 with a word in P 2 . This operation is regularity-preserving, so P 1 P 2 ∈ Reg(Σ). Let Z l ⊆ ∆ 1 be the set of all sender rules which test the emptiness of l (which are the only test rules in S). We define R and R as the following regular languages:

R = E * r ∩ (P 1 P 2 ), R = Z l • ∆ 1 ∪ ∆ 2 * .
Finally, the morphisms u, v : Σ * → Γ * are given by u Proof. We first introduce a notion bridging the difference between runs of S and solutions of P . We call σ ∈ (∆ 1 ∪ ∆ 2 ) * a pre-solution if all the following conditions hold:

1. σ ∈ P 1 P 2 ; 2. read_r(σ) = write_r(σ); 3. read_r(σ 1 ) is a prefix of write_r(σ 1 ) for each prefix σ 1 of σ; 4. read_l(σ) write_l(σ); 5. for each factorization σ = σ 1 zσ 2 where z ∈ Z l we have read_l(σ 2 ) write_l(σ 2 ).

A pre-solution σ has a receiver-advancing switch if σ = σ 1 δδ σ 2 where δ is a sender rule, δ is a receiver rule, and σ = σ 1 δ δσ 2 is a pre-solution. A receiver-postponing switch is defined analogously, for δ being a receiver rule and δ being a sender rule.

It is obvious that if there is a pre-solution σ then there is an advance-stable presolution σ , which means that σ has no receiver-advancing switch; there is also a postpone-stable pre-solution σ which has no receiver-postponing switch.

Claim. Any advance-stable pre-solution σ is in E * r , and it is thus a solution of P .

Proof of the claim. Let us write an advance-stable pre-solution σ as σ 1 σ 2 where σ 1 is the longest prefix such that σ 1 ∈ E * r ; hence read_r(σ 1 ) = write_r(σ 1 ) by the definition of

E r = E 1 ∪ E 2 . Now suppose σ 2 = ε. Then σ 2 = δ 1 δ 2 • • • δ k where δ 1 ∈ E 1 . Since now σ 1 ∈ E *
r , hence read_r(σ 1 ) = write_r(σ 1 ), δ 1 must be of the form . Let us pick the smallest such that δ = .

r?x -→ . (which must exist by 2.) and note that ≥ 3 since σ 1 δ 1 δ 2 ∈ E * r . If we now pick the first j with 1 ≤ j ≤ -1 and such that δ j is a sender rule and δ j+1 is a receiver rule, switching δ j , δ j+1 leads again to a pre-solution (as can be checked by inspecting 1.-5.). This contradicts the assumption that σ is an advance-stable pre-solution.

Claim. Any postpone-stable pre-solution σ corresponds to a run

C in * - → C fi of S.
Proof of the claim. Consider a presentation σ = σ 1 σ 2 zσ 3 where z ∈ Z l , σ 2 contains no rules from Z l , and σ 1 is either empty or finishes with some z ∈ Z l ; recall that read_l(σ 2 zσ 3 ) write_l(σ 2 zσ 3 ) and read_l(σ 3 ) write_l(σ 3 ). We then must have read_l(σ 2 ) write_l(σ 2 ): otherwise we had σ 2 = σ δσ where δ is of the form . l?x -→ ., σ contains no l-reading rules and read_l(δσ zσ 3 ) write_l(σ 3 ); then switching the leftmost receiver-sender pair in δσ z would lead to a pre-solution, as can be easily checked. Moreover, in σ 2 each sender rule precedes all receiver rules. It is now easy to verify that there is a run C in

δ 1 - → C 1 δ 2 - → • • •C n-1 δ n - → C fi of S where δ 1 δ 2 • • • δ n = σ. Finally we observe that if C in δ 1 - → C 1 δ 2 - → • • •C n-1 δ n - → C fi is a run of S then σ = δ 1 δ 2 • • • δ n
is a pre-solution; then there is also an advance-stable pre-solution, i.e. a solution of P . On the other hand, if σ is a solution of P then σ is a pre-solution, and then there is a postpone-stable pre-solution, which corresponds to a run C in * -→ C fi of S. Proof (Idea). These reductions are easy and follow basically the same pattern: a UCST system nondeterministically guesses a solution and validates it. As an example, let us informally describe the simplest one and show how to solve a PEP partial dir instance with a UCST[Z r 1 ] system. We recall from [START_REF] Karandikar | Cutting through regular Post embedding problems[END_REF] that PEP partial dir is the question whether there is a σ ∈ R such that u(σ) v(σ) and furthermore u(σ ) v(σ ) for all prefixes of σ that belong to R (thus PEP partial dir and PEP partial codir are equivalent problems and one switches from one to the other by taking the mirror images of u, v, R, R ).

Actually, PEP

Given (Σ, Γ, u, v, R, R ) we build an UCST where Sender nondeterministically generates a σ ∈ R, sending u(σ) on channel r and v(σ) on channel l. A subword of v(σ) is written on l. Receiver checks that l and r contain exactly the same sequence of messages, that is, u(σ). Whenever the prefix of σ generated so far (call it σ ) is in R , Sender waits for r to be empty before going on with the generation of σ. This forces Receiver to match u(τ) with a prefix of v(τ), or more precisely, with a prefix of the subword of v(τ) that ends up in l after message losses may have occurred.

The other three reductions are similar.

6 Reducing UCST[Z Z Z 1 1 1 ] to UCST[Z Z Z l 1 1 1 ]
In this section we prove the decidability of reachability for UCST[Z 1 ] by reducing to UCST[Z l 1 ]. Since this involves eliminating Z tests on r, the configurations in which r is empty are of interest. For a UCST S, we let Conf r=ε be the subset of configurations (p, q, ε, v) in which r is empty. We abuse terminology and say that a subset W ⊆ Conf r=ε is regular if there are some state-indexed regular languages (V p,q ) p∈Q 1 ,q∈Q 2 in Reg(M) such that W = {(p, q, ε, v) | v ∈ V p,q }. Such regular subsets of Conf r=ε can be finitely represented using, e.g., regular expressions or finite-state automata.

We have put C = (p, q, u, v) C = (p , q , u , v ) iff p = p , q = q , u = u , and v v . Conf r=ε is thus a well-quasi order under , unlike Conf . 1 ], then Pre * (W ) is upward-closed and is computable uniformly from S and W . Proof (Sketch). That Pre * (W ) is upward-closed is an immediate consequence of the definition of lossy steps in Eq. [START_REF] Brand | On communicating finite-state machines[END_REF]. That it is computable from S and W is more interesting: this is an application of the VJGL Lemma: "an upward-closed set U is computable if one can decide C ∈ U and V ∩U = ∅ for arbitrary configurations C and regular sets V " (see [START_REF] Goubault-Larrecq | On a generalization of a result by Valk and Jantzen[END_REF]Theorem 2] for details). Here the two questions, "C ∈ U?" and "V ∩U = ∅?", i.e., "C * -→ W ?" and "U * -→ W ?", reduce to instances of the extended reachability problem for UCST[Z l 1 ], hence are decidable. Theorem 6.2. Reachability is decidable for UCST

W ⊆ Conf r=ε is upward-closed (in Conf r=ε ) if C ∈ W , C C and C ∈ Conf r=ε imply C ∈ W . It is downward-closed if Conf r=ε W is upward-closed. The upward- closure ↑W of W ⊆ Conf
[Z 1 ]. Proof (Sketch). Given a UCST[Z 1 ] S, a run π = C in * - → C fi can be presented in the form (C in =) C 0 * - → S D 1 Z:r -→ C 1 * - → S D 2 Z:r -→ C 2 • • • * - → S D m (= C fi )
where the D i -→ C i steps gather all occurrences of Z r 1 tests: note that necessarily D i and C i are in Conf r=ε . The C i-1 * -→ S D i subruns can be seen as runs of a new system S , which is obtained from S by removing all Z r 1 testing rules from ∆ 1 . The point is that we can apply Lemma 6.1 to S since it is a UCST[Z l 1 ]. So for k = 0, 1, . . ., we define T k and T k by letting T 0 = ↑C fi , T k = Pre * S (T k ) and

T k+1 = T k ∪ {C | ∃D ∈ T k : C Z:r
-→ D} (note that T k is defined with a Pre * S restricted to S ). T k collects all configurations C ∈ Conf r=ε from which one can reach T 0 with at most k uses of a Z : r test. We observe that all T k , T k are upward-closed subsets of Conf r=ε , that T k is computable from T k by Lemma 6.1, and that T k+1 is obviously computable from T k and T k . Furthermore, the T k 's are increasing:

T 0 ⊆ T 1 ⊆ • • • T k ⊆ T k+1
= k∈N T k , there is n such that T n = T n+1 = T ω . Since there is a run C in * - → C fi of S iff C in ∈ T ω , the proof is finished.
Observe that Lemma 6.1 and Theorem 6.2 exhibit a Turing reduction (from reachability for UCST[Z 1 ] to reachability for UCST[Z l 1 ]) and not a many-one reduction like all the other reductions in this paper.

With the results of sections 4 and 5, one obtains the following corollary. (see [START_REF] Schmitz | Multiply-recursive upper bounds with Higman's lemma[END_REF][START_REF] Karandikar | Cutting through regular Post embedding problems[END_REF]), our reductions prove that reachability for UCST[Z, N] is at level F ω ω in the extended Grzegorczyck hierarchy, and at level F ω m-1 , where m = |M|, when we restrict to systems with a fixed-sized alphabet of messages.

7 Some undecidable problems for UCST[Z Z Z, , , N N N]

The main result of this paper is that reachability is decidable for UCST[Z, N] (Theorem 6.3). In this section we argue that emptiness and non-emptiness tests strictly add to the expressive power of UCS's. This point is made in two different ways.

We start with recurrent reachability. Formally, the Recurrent Reachability Problem asks whether a given S has an infinite run C in

+ - → (p, q, u 1 , v 1 ) + - → (p, q, u 2 , v 2 ) + - → • • • visiting infinitely often a given control pair (p, q) ∈ Q 1 × Q 2 (
but with no constraints on channel contents). Proof (Idea). We prove Theorem 7.1 by reducing from the undecidable question whether a length-preserving string rewrite system (aka semi-Thue system) has a loop x + -→ x. We design a UCST S where Sender guesses a word y 0 , writes it on l, and then guesses pairs x i , y i for i = 1, 2, . . . such that each x i -→ y i is a rewrite step. It writes x i on r and y i on l. Receiver's job is to check that y i-1 = x i . With Z r 1 tests, Sender can wait for a check on x i to be concluded before issuing the next pair. This way we ensure progress of the checking phase and avoid confusion between pairs if a separator is lost. Since the rewrite system is length-preserving, any infinite run of S must eventually stop losing messages and witness a loop.

Since recurrent reachability is decidable for UCS (see [START_REF] Chambart | The ω-Regular Post Embedding Problem[END_REF]), Theorem 7.1 shows that Z tests, even just Z r 1 tests, cannot be simulated in UCS's.

As another illustration, we consider UCST's with write-lossy semantics, that is, UCST's with the assumption that messages are only lost during steps that (attempt to) write them to l. Once they are in l, they are never lost. This is formalized via a new transition relation C -→ wrlo C (definition omitted, but as expected) that is intermediary between -→ rel and -→ los . In many cases the two lossy semantics coincide: Remark 7.4. Write-lossy semantics is meaningful when modeling unreliability of the writing actions as opposed to unreliability of the channels. However, in the literature, write-lossy semantics is mostly used as a way of restricting the nondeterminism of lossy channel systems without losing any essential generality, as stated by Lemma 7.2.

Write-lossy and (plain) lossy semantics do not coincide when N tests are allowed. In fact, Theorem 6.3 does not extend to write-lossy systems.

Theorem 7.5. Reachability is undecidable for UCST[Z l 1 , N l 1 ] with write-lossy semantics.

Proof (Idea). As before, Sender simulates queue automata using tests and the help of Receiver. See Fig. 3. Channel l is initially empty. To read a from r, Sender does the following: (1) write a on l; (2) check that l is nonempty (hence the write was not lost);

(3) check that, or wait until, l is empty. Meanwhile, Receiver reads identical letters from r and l.

Conclusion

UCS's are communicating systems where a Sender can send messages to a Receiver via one reliable and one unreliable, lossy, channel, but where no direct communication is possible in the other direction. We introduced UCST, an extension of UCS's where steps can be guarded by tests, i.e., regular predicates on channel contents. This extension introduces limited but real possibilities for synchronization between Sender and Receiver. For example, Sender (or Receiver) may use tests to detect whether the other agent has read (or written) some message. As a consequence, adding tests leads to undecidable reachability problems in general. Our main result is that reachability remains decidable when only emptiness and non-emptiness tests are allowed. The proof goes through a series of reductions from UCST[Z, N] to UCST[Z l 1 ] and finally to PEP partial codir , an extension of Post's Embedding Problem that was motivated by the present paper and whose decidability was recently proved by the last two authors [START_REF] Karandikar | Cutting through regular Post embedding problems[END_REF].

We see two main directions for future works:

1. The limits of decidability: is it possible to characterize precisely the families of tests T ⊆ Reg(M) for which UCST[T ] has a decidable reachability problem? We gave positive and negative examples, but a precise characterization would help understand the phenomenon at hand. 2. Beyond reachability: we focused on reachability questions since they are the most natural starting point as far as verification is concerned. However several other natural verification problems, e.g., termination, are known to be decidable for UCS's.

Fig. 1 .

 1 Fig. 1. Unidirectional channels: Sender on the right, Receiver on the left

  In the above reduction only parity tests were used. When T ⊆ Reg(M), we write UCST[T ] to denote the class of UCST's where only tests belonging to T are allowed. Thus UCST and UCS coincide with UCST[Reg(M)] and UCST[∅], respectively. More interestingly, defining Odd, Even ∈ Reg(M) with Even def = (M.M) * and Odd def = M.Even, and letting P def = {Even, Odd} denote the parity tests, section 3.1 shows that reachability is undecidable already for UCST[P].

Theorem 4 . 1 .

 41 Reachability for UCST[Z, N] many-one reduces to reachability for UCST[Z 1 ].

, p 2 c-

 2 2): -S uses the special new messages z, n, and it thus has alphabet M def = M ∪ {n, z}; for each channel c ∈ {r, l} and each sender state p ∈ Q 1 we add new states p 1 c and an "(emptiness) testing loop" p for every sender rule θ of the form p c!x -→ p we add a new state p θ , and the rule is replaced in S by the following three rules: p -→ p θ , p θ c!n -→ p θ (a "padding loop"), and p θ c!x

Fig. 2 .

 2 Fig. 2. From S to S : eliminating Receiver's N and Z tests

Lemma 4 . 3 (

 43 Correctness of the reduction). S has a run C in * -→ los C fi if, and only if, S has a run C in * -→ los C fi (where C in and C fi are the configurations in S corresponding to C in and C fi with empty auxiliary buffers).

def = read_l and v def = write_l. Lemma 5 . 3 (

 53 Correctness). S has a run C in * -→ C fi iff P has a solution.

  (to keep 3.).

  partial codir and UCST[Z l 1 ] are equivalent (inter-reducible) problems: Theorem 5.4. PEP partial codir many-one reduces to the Reachability Problem for UCST[Z c i ] for any i ∈ {1, 2} and c ∈ Ch.

  r=ε is the smallest upward-closed set that contains W . A wellknown consequence of Higman's Lemma is that upward-closed and downward-closed subsets of Conf r=ε are regular, and that upward-closed subsets can be canonically represented by their finitely many minimal elements.For W ⊆ Conf r=ε , we let Pre * (W ) def = {C ∈ Conf r=ε | ∃D ∈ W : C * -→ D}: observe that Pre * (W ) only contains configurations with empty r. Lemma 6.1. If W is an upward-closed subset of Conf r=ε and if S is a UCST[Z l

Theorem 6 . 3 .Remark 6 . 4 (

 6364 Reachability is decidable for UCST[Z, N]. On complexity). Based on known results on the complexity of PEPpartial codir

Theorem 7 . 1 .

 71 Recurrent reachability is undecidable for UCST[Z r 1 ].

Lemma 7 . 2 .Corollary 7 . 3 .

 7273 Assume S is a UCST[Z] system. Then C in * -→ los C fi iff C in * -→ wrlo C fi . Proof (Idea). Prove that C δ -→ los C iff D δ -→ wrlo C for some D C. Deduce C in n+1 --→ los C iff C in n+1 --→ wrlo Cby induction on n. See [18, App. A]. Reachability is decidable for UCST[Z] with write-lossy semantics.

Fig. 3 .

 3 Fig. 3. Write-lossy Sender simulates "p 1 r?a -→ p 2 " with N and Z tests and proxy Receiver

  in that their outcome depends on the entire contents of a channel. With H tests, only one message at the head needs be scanned. Still, "local" H tests are sufficient for undecidability:

	Theorem 3.3. Reachability is undecidable for UCST[H r 1 ].
	Proof (Idea). Sender can simulate parity tests P r

other words, Z is the emptiness (or "zero") test, N is the non-emptiness test and H are the head tests (that allow checking what is the first message in a channel without consuming it). Note that non-emptiness tests can be simulated with head tests, hence are weaker. Below we abuse notation and, when R, R ∈ Reg(M * ), we write UCST[R] and UCST[R, R ] rather than UCST[{R}] and UCST[{R, R }].

One difference with parity tests and the Z, N, H tests is that parity tests are "global"

  • • • . Since they are upward-closed, they eventually stabilize by the well-quasi-ordering property: letting T ω

	def

Note that (Conf , ) is not a well-quasi-order since C D requires equality on channel r.

We describe the protocol informally but Fig. 1 page 2 depicts exactly how Receiver implements a proxy on M = {a, b, c} and how Sender simulates a rule p 1 r?a -→ p 2 for a queue automaton.

Supported by the European Regional Development Fund in the IT4Innovations Centre of Excellence project (CZ.1.05/1.1.00/02.0070), and by the project GA ČR:P202/11/0340. Partially funded by Tata Consultancy Services. Currently visiting Oxford Univ. Comp. Sci. Dept, supported by Grant ANR-11-BS02-001 and by the Leverhulme Trust.

-→ p 2 c , σ, p