Compact Transition Systems

A major drawback of representing concurrent systems as transition systems is the exponential size of their semantic representations. We present a way of obtaining compact transition systems that are mildly exponential in average. The idea is to have (at least) one computation to represent all the ones only differing for the temporal ordering in which concurrent transitions occur. We characterise through axioms the transition systems which may be reduced in size, still preserving non interleaving bisimulation equivalences. We also exemplify our reduction technique on a process calculus whose compact transition system is generated in SOS style.