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 wrong formula states. This is a typo, the upper bound on the number of states should rather be correct formula.

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 formula by a reactive system for the given interface is equivalent to the satisfaction of the specification formula for formula. The latter formula however ignores the fact that the coffee machine could also produce coffee immediately after the coffee button is pressed. Thus, formula should rather be formula.