Safety first: A two-stage algorithm for LTL games

In the game theoretic approach to the synthesis of reactive systems, specifications are often given as a conjunction of linear time properties. An implementation can be obtained from a winning strategy derived from a suitable generalized parity game in which each property produces a parity acceptance condition. Safety and persistence properties usually make up the majority of the specification. We show how this can be exploited to play the game in two stages and substantially speed up synthesis without sacrificing generality and conciseness of specification.