Hilbert Composition of Multilabelled Events

Any language for modelling concurrent and distributed systems features some sorts of composition and synchronization. This is usually beneficial in the design and verification of complex models. The focus of the paper is on events, like events in Discrete Events Dynamic Systems, or transitions in Petri nets, in which events are labelled with multisets of (conjugated) symbols. We propose a novel synchronization approach that is based on a well-grounded mathematical theory. Using a simple and intuitive pairwise composition with regular labels, we show that the synchronization generates a set of events that is equivalent to a set of Hilbert bases of polyhedral convex cones. Such connection with the theory of Hilbert bases allows us to prove several useful properties of the composition, as well as an effective algorithm to compute such synchronizations. Finally a calculus of events, named Hilbert Calculus of Events, is formulated, for which basic properties are proved.