Matthias Raffelsieper, MohammadReza Mousavi and Hans Zantema. IET Computers & Digital Techniques, Institution of Engineering and Technology (IET), 2011. To appear.
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 its constituting 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 micro-steps 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 are only interested in the long-run behavior of the modeled system. Therefore, we also identify orders of interleaving input changes that behave differently during start-up, but compute the same next states afterwards. We demonstrate the applicability of our abstract criteria to the specification of transistor netlists.
@aricle{MousaviIET-CDT2011,
author = "Raffelsieper, Matthias and Mousavi, MohammadReza and Zantema, Hans",
title = "Long-Run Order-Independence of Vector-Based Transition Systems",
journal = "IET Computers \& Digital Techniques",
publisher = "Institution of Engineering and Technology (IET)",
year = "2011"
}