Publications:Long-run order-independence of vector-based transition systems
From CERES
| Title | Long-run order-independence of vector-based transition systems |
|---|---|
| Author | Matthias Raffelsieper and Mohammad Reza Mousavi and Hans Zantema |
| Year | 2011 |
| PublicationType | Journal Paper |
| Journal | IET Computers & Digital Techniques |
| HostPublication | |
| DOI | |
| Conference | |
| Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:583422 |
| 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 transition systems, each macro-step transition is labeled by a vector of inputs in which several inputs may change simultaneously. Each macro-step can thus be decomposed into a number of micro-steps, considering one input change at a time. This is akin to an interleaving semantics, where a concurrent step is represented by an interleaving of its constituting components. In this paper, the authors present abstract criteria on vector-based transition systems, which guarantee the next state computation to be independent of the execution order of micro-steps. If these abstract criteria are satisfied, then state-space generation or exploration algorithms only need to consider one representative among all possible permutations of micro-steps. For most practical applications only the system's long-run behaviour is of relevance and the transient start-up phase can be ignored. Hence, the authors customise their generic techniques to focus on the long-run behaviour and identify orders of interleaving input changes that may behave differently during start-up, but compute the same next states in the long-run behaviour. Applicability of the developed abstract criteria is demonstrated for specifications of transistor netlists. ©2011, IEEE. |
