Labelled transition systems =========================== An LTS consists of a set of *states* and a set of *transitions* between those states. These transitions are labelled by *actions* and one state is designated as the *initial state*. Formally, an LTS is a tuple :math:(S, A, \to, s_0) where: - :math:S is a (finite) set of states; - :math:A is a set of actions; - :math:\to \subseteq S \times A \times S is a transition relation; - :math:s_0 \in S is the initial state. For any set of actions :math:A we denote by :math:A^* the set of all finite sequences of elements of :math:A. An element of :math:A^* is called an action sequence or *trace* and the empty trace is denoted by :math:\epsilon. For any LTS :math:(S, A, \to, s_0), states :math:s,t \in S and action sequence :math:\sigma \in A^*, with :math:\sigma = a_1 \ldots a_n for some :math:n \ge 0, we denote by :math:s \to^\sigma t the fact that there exist :math:s_0 \ldots s_n \in S such that :math:s = s_0, :math:t = s_n, and :math:(s_i, a_{i+1}, s_{i+1}) \in \to for all :math:0 \le i < n. Note that for all states :math:s it holds that :math:s \to^\epsilon s. An LTS usually describes the (discrete) behaviour of some system or protocol: in any state of the system, a number of actions can be performed, each of which leads to a new state. The initial state corresponds to the state in which the system resides before any action has been performed. This LTS model can be extended in various ways. We briefly describe the addition of internal actions and of state values below. Internal actions ---------------- When studying the behaviour of a system, one often wants to view the system as a *black box*. Only the interactions of the system with its environment are of interest and all internal behaviour should be hidden. For this, a special action called the *internal action* is introduced. It is often designated by :math:\tau. The internal behaviour of a system can now be hidden by renaming all actions that it performs internally, to :math:\tau. In the LTS model, the :math:\tau is a special label that can be carried by a transition. We can then consider traces between states on which any number of :math:\tau actions may occur in between; we do not care how many. For convenience we introduce additional notation to express this. Let :math:\tau^* denote any finite sequence of :math:\tau actions. For any LTS :math:(S, A, \to, s_0), states :math:s,t \in S and action sequence :math:\sigma \in (A \setminus \tau)^*, with :math:\sigma = a_1 \ldots a_n for :math:n \ge 0, we denote by :math:s \to^\sigma t the fact that there exist :math:s_0 \ldots s_n \in S such that :math:s = s_0, t = s_n, and :math:s_i \to^{(\tau^* a_{i+1})} s_{i+1} for all :math:0 \le i < n. State values ------------ The state of a system can be defined as the combination of the *values* of all relevant *parameters* or *variables*. Hence, the LTS model can be extended by associating a *state vector* with every state. This is the list of parameters along with their values in that specific state. Formally, we write a state vector declaration as a tuple :math:(d_1: D_1, \ldots, d_n: D_n) where :math:d_i is the name and :math:D_i is the domain (the set of possible values) of parameter :math:i. The set of states of an LTS now becomes a subset of :math:D_1 \times \ldots \times D_n. Hence, every state is an *n*-tuple that contains one specific value for every declared parameter. Equivalences ------------ Given two LTSs, a natural question is whether they describe the same behaviour. To answer this question we must first specify what we mean by "the same". For example, are we satisfied if both LTSs can perform the same sequences of actions (starting from their initial states) or do we want to impose stricter criteria? In other words, we have to specify when we consider two LTSs to be *equivalent*. Various notions of equivalence have been defined in the literature. Some are finer than others, meaning that the criteria that two LTSs should meet for them to be called equivalent, are stronger. The equivalences that we consider here are explained in the following sections. Trace equivalence """"""""""""""""" According to *trace equivalence*, two LTSs are equivalent if and only if they can perform the same sequences of actions, starting from their initial states. .. math:: \newcommand{\Tr}[1]{\mathrm{Tr}(#1)} \newcommand{\Trw}[1]{\mathrm{Tr_w}(#1)} \newcommand{\trans}[1]{\mathop{\stackrel{#1}{\longrightarrow}}} \newcommand{\ttrans}[1]{\mathop{\stackrel{#1}{\Longrightarrow}}} Formally, for any LTS :math:(S, A, \to, s_0) and state :math:s \in S we define :math:\Tr{s} to be the set of traces possible from :math:s: .. math:: \Tr{s} = \{ \sigma \in A^* | \exists_{t \in S}~ \trans{\sigma} t \} Given two LTSs :math:T = (S, A, \to, s_0) and :math:T' = (S', A', \to', s'_0), we say that :math:T and :math:T' are trace equivalent iff :math:\Tr{s_0} = \Tr{s'_0}. Weak trace equivalence """""""""""""""""""""" Weak trace equivalence* is very similar to trace equivalence. The only difference is that it "skips" any :math:\tau actions that appear on the traces. Hence, weak trace equivalence is particularly useful when some parts of the behaviour have been hidden. For example, if one LTS describes the desired, external behaviour of a system and another LTS describes its implementation with internal actions renamed to :math:\tau, then a natural question would be whether the two LTSs are weakly trace equivalent. In this case, "normal" trace equivalence would be too strong. Formally, for any LTS :math:(S, A, \to, s_0) and state :math:s \in S we define :math:\Trw{s} to be the set of weak traces possible from :math:s: .. math:: \Trw{s} = \{ \sigma \in (A \setminus \{\tau\})^* ~|~ \exists_{t \in S}~ s \ttrans{\sigma} t \} Given two LTSs :math:T = (S, A, \to, s_0) and :math:T' = (S', A', \to', s'_0), we say that :math:T and :math:T' are weakly trace equivalent iff :math:\Trw{s_0} = \Trw{s'_0}. Obviously, if :math:s \trans{\sigma} t then there exists a sequence :math:\pi (possibly containing :math:\tau steps) such that :math:s \trans{\pi} t. Using this fact, it is not hard to see that if two LTSs are trace equivalent then they are also weakly trace equivalent. Strong bisimilarity """"""""""""""""""" *Strong bisimilarity* (or *strong bisimulation equivalence*) relates two LTSs in the following way: if one LTS can perform an action :math:a then the other LTS must also be able to perform an :math:a action and in such a way that the resulting states are again related. This relation works both ways simultaneously (which is suggested by the "bi-" prefix in the name of the equivalence). The formal definition is as follows. - A relation :math:R on the states of an LTS is called a *simulation* if for any states :math:s, s', t and action :math:a, if :math:s \trans{a} s' and :math:s \mathrel{R} t then there exists a state :math:t' such that :math:t \trans{a} t' and :math:s' \mathrel{R} t'. - A symmetric simulation is called a *bisimulation*. - Two states :math:s and :math:t are called *strongly bisimilar* (or *strongly bisimulation equivalent*) iff there exists a bisimulation :math:R such that :math:s \mathrel{R} t. - Given two LTSs :math:T = (S, A, \to, s_0) and :math:T' = (S', A', \to', s'_0), we say that :math:T and :math:T' are strongly bisimilar iff :math:s_0 and :math:s'_0 are strongly bisimilar. .. figure:: /_static/articles/bisim_vs_trace.* :width: 50% :align: center These LTSs are trace equivalent, but not strongly bisimilar. Strong bisimilarity is a finer equivalence than trace equivalence, meaning it is stricter and relates less LTSs. An example showing the difference between strong bisimilarity and trace equivalence is given in the figure above. These LTSs model a game show in which the contestant can open one of two doors to determine the prize he/she will win. Behind one is a very luxurious car, behind the other a nice bouquet of flowers. In the red model, the contestant can somehow still choose the prize after opening a door. In the blue model, the choice is made as soon as he/she opens a door. According to trace equivalence, these models are equivalent. However, strong bisimilarity distinguishes the two: the blue model can simulate the *open_door* action by the red model, but in each of the resulting states it cannot simulate one of the *win* actions that the red model can perform. Branching bisimilarity """""""""""""""""""""" *Branching bisimilarity* (or *branching bisimulation equivalence*) is a variant of strong bisimilarity that treats :math:\tau actions in a special way. In cases where one of the LTSs under comparison contains internal actions, strong bisimilarity is often too strict and branching bisimilarity makes more sense. The idea behind branching bisimilarity is that an LTS may skip :math:\tau actions when simulating an action of the other LTS, but the intermediate states need to be related. (If the latter requirement is lifted, we obtain an equivalence known as *weak bisimilarity*.) Branching bisimilarity is formally defined as follows. - A relation :math:R on the states of an LTS is called a *branching simulation* if for any states :math:s, s', t and action :math:a, if :math:s \trans{a} s' and :math:s \mathrel{R} t then: - either :math:a = \tau and :math:s' \mathrel{R} t - or there exist states :math:t_1, t_2, t' such that :math:t \trans{\tau^*} t_1 \trans{a} t_2 \trans{\tau^*} t' and :math:s \mathrel{R} t_1, s' \mathrel{R} t_2 and :math:s' \mathrel{R} t'. - A symmetric branching simulation is called a *branching bisimulation*. - Two states :math:s and :math:t are called *branching bisimilar* (or *branching bisimulation equivalent*) iff there exists a branching bisimulation :math:R such that :math:s \mathrel{R} t. - Given two LTSs :math:T = (S, A, \to, s_0) and :math:T' = (S', A', \to', s'_0), we say that :math:T and :math:T' are branching bisimilar iff :math:s_0 and :math:s'_0 are branching bisimilar. Isomorphism """"""""""" One of the strongest equivalences is *isomorphism*. Two labelled transition systems are isomorphic if their *structure* is exactly the same. To compare, trace equivalence preserves a minimal amount of structure; only the order in which actions can occur is preserved. Bisimilarity, on the other hand, also preserves the branching structure. Formally, two LTSs :math:T = (S, A, \to, s_0) and :math:T' = (S', A', \to', s'_0) are isomorphic if, and only if, :math:A = A' and there is a bijective function :math:f mapping states from :math:S to :math:S' such that :math:f(s_0) = s'_0 and :math:s \trans{} s', for some :math:s, s' \in S, if and only if :math:f(s) \trans{}' f(s'). Effectively this means that the isomorphic LTSs are only allowed to differ in their labelling of states. Determinism ----------- An LTS is called *deterministic* if for every state :math:s and action :math:a, there is at most one state :math:t such that :math:s \trans{a} t. (Note that in the classical definition of determinism, in the context of finite state acceptors, there should be *precisely* one such :math:t for every :math:s and :math:a.) For example, in the figure above, the red LTS is deterministic, while the blue one is not. For deterministic LTSs, trace equivalence and strong bisimilarity coincide. This means that two LTSs are trace equivalent *if and only if* they are strongly bisimilar. As mentioned before, for nondeterministic LTSs we do not have the *only if* part, just the *if* part. We can also refer to determinism *modulo* an equivalence. We say an LTS :math:l is deterministic modulo an equivalence :math:e if, and only if, there is a deterministic LTS that is :math:e-equivalent to :math:l. Note that modulo trace equivalence every LTS is deterministic and that the normal notion of determinism (i.e. without *modulo*) corresponds to determinism modulo isomorphism.