Conditional Transition Systems with Upgrades

TL;DR

This paper introduces conditional transition systems with environment-dependent transitions and upgrades, modeling them as lattice transition systems, and develops symbolic bisimilarity computation methods with practical implementation results.

Contribution

It presents a novel formalism for transition systems with upgrades, linking them to lattice theory, and provides a symbolic bisimilarity algorithm with implementation.

Findings

Bisimilarity can be characterized via a bisimulation game.

Symbolic bisimilarity computation is feasible using BDDs.

The implementation shows practical runtime performance.

Abstract

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.