Affiliations: [a] Department of Computing and Software, McMaster University, Hamilton, ON, L8S 4K1, Canada. janicki@mcmaster.ca | [b] LIACS, Leiden University, P.O.Box 9512, NL-2300 RA Leiden, The Netherlands. h.c.m.kleijn@liacs.leidenuniv.nl | [c] School of Computing Science, Newcastle University, Newcastle upon Tyne NE1 7RU, UK. maciej.koutny@ncl.ac.uk | [d] Faculty of Mathematics and Computer Science, Nicolaus Copernicus University, Toruń, Chopina 12/18, Poland. frodo@mat.umk.pl
Correspondence:
[*]
Address for correspondence: LIACS, Leiden University, P.O.Box 9512 NL-2300 RA Leiden, The Netherlands
Abstract: A step trace is an equivalence class of step sequences which can be thought of as different observations of the same underlying concurrent history. Equivalence is determined on basis of a step alphabet that describes the relations between events in terms of potential simultaneity and sequentialisability. Step traces cannot be represented by standard partial orders, but require so-called invariant structures, extended order structures that capture the phenomena of mutual exclusion and weak causality. In this paper, we present an effective way of deciding whether an invariant structure represents a step trace over a given step alphabet. We also describe a method by which one can check whether a given invariant structure can represent a step trace over any step alphabet. Moreover, if the answer is positive, the method provides a suitable step alphabet.
