Confluence Detection for Transformations of Labelled Transition Systems

TL;DR

This paper introduces new methods for efficiently detecting confluence in Labelled Transition System transformations, ensuring consistent model outputs regardless of transformation order.

Contribution

It presents novel observations, algorithms for confluence detection, and conflict resolution specifically tailored for LTS transformation systems.

Findings

New confluence detection algorithm for LTSs

Conflict resolution algorithm based on structural properties

More efficient confluence detection compared to general graph methods

Abstract

The development of complex component software systems can be made more manageable by first creating an abstract model and then incrementally adding details. Model transformation is an approach to add such details in a controlled way. In order for model transformation systems to be useful, it is crucial that they are confluent, i.e. that when applied on a given model, they will always produce a unique output model, independent of the order in which rules of the system are applied on the input. In this work, we consider Labelled Transition Systems (LTSs) to reason about the semantics of models, and LTS transformation systems to reason about model transformations. In related work, the problem of confluence detection has been investigated for general graph structures. We observe, however, that confluence can be detected more efficiently in special cases where the graphs have particular structural properties. In this paper, we present a number of observations to detect confluence of LTS transformation systems, and propose both a new confluence detection algorithm and a conflict resolution algorithm based on them.