Comparing disjunctive modal transition systems with an one-selecting variant

models, used for specification, analysis and verification, usually describe sets of implementations by means of a refinement relation. In the branching time setting, implementations are commonly modeled as labeled transition systems (LTS). ssive class of abstractions for LTSs is that of disjunctive modal transition systems (DMTS), featuring may- and must transitions as well as disjunctive hypertransitions (OR). In order to describe exclusive choice adequately, we develop a variant of DMTSs called 1-selecting modal transition systems (1MTS) that, roughly , interprets hypertransitions exclusively (XOR). These abstract models, DMTSs and 1MTSs, are compared with respect to their expressive power. By giving transformations or showing their non-existence, we show that the two setting can express the same sets of implementations, but 1-selecting modal transition systems have a richer refinement preorder. s: underspecification, abstraction, refinement, expressiveness, branching time

• Type: Journal
• Year: 2008
• Where: JLP
• Authors: Harald Fecher, Heiko Schmidt
• Keywords: Disjunctive Modal Transition, JLP 2008, Modal Transition Systems, Transition Systems