Please use this identifier to cite or link to this item:
Title: Modal Transition System Encoding of Featured Transition Systems
Authors: Varshosaz, Mahsa
Luthmann, Lars
Mohr, Paul
Lochau, Malte
Mousavi, Mohammad Reza
First Published: 19-Mar-2019
Publisher: Elsevier
Citation: Journal of Logical and Algebraic Methods in Programming, 2019
Abstract: Featured transition systems (FTSs) and modal transition systems (MTSs) are two of the most prominent and well-studied formalisms for modeling and analyzing behavioral variability as apparent in software product line engineering. On one hand, it is well-known that for finite behavior FTSs are strictly more expressive than MTSs, essentially due to the inability of MTSs to express logically constrained behavioral variability such as persistently exclusive behaviors. On the other hand, MTSs enjoy many desirable formal properties such as compositionality of semantic refinement and parallel composition. In order to finally consolidate the two formalisms for variability modeling, we establish a rigorous connection between FTSs and MTSs by means of an encoding of one FTS into an equivalent set of multiple MTSs. To this end, we split the structure of an FTS into several MTSs whenever it is necessary to denote exclusive choices that are not expressible in a single MTS. Moreover, extra care is taken when dealing with infinite behaviour: loops may have to be unrolled to accumulate FTS path constraints when encoding them into MTSs. We prove our encoding to be semantic-preserving (i.e., the resulting set of MTSs induces, up to bisimulation, the same set of derivable variants as their FTS counterpart) and to commute with modal refinement. We further give an algorithm to calculate a concise representation of a given FTS as a minimal set of MTSs. Finally, we present experimental results gained from applying a tool implementation of our approach to a collection of case studies.
DOI Link: 10.1016/j.jlamp.2019.03.003
ISSN: 2352-2208
Embargo on file until: 19-Mar-2020
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: Copyright © Elsevier 2019. After an embargo period this version of the paper will be an open-access article distributed under the terms of the Creative Commons Attribution-Non Commercial-No Derivatives License (, which permits use and distribution in any medium, provided the original work is properly cited, the use is non-commercial and no modifications or adaptations are made.
Description: The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
main.pdfPost-review (final submitted author manuscript)473.2 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.