Publications:Order-independence of vector-based transition systems

Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Order-independence of vector-based transition systems
Author M. Raffelsieper and Mohammad Reza Mousavi and H. Zantema
Year 2010
PublicationType Conference Paper
HostPublication Proceedings 10th International Conference on Application of Concurrency to System Design (ACSD’10, Braga, Portugal, June 21-25, 2010)
Conference The 10th International Conference on Application of Concurrency to System Design
Diva url
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. © 2010 IEEE.