Diagonal compositionality of concurrent, finite state systems

Abstract

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 <p: N1 ~ tcN2 maps transitions into transactions reflecting an implementation of an automaton on top of another, where the target object (more concrete) is enriched with its transitive closure. In fact, since a reification should to not preserve labeling, the mapping is restricted to the "shape" of component automata (and therefore, it is not an automaton morphism). However, we show that each reification induces a nonsequential finite automaton morphism and therefore, we may define a category whose morphisms are nonsequential finite automaton morphisms induced by reifications. In any case, the composition of morphisms is as in Kleisli categories (the right categoria! setting to describe the composition of morphisms where the target object is enriched through an endofunctor). Both categories are isomorphic. Therefore, reifications compose, i.e. , the vertical compositionality requirement is achieved. Synchronization and hiding are functorial operations defined using fibration and cofibration techniques based on [9], [12] and inspired by [24] . Both functors are induced by morphisms at the label level. Also, we show a categoria! way to construct tables of synchronizations for calling and sharing and the corresponding synchronization morphism. The table of synchronizations is given by a colimit whose resulting diagram has a shape illustrated in the Figure 3 where the central arrow has as source an object named channel and as target the table of synchronizations. The synchronization of reified automata is the synchronization of the source automata whose reification is induced by component reifications (in this construction, the horizontal compositionality is an essential property). An important result is that the horizontal compositionality requirement is extended for synchronization. A view of an automaton is obtained through hiding of transitions introducing an internai nondeterminism as e-moves in the sense of [5] . A hidden transition cannot be used for synchronization. The hiding of a reification is induced by the hiding of the source automaton. The clarification of the relationship between nonsequential finite automata and (sequential) finite automata is done through translation functors, inspired by [17]. From the steps of abstractions that are involved, we can infer (as expected) that nonsequential finite automata are more concrete than finite automata (in the sense of [17]). At this moment we are extending the framework for nonsequential finite automata with output, developing tools and working on some specific problems related to language recognition. Also, following the same approach, we are starting some works toward nonsequential pushdown automata.