Transition Systems

A transition system (warning: this is not what is often called a labelled transition system) is an object of type:
         (Sigma S : Set) S -> 
         (Sigma T : Set) T -> S
[ I use the convention that the scope of a quantifier like (Sigma x : T)... extends as far to the right/down as possible. ] So a transition system has the generic form:
         (S, \s->(T(s),\t->p(s,t)))
     where    S is a set                       -- base set of states
              T(s) is a set, for s : S         -- transitions from s
              p(s,t) : S, for s : S, t : T(s)  -- destination of t from s
For the sake of readability, I often write the destination of a transition using square brackets, writing s[t] instead of p(s,t) . Usually one can tell which destination function is meant from the context.

In terms of the notion of family, one can define a transition system to be a coalgebra for the endofunctor Fam (on a suitable category of types).

          S : Set, Tp : S -> Fam S
Compare this with a binary relation:
          S : Set,  R : S -> Pow S
where Pow refers to the contravariant endofunctor Pow .

It is useful to refer to a function f : S -> Fam S as a transition structure for a set S . So a transition system is a set together with a transition structure on it.


So what are morphisms between transition systems? Personally, I am not sure, and do not mind not being sure, so long as it isn't a permanent condition. All the formulations that have occurred to me have involved a notion of equality between states. For example it would be quite natural to define a map between (S1,T1,p1) and (S2,T2,p2) to be

I do not like postulating that there is an a-priori equivalence relation between states. There is something very odd about the idea of equality between states - where "state" refers to something real we are interested in modelling, rather that the mathematical value with which we model it. What does it mean that state1 = state2 or state1 /= state2 if the variables state1, state2 refer to states of the physical universe? In principle that is something you could never detect, within the universe. I prefer to think about "states" as a construction from transitions, or rather the actions by which transitions are brought about. If the notion of equality between states is subtle, then the notion of equality between transitions from "the same" state is obviously even more subtle.

Conceptual cousins

Transition systems are related conceptually to what I call interactive systems, which `split' a transition into a positive and negative part. I don't fully understand the relationship between transition systems and interactive systems. One can in some senses "capture" an interactive system with a pair of transition systems. Interactive systems are closer to the concurrency-theorists' labelled transition systems; namely, (in their unrooted form,) triples (S,L,R) where S, L : Set and R : Pow (S*L*S) . The differences lie in replacing the set L with a family of sets indexed by S ( L(s) is the set of labels emerging from a given state), and the ternary relation R by a binary function mapping a state and a label leading from it to the family of states to which it can lead.

A transition structure on families

A family of sets is an ordered pair (A,B) where A : Set and B : A -> Set . So Fam Set is a type, or large set. Let us however ignore this "size consideration" for the moment and pretend that F = Fam Set is a set, and so can be the state space of a transition system. We can put the following transition structure on F . The transitions from (A,B) are defined to have type
        Tfam (A,B) = (Sigma a : A) B a -> A : Set
The destination states of the transitions are given by
        (A,B)[a,b] = (B a, B . b) : F 
where ` _ . _ ' refers to composition. To see that this type checks, remember that a : A , b : B a -> A and B : A -> Set , so B a : Set and B . b : B a -> Set .

A chain starting from (A,B) : Fam Set has the form

              | (a,b) : (Sigma a : A) B a -> A
            (A',B') = (B a, B . b) 
              | (a',b') : (Sigma a' : B a) (B . b) a' -> B a
            (A'',B'') = ((B . b) a', B . b . b')
              | (a'',b'') : (Sigma a'' : (B . b) a') (B . b . b') a'' -> (B . b) a'
             (A''',B''') = ((B . b . b') a'', B . b . b' . b'')
and so on. Each successive family of sets is a "internal refinement" or restriction of its predecessor.

Now, what about size questions? I have defined a transition system to have a set of states. The situation appears to be this. For each fixed family of sets (A,B) we can put a transition structure on the set of "internal-families" of (A,B) , ie the set

            sfam (A,B) = (Sigma a : A) B a -> A 
Namely, we take as transition sets
             T : sfam (A,B) -> Set
             T(a,b) =  (Sigma c : B a) B (b c) -> B a
                    =  sfam (B a, B . b) 
and as destinations
             _[_] : (Pi (a,b) : sfam (A,B)) T (a,b) -> sfam (A,B) 
             (a,b)[c,d] = (b c, b . d) 
                          where a : A
                                b : B a -> A
                                c : B a
                                d : B (b c) -> B a
In other words, we can replace talk of "sets" by talk of "small sets".

At the moment I don't understand this transition structure. Is it well-founded? Transitive? I need some examples.

Suppose (A,B) is the family of finite sets. ...

Reflexive and transitive closure

If Phi(s) = (T(s), \t-> s[t]) is a transition structure on a set S , then we can form its reflexive and transitive closure Phi*(s) = (T^{t}(s), \t-> s[t]) as follows.
          T^{t} (s : S) = 1 + (Sigma t : T(s)) T^{t} (s[t])
          s[0] = s
          s[(t,ts)] = s[t][ts]
Note how the notation here is actually slightly abusive: s[t] is the t 'th immediate predecessor of s with respect to the original transition structure, while s[t][ts] is the ts 'th of that predecessor with respect to the transition structure T^{t} . To be pedantic, I should write something like s[(t,ts)]^{t} = s[t][ts]^{t} .

One can present reflexive and transitive closure as the least fixed point of a certain monotone operation on transition structures, as follows. (The order, and hence monotonicity will not be apparent yet.)

Then the reflexive and transitive closure of a transition structure phi : S -> Fam S can be written as a least fixed point
          mu psi : S -> Fam S .
             SKIP |_| (phi ; psi)
of the monotone operator
          X |->  SKIP |_| (phi ; X)
on the transition structures on a set. (Here we define f .le. g to mean that the induced predicate transformers are pointwise related by inclusion. (f^{d}) \subseteq (g^{d}) . See below.)

One can compare the construction of the free category over a directed graph with the construction of the reflexive transitive closure of a transition structure. One can think of the set S of states of a transition system as vertices of a directed graph, of T(s) as the set of arrows with source/target s and of s[t] as the target/source of arrow t . To form the free category over such a graph, one takes the arrows in it to be paths (ie. finite sequences of zero or more consecutive edges) in the graph. I have chosen to build up paths `cons' style, with the new edge going always `on the left'. there are other definitions. For example, `snoc'-style, with the new edge going always `on the right'. Also `cat' paths, built up from the empty path and the given edges by binary concatenation; in this case however one has to build into the definition of equality between such paths that they form a monoid.

Predicate transformers

Associated with a transition structure Phi(s) = (T(s), \t-> s[t]) on a set S are two predicate transformers which I shall write Phi^{a} and Phi^{d} for `angelic' and `demonic'. (Just regard these as labels. I doubt the metaphor of angels and demons is really appropriate.)
          Phi^{a}, Phi^{d}  :  Pow S -> Pow S
          Phi^{a} (P : Pow S, s : S)   = (Pi    t : T s) P (s[t])
          Phi^{d} (P : Pow S, s : S)   = (Sigma t : T s) P (s[t])
I define f .le. g to mean f^{d} .le. g^{d} as predicate transformers.

Note that (where x . y means composition)

          (f;g)^{a}    = (f^{a}) . (g^{a})
          (f;g)^{d}    = (f^{d}) . (g^{d})

          (SKIP)^{a} = (SKIP)^{d} 
          = the identity predicate transformer

          -- ? (f |_| g)^{a}(P) = (f^{a})(P) \cap (g^{a})(P)
          (f |_| g)^{d}(P) = (f^{d})(P) \cup (g^{d})(P)
(Or should that be the other way round?) Clearly both these predicate transformers are monotone (with respect to the inclusion ordering on predicates). The least fixed point of (Phi^{a}) is the predicate which describes the well-founded (aka accessible) states in the transition system: any sequence of transitions from such a state terminates in a dead state. (Such a state might be called mortal in the sense that it will inevitably die.) On the other hand, the greatest fixed-point of (Phi^{d}) is the predicate which describes `potentially immortal' states from which there is an infinite sequence of transitions.

The other extreme fixed points of these predicate transformers are uninteresting. The greatest fixed-point of (Phi^{a}) is extensionally equal to the predicate which is everywhere True . The least fixed-point of (Phi^{d}) is extensionally equal to the predicate which is everywhere empty.

Relation transformers

If (S,\s->(T(s),\t->s[t])) is a transition system, then a binary relation R between states is a simulation if R is included in R' where
      R'(s1,s2) = (Pi t1 : T(s1))(Sigma t2 : T(s2))R(s1[t1],s2[t2])
It is a bisimulation if R is included in both R' and (converse of R)' . Note that being a simulation or a bisimulation is a second order, impredicative property of binary relations. It requires an existential quantifier over all binary relations to form the union of all simulations or all bisimulations on a set. The relation
    \ (s,s') -> (Sigma R : S -> S -> Set) R \subseteq R' /\ R(s,s') 
is large.

As a kind of dual of the transformer ()' above, we can consider

      R`(s1,s2) = (Sigma t1 : T(s1))(Pi t2 : T(s2))R(s1[t1],s2[t2])
The property that R` is included in R , is equivalent to
      (Pi t1 : T(s1)) [(Pi t2 : T(s2))R(s1[t1],s2[t2])] => R(s1,s2) 
I have no idea what to call a relation with this property.

My best intuition of what S is is as follows. Imagine a 2-player game in which the protagonist first chooses a transition from s1 , and the responder next chooses a transition from s2 , and so on. The protagonist wins by making a move to which there is no response, i.e. when the responder is in a dead (minimal) state. In terms of this game, S(s1,s2) holds if the protagonist has a winning strategy when starting in state s1 with the responder in state s2 . The strategy can be represented by a well-founded tree, with the nodes represented by the protagonist's transitions, and the arrows by the reponder's. One might say that s1 exceeds, or is beyond s2 , which has shortcomings with respect to s1 . The intuition is that part of s1 cannot be simulated by s2 .

We can also define the notion of a win by the responder, in which the protagonist reaches a state in which there are no further moves. (It is not meaningful to ask whether the responder might somehow have run out of moves at the same time.)

These are interesting notions, I think, because winning and losing correspond to "bugs", or contests in which one player vanquishes the other at some point in time. The complementary situation is one in which there is no winning and losing, but the game runs harmoniously forever. (This is something we desire in real-life "games", like sending requests to servers and getting responses, and perhaps too in marriage.)

Suppose we say that two states are upper-equivalent when the same states are beyond them, and lower-equivalent when they are beyond the same states. These are obviously equivalence relations.

Arithmetic of transition systems

Peter Hancock
Last modified: Fri Sep 15 17:43:33 BST 2000