Module 2.2: Non-deterministic automata

Depending on the context in which it is used, non-determinism can mean different things. Different communities also use different definitions, and some communities only use one of the definitions, and use a different name to refer to the other concept.

One definition of non-determinism is that multiple transitions are possible, for different events. In other words, there are multiple possible traces through the state space. In this course, as well as generally in CIF, this is not considered non-determism as it involves different events.

Another definition of non-determinism, and the one used in this course and also generally in CIF, is the presence of multiple possible transitions for the same event from a single state. For instance, consider the following CIF model:

                        
                            automaton coin_toss:
                                event toss, pick_up;

                                location coin_in_hand:
                                    initial;
                                    marked;
                                    edge toss goto heads;
                                    edge toss goto tails;

                                location heads:
                                    edge pick_up goto coin_in_hand;

                                location tails:
                                    edge pick_up goto coin_in_hand;
                            end
                        
                    

Initially, a coin is in your hand. You can toss the coin, and it can land in two different ways, with either heads or tails on top. In either case, you can pick up the coin and toss it again. The outcome of the coin toss is non-deterministic, as it is either heads or tails, and this is not known in advance. That is, in location coin_in_hand, two transitions are possible for the same event, with different next states (going to location heads or tails), and this choice is random.

In the coin toss example, the presence of non-determinism is easy to spot, as there are two edges for event toss in location coin_in_hand, and they lead to different states (different target locations). But, multiple edges for the same event in the same location does not always lead to non-determinism. If the edges lead to the same state, they are essentially the same edge, and thus there is no non-determinism. And if the edges have guards that ensure they are not enabled at the same time, then there is also no non-determinism. For instance, consider the following model:

                        
                            automaton a:
                                event e;
                                disc bool v;

                                location x:
                                    initial;
                                    marked;
                                    edge e when     v goto y;
                                    edge e when not v goto z;

                                location y;

                                location z;
                            end
                        
                    

There are two edges for event e from location x, but they are never enabled at the same time. If v is true then the first edge is enabled, but the second is not. And if v is false then the second edge is enabled, while the first is not. Thus always only one of the edges is enabled, and there is no non-determinism.

Non-determinism can be useful, like when modeling the coin toss, but for most models it is not needed. And some CIF tools do not support non-determinism in certain cases.

Quiz

                                        
                                            automaton a:
                                                event e, f, g, h, i;
                                                disc int v;

                                                location x:
                                                    initial;
                                                    marked;
                                                    edge e when v <  4           goto y;
                                                    edge e when v >  4           goto z;
                                                    edge f when v <= 4           goto y;
                                                    edge f when v >  4           goto z;
                                                    edge g when v <= 4           goto y;
                                                    edge g when v >= 4           goto z;
                                                    edge h when v <  4 and 4 < v goto y;
                                                    edge h when v  = 4           goto z;
                                                    edge i when v  = 4           goto y;

                                                location y;
                                                    edge i when v  = 4           goto z;

                                                location z;
                                            end