Sciweavers

JLP
2008

Comparing disjunctive modal transition systems with an one-selecting variant

13 years 11 months ago
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
Harald Fecher, Heiko Schmidt
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JLP
Authors Harald Fecher, Heiko Schmidt
Comments (0)