Labelled 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 can interleave arbitrarily, and the resulting LTS quickly becomes too complex for the human eye to understand easily.
With that in mind, we propose a formalization of these arbitrary interleavings, dubbed diamond patterns. We present the current work on these diamonds and their related properties.
And, hoping to reduce the aforementioned visual complexity caused by these patterns, we present an algorithm to find such diamonds in deterministic LTSs, such that the multiple states and transitions that make up a diamond can be rewritten into a simple singular macro-action.
This is joint work with Kevin Jilissen.