Abstract
Embedded-systems designers often use transition system-based notations for specifying, with respect to some refinement preorder, sets of deterministic implementations. This paper compares popular such refinement settings - ranging from transition systems equipped with failure-pair inclusion to disjunctive modal transition systems - regarding the sets of implementations they are able to express. The paper's main result is an expressiveness hierarchy, as well as language-preserving transformations between various settings. In addition to system designers, the main beneficiaries of this work are tool builders who wish to reuse refinement checkers or model checkers across different settings. © 2010 Springer.
Cite
CITATION STYLE
Fecher, H., De Frutos-Escrig, D., Lüttgen, G., & Schmidt, H. (2010). On the expressiveness of refinement settings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5961 LNCS, pp. 276–291). https://doi.org/10.1007/978-3-642-11623-0_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
