Pomset Logic was defined in Retoré's PhD thesis (1993) through the study of coherent spaces, a categorical interpretation of Linear Logic. It is characterized by the presence of a non-commutative sulf-dual binary connective, which can be used to internalize a notion of order, and the study of its proof theory has led to the introduction of completely novel approaches and techniques in the field.
The aim of this talk is to provide an overview of the results on Pomset logic and its "offspring" (the logic BV and its extensions), as well as their connections with the theory of pomsets, concurrent Kleene algebras, and applications to process calculi.

In Time Petri nets (TPNs), time and control are tightly connected: time measurement for a transition starts only when all resources needed to fire it are available. For many systems, one wants to start measuring time as soon as a part of the preset of a transition is filled, and fire it after some delay and when all needed resources are available.
This work considers an extension of TPN called waiting nets decoupling time measurement and control. Their semantics ignores urgency when upper bounds of intervals are reached but some resources needed to fire are not yet available. Firing of a transition is then allowed as soon as missing resources become available. This semantics extension resembles stopwatches, but is in fact weaker.
It is known that extending bounded TPNs with stopwatches leads to undecidability. Our extension is weaker, and bounded Waiting nets are not Turing powerful. Interestingly, state classes, a standard technique to build a finite abstract representation of the sate space and analyze bounded time Petri nets extends to waiting nets. We show how to compute a finite state class graph for bounded waiting nets, yielding decidability of reachability and coverability. We then compare expressiveness of waiting nets with that of other models and show that they are strictly more expressive than TPNs.

We propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal and al. via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueings of paths. We show that transition systems and presheaf models are instances of our framework. We also prove that in our framework, several notions of bisimulation coincide, in particular an “operational one” akin to the standard definition in transition systems. Also, our notion of accessibility is preserved by coreflections. This also leads us to a notion of unfolding that behaves well in the accessible case: it is a right adjoint and is a universal covering, i.e., it is initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, is an unfolding, when the category of path shapes is well chosen. Joint work with Éric and Jean Goubault.

Message sequence charts (MSCs) are partial orders representing executions of message-passing systems. They arise as executions of communicating automata, in which a fixed number of finite-state processes communicate through FIFO channels: Where a standard finite automaton defines a language of words, communicating automata define languages of MSCs. In this talk, I will give an overview of different formalisms that can be used to specify sets of MSCs, and explain how fundamental results from formal language theory such as the Büchi-Elgot-Trakhtenbrot theorem can be extended to MSCs.

Kleene Algebra (KA) is the algebra of regular expressions. Central to the study of KA is Kozen's (1994) completeness result, which says that any equivalence valid in the language model of KA follows from the axioms of KA. Also of interest is the finite model property (FMP), which says that false equivalences always have a finite counterexample. Palka (2005) showed that, for KA, the FMP is equivalent to completeness.
We provide a unified and elementary proof of both properties. In contrast with earlier completeness proofs, this proof does not rely on minimality or bisimilarity techniques for deterministic automata. Instead, our approach avoids deterministic automata altogether, and uses Antimirov's derivatives and the well-known transition monoid construction.
Towards the end, we will offer some thoughts on whether or not these techniques can be generalized to attack the open completeness problem for downward-closed series-parallel rational expressions.

In order to model concurrency, Lodaya and Weil extended automata theory from the usual word languages to sets of labelled series-parallel posets (pomset) languages. These languages are subsets of SP($A$): the smallest class containing the empty pomset, the letters of $A$ and being closed under sequential product (concatenation) and parallel product, or equivalently, the class of posets labelled by the alphabet $A$, having finite antichains and not containing four distinct elements $x$, $y$, $z$, $t$ whose relative order form an N: $x < y$, $z < y$ and $z < t$.
In this talk we focus on a Kleene-like theorem and a Büchi-Elgot-Trakhtenbrot-like theorem on languages of SP($A$). Lodaya and Weil introduced a notion of branching automata. It is a generalization of Kleene automata with two new types of transitions: fork and join transitions, in addition to the usual sequential transitions of Kleene automata. The fork transitions allow to execute concurrently a finite number of instruction flows and the join transitions merge them. These automata accept subsets of SP($A$) of unbounded width. Lodaya and Weil introduced a generalization of the usual rational expressions to catch the expressivity of branching automata. These two equivalent models can be restricted to both accept, in an equivalent way, subsets of SP($A$) of bounded width.
From a logical point of view, Kuske showed that a rational language of SP($A$) is of bounded width if and only if it is definable in monadic second order (MSO) logic. However, MSO alone does not suffice for rational languages of unbounded width. The finite parallel iteration is not MSO-definable. Bedon introduced P-MSO, which is monadic second order mixed with Presburger arithmetic. He shows that the languages of branching automata are exactly those definable in P-MSO logic. As a consequence, the P-MSO theory of SP($A$) is decidable.

Tasks and objects are two predominant ways of specifying distributed problems where processes should compute outputs based on their inputs. Roughly speaking, a task specifies, for each set of processes and each possible assignment of input values, they're valid outputs. In contrast, an object is defined by a sequential specification. Also, an object can be invoked multiple times by each process, while a task is a one-shot problem. Each one requires its own implementation notion, stating when an execution satisfies the specification. For objects, linearizability is commonly used, while tasks implementation notions are less explored.
The talk overviews results presented in JACM 2018 together with Castañeda and Raynal, about the notion of interval-sequential object, and the corresponding implementation notion of interval-linearizability, to encompass many problems that have no sequential specification as objects. A main result of the article is that interval-sequential objects and (refined) tasks have the same expressive power and both are complete in the sense that they are able to specify any prefix-closed set of well-formed executions.

The categorical approach of Nielsen & Winskel came up with a unifying understanding of models of concurrency. Previous applications of this method to higher dimensional automata (HDA) have not treated the logic that it yields in much detail. In this work, we follow the same approach to introduce a new notion of Bisimulation from open maps and its characteristic path logic. Further, we investigate fragments of the logic and the bisimulations that they capture. To this end, we rely on the recent categorical definition of HDA and the notion of track objects. The motivation for this study is to develop modal characterization for all concurrency bisimulations.

Website design based on Blue Haze by haran from OSWD.