Publications:Order-independence of vector-based transition systems
From CERES
| Title | Order-independence of vector-based transition systems |
|---|---|
| Author | M. Raffelsieper and Mohammad Reza Mousavi and H. Zantema |
| Year | 2010 |
| PublicationType | Conference Paper |
| Journal | |
| HostPublication | Proceedings 10th International Conference on Application of Concurrency to System Design (ACSD’10, Braga, Portugal, June 21-25, 2010) |
| DOI | http://dx.doi.org/10.1109/ACSD.2010.24 |
| Conference | The 10th International Conference on Application of Concurrency to System Design |
| Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584488 |
| 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. |
