Mining Diamonds in labeled Transition Systems

TL;DR

This paper introduces a formal method and algorithm to identify all possible interleavings in deterministic labeled transition systems, simplifying their visualization by reducing complexity caused by parallel process interleavings.

Contribution

It provides an exact formalization and an efficient algorithm to enumerate all interleavings in deterministic LTSs, aiding better understanding of system behaviors.

Findings

Algorithm successfully enumerates all interleavings

Reduces visual complexity of LTS diagrams

Enhances comprehension of parallel system behaviors

Abstract

Labeled transition systems can be a great way to visualize the complex behavior of parallel and communicating systems. However, if, during a particular timeframe, no synchronization or communication between processes occurs, then multiple parallel sequences of actions are able to interleave arbitrarily, and the resulting graph quickly becomes too complex for the human eye to understand easily. With that in mind, we propose an exact formalization of these arbitrary interleavings, and an algorithm to find all said interleavings in deterministic LTSs, to reduce the visual complexity of labeled transition systems.