Order-Independence of Vector-Based Transition Systems

Abstract--Semantics of many specification languages, particularly those used in the domain of hardware, is described in terms of vector-based transition systems. In such a transition system, each macro-step transition is labeled by a vector of inputs. When performing a macro-step, several inputs may potentially change. Each macro-step can thus be decomposed in a number of micro-steps, taking one input change at a time into account. This is akin to an interleaving semantics, where a concurrent step is represented by an interleaving of tituting components. We present abstract criteria on vector-based transition systems, which guarantee that the next state computation is independent of the order in which these eps are executed. If our abstract criteria are satisfied by the semantic definition of a certain specification, then its state-space generation or exploration algorithm needs to only consider one representative among all possible permutations of such micro-steps. We demonstrate the ...

• Type: Journal
• Year: 2010
• Where: ACSD
• Authors: Matthias Raffelsieper, Mohammad Reza Mousavi, Hans Zantema
• Keywords: ACSD 2010, Hardware, Semantic, Transition Systems, Vector-based Transition Systems