Non-reducible Modal Transition Systems

Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Modal refinement (≼_m) of MTS represents a step of the design process, namely the one in which some optional behaviour is discarded while other optional behaviour becomes necessary. Whenever two MTS are not in modal refinement relation, it could still be the case that the set of implementations of one MTS is included in the set of implementations of the other. The challenge of devising an alternative notion of modal refinement that is both sound and complete with respect to the set of implementations, without disregarding valuable implementations, remains open. We introduce a subset of MTS called Non-reducible Modal Transition Systems (NMTS), together with a novel refinement relation ≼_n for NMTS. We illustrate through examples the additional constraints imposed by NMTS. Furthermore, we discuss a property holding for NMTS whose implementations are non-deterministic.