We construct various kinds of strategy models by defining the plays they use and a corresponding prefix ordering, then choosing a free completion corresponding to the kind of nondeterminism we wish to consider. In particular, the traditional construction of strategies as prefix-closed sets of plays corresponds to the downset completion, which is initial in the category of distributive lattices and join-distributive morphisms. This introduces angelic nondeterminism, which lets us consider all possible choices of the environment. We go one step further and consider the free completely distributive lattice over plays, which is initial wrt. complete morphisms. This models demonic as well as angelic nondeterminism and allows us to model strategy specifications permitting several possible system behaviors. This library captures the general pattern poset completions definitions as a module type and proves general properties which hold in all of them. This allows parts of our development to be carried out in a modular way and be instantiated for arbitrary lattice completions.

Poset completions

Each of the completions we will consider is a free completion for a specific category of completely distributive lattices. Hence, the first step when constructing a completion procedure is to specify the kind of morphisms used in that category.

Then a free completion has the following interface. Note that the type of morphism used fully characterizes the completion, so that we can always use an opaque implementation.