Mining Diamonds in labeled Transition Systems

TL;DR

The paper addresses visual clutter in labeled transition systems (LTSs) caused by independent interleavings of asynchronous actions. It defines the diamond pattern as the interleaving of monotone sequences with non-monotone sequences, enabling a compact representation where a diamond captures parallelism with counts described by components $C_a$ and $C_s$. The authors prove that strong bisimulation exactly preserves diamond convergence and present a constructive algorithm to enumerate all maximal diamonds in any LTS, with correctness guarantees. They discuss connections to partial order reduction (POR), arguing that diamond-based reduction preserves a stronger set of properties (e.g., CTL$^*$) and outline future work and practical implications for visualisation and state-space reduction.

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.