## 1 Introduction

### 1.1 Related work

### 1.2 Structure of this article

## 2 Preliminaries

### 2.1 HyperLTL

### 2.2 Strategies

## 3 HyperLTL synthesis

### 3.1 Incomplete information

### 3.2 Distributed synthesis

### 3.3 Asynchronous distributed synthesis

### 3.4 Symmetric synthesis

### 3.5 Fault-tolerant synthesis

## 4 Deciding \(\text {HyperLTL}\) synthesis

\(\exists ^*\) | \(\forall ^*\) | \({ linear }\;\forall ^*\) | \(\exists ^* \forall ^1\) | \(\exists ^* \forall ^{>1}\) | \(\forall ^* \exists ^*\) |
---|---|---|---|---|---|

\(\textsc {PSpace}\)-complete | Undecidable | Non-elem. | \(\textsc {3ExpTime}\) | Undecidable | Undecidable |

### 4.1 \(\exists ^*\) Fragment

### 4.2 \(\forall ^*\) Fragment

### 4.3 Linear \(\forall ^*\) fragment

### 4.4 \(\exists ^* \forall ^1\) Fragment

### 4.5 \(\forall ^* \exists ^*\) Fragment

- . Here, we associate the left part of the pairs with the upper (\(\alpha \)) part of the domino stones and the right part with the lower (\(\beta \)) part of the domino stones. And only taking the left side of the pairs along the path \(\pi \) we should get \(i_\alpha \), respectively for \(i_\beta \). Therefore, this formula essentially states that the path which has encodes our solution and has \(i_\alpha =i_\beta \). The \(\#\) symbols at the end are placeholders for ensuring that the sequence has a finite size.
- . This defines the set of relevant traces trough our strategy tree. They can be imagined being parallel to each other or thought of as the solution trace but with some additional \(\lnot i\) in front.
- . This defines that a trace \(\pi '\) is a successor of \(\pi \). It essentially states that \(\pi '\) has exactly one more \(\lnot i\) at the beginning than \(\pi \), i.e., it is the next parallel trace.
- Essentially, we now want \(\pi '\) to be exactly \(\pi \) but with the first stone removed and the rest shifted to the front. This can be best illustrated with the example from above. The full sequence at the trace represents the solution with the outputsThe next trace, which is the one with \(\lnot i\) in front and then is$$\begin{aligned} ({\dot{b}}, {\dot{b}})(b, b)(a, {\dot{a}})({\dot{a}}, a)(b, {\dot{b}})({\dot{b}}, b)(b, {\dot{b}})(a, a)({\dot{a}}, a)(\#, \#)(\#, \#)\dots \end{aligned}$$Note that now the symbols are not aligned any more because the first stone did not have an equal length of the upper and lower part. We continue this sequence by removing the next stones:$$\begin{aligned} ({\dot{a}}, {\dot{a}})(b, a)({\dot{b}}, {\dot{b}})(b, b)(a, {\dot{b}})({\dot{a}}, a)(\#, a)(\#, \#)(\#, \#)\dots \end{aligned}$$Now, the formula \( \varphi _{ stone \& shift }(\pi ,\pi ')\) encodes that \(\pi '\) is \(\pi \) with the first stone removed and the rest shifted as illustrated in the example. This can be done with a disjunction over all possible stones. See [18] for more details.$$\begin{aligned}&({\dot{b}}, {\dot{b}})(b, b)(a, {\dot{b}})({\dot{a}}, a)(\#, a)(\#, \#)(\#, \#)\dots \\&({\dot{a}}, {\dot{b}})(\#, a)(\#, a)(\#, \#)(\#, \#)\dots \\&(\#, \#)(\#, \#)\dots \end{aligned}$$
- cuts off the irrelevant prefix until \(\varphi \) starts. This irrelevant prefix is exactly the part where the \(\lnot i\) appear. We are only interested in looking at the part of the traces because they are not shared by the different relevant traces.
- We furthermore assume that only singletons are allowed what can be achieved by a disjunction for each pair of atomic propositions. See [18] as well.

## 5 Bounded realizability

### 5.1 Transition systems

### 5.2 Overview

### 5.3 Automata

### 5.4 Run graph

### 5.5 Self-composition

### 5.6 Synthesis

## 6 Bounded unrealizability

## 7 Evaluation

^{1}for universal \(\text {HyperLTL}\) based on the bounded synthesis algorithm described in Sect. 5. Furthermore, we implemented the search for counterexamples proposed in Sect. 6. Thus, \(\text {BoSyHyper}\) is able to characterize realizability and unrealizability of universal \(\text {HyperLTL}\) formulas.

### 7.1 Symmetric mutual exclusion

### 7.2 Distributed and fault-tolerant systems

Benchmark | Instance | Result | States | Time [s] | ||
---|---|---|---|---|---|---|

Moore | Mealy | Moore | Mealy | |||

Symmetric mutex | Non-sym | Realizable | 2 | 2 | 1.4 | 1.3 |

Sym | Unrealizable (\(k=2\)) | 1 | 1 | 1.9 | 2.0 | |

Tie | Realizable | 3 | 3 | 1.7 | 1.6 | |

Full-non-sym | Realizable | 4 | 4 | 1.4 | 1.4 | |

Full-sym | Unrealizable (\(k=2\)) | 1 | 1 | 4.3 | 6.2 | |

Full-tie | Realizable | 9 | 5 | 1 802.7 | 5.2 | |

Encoder/decoder | 1-2-Hamming-2 | Realizable | 4 | 1 | 1.6 | 1.3 |

1-2-Fault-tolerant | Unrealizable (\(k=2\)) | 1 | – | 54.9 | – | |

1-3-Fault-tolerant | Realizable | 4 | 1 | 151.7 | 1.7 | |

2-2-Hamming-2 | Unrealizable \((k=3)\) | – | 1 | – | 10.6 | |

2-3-Hamming-2 | Realizable | 16 | 1 | \(> 1\) h | 1.5 | |

2-3-Hamming-3 | Unrealizable \((k=3)\) | – | 1 | – | 126.7 | |

CAP Theorem | cap-2-linear | Realizable | 8 | 1 | 7.0 | 1.3 |

cap-2 | Unrealizable \((k=2)\) | 1 | – | 1 823.9 | – | |

ca-2 | Realizable | – | 1 | – | 4.4 | |

ca-3 | Realizable | – | 1 | – | 15.0 | |

cp-2 | Realizable | 1 | 1 | 1.8 | 1.6 | |

cp-3 | Realizable | 1 | 1 | 3.2 | 10.6 | |

ap-2 | Realizable | – | 1 | – | 2.0 | |

ap-3 | Realizable | – | 1 | – | 43.4 | |

Bus protocol | NI1 | Unrealizable \((k=2)\) | 1 | 1 | 75.2 | 69.6 |

NI2 | Realizable | 8 | 8 | 24.1 | 33.9 | |

Dining cryptographers | Secrecy | Realizable | – | 1 | – | 82.4 |