[MUSIC] In this lecture we will define what it means for two transition systems to be trace equivalents. So we are now interested in the notion of trace equivalence and for that we need to know what a trace of a system is. So a trace is essentially a sequence of actions that can be executed and here we will write down the set of traces of this process. So the first trace that you can do is simply the empty trace, the trace where you do no action at all and that's generally written as an epsilon. Here we have an a action, that's the action you can do from the initial state. You can do an a b action, and you can do the trace a c, and there are all the possibilities of this transition system. When are two transition systems equivalent? Well, they are equivalent if the set of traces of the two transition systems are the same. So consider these two transition systems. Are they the same? Well for that purpose, we need to find down a set of traces of the transition system on the right hand here, it is. And what we see is that the set of transition consists of epsilon and a, the a only occurs once of the epsilon only occur once in the set. We have ab and ac, and what we see is that this set is exactly the same as the set to the left. And so these two transition systems are trace equivalent. Okay, let's look at this example and let's add a tick to indicated absolute a and to b you can actually terminate. What are the traces now? Well what we do is we allow it to add optionally, the possibility to write down the stick after a trace to indicate that you can terminate after the ab actions. So this is the set of traces. Is this transition system now equivalent to the transition system on the right? The answer is no. Because we had already seen this set of traces and this set of traces is different from the set of traces at left. Trace equivalence, although it's an intuitive notion has a number of nasty properties and the most unpleasant one is that it does not preserve all those notions that we expect a behavioral equivalence to preserve. One of these examples is a deadlock. So a look at this tradition system, we can do an a and a b and then it terminates. And now, also look at this transition system which is almost the same, except that it can also an a transition to a deadlocked stage. If we write down the traces of this transition system and of this one. We notice that the tracers are exactly the same. So these two transition systems are equivalent but one has deadlock and the other has not. bisimulation does not have this nasty property. A trace equivalent is sometimes affected, does have this. A few properties about bisimulation and trace equivalence. So one of the observations that people did to do was that calculation, the calculation of bisimulation is relatively efficient. There is a well-known algorithm of that's required order m log n time, n the number of states m the number of transitions of a transition system. And that is pretty efficient. For trace equivalence we have a completely different situation. Determining trace equivalency is PSpace complete and this means that it's not conceivable that we can ever calculate trace equivalency in an efficient way at all. Another useful fact is the following, namely if two states are bisimilar, then they are also trace equivalent. And if we have two deterministic transition systems and we would like to know whether they are the same, then it's useful to know that bisimulation and trace equivalence coincides. So just to recall, if a transition system has this pattern with two outgoing a's from one state then it's non-deterministic. And then bisimulation and trace equivalence are really different notions. Okay, let's do an exercise. Look at these two transition systems that represents the behavior of an alarm clock. And the question is are these two trace equivalent? Another exercise here we have two slightly more complex looking transition systems. And the question is can you determine whether they are trace equivalent? And here we have a question that is known to be somewhat tricky. Can you determine whether these two transition systems are actually bisimular or not? Okay, we defined the notion of trace equivalence, conceptually trace equivalents are very easy and much easier than the definition of bisimulation. But trace equivalence relates behaviors that are sometimes not seen as being equivalent such as behaviors with deadlock and behaviors without deadlock. And quite remarkably bisimulation is rather easy to compute and trace equivalence on average is rather harder to compute by computers. Thank you for watching. In the next lecture, we will do something fairly important, namely introduce the notion of a hidden or internal action. [MUSIC]