This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2010 10th International Conference on Application of Concurrency to System Design
Order-Independence of Vector-Based Transition Systems
Braga, Portugal
June 21-June 25
ISBN: 978-0-7695-4066-5
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 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 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 criteria to the specification of transistor netlists.
Index Terms:
Vector-based transition systems, Moore machines. Order independence, Partial order reduction, Model checking
Citation:
Matthias Raffelsieper, MohammadReza Mousavi, Hans Zantema, "Order-Independence of Vector-Based Transition Systems," acsd, pp.115-123, 2010 10th International Conference on Application of Concurrency to System Design, 2010
Usage of this product signifies your acceptance of the Terms of Use.