Fourth Meeting of the Formal Methods Reading Group

The fourth set of notes is up as FMRG-4. In this we study automata for which there is no start state specified and all states are considered to be accepting states. This is defined as a set together with a collection of choice maps on the set. We define the notion of a strong simulation as a choice map that carries a transition between states to a transition between sets of states. Other ideas of Milner are expressed in similar terms. Would like to know from the readers if this makes it easier to understand Milner's ideas.