Interleaving isotactics - An equivalence notion on behaviour abstractions

We study the equivalence of models that capture the behaviour of systems, such as process-oriented information systems. We focus on models that are not related by a bijection over their actions, but by an alignment between sets of their actions. For this setting, we propose interleaving isotactics as an equivalence notion based on abstractions that are induced by the alignment. We demonstrate that this notion is grounded in trace equivalence, provide a temporal logic characterisation of the properties it preserves, prove decidability of the respective verification problems, and present an implementation of a decision procedure for the equivalence notion.