Towards a theory of simulation for verification of concurrent systems

We here investigate whether it is possible to provide the designer of a concurrent system with a sound and efficient simulation technique enabling reasoning about important behavioural properties of the system. We introduce the notion of a simulation defined as a subset of the possible execution paths generated by the system, and demonstrate that under some conditions the simulation provides a sufficient information to reason about a number of interesting properties of the system. We then show that there always exists a simulation which provides the required behavioural information and involves a minimal computational effort.