Two abstractions from the branching discrete to the linear discrete model are given. They shed some light on the roles of consistency, deadlock and determinacy. The stronger of the two depends on a notion of dynamic type for processes which ensures deadlock freedom.
A reasonably strong abstraction from the branching real to the branching discrete model is given. This depends on a finer notion of type which is a reasonably physically plausible formalisation of the timing properties of certain real components.
Back to my home page.