The Power of Prime Cycles

In this paper, we shall examine properties of labelled transition systems which are motivated by system synthesis. Most of them are necessary conditions for synthesis by Petri nets to be successful. They can be checked in a pre-synthesis phase, allowing the immediate rejection of transition systems not satisfying them as non-synthesisable. The order of checking such conditions plays an important role in pre-synthesis optimisation. It is particularly desirable to know which conditions are implied by others, especially if the latter can be machine-verified more simply than the former. The purpose of this paper is to describe some mathematical results exhibiting a number of such implications.Two properties called strong cycle-consistency and full backward determinism, respectively, are particularly hard to check. They are generalised counterparts of the marking equation of Petri net theory. We show that under some circumstances, they may be deduced from other properties which are easier to check. Amongst these other properties, the prime cycle property plays a particularly important role, not just because it is strong enough to imply others, but also because it is interesting to be checked on its own, if synthesis is targetted towards choice-free Petri nets.