Nonsequential automata semantics for a concurrent object-based language

Abstract

Nonsequential automata constitute a categoria! semantic domain based on labeled transition system with full concurrency, where synchronization and hiding are functorial anda class of morphisms stands for reification. It is, for our knowledge, the first model for concurrency which satisfies the diagonal compositionality requirement, i. e., reifications compose (vertical) and distribute over combinators (horizontal). To experiment with the proposed semantic domain, a semantics for a concurrent, object-based language is given. 1t is a simplified and revised version of the object-oriented specification language GNOME, introducing some special features inspired by the semantic domain such as reification and aggregation. The diagonal compositionality is an essential property to give semantics in this context.