eighty-twenty

This talk was about a particular graph language used to describe concurrent systems. The work focussed on analysing the graphs to identify symmetry in their Kripke structures, so that the symmetry could be reduced, thereby making the model more tractable.

Notes:

• using Promela to construct models

• is constructing the entire Kripke structure the expensive bit?

• processes and channels are typed; processes and channels are coloured by type in the diagrams

• only need to consider static topology, because if there’s symmetry in the static case, then all instances of the symmetry will introduce the same patterns of new channels later on

• “automorphism group”?