Order-independence of vector-based transition systems

M. Raffelsieper, M.R. Mousavi, H. Zantema

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)
2 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings 10th International Conference on Application of Concurrency to System Design (ACSD'10, Braga, Portugal, June 21-25, 2010)
PublisherIEEE Computer Society
ISBN (Print)978-1-4244-7266-6
Publication statusPublished - 2010

Fingerprint Dive into the research topics of 'Order-independence of vector-based transition systems'. Together they form a unique fingerprint.

Cite this