## Errata to the paper “Reactive Safety” by RĂ¼diger Ehlers and Bernd Finkbeiner

### Complexity bounds

On page 11 of the paper (page 188 in the procedings), line 31, it is stated that we can translate an LTL formula of size n into a deterministic parity word automaton with at most states. This is a typo, the upper bound on the number of states should rather be .

### Running example

In the running example (occurring in the introduction, Section 3 and Section 5.3), it is claimed that the satisfaction of the specification by a reactive system for the given interface is equivalent to the satisfaction of the specification for . The latter formula however ignores the fact that the coffee machine could also produce coffee immediately after the coffee button is pressed. Thus, should rather be .