A partially ordered set, or poset for short, is a set (of events) together with a partial order on it. A poset of events can be used to model both sequential and parallel behaviour. For instance, we can represent two events that can execute in parallel by a two-element poset with no order between the two events and their sequential execution by a two-element poset with the two events ordered. The series-parallel posets are restricted class of posets that are generated from single event posets by a finite number of sequential and parallel compositions. The isomorphic class of Sigma-labelled series-parallel posets over a finite alphabet Sigma have been extensively studied as an algebraic model of concurrency.
We investigate posets with interfaces, or iposets for short, as a concurrency model, and explore their language theoretic properties. In this model, an interface is defined as the image of a monomorphism on the minimal and maximal events of the poset. Compared to series-parallel posets, iposets admit richer algebraic properties. Further, we define axioms of domain operations for iposet languages, which lead to a simple and natural algebraic approach to modal logic based on equational reasoning. Such algebraic approaches to modal operators are known to be suitable for automated reasoning, for example, using tools like Isabelle.
| supervisors | Christian Johansen, Martin Steffen, Uli Fahrenberg |
| IFI links | abstract, thesis, presentation |