Layered Reduction for Modal Specification Theories

摘要

Modal transition systems (MTSs) are a well-known formalism used as an abstraction theory for labeled transition systems (LTSs). MTS specifications support compositionality together with a step-wise refinement methodology, and thus are useful for component-oriented design and analysis of distributed systems. This paper proposes a state-space reduction technique for such systems that are modeled as a network of acyclic MTSs. Our technique is based on the notion of layered transformation. We propose a layered composition operator for acyclic MTSs, and prove the communication closed layer (CCL) laws. Next, we define a partial order (po) equivalence between acyclic MTSs, and show that it enables performing layered transformation within the framework of CCL laws. We also show the preservation of existential ((E)) and universal ((A)) reachability properties under this transformation.