TY  - GEN
EP  - 8
KW  - Lattices
KW  -  Boolean algebra
KW  -  Runtime
KW  -  Software product lines
KW  -  Encryption
KW  -  Games
CY  - Danvers (MA), USA
A1  - Beohar, H
A1  - König, B
A1  - Küpper, S
A1  - Silva, A
SP  - 1
AV  - public
ID  - discovery10060796
N1  - This version is the author accepted manuscript. For information on re-use, please refer to the publisher?s terms and conditions.
TI  - Conditional transition systems with upgrades
PB  - IEEE
N2  - We introduce a variant of transition systems, where activation of transitions depends on conditions of the environment and upgrades during runtime potentially create additional transitions. Using a cornerstone result in lattice theory, we show that such transition systems can be modelled in two ways: as conditional transition systems (CTS) with a partial order on conditions, or as lattice transition systems (LaTS), where transitions are labelled with the elements from a distributive lattice. We define equivalent notions of bisimilarity for both variants and characterise them via a bisimulation game. We explain how conditional transition systems are related to featured transition systems for the modelling of software product lines. Furthermore, we show how to compute bisimilarity symbolically via BDDs by defining an operation on BDDs that approximates an element of a Boolean algebra into a lattice. We have implemented our procedure and provide runtime results.
UR  - https://doi.org/10.1109/TASE.2017.8285624
Y1  - 2018/02/12/
ER  -