Step transition systems form a powerful model to describe the concurrent behaviors of distributed or parallel systems. They offer also a general framework for the study of marking graphs of Petri nets [22]. In this paper we investigate a natural labeled partial order semantics for step transition systems. As opposed to [19] we allow for autoconcurrency by considering steps that are multisets of actions. First we prove that the languages of step transition systems are precisely the width-bounded languages that are step-closed and quasi-consistent. Extending results from [19] we focus next on finite step transition systems and characterize their languages in the line of Buchi's theorem. Our main result present six equivalent conditions in terms of regularity and MSO-definability for a set of labeled partial orders to be recognized by some finite step transition system.
展开▼
