Errata List for 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 into a deterministic parity word automaton with at most $2^{2^n log n}$ states. This is an error, the upper bound on the number of states should rather be $2^{O(2^n n log n)}$ .

Running Example

In the running example (described in the introduction, Section 3 and Section 5.3), it is claimed that the satisfaction of the specification psi_1 wedge psi_2 by a reactive system for the given interface is equivalent to the satisfaction of the specification psi'_1 wedge psi_2 for $psi'_1 = mathsf{G}(c rightarrow mathsf{X},f)$ . The latter formula however ignores the fact that the coffee machine could also produce coffee immediately after the coffee button is pressed. Thus, psi'_1 should rather be mathsf{G}(x rightarrow mathsf{X}(b vee f)) .