STS reduction

[lou1306]

If two transitions t1, t2 have the same action and the same exit condition, then (maybe) we could remove t2 and update all transitions leading to t2 so that their exit condition leads to t1.

A simple case

Consider a.(b.0 + c.b.0). This gets encoded as

<1, a, 2 \/ 3> 
<2, b, 0> (t_b1)
<3, c, 4> (t_c)
<4, b, 0> (t_b2)

If we remove t_b2, and fix the exit condition of t_c, we get:

<1, a, 2 \/ 3>
<2, b, 0> 
<3, c, 2>

which still captures the behaviour of the process.

Rationale

This reduction could be applied repeatedly until no more triples are removed. If two agents share (partially or completely) the same behaviour, the reduction should significantly reduce the number of triples needed to encode the whole system