Mixed Transition Systems Revisited

—A variety of partial modeling formalisms, aimed re and reason about abstractions, have been proposed. Some, e.g., Kripke Modal Transition Systems (KMTSs) put strong restrictions on necessary and possible behaviours. Some, e.g., Mixed Transition Systems (MixTSs), relax these restrictions. Yet others, e.g., Generalized Kripke MTSs (GKMTSs), allow hypertransitions. In this paper, we aim to understand trade-offs between these formalisms w.r.t. their applicability to symbolic model-checking. We establish that these formalisms have the same expressive power while differing in succinctness. We also measure the analyzability of these formalisms, measured as the precision of computing compositional semantics of temporal logic formulas. We show that the standard compositional semantics is not preserved between equivalent GKMTSs and MixTSs, and introduce a novel semantics, called reduced, which remains compositional while being both more precise than the standard one and preserved by the seman...

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Ou Wei, Arie Gurfinkel, Marsha Chechik
• Keywords: Compositional Semantics, Partial Modeling Formalisms, Software Engineering, Transition Systems, VMCAI 2009