{'fraction_non_alphanumeric': 0.04736842105263158, 'fraction_numerical': 0.009143754909662216, 'mean_word_length': 4.097381276527589, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 33, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Detecting Unrealizability of Distributed Fault-tolerant Systems

Writing formal specifications for distributed systems is difficult. Even simple consistency requirements often turn out to be unrealizable because of the complicated information flow in the distributed system: not all information is available in every component, and information transmitted from other components may arrive with a delay or not at all, especially in the presence of faults. The problem of checking the distributed realizability of a temporal specification is, in general, undecidable. Semi-algorithms for synthesis, such as bounded synthesis, are only useful in the positive case, where they construct an implementation for a realizable specification, but not in the negative case: if the specification is unrealizable, the search for the implementation never terminates. In this paper, we introduce counterexamples to distributed realizability and present a method for the detection of such counterexamples for specifications given in linear-time temporal logic (LTL). A counterexample consists of a set of paths, each representing a different sequence of inputs from the environment, such that, no matter how the components are implemented, the specification is violated on at least one of these paths. We present a method for finding such counterexamples both for the classic distributed realizability problem and for the fault-tolerant realizability problem. Our method considers, incrementally, larger and larger sets of paths until a counterexample is found. For safety specifications in weakly ordered architectures we obtain a decision procedure, while counterexamples for full LTL and arbitrary architectures may consist of infinitely many paths. Experimental results, obtained with a QBF-based prototype implementation, show that our method finds simple errors very quickly, and even problems with high combinatorial complexity, like the Byzantine Generals' Problem, are tractable.


Introduction
The goal of program synthesis, and systems engineering in general, is to build systems that satisfy a given specification. Sometimes, however, this goal is unattainable, because the conditions of the specification are impossible to satisfy in an implementation. A textbook example for such a case is the Byzantine Generals' Problem, introduced in the early 1980s by Lamport et al. [LSP82]. Three generals of the Byzantine army, consisting of one commander and two lieutenants, need to agree on whether they should "attack" or "retreat." For this purpose, the commander sends an order to the lieutenants, and all generals then exchange DETECTING UNREALIZABILITY OF DISTRIBUTED FAULT- TOLERANT SYSTEMS 3 In both examples, a finite set of input sequences suffices to force the system into violating the specification on at least one of the input sequences. In this paper, we present an efficient method for finding such counterexamples. It turns out that searching for counterexamples is much easier than the classic synthesis approach of establishing unrealizability by the nonexistence of strategy trees [PR90,KV01b,FS05]. The difficulty in synthesis is to enforce the consistency condition that the strategy of a process must act the same way in all situations the process cannot distinguish. On the strategy trees, this consistency condition is not an ωregular (or even decidable) property. When analyzing a counterexample, on the other hand, we only check consistency on a specific set of sequences, not on a full tree. This restricted consistency condition is an ω-regular property and can, in fact, simply be expressed in LTL as part of the temporal specification. Our QBF-based prototype implementation finds counterexamples for the Byzantine Generals' Problem and the CAP Theorem within just a few seconds.
Related Work. To the best of the authors' knowledge, there has been no attempt in the literature to characterize unrealizable specifications for distributed systems beyond the restricted class of architectures with decidable synthesis problems, such as pipelines and rings [KV01b,FS05]. By contrast, there is a rich literature concerning unrealizability for open systems, that is, single-process systems interacting with the environment [Chu63, ALW89,KV97]. Schuppan [Sch12] introduced the notion of unrealizable cores to identify a minimal subformula that contains the reason for unrealizability. In robotics, there have been recent attempts to analyze unrealizable specifications [RKG11]. The results are also focused on the reason for unrealizability, while our approach tries to determine if a specification is unrealizable. Moreover, they only consider the simpler non-distributed synthesis of GR(1) specifications, which is a subset of LTL. There are other approaches concerning unrealizable specifications in the non-distributed setting that also use counterexamples [CHJ08,LDS11]. There, the system specifications are assumed to be correct and the information from the counterexamples are used to modify environment assumptions in order to make the specifications realizable. The Byzantine Generals' Problem is often used as an illustration for knowledge-based reasoning in epistemic logics, see [HM84] for an early formalization. Concerning the synthesis of fault-tolerant distributed systems, there is an approach to synthesize fault-tolerant systems in the special case of strongly connected architectures [DF09]. A preliminary version of this paper appeared as [FT14]. The present paper extends our earlier work by removing restrictions to acyclic architectures and providing a completeness result for safety specifications and weakly ordered architectures, as well as a general encoding of fault-tolerant synthesis.

Distributed Realizability
A specification is realizable if there exists an implementation that satisfies the specification. For distributed systems, the realizability problem is typically stated with respect to a specific system architecture. Figure 1 shows some typical example architectures: an architecture consisting of independent processes, a pipeline architecture, and a join architecture. The architecture describes the communication topology of the distributed system. For example, an edge from p 1 to p 2 labeled with (x, b) indicates that x and b are shared variables between processes p 1 and p 2 , where p 1 writes to x and p 2 reads from b. The classic distributed realizability problem is to decide whether there exists an implementation (or strategy) for each process in the architecture, such that the joint behavior satisfies the specification. In this case, the distinction between the shared variables is unnecessary as the valuation of the variable that is read from is always equal to the valuation of the variable that is written to. In this paper, we are furthermore interested in the synthesis of fault-tolerant distributed systems, where the processes and the communication between processes may become faulty. Here, the distinction of the shared variables is used to model the different types of faults.
Coordination Logic. We use Coordination logic (CL) [FS10] to give uniform and precise definitions of the various realizability problems of interest. CL is a game-based extension of LTL that makes strategies-and their observations-to first class citizens of the logic. CL divides the set of atomic propositions into strategic and coordination variables, where the latter represent observations for the strategies represented by strategic variables. The strategy quantifier ∃C ⊲ s introduces a strategy for s that bases its decisions only on the history of valuations of the variables in C. This allows us to pose queries on the existence of strategies, with specific observations, within the logic. In order to specify the realizability of distributed systems, we use the strategy quantifier ∃C ⊲ s to express the existence of an implementation for a process output s based on input variables C.
y c a a (c) Figure 1: Example architectures CL Syntax. CL formulas contain two types of variables: the set C of input (or coordination) variables, and the set S of output (or strategy) variables. In addition to the usual LTL operators Next , Until U , and Release R, CL has the strategy quantifier ∃C ⊲ s, which introduces an output variable s whose values must be chosen based on the history of valuations of the inputs C. The syntax 1 is given by the grammar where x ∈ C∪ S, C ⊆ C, and s ∈ S. Beside the standard abbreviations true ≡ x ∨ ¬x, false = x ∧ ¬x, ϕ ≡ true U ϕ, and ϕ ≡ false R ϕ, we use n ϕ as an abbreviation of n consecutive Next operators.
We denote by Q the (possibly empty) quantification prefix of a formula and call the remainder the body. For Q ∈ {∃, ∀}, we use Q Q if the prefix contains only Q-quantifiers. For the purposes of this paper, it suffices to consider the fragment CL ∃ that contains only existential quantifiers. We furthermore assume that the body is quantifier-free, i.e., that the formulas are in prenex normal form (PNF).
Examples. We demonstrate how to express distributed realizability problems in CL ∃ with the example architectures from Fig. 1. The realizability of an LTL formula ψ 1 in the architecture from Fig. 1(a) is expressed by the CL ∃ formula ∃{a} ⊲ x. ∃{b} ⊲ y. ψ 1 . (2.1) Interprocess communication via a shared variable b, as in the pipeline architecture from Fig. 1(b), is expressed by separating the information read from b from the output written to b. In the following CL ∃ formula we use output variable x to denote the output written to b: 2) The LTL specification ψ 2 is qualified by the input-output specification (b = x), which expresses that ψ 2 is required to hold under the assumption that the information written to b by process x is also the information read from b by process y. This separation between sent and received information is useful to model faults that disturb the transmission. Failing processes are specified by omitting the input-output specifications that refer to the failing processes. As an example, consider the architecture in Fig. 1(c). The CL ∃ formula specifies that there exists an implementation such that ψ 3 is guaranteed to hold even if process x or y (but not both) fails.  For a formula Φ, we differentiate two types of coordination variables, external and internal. A coordination variable c ∈ C is internal iff the value of c is uniquely defined by the input-output specifications. In contrast, external coordination variables provide input from the environment. For example, the input a in (2.2) is external while b is internal.
CL ∃ Semantics. We give a quick definition of the CL ∃ semantics for formulas in PNF and refer the reader to [FS10] for details and for the semantics of full CL. The semantics is based on trees as a representation for strategies and computations. Given a finite set of directions Υ and a finite set of labels Σ, a (full) Σ-labeled Υ-tree T is a pair Υ * , l , where l : Υ * → Σ assigns each node υ ∈ Υ * a label l(υ). For two trees T and T ′ , we define the joint valuation T ⊕ T ′ to be the widened tree with the union of both labels. We refer to [FS10] for a formal definition. A path σ in a Σ-labeled Υ-tree T is an ω-word σ 0 σ 1 σ 2 . . . ∈ Υ ω and the corresponding labeled path σ T is (l(ǫ), σ 0 )(l(σ 0 ), σ 1 )(l(σ 0 σ 1 ), For a strategy variable s that is bound by some quantifier QC ⊲ s. ϕ, we refer to C as the scope of s, denoted by Scope(s). The meaning of a strategy variable s is a strategy or implementation f s : (2 Scope(s) ) * → 2 {s} , i.e., a function that maps a history of valuations of input variables to a valuation of the output variable s. We represent the computation of a strategy f s as the tree (2 Scope(s) ) * , f s where f s serves as the labeling function (cf. Fig. 2(a)-(b)). CL ∃ formulas are interpreted over computation trees, that are the joint valuations of the computations for strategies belonging to the strategy variables in S, i.e., s∈S (2 Scope(s) ) * , f s (cf. Fig. 2(c)). Given a CL ∃ formula Q ∃ . ϕ in prenex normal form over strategy variables S and coordination variables C, the formula is satisfiable if there exists a computation tree T (over S), such that all paths in T satisfy the LTL formula ϕ, i.e., ∀σ ∈ (2 C ) ω . σ T , 0 LTL ϕ.
From Distributed Realizability to CL ∃ . We formally introduce the distributed realizability problem and show reductions from the distributed realizability problem to CL ∃ . Let V be a finite set of variables. An architecture A is a tuple (P, p env , {I p } p∈P , {O p } p∈P ), where P is the set of processes and p env / ∈ P is the distinct environment process. I p ⊆ V denotes the set of input variables for process p and O p ⊆ V denotes the set of output variables for process p. We denote by I = p∈P I p the set of all input variables and by O = p∈P O p the set of all output variables. The input given by the environment is I env := I \ O, the communication variables are I ∩ O. While some input may be shared across processes in the case of broadcasting, the output variables of every pair of processes are assumed to be disjoint, i.e., O p ∩ O p ′ = ∅ for all p = p ′ ∈ P . We represent the architecture A by a directed graph G A = (N, E), where N = P ∪ P env is the set of vertices and E = N × N the set of edges. There is an edge between two vertices (p, p ′ ) ∈ E if O p ∩ I p ′ , i.e., there is a communication over shared variables between p and p ′ .
An implementation of a process p is a function f p : (2 Ip ) * → 2 Op which maps the history of valuation of the input variables to a subset of output variables. We say an implementation is finite state, if it can be represented by a finite transducer. An implementation for A is a set of implementations for each process. The distributed realizability problem for architecture A and LTL formula ϕ is to decide whether there is a finite state implementation for every process in A such that the system satisfies ϕ against the environment, i.e., the joint behavior of the implementations satisfies ϕ against all input sequences given by the environment: The distributed realizability problem is decidable for the class of weakly ordered architectures [FS05], which includes pipelines and rings. Weakly ordered architectures are characterized by the absence of pairs of processes, called information forks, that each have access to some information that is hidden from the other process. Consider a tuple (P ′ , V ′ , p, p ′ ), where P ′ is a subset of the processes P ∪ {p env }, V ′ is a subset of the variables disjoint from I p ∪ I p ′ , and p, p ′ ∈ P (P ′ ∪ {p env }) are two different system processes. Such a tuple is an information fork if P ′ together with the edges that are labeled with at least one variable from V ′ forms a subgraph rooted in the environment and there exist two nodes q, q ′ ∈ P ′ that have edges to p, p ′ , respectively, but are labeled with incomparable sets of variables (i.e., neither set is a subset of the other). For example, the architecture in Fig. 1(a) contains the information fork ({p env }, ∅, p 1 , p 2 ). A weakly ordered architecture is an architecture that does not contain an information fork.
Definition 2.1. Given a CL ∃ formula Φ = Q ∃ . ϕ path → ϕ, where ϕ path = (s,c)∈R (c = s) for some R ⊆ C × S, the induced architecture A Φ = (P, p env , {I p } p∈P , {O p } p∈P ) is defined as follows. By abuse of notation, we use V = S ∪ C as the set of variables in the architecture and define a process p ∈ P as a set of strategy variables p ⊆ S.
Let P be the quotient of S according to the equivalence relation ⊆ (S × S) with s s ′ if Scope(s) = Scope(s ′ ), i.e., we group the strategy variables with the same inputs together as a single process. For all p ∈ P , we define I p as Scope(s) for some s ∈ p and O p as the union over the defined communication variables {c | (s, c) ∈ R for some s ∈ p} and the strategy variables that are not used for communication {s | (s, c) / ∈ R for all c ∈ C}.
Theorem 2.1. The distributed realizability problem over architecture A and LTL formula ϕ can be encoded as CL ∃ formula Φ = Q ∃ . ϕ path → ϕ with only prenex existential quantification.
Proof. Consider an arbitrary architecture A = (P, p env , {I p } p∈P , {O p } p∈P ) and an LTL formula ϕ. We give a CL ∃ formula Φ that is satisfiable if, and only if, ϕ is realizable in A.
For variable v ∈ V , we denote the coordination variable and strategy variable used in the encoding by c v and s v , respectively. Analogously we use C := {c v | v ∈ I} as the set of coordination variables and S := {s v | v ∈ O} as the set of strategy variables. For each process p ∈ P we introduce a set of strategy variables S p := {s v | v ∈ O p } with the scope C p := {c v | v ∈ I p }. We take care of the input-output specifications by restricting the paths such that ϕ path := v∈I∩O (c v = s v ) holds, i.e., we only consider paths where the valuation of the strategy variables S representing the output variables is equal to the 8 FINKBEINER AND TENTRUP valuation of the coordination variables I ∩ O representing the input variables. The resulting formula Φ for processes p 1 , . . . , p n is The correctness of the encoding follows from the semantics of CL ∃ and A = A Φ .
Realizability under Byzantine faults. We model the occurrence of a Byzantine fault as a modification of the architecture, where a process reading from some shared variable no longer reads the output written by the other process, but instead some arbitrary input. An implementation is fault-tolerant if it works both in the original architecture and in the modified architecture. We encode fault-tolerant realizability as CL ∃ formulas of the general where the formulas ϕ path i are obtained from ϕ path by omitting constraints (c = s), which indicates that there is a Byzantine fault on the shared variable s: the coordination variable c can deviate arbitrarily from s. A disadvantage of this encoding is that we can no longer partition the coordination variables into internal and external variables, because the coordination variable c is external in the architecture where the shared variable is faulty and internal in the other architectures. In order to retain the partitioning, we use the following satisfiability preserving transformation partition(Φ): For each coordination variable c that is neither internal nor external, we introduce a fresh coordination variable c * that represents the external information given in the fault architectures. Consequently, we add the condition (c = c * ) to all path specifications ϕ path i where c is not contained, thus, making the value c deterministic in all architectures. In the transformed formula partition (Φ), c is an internal coordination variable as its value is in every architecture uniquely determined and c * is an external coordination variable as it provides environmental input to the system.

Counterexamples to Distributed Realizability
We now introduce counterexamples to realizability, which are actually counterexamples to satisfiability for the CL ∃ formula encoding the realizability problem. The satisfiability problem for a CL ∃ formula in prenex form asks for an implementation for all strategy variables in the quantification prefix of the formula such that the temporal specification in the body is satisfied.
Let Φ = Q ∃ . ϕ be a CL ∃ formula in prenex form over coordination variables C and strategy variables S, where the body of the formula is the LTL formula ϕ. A counterexample to satisfiability for Φ is a (possibly infinite) set of paths P ⊆ (2 C ) ω , such that, no matter what strategies are chosen for the strategy variables in S, there exists a path σ ∈ P that violates the body ϕ. Formally, P ⊆ (2 C ) ω is a counterexample to satisfiability iff, for each s ∈ S and every strategy f s : (2 Scope(s) ) * → 2 {s} , it holds that there exists a path σ ∈ P such that σ T LTL ¬ϕ where T = s∈S (2 Scope(s) ) * , f s .
Proposition 3.1. A CL ∃ formula Φ over coordination variables C and strategy variables S is unsatisfiable if, and only if, there exists a counterexample to satisfiability P ⊆ (2 C ) ω .
Proof. By the semantics of CL ∃ and P = (2 C ) ω .

DETECTING UNREALIZABILITY OF DISTRIBUTED FAULT-TOLERANT SYSTEMS 9
The distributed realizability problem without faults corresponds to CL ∃ formulas of the form Φ = Q ∃ . ϕ path → ϕ, where the ϕ path defines the architecture A Φ : there is an edge from one strategy variable to another if the input-output specification occurs in ϕ path . A finite counterexample to satisfiability of Φ is a finite set of paths P ⊆ (2 Cext ) ω corresponding to external coordination variables C ext = {c | c is an external coordination variable in Φ}, such that for every implementation T there exists a path σ ∈ P such that an extension Note that the extension of σ by the valuation of the internal coordination variables is uniquely specified by the input path σ and the system implementation T .
Proposition 3.2. A CL ∃ formula Φ = Q ∃ . ϕ path → ϕ over coordination variables C and strategy variables S is unsatisfiable if there exists a finite counterexample to satisfiability P ⊆ (2 Cext ) ω of Φ.
As an example consider again the CL ∃ formula (2.1) ∃{a} ⊲ x. ∃{b} ⊲ y. ψ 1 , corresponding to the architecture from Fig. 1(a) in the previous section. Let ψ 1 := ( y ↔ a), i.e., y must output the input a with an one-step delay. A simple counterexample for this formula consists of two paths P 1 := { ∅ ω , {a} ω } that differ in the values of a, but not in the values of b. Since process y cannot distinguish the two paths, but must produce different outputs, this leads to contradiction. Consider the same formula ψ 1 for the pipeline architecture specified by The formula is unsatisfiable due to the delay when forwarding the input a over shared variable b (cf. CL ∃ semantics in Section 2, the current output of x is only visible to y in the next step). P 1 is a finite counterexample in this case, too: Given an implementation of x and y, we extend both paths such that the input-output specification (b = x) is satisfied.
The fault-tolerant distributed realizability problem corresponds to CL ∃ formulas of the form Φ = Q ∃ . 1≤i≤n ϕ path i → ϕ i . If ϕ i = ϕ for all i, the formula states that there exists an implementation such that the specification ϕ should hold in all architectures induced by the path specifications ϕ path i . Omitted specifications (b = x) in one of these formulas ϕ path i represent an arbitrary communication error at input b in architecture i. In this case, a counterexample identifies for each implementation one of these architectures where a contradiction occurs. A finite counterexample to satisfiability of Φ are n finite sets of paths P i ⊆ (2 C i ext ) ω each corresponding to external coordination variables C i ext in the respective architecture i, such that for any implementation T there exists an architecture j and a path σ ∈ P j such that an extension σ ′ ∈ (2 C ) ω of σ violates ϕ j .
introduces paths for inputs as well as for every faulty node such that some paths model the exact input-output specification and other paths model the arbitrary node failures. The node that reads from a shared variable can, in contrast to incomplete information, react differently on the given paths, but the reaction must be consistent regarding its observations on all paths. Consider for example the specification ψ 3 := ( 2 z ↔ a) for the CL formula in (2.3), that is, process z should output the input a of nodes x and y. In both architectures, depicted in Fig. 3, we introduce additional paths for the coordination variable that is omitted in the input-output specification, i.e., b and c for the first and second conjunct, respectively. Process z cannot tell which of its inputs come from a faulty node. Since z must produce the same output on two paths it cannot distinguish, the implementation of z contradicts the specification in either architecture.

Computing Finite Counterexamples
We encode the existence of finite counterexamples to realizability as a formula of quantified propositional temporal logic (QPTL) [KP95]. QPTL extends LTL with a path quantifier ∃p, where a path σ ∈ 2 Σ satisfies ∃p. ϕ at position i ≥ 0, denoted by σ, i QPTL ∃p. ϕ, if there exists a path σ ′ ∈ 2 Σ∪{p} which coincides with σ except for the newly introduced atomic proposition p, such that σ ′ , i QPTL ϕ. We define the universal path quantifier ∀p. ϕ as ¬∃p. ¬ϕ. In the following encoding, we use the path quantifier to explicitly name the paths in the counterexample.
Distributed Realizability. We consider first the distributed realizability problem, represented by CL ∃ formula Φ = Q ∃ . ϕ path → ϕ. Before proceeding with the general encoding, we show an example query that encodes the existence of a counterexample to satisfiability by using two external paths, represented by the path variables a 1 and a 2 . The QPTL query is This query is satisfiable, one satisfying assignment for a 1 and a 2 is {a 1 }∅ ω and ∅ ω , respectively. The assignments for b i is a (alpha renamed) copy of the assignment for x i , satisfying the condition (b i = x i ) for i ∈ {1, 2}. As already mentioned in the previous section, the value of b i is uniquely determined by the strategies. Thus, we could optimize the query by removing b i altogether. However, we need the distinction between reading and writing variables later in this section. The valuations of a 1 and a 2 represent two paths in the computation tree of the original CL ∃ formula. In the query above, the strategies for x and y are also evaluated on these two paths. To make the connection between the path variables x 1 and x 2 and the strategy variable x, we introduce consistency conditions between all paths considered in the query. These consistency conditions (4.1) state that valuations of universal path variables are only valid if they can be generated by the corresponding strategy. For example, the consistency condition for x, (x 1 = x 2 R a 1 = a 2 ), states that a 1 and a 2 must be different in some step i ≥ 0 before x 1 and x 2 can be different in some step j > i. Hence, according to (4.1), x 1 = x 2 and y 1 = y 2 hold in the first step. As b 1 = b 2 holds in the first step as well, the consistency condition for y 1 = y 2 extends to the second step as well. Hence, we have two paths, given by the assignments for a 1 and a 2 , where a 1 and a 2 differ in the first position, but y 1 = y 2 in the second position. Consequently, either ( y 1 a 1 ) or ( y 2 a 2 ) holds and we have obtained a counterexample to satisfiability of the CL ∃ formula.
In the following, we introduce the general encoding for computing finite counterexamples of CL ∃ formulas Φ = Q ∃ . ϕ path → ϕ by bounding the number of paths regarding the external coordination variables C ext . The bound on the number of paths is given as a function K : C → N that maps each coordination variable to the number of branchings that should be considered for this variable. W.l.o.g. we can assume that K(c) = 0 for every internal coordination variable c ∈ C int . For example, for coordination variables a and b, and K(a) = K(b) = 1, we encode 4 different paths, one per possible combination for the two paths for each variable. We fix an arbitrary strict order ≺ ⊆ C × C between the coordination variables. For a set C ⊆ C, we identify K(C) by the vector in N |C| where the position of the value K(c) for a coordination variable c ∈ C is determined by ≺. For our encoding in QPTL, we use the following helper functions: • deps(v) returns the set of external coordination variables that influence variable v. An external coordination variable c ∈ C ext influences variable v if there is a directed path from c to v in A Φ . For example in the architecture of Fig. 1(c), x, y, and z are influenced by a. A coordination variable is influenced by itself. • branches(C, K) returns the set of branches belonging to coordination variables C. A branch π is referenced by a vector in N |C| and the set of branches is • paths (C, K) and strategies(S, K) represent the set of (path) variables in the QPTL formula that belong to the variables of the CL ∃ formula. For a variable v ∈ C ∪ S it introduces for each branch π ∈ branches(deps(v), K) a separate variable p v π that represents the variable v belonging to this branch π. Formally, we define the sets paths (C, K) := {p c π | c ∈ C ∧ π ∈ branches(deps(c), K)} and strategies(S, K) := {p s π | s ∈ S ∧ π ∈ branches(deps(s), K)} . • header (S, K) creates the alternating introductions of strategies and paths according to the (partial) order given the subset relation of the strategy variables on deps. For every strategy variable s ∈ S we introduce all paths belonging to external coordination variables c ∈ deps(s) prior to s and avoid duplicate path introductions: where s 1 , . . . , s n are ordered such that for all i, j with i < j ≤ n, either deps(s i ) ⊆ deps(s j ) or deps(s j ) deps(s i ), i.e., either deps(s i ) is a subset of deps(s j ) or both are incomparable.
• consistent (S, K) specifies the consistency condition for the variables belonging to the strategy variables on the different branches. The variables p s π 1 , . . . , p s π k belonging to a strategy variable s ∈ S must be equal as long as the coordination variables in the scope of s on the branches π 1 , . . . , π k are equal. This is expressible in LTL as we only consider a finite number of branches. In detail, the formula states that for every strategy variable s ∈ S and every pair of branches (π, π ′ ) that belongs to s, we ensure that the valuation of s on these two branches differ only if one of the variables in the scope of s was different in a prior step. Finally, we define the QPTL encoding for CL ∃ formula Φ and function K : C → N as where ϕ(π) is the initialization of LTL formula ϕ on branch π, that is we exchange v by p v π ′ for v ∈ C ∪ S where π ′ is the subvector of π that contains the values for coordination variables in deps(v).
Fault-tolerant Realizability. In the case of possible failures, the CL ∃ formulas Φ have the more general form Q ∃ . 1≤i≤n ϕ path i → ϕ i . In this setting, the set of coordination variables C is in general not partitioned into external and internal coordination variables. In the first step, we apply the transformation partition(Φ) given in Section 2 in order to get a partitioning into external and internal coordination variables. Furthermore, we generalize deps(v) to multiple architecture: An external coordination variable c ∈ C ext influences variable v if there is a directed path from c to v in one of the architectures. The QPTL query for counterexamples to CL ∃ formula Φ and a bound on the number of paths, given by the functions K 1 . . . K n : C → N, is (4.5) where K : C → N is defined as K(c) := max 1≤i≤n K i (c) for every c ∈ C.
In architecture (b), the link between shared variables b and x is faulty, hence, b is an external input.
Consider the example formula that models the two-way pipeline architecture, depicted in Fig. 3, where the connection between shared variables b and x may fail. We apply the transformation partition(Φ) and get the formula (4.7) In difference to distributed realizability, the encoding states that there must be a violation of the specification in some architecture. Also, not every architecture is challenged with all paths, e.g., in the query (4.6) for the first architecture, we use only one path as the path specification states that the connection between b and x is correct, while in the second architecture (4.7) we use two paths that are generated by the external inputs b * 1 and b * 2 . Theorem 4.1 (Correctness unsat fault ). Given a CL ∃ formula Φ = Q ∃ . 1≤i≤n ϕ path i → ϕ i over coordination variables C and strategy variables S. Φ is unsatisfiable if there exist functions K 1 . . . K n : C → N such that the QPTL formula unsat fault (Φ, K 1 , . . . , K n ) is satisfiable.
Proof. Let Φ ′ be an arbitrary CL ∃ formula after applying the transformation partition(Φ) given in Section 2 in order to recover the partitioning into external and internal coordination variables. Assume there exists functions K 1 . . . K n : C → N such that the QPTL formula unsat fault (Φ ′ , K 1 , . . . , K n ) is satisfiable. From the satisfiability of this QPTL formula we construct the proof that the CL ∃ formula Φ ′ is unsatisfiable (Proposition 3.3), i.e., that for all strategies there exists a path σ that satisfies 1≤i≤n ϕ path i ∧ ¬ϕ i .
We introduce the following auxiliary notation for this proof. We define Prev (v) to be the set of variables that are quantified prior to v. Prev Q (v) denotes the set Prev (v) when only considering the existential variables (Q = ∃), respectively universal variables (Q = ∀). For a variable v ∈ C ∪ S and a branch π, we define the branching operator v[π] := p v π ′ , where π ′ is the subvector of π that contains only values for variables in deps(v). v[π] is used to relate CL variables to QPTL variables, i.e., it selects the variable in QPTL formula that belongs to the branch π. Note that one QPTL variable can belong to more than one branch, for example, v[π] = v[π ′ ] if the branches π and π ′ differ only in the values for variables not contained in deps(v). For V ⊆ C ∪ S, we write V [π] := {v[π] | v ∈ V } for the set of QPTL variables belonging to the CL variables V on branch π.
Let s 1 , . . . , s m be the strategy variables S ordered according to the subset relation on deps(s). Let α(s) : (2 Scope(s) ) * → 2 {s} be an arbitrary strategy for strategy variable s ∈ S and fix a set of strategies A = {α(s) | s ∈ S}. By the semantics of CL ∃ we need to show that in the composition of these strategies α∈A α there exists a path such that the LTL formula 1≤i≤n ϕ path i ∧ ¬ϕ i is satisfied. We build the paths that satisfy the LTL formula from the branches Π = branches(C, K) encoded in the QPTL formula. Let β(c, π) : (2 Prev ∀ (c[π]) ) ω → (2 {c} ) ω be the valuation of the existential path variable in the QPTL formula belonging to coordination variable c on branch π ∈ Π. Note that β(c, π) depends on all prior universal quantified variables, especially also on universal quantified variables (representing strategy variables) on different branches. The strategies β(c, π) for c ∈ C ext correspond to the external coordination variables, while strategies β(c, π) for c ∈ C int correspond to the extensions defined in the finite counterexamples (Section 3). We view the existential quantified variables in the formula that correspond to the external coordination variables as inputs to our system strategies A and get the canonical tuple of paths P = (σ π 1 , . . . , σ π k ), one path σ π ⊆ (2 C∪S ) ω for each branch π ∈ Π.
Since the α ω s are derived from the system strategies, it holds that they satisfy the consistency condition consistent ({s}, K) (4.3) in the QPTL encoding. From the satisfaction of the QPTL formula, we conclude that 1≤i≤n π∈branches(C,K i ) OF DISTRIBUTED FAULT-TOLERANT SYSTEMS   15 is satisfied, i.e., there exists an index i and branches Π i = branches(C, K i ) such that π∈Π i ϕ path i (π) ∧ π∈Π i ¬ϕ i (π) holds. From the first conjunct it follows that each path σ π from P corresponding to a branch π ∈ Π i satisfies the path specification ϕ path i . We conclude with the second conjunct that one of the branches from Π violates the specification ϕ i .
Corollary 4.2 (Correctness unsat dist ). Given a CL ∃ formula Φ = Q ∃ . ϕ path → ϕ over coordination variables C and strategy variables S. Φ is unsatisfiable if there exists a function K : C → N such that the QPTL formula unsat dist (Φ, K) is satisfiable.

Remark 4.3 (Monotonicity of K).
For the distributed synthesis encoding it holds that K is monotone with respect to the satisfiability of unsat dist (Φ, K), however, for the fault-tolerant synthesis this is not necessarily true because of the complex information dependencies between different architectures. By increasing the number of paths for a coordination variable c in an architecture i where c is not involved in a fault, i.e., (c = s) is contained in ϕ path i , we restrict the choice of the environment in another architecture (where c could be involved in a fault). Hence, we have the following monotonicity condition: K 1 . . . K n is monotone with respect to the satisfiability of unsat fault (Φ, K 1 , . . . , K n ) if K i (c) is only increased if c is not contained in the input-output specification ϕ path i .
(operational 2,3 → consensus 2,3 ) ∧ i∈{2,3} (operational 1,i → correctval i ) , (4.8) where we use the following definitions operational 2,3 := (c 23 = g 23 ∧ c 32 = g 32 ), operational 1,3 := (c 12 = g 12 ∧ c 13 = g 13 ∧ c 32 = g 32 ), operational 1,2 := (c 12 = g 12 ∧ c 13 = g 13 ∧ c 23 = g 23 ), consensus i,j := 3 (g i = g j ), and The quantification prefix introduces the strategies for the generals g 2 and g 3 , as well as the communication between the three generals as depicted in the architecture in Fig. 5(a). Note that we omit the vote of the commander g 1 as it is not used in the specification. In the temporal part, we specify which failures can occur. The first conjunct, corresponding to Fig. 5(b), states that the commander is a traitor (operational 2,3 ) which implies that the other two generals have to reach a consensus whether to attack or not (consensus 2,3 ). The other two cases, depicted in Fig. 5(c)-(d), are symmetric and state that whenever one general is traitor the other one should agree on the decision made by the commander. The consistent ({g 12 , g 13 , g 23 , g 32 , g 2 , g 3 }, K) → π∈branches(C,K 1 ) ¬correctval 2 (π) .
By using the functions K i for 1 ≤ i ≤ 3 which are defined as K 1 (c 12 ) = K 1 (c 13 ) = K 2 (c 23 ) = K 3 (c 32 ) = 1 , and 0 otherwise, we get a satisfying QPTL instance and, hence, proved the unsatisfiability of Φ bgp . This resembles the manual proof for the Byzantine Generals' Problem. In every situation where one of the generals is a traitor, one has to consider the possible deviations from the loyal behavior.

Completeness
In practice, finite external counterexamples are often sufficient to detect unrealizable specifications. In this section, we show that our method is in fact complete for the case of safety specifications and weakly ordered architectures. It turns out that if one of these restrictions is dropped, i.e., if one is interested in general LTL specifications, or in architectures that are not weakly ordered, then finite counterexamples may no longer exist, and the method, therefore, becomes incomplete. A universal safety (tree) automaton is a tuple U = (Σ, Υ, Q, q 0 , δ) where Σ denotes a finite set of labels, Υ denotes a finite set of directions, Q is a finite set of states, q 0 ∈ Q the designated initial state, and δ denotes the transition function. The transition function δ : Q × Σ → B + ∧ (Q × Υ) maps a state and a input letter to a positive and conjunctive Boolean formula over Q × Υ. We allow the abbreviations δ(q, σ) = true and δ(q, σ) = false.
A Σ-labeled Υ-transition system is a tuple T = (T, t 0 , τ, o) where T is a finite set of states, t 0 ∈ T is the designated initial state, τ : T × Υ → T is the transition function, and o : T → Σ is the state labeling function. A universal safety automaton accepts a Σ-labeled Υ-transition system T if T has a run graph. A run graph is a directed graph G = (G, E) that satisfies the following constraints: • The vertices G ⊆ Q × T are a subset of the product of Q and T .
• The pair of initial states (q 0 , t o ) ∈ G is a vertex of G.
If we start with a temporal specification instead of a universal safety automaton, we first need the following transformations. As we only consider safety languages, we restrict the temporal specifications to syntactically safe [Sis94] formulas, i.e., LTL formulas where the only temporal operator is the weak until ϕ W ψ. (The weak until subsumes the globally operator ϕ, which is equivalent to ϕ W false.) . Given a syntactically safe LTL formula ϕ, we can construct a non-deterministic automaton N ¬ϕ on finite words that accepts the (not necessarily minimal) good prefixes of the co-safety formula ¬ϕ. The size of N ¬ϕ is on 2 O(|ϕ|) .
Using this result, we build the universal safety automaton U ϕ by simulating the automaton N ¬ϕ along each path: if each path is not a good prefix for the negation of ϕ, then ϕ holds on every path.
Proposition 5.2. Given a syntactically safe LTL formula ϕ, we can construct a universal safety automaton U ϕ with 2 O(|ϕ|) states that accepts a transition system T if, and only if, T satisfies ϕ.
We use the bound on the size of a transition system that is accepted by a universal safety automaton U in order to derive a upper bound on the number of counterexample paths needed to refute the existence of an implementation.

Proposition 5.3 ([FS13]
). If a universal safety automaton U with n states accepts a transition system, then U accepts a finite transition system T with (n!) 2 states. Proof. Let U be the universal safety automaton for ϕ according to Proposition 5.2. By the contraposition of Lemma 5.3 it holds that U rejects all transition systems if U rejects all finite transition systems with (n!) 2 states. Hence, all finite transition systems with size (n!) 2 have a finite counterexample path in the run of U . We show that every minimal counterexample path is bounded by d = (n!) 2 · p, where p is the longest loop-free path in the safety automaton U .
Assume by contradiction that there exists a transition system T of size (n!) 2 , where the length of the minimal counterexample path σ ∈ (Q × T ) * exceeds d. As d is the size of the product of U and T , there must be a repetition on σ, i.e., there exists i < j ≤ |σ| such that σ[i] = σ[j]. Thus, we can shorten the counterexample to σ 0..i−1 · σ j..n−1 violating our minimality assumption.
As the length of the minimal counterexample is bounded by d, all minimal counterexamples are contained in the full tree of depth d that has (2 |I| ) d paths.
This argumentation can be generalized to weakly ordered architectures since we have an upper bound on the size of implementations, too. Given an architecture A and an implementation for each process, we call the resulting system the distributed product according to architecture A as the system state consist of the product of the states of the process implementations. The meaning of the distributed product is a strategy (2 Ienv ) → 2 O that maps finite input sequences from the environment to the valuations of the process outputs.
Proposition 5.5 ( [FS05]). For a weakly ordered architecture and a realizable specification ϕ, the size of the smallest implementation of every process is n-exponential, where n is the number of processes.
Theorem 5.6. Given a syntactically safe LTL formula ϕ and a weakly ordered architecture A, ϕ is unrealizable in A if, and only if, there exists a finite counterexample.
Proof. Let U be the universal safety automaton for ϕ. By Proposition 5.5 and the unrealizability of ϕ in A it holds that there does not exist n-exponential strategies for the processes. Let t 1 , . . . , t n be arbitrary n-exponential strategies for the n processes and T : (2 Ienv ) * → 2 O be the (n-exponential) distributed product according to architecture A.
We choose a bound d that is greater than the size of the product of U and T . By the same argument as in the proof of Theorem 5.4, it follows that the length of the minimal counterexample for every such T is bounded by d, hence the number of paths is bounded by (2 |Ienv | ) d .
Proposition 3.1 states that the characterization of unsatisfiable formulas with counterexamples is complete. Our method, however, searches for counterexamples involving only a bounded number of external paths. In general, this is not enough, as the following propositions show.
Proposition 5.7. For full LTL, the unrealizability of a specification does not imply the existence of a finite counterexample.
Proof. Consider the CL ∃ formula Φ inf := ∃{x} ⊲ y. ϕ inf with temporal specification ϕ inf := (y = x). Φ inf is unsatisfiable because for every strategy f y : (2 {x} ) * → 2 {y} it holds that f y cannot correctly guess the future value of x on every path, as the formula is evaluated over the full binary tree that branches by the valuation of x (cf. CL ∃ semantics in Section 2). Assume for contradiction that a finite set of paths P ⊆ (2 {x} ) ω suffices to satisfy ¬ϕ inf = (y = x) against every strategy f y . As there are only a finite set of paths P , there exists a level in the full binary tree such that every node in this level has at exactly one successor path in P . Choose the strategy f y that assigns the nodes in this level with one successor the labeling of the next input. Such a finite state strategy exists because the nodes in each level are distinguishable by the strategy. Hence, for all paths in P it holds that (y = x) and thus no path satisfies ¬ϕ inf .
Proposition 5.8. For the architecture in Fig. 1(a), the unrealizability of a safety specification does not imply the existence of a finite counterexample.
Proof. Let D be a deterministic Turing machine that implements a unary counter. We use the encoding of D into the realizability problem of a safety LTL formula ϕ D in the architecture of Fig. 1(a) [Sch14]. There does not exist a finite state implementation that satisfies ϕ D , but for every finite set of environment input paths, only a finite number of correct configurations of D can be asserted. Hence, for every such finite set of paths, there exists an implementation that fulfills these assertions.

Approximations
Presently available QPTL solvers were unable to handle even small instances of our problem. In this section, we present two simplifications of the finite counterexample problem and their corresponding encodings. We consider the problem where we restrict the counterexample paths to a finite length by using a weak monadic second order logic of one successor (WS1S) encoding. Afterwards, we show a practical encoding in quantified Boolean formulas (QBF) that bounds the length of a counterexample path. We only consider the more general form of CL ∃ formulas modeling the fault-tolerance case, i.e., Φ = Q ∃ . 1≤i≤n ϕ path i → ϕ i .
It is well known that QPTL and S1S are equally expressive [SVW85]. We use the following transformation from QPTL to S1S.
Finite-length Counterexamples. When we restrict the counterexamples to finite length, we lose the ability to detect violations of liveness properties. Thus, we restrict the LTL specifications ϕ i in Φ to syntactic safety properties [KV01a]. As these specifications are negated in the encoding, the resulting LTL specifications describe co-safety properties [KV01a]. A property P ⊆ (2 Σ ) ω is co-safety if every ρ ∈ P has a good prefix, that is a prefix w ∈ (2 Σ ) * of ρ such that for all ρ ′ ∈ (2 Σ ) ω it holds that w · ρ ′ ∈ P .
In the weak version of S1S, the second-order quantification is restricted to finite sets. While syntactically equivalent to S1S, we change the semantics S1S by replacing the secondorder quantification rule by We define a S1S formula Fin(X) that asserts that the valuation of the second-order variable X is a finite set: We define ws1s(ϕ, i) as s1s(ϕ, i) with the difference that we interpret the result of ws1s(ϕ, i) as a WS1S formula and we only apply it to co-safety LTL formulas.
Proof. Let ws1s(Φ, 0) be satisfiable. By Lemma 6.1, it suffices to argue that s1s(Φ, 0) is satisfiable. First, we can extend any existential quantification ∃X. ϕ to infinite quantification as the WS1S restriction to quantification over finite sets are special cases of the S1S semantics (these where ∃X. Fin(X) ∧ ϕ holds). Next, we show that finite universal quantification is as powerful as infinite universal quantification. Consider the co-safety LTL formula ϕ. It holds that every satisfying assignment has a good prefix [KV01a]. Hence, the satisfaction of an infinite word ρ ∈ (2 Σ ) ω depends only on a finite prefix. Thus, a satisfying assignment against universal quantified finite sequences implies the satisfaction against universal quantified infinite sequences.
The WS1S encoding of CL ∃ formula Φ and functions K 1 . . . K n : C → N is ws1s(¬ϕ i (π), 0) , (6.1) where K : C → N is defined as K(c) := max 1≤i≤n K i (c) for every c ∈ C. header WS1S introduces the second-order variables V x that correspond to the path variables x, but is otherwise identical to the QPTL version. Furthermore, ϕ WS1S path uses second-order equivalence V s = V c for (c ↔ v). The consistency condition consistent WS1S (S, K) in WS1S is defined as the conjunction of (π,π ′ )∈branches (deps(s),K) 2 for every s ∈ S. This formula ensures different reactions of a universal variable on two branches is based on different prior valuations of the dependencies (cf. QPTL consistency condition (4.3)).
We give an example query based on CL ∃ formula (2.2) ∃{a} ⊲ x. ∃{b} ⊲ y. (b = x) → ( y ↔ a). The WS1S query is Theorem 6.3 (Correctness unsat WS1S fault ). Given a CL ∃ formula Φ = Q ∃ . 1≤i≤n ϕ path i → ϕ i over coordination variables C and strategy variables S. Let ϕ i be a syntactically safe LTL formula for each 1 ≤ i ≤ n. Φ is unsatisfiable if there exists functions K 1 . . . K n : C → N such that the WS1S formula unsat WS1S fault (Φ, K 1 , . . . , K n ) is satisfiable. Proof. Assume unsat WS1S fault (Φ, K 1 , . . . , K n ) is satisfiable. We show that this implies the satisfiability of unsat fault (Φ, K 1 , . . . , K n ) and use Theorem 4.1 that states the correctness of the QPTL encoding. Lemma 6.2 states that we only have to consider finite state sequences for the LTL specifications ϕ i . What is missing in the argumentation are the paths specifications ϕ WS1S path i and the consistency condition consistent WS1S (Φ, K). The transformed path specifications are equisatisfiable under WS1S and QPTL semantics as the (existential quantified) input variables appear after the (universal quantified) strategy variables in header WS1S (S, K). Lastly, the consistency condition restricts the finite behavior of the universal quantified strategy variables and the infinite behavior does not affect the satisfiability of the co-safety properties. Hence, there exists an infinite path extension for every 22 FINKBEINER AND TENTRUP existentially quantified second-order variable, and the formula remains satisfiable against any infinite path extension of the universally quantified second-order variables.
WS1S is supported by the Mona [HJJ + 95] tool. Some of our smaller instances were solved by Mona, but the Byzantine Generals' Problem failed due to memory constraints in the BDD library.
Bounded-length Counterexamples. Taking the simplifications even further, we not only bound the number of paths but also the length of the paths by translating the problem to the satisfiability problem of quantified Boolean formulas (QBF). Quantified Boolean formulas are the extension of Boolean formulas by quantification over variables. Let V = {v 1 , . . . , v n } be a finite set of variables. The syntax of QBF is given by the grammar where x ∈ V . We define the usual abbreviations ∧, ∀, true, false, →, and ↔. The semantics is defined over valuations σ : V → {0, 1}. The satisfaction of an valuation σ is defined as Theorem 6.5 (Correctness unsat QBF fault ). Given a CL ∃ formula Φ = Q ∃ . 1≤i≤n ϕ path i → ϕ i over coordination variables C and strategy variables S. Let ϕ i be a syntactically safe LTL formula for each 1 ≤ i ≤ n. Φ is unsatisfiable if there exists functions K 1 . . . K n : C → N such that the QBF query unsat QBF fault (Φ, k, K 1 , . . . , K n ) is satisfiable for some k > 0. Proof. The encoding is a special case of Theorem 6.3. If the Boolean formula that is a finite k-unrolling of the LTL formula is satisfied against a finite sequence of length k, i.e., we found a counterexample within the first k steps, then it is also satisfied against any (possibly infinite) strategy.

Experimental Results
We have carried out our experiments on a 2.6 GHz Opteron system. For solving the QBF instances, we used a combination of the QBF preprocessor Bloqqer [BLS11] in version 031 and the QBF solver DepQBF [LB10]  Byzantine Generals' Problem. Table 1 demonstrates that the Byzantine Generals' Problem remains, despite the optimizations described above, a nontrivial combinatorial problem: we need to find a suitable set of paths for every possible combination of the strategies of the generals. The bound given in the first row reads as follows: The first component is the number of branchings for the input variable v in all three architectures. The last three components state the number of branchings for the outputs of the faulty nodes in their respective architectures. For example, bound (1, 1, 0, 0) means that we have two branches for v, c 12 , and c 13 , while we have only one branch for c 23 and c 32 . More precisely, starting from constant zero functions K 1 , K 2 , K 3 , the bound (1, 1, 0, 0) sets K 1 (v) = K 2 (v) = K 3 (v) = K 1 (c 12 ) = K 1 (c 13 ) = 1 and K 2 (c 23 ) = K 3 (c 32 ) = 0. To prove the unrealizability, we need one branching for the input v and one branching for every coordination variable that serves as a shared variable for a faulty node, i.e., the bound (1, 1, 1, 1). The number of branches and thereby the formula size grows exponentially with the number of branchings for the input variables. Byzantine Firing Squad Problem. We consider another classical consensus problem, the Byzantine Firing Squad Probem [FLM85]. In this setting, we have a set of synchronous processes, each having a distinct input and a broadcasting mechanism for communication with the other processes, depicted in Fig. 7(a). The goal of these processes is to synchronously enter a fire state whenever the input was initially given at one process. As before, we consider architectures with up to one faulty process, but in contrast to the Byzantine Generals' Problem, we require that this specification holds only if all processes are correct. Furthermore, we require that the non-faulty processes act uniformly, i.e., if a non-faulty process enters the firing state, all other non-faulty processes enter the firing state. It was shown in [FLM85] that there is no protocol that ensures correct behavior in the presence of faults. The encoding Φ bfsp for three nodes is given by the CL ∃ formula ∃{req 1 } ⊲ bcast 1 . ∃{req 1 , chan 21 , chan 31 } ⊲ out 1 .
CAP Theorem. The CAP Theorem due to Brewer [Bre00] states that it is impossible to design a distributed system that provides Consistency, Availability, and Partition tolerance (CAP) simultaneously. For the encoding in CL ∃ , we assume there is a fixed number n of nodes, that every node implements the same service, and that there are direct communication links between all nodes, depicted in Fig. 7(b). We use the variables req i and out i to denote input and output of node i, respectively. The consistency and availability requirements are encoded as the LTL formulas 1≤i<n (out i ↔ out i+1 ) and ( 1≤i≤n req i ) ↔ ( 2 1≤i≤n out i ). The partition tolerance is modeled in a way that there is always at most one node partitioned from the rest of the system, i.e., we have n different architectures and in every architecture all communication links to one node are faulty. For two nodes, we get the CL ∃ formula Φ cap ( (chan 1 = com 1 ) → ((out 1 = out 2 ) ∧ ((req 1 ∨ req 2 ) ↔ 3 (out 1 ∨ out 2 )))) ∧ ( (chan 2 = com 2 ) → ((out 1 = out 2 ) ∧ ((req 1 ∨ req 2 ) ↔ 3 (out 1 ∨ out 2 )))) . (7.3) Table 3 shows that our method is able to find conflicts in a specification with an architecture up to 50 nodes within reasonable time. When we drop either Consistency, Availability, or Partition tolerance, the corresponding instances (AP, CP, and CA) become satisfiable. Hence, our tool does not find counterexamples in these cases.  Discussion. Table 4 shows a comparison of the the different encodings that we have presented in the paper. There does not exist an algorithm that decides whether a given CL ∃ formula is unsatisfiable. We presented an approach that bounds the number of paths and used an encoding to QPTL. The reason for incompleteness was shown in Section 5: for liveness properties one may need infinitely many paths to show unsatisfiability. Our encoding in WS1S (Mona) loses the ability to find counterexample paths of infinite length, e.g., the CL ∃ formula ∃∅ ⊲ y.
( y ↔ x) (7.4) with free coordination variable x is unsatisfiable and two paths that are infinitely often different are sufficient to prove it. The QPTL encoding is capable of finding these paths while neither the WS1S, nor the QBF, encoding is applicable. However, Mona failed to solve larger instances from Tables 1 to 3, especially it could not handle the encoding of the Byzantine Generals' Problem. For the translation to QBF we bounded the length of the paths to k where k is an additional parameter. With this encoding we approximate the reactive behavior of our system by a finite prefix. Despite this restriction, we could prove unsatisfiability for many interesting specifications from literature. In some instances, the WS1S approximation provides stronger unrealizability guarantees. For example in the Byzantine Firing Squad Problem, the WS1S encoding is able to prove that any finite uniform reaction leads to an unrealizable instance (cf . Table 4), while in the QBF encoding, we have to bound the uniform reaction (7.2) to a fixed length. In practice, one would first use the QBF approximation in order to find "cheap" counterexamples. After hitting the number of paths that the QBF solver can no longer handle within reasonable time, one proceeds with more costly approximations like the WS1S encoding.

Beyond the Byzantine Fault Model
We formalize the fault-tolerant synthesis problem regarding multiple types of faults, their durations, observability, and the fault-tolerance requirements and provide a uniform encoding into CL ∃ . Faults are modeled by allowing the environment to take over the control of the faulty processes.
Types of Faults. We review types of faults that were considered in previous work [DS86,AAE04,DF09]. Stuck-at faults occur when a process stops reacting on new inputs and keep their last outputs. On fail-stop faults or crashes the process halts immediately, i.e., they stop producing any outputs. While fail-stop faults are detectable, crashes are not detectable [DS86]. Omission faults subsume these faults and are characterized as failures on the specified input-output specification. The most general fault type are the Byzantine faults, where a process can deviate arbitrarily from its specification, even in a malicious way. The duration of a fault can be permanent, intermittent, or transient. Some failures may be detectable or undetectable depending on the architecture and the type of fault. Lastly, the system usually has to fulfill different kind of specifications in the presence of faults and we use the classification of fault-tolerance requirements from [DF09]: Masking tolerance means that the system has to fulfill both safety and liveness specifications, nonmasking tolerance allows the system to temporarily violate its safety properties while failsafe tolerance specifies that after a fault, only the safety requirements have to be fulfilled.
Fault-tolerance Specifications. For simplicity, we restrict the failures to processes, but it can be easily adapted to failures of individual communication links. Consider an arbitrary architecture A = (P, p env , {I p } p∈P , {O p } p∈P ). A fault-tolerance scenario F is a tuple (P f , T, D, Obs, ϕ) where P f ⊆ P is a subset of processes that simultaneously suffer from a fault of type T ∈ {stuck -at, fail-stop, omission, Byzantine} and duration D ∈ {permanent , intermittent , transient }, Obs ∈ {⊤, ⊥} denotes the observability, and ϕ is an LTL formula specifying the fault-tolerance requirements. Not all combinations of fault types and durations are possible, e.g., stuck-at faults and fail-stop faults are always permanent. A fault-tolerance specification F is a set of fault-tolerance scenarios.
Fault-tolerant Realizability. The distributed fault-tolerant realizability problem is to decide, given an architecture A and a fault-tolerance specification F, whether there exists a finite state implementation for the processes in A such that the system satisfies the fault-tolerance specification F. We formalize this problem by giving a CL ∃ formula Φ = Q ∃ . F ∈F ϕ path F → ϕ F that models the description of the fault-tolerance scenarios given above.
Consider an arbitrary architecture A = (P, p env , {I p } p∈P , {O p } p∈P ) and a fault-tolerance specification F. Using Theorem 2.1 we get the CL ∃ encoding Ψ = Q ∃ . ϕ path → ϕ of the distributed realizability problem for architecture A and an arbitrary LTL formula ϕ. For every fault-tolerance scenario F ∈ F, we introduce a new architecture that modifies the input-output specifications for processes affected by F according to the scenario. We denote the resulting path specification by the LTL formula ϕ path F and the fault-tolerance requirement for F as ϕ F . The resulting CL ∃ formula contains a conjunct over all scenarios F: We now define the path specifications ϕ path F . Let F = (P f , T, D, Obs, ϕ F ) be a faulttolerance scenario. For every process p ∈ P f we introduce a fresh coordination variable fault F p that immediately signals whether a fault occurred at process p in the last step. If the faults are observable (Obs = ⊤) we extend the scope of every strategy variable by {fault F p | p ∈ P f } 2 . Let ϕ path F = ϕ path = v∈I∩O (c v = s v ). We remove every conjunct (c v = s v ) from ϕ path F where v ∈ O P f is the output of a faulty process. For every v ∈ I ∩ O P f we add the following new constraints to ϕ path F depending on the type of faults T . For readability, we Lastly, we add a requirement for every fault F p variable regarding the specified duration D: ¬fault. If we want to have tighter control about the duration of faults we can use the parametric LTL operators [AELP01] to bound the length n of a fault ≤n ¬fault, or require that length of a correct behavior is longer than m by formula fault → fault U (¬fault U >m fault) . • D = transient : ¬fault W fault U ≤n ¬fault where n is the maximal duration of the fault. We simplify the undetectable permanent fault encoding by removing the fault variables, as these variables are not used in the specification. Our formulation allows for many types and durations of faults that cannot be captured with a fault-tolerance scenario. Indeed, it is possible to use arbitrary LTL formulas to specify the type and duration of a fault. Computing counterexamples for these general types of faults can be integrated into the method described in Section 4.

Conclusion
We have introduced counterexamples for distributed realizability and shown how to automatically derive counterexamples from given specifications in CL ∃ . We used encodings in QPTL, WS1S, and QBF. In our experiments, the QBF encoding was the most efficient. Even problems with high combinatorial complexity, such as the Byzantine Generals' Problem, are handled automatically. Given that QBF solvers are likely to continue to improve in the future, even larger instances should become tractable. In future work, we plan to extend the method to a larger class of infinite counterexamples, which will support liveness specifications. Furthermore, we want to investigate approximation techniques for more general types of faults.