|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| 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
| ASCII Text | x | ||
| Matthias Raffelsieper, MohammadReza Mousavi, Hans Zantema, "Order-Independence of Vector-Based Transition Systems," 2010 10th International Conference on Application of Concurrency to System Design, pp. 115-123, 2010 10th International Conference on Application of Concurrency to System Design, 2010. | |||
| BibTex | x | ||
| @article{ 10.1109/ACSD.2010.24, author = {Matthias Raffelsieper and MohammadReza Mousavi and Hans Zantema}, title = {Order-Independence of Vector-Based Transition Systems}, journal ={2010 10th International Conference on Application of Concurrency to System Design}, volume = {0}, year = {2010}, issn = {1550-4808}, pages = {115-123}, doi = {http://doi.ieeecomputersociety.org/10.1109/ACSD.2010.24}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - 2010 10th International Conference on Application of Concurrency to System Design TI - Order-Independence of Vector-Based Transition Systems SN - 1550-4808 SP115 EP123 A1 - Matthias Raffelsieper, A1 - MohammadReza Mousavi, A1 - Hans Zantema, PY - 2010 KW - Vector-based transition systems KW - Moore machines. Order independence KW - Partial order reduction KW - Model checking VL - 0 JA - 2010 10th International Conference on Application of Concurrency to System Design ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2010.24
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.
