Linear temporal logic (LTL) is a popular language in formal verification, especially in the domains of model checking and reactive synthesis. Because its semantics is defined in terms of infinite sequences of symbols ...

Obliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to ...