 Here, the basic component spaces are indexed by Comp, the states of each component are taken from States (with different components using maybe only a few of the elements of States), and the global states of the system are global valuations, that is, functions that assign a state to each basic component Comp. Not all such functions are allowed, only those in \(C\). Finally, Pred is a labelled family of predicates (sets of global states). 