Diagonal compositionality of concurrent, finite state systems

In previous works together with J . Félix Costa and A. Sernadas, we construct a categoria} semantic domain called Nonsequential Automata (first introduced in [10]), based on labeled transition systems [15] with full concurrency, inspired by [14], where synchronization and hiding are functorial defined using fibration and cofibration techniques based on [9] and inspired by [24] . Moreover, a class of morphisms stands for reification which satisfies the diagonal compositionality requirement, i.e., reifications compose (vertically), reflecting the stepwise description of systems, involving severallevels of abstraction, and distributes through combinators (horizontally), meaning that the reification of a composite system is the composition of the reification of its parts. In [10] and [11] we show (through adjunctions) that nonsequential automata are more concrete then Petri nets extending the approach in [17] , where a formal framework for classification of models for concurrency is set. In fact, nonsequential automaton is the Ieast concrete (or more abstract) levei among related models which satisfies the diagonal compositionality requirement. To experiment with the proposed semantic domain, a semantics for a concurrent, object-based specification language (using the terminology of [23]) is given in [13] . The language named Nautilus is based on the object-oriented language GNOME [18] which is a simplified and revised version ofOBLOG [20], [21], [19] . Some features inspired by the semantic domain (and not present on GNOME) such as reification and aggregation are introduced. Also, the state-dependent calling of GNOME is extended for interaction, aggregation and reification in Nautilus. The diagonal compositionality requirement is essential to give semantics for Nautilus. Since the techniques proposed for nonsequential automata such as the reification and synchronization could provide some interesting and elegant solutions for finite state systems, we derive a new categoria} framework named Nonsequential Finite Automata which is outlined in this paper. A nonsequential finite automaton is a kind of automaton with structured states and transitions. Structured states, inspired by [14] are "bags" of local states like tokens in Petri nets (as in [16]) and structured transitions are finite and specify a concurrency relationship between component transitions in the sense of [1] and [7] . Comparing the graphical representations of nonsequential finite automata and asynchronous transition systems, the independence relation in a nonsequential finite automaton is explicit. The labeling of transitions is not extensional in the sense that it allows the occurrence of more than one transition with the same label. Also, nonsequential finite automata are equipped with initial and final states, inspired by [8]. The resulting category is complete and cocomplete with products isomorphic to coproducts. The categoria! product (or coproduct) stands for parallel composition. The behavior of a nonsequential finite automaton is given by its transitive closure, i.e. , the automaton is enriched with ali conceivable sequential and nonsequential computations that can be split into permutations of original transitions, respecting source and target states, inspired by [14] . This transitive closure is induced by an adjunction between a category of categorias and the category of nonsequential tini te automata, as illustrated in the Figure 1, where te = a° c. The functor c has a requirement about concurrency which is (t;u) 11 (t';u') = (t il t');(u 11 u'). That is, the computation determined by two independent composed transitions t;u and t';u' is equivalent to the computation whose steps are the independent transitions tllt' and ullu'. The (regular) language accepted by a nonsequential finite automaton is induced by its transitive closure considering the label of each transition that has an initial and final state as source and target, respectively. A reification morphism