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 .