Modelling Processes

Abstract

This chapter introduces labelled transition systems as a simple graphical formalism for modelling processes. Labelled transition systems consist of states and transitions between states that are labelled by action symbols; they describe how computing systems change their states when performing certain actions. Various puzzles are modelled using labelled transition systems, followed by more serious examples including a program for computing greatest common divisors, a lamp controller, and an elevator controller. Next, a simple language for describing processes that are formed from the actions in labelled transition systems is introduced. It is shown abstractly and in several concrete examples how processes correspond to labelled transition systems by writing down process equations. The most important operations on processes are action prefix and choice. Using the example of a simple vending machine it is then examined at an informal level how processes or behaviours of computing systems could be identified or distinguished, and a simple necessary criterion for process equivalence is introduced.