Transition systems are widely used to model computer programs and systems. They consist of states, representing possible configurations, and transitions, representing possible state changes. Such changes may be governed by an action induced by the system itself or by an external event. This is a fundamental model to define the semantics of computer systems or abstract computational devices such as finite statemachines, pushdown systems, Turing machines, counter machines, timed automata, etc. Besides, many other models of sequential, parallel, reactive and interactive processes and computations, such as Petri nets, process calculi such as CCS and CSP, etc., can naturally be recast as transition systems.

Transition systems are mathematically quite simple, as they can be viewed as (possibly infinite) directed graphs with labels on vertices or on edges. Yet, theoretical tools developed for them have allowed striking breakthroughs to be made for software verification, in particular due to the approach of verification by model checking.

In the context of this book, transition systems appear in two capacities: as object of primary interest and study, in Part I of the book, and as models for the temporal logics which we will study further. A real system can be modelled by different abstract transition systems and in different levels of detail. It is therefore important to have precise criteria whether a given abstract model faithfully captures the formally specified behaviour of the given real transition system. For that it is necessary to have a precise notion of behaviour of a transition system, so later in this chapter we also address the question:

When should two transition systems be considered to be behaviourally equivalent?

This question does not have a unique answer, as the notion of equivalence depends on the behavioural features of transition systems that are considered of importance for the real systems they model. Such features may involve local behaviour (pre- and postconditions), generated paths and computations, as well as reachability, safety, liveness, fairness, etc., types of system properties. Accordingly, a variety of natural notions of behavioural equivalence arise. We will concentrate on two of them – bisimilarity and trace equivalence – because they are inherently linked to the notion of logical equivalence.