Math. Struct in Comp. Science 9 1999 687-718

Given an automaton, its behaviour can be modelled as the sets of strings over an alphabet A that can be accepted from any of its states. When considering concurrent systems, we can see a concurrent agent as an automaton, where nondeterminism derives from the fact that its states can offer a different behaviour at different moments in time. Nondeterministic computations between a pair of states cannot anymore be described as a ``set'' of strings in a free monoid. Consequently, between two states we will have a labelled structured set of computations, where the structure describes the possibility for two computations of parting from each other while maintaining the same observable steps. In this paper, we shall consider different kinds of observation domains and related structured sets of computations. Structured sets of computations will be organised as a category of generalised trees built over a meet-semilattice monoid formalizing the observation domain. Theorems allowing us to introduce the usual concurrency operators in the models and relating different models will then be obtained by first considering ordinary functors (on and between the observation domains) and then lifting them to the categories of structured sets of computations.

J. of Comp. Sys. Science 59 1999 412-449

An alternative (tree-based) semantics for a class of regular expressions is proposed that assigns a central role to the + operator and thus to nondeterminism and nondeterministic choice. For the new semantics a consistent and complete axiomatization is obtained from the original axiomatization of regular expressions by Salomaa and by Kozen by dropping the idempotence law for + and the distribution law of multiplication over sum.

Theor. Informatics and Appl. 33 1999 447-465

A finite axiomatization of nondeterministic regular expressions is provided under a weak restriction on the form of terms analogous to the non empty word property by Salomaa.

Submitted 2000

We provide a finite equational axiomatization for bisimulation equivalence over regular expressions. Our axiomatization is heavily based on the one by Salomaa, that provided an implicative axiomatization for a large subset of regular expressions, namely all those that satisfy the non-empty word property (i.e. without 1 summands at the top level) in *-contexts. Our restriction is similar, it essentially amounts to requiring that the non-empty word property be satisfied not just at top level but at any depth.

Submitted 2000

Models for parallel and concurrent processes lead quite naturally to the study of monoidal categories. In particular a category Tree of trees equipped with a non symmetric tensor product, interpreted as concatenation, seems to be of particular interest in representing (local) behavior of non deterministic agents able to communicate. The category Tree is also provided with a coproduct (corresponding to choice between behaviors) and the tensor product is only partially distributive w.r.t. it, in order to preserve non determinism. Such a category can be properly defined as the category of the (finite) symmetric categories on a free monoid thought of as a 2-category. The monoidal structure is inherited from the concatenation in the monoid. In this paper we prove that for every alphabet A, Tree(A), the category of finite A-labeled trees, is equivalent to the free category generated by A and enjoying the above mentioned properties.

Applied Categorical Structures 9 } 2001 173--216

The axioms of iteration 2-theories capture, up to isomorphism, the equational properties of iteration in conjunction with horizontal and vertical composition in all algebraically complete categories. We give a concrete representation of the free iteration 2-theory generated by a 2-signature.

J. of Pure and Applied Algebra to appear 2001

We introduce morphisms of bicategories, more general than the original ones. When its domain is 1, such a morphism is a category enriched on the codomain. Therefore these morphisms can be regarded as categories enriched in bicategories "on two sides". There is a composition of such enriched categories, leading to a simple kind of tricategory Caten whose objects are bicategories. Left adjoints in Caten are homomorphisms in the sense of Benabou, while right adjoints are not. The 2-cells of Caten are functors; modules can also be defined, and we examine the structures associated to them.

J. of JLC to appear 2001

We provide a finite equational axiomatization for bisimulation equivalence of nondeterministic interpretation of regular expressions. Our axiomatization is heavily based on the one by Salomaa, that provided an implicative axiomatization for a large subset of regular expressions, namely all those that satisfy the non-empty word property (i.e.,without 1 summands at the top level in *-contexts. Our restriction is similar, it essentially amounts to recursively requiring that the non empty word property be satisfied not just at top level but at any depth. We also discuss the impact on the axiomatization of different in terpretation of the 0 term, interpreted either as a null process or as a deadlock.

submitted

We define the class of the linear systems whose solution is expressible as a tuple of non-deterministic regular expressions when they are interpreted as trees of actions rather than as sequences. We precisely characterize the systems that have a regular expression as "canonical" solution, and show that any regular expression can be obtained as a canonical solution of a system of the defined class.