UTILIZING SYMMETRY WHEN MODEL-CHECKING UNDER FAIRNESS ASSUMPTIONS - AN AUTOMATA-THEORETIC APPROACH

One useful technique for combating the state explosion problem is to e xploit symmetry when performing temporal logic model checking. In prev ious work it is shown how, using some basic notions of group theory, s ymmetry may be exploited for the full range of correctness properties expressible in the very expressive temporal logic CTL. Surprisingly, while fairness properties are readily expressible in CTL, these metho ds are not powerful enough to admit any amelioration of state explosio n, when fairness assumptions are involved. We show that it is nonethel ess possible to handle fairness efficiently by trading some group theo ry for automata theory. Our automatatheoretic approach depends on dete cting fair paths subtly encoded in a quotient structure whose arcs are annotated with permutations, by using a threaded structure that refle cts coordinate shifts caused by the permutations.