Order-Independence of Vector-Based Transition Systems

M. Raffelsieper, M.R. Mousavi and H. Zantema. . Proceedings of the 10th International Conference on Application of Concurrency to System Design (ACSD'2010), Braga, Portugal, IEEE Computer Society Press, June 2010.

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 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 demonstrate the applicability of our abstract criteria to the specification of transistor netlists.

(Paper in .pdf format)  

@InProceedings{MousaviAcsd10,
    author      = "Raffelsieper, Matthias and Mousavi, MohammadReza and Zantema, Hans",
    title       = "Order-Independence of Vector-Based Transition Systems",
    booktitle   = "Proceedings of the 10th International Conference on Application of Concurrency to System Design (ACSD'2010)",
    publisher   = "IEEE Computer Society Press, 2010"
}