Programme

• Marco Peressotti, 13:30 – 14:15

• Daniela Petrișan, 14:30 – 15:15

• Jurriaan Rot, 15:30 – 16:15

Behavioural equivalences for coalgebras with unobservable moves

Marco Peressotti ¹

We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on parameterised saturation categories, i.e., categories whose hom-sets are endowed with complete orders and a suitable iteration operators. This structure allows us to provide the abstract definitions of various (weak) behavioural equivalences. We show that the Kleisli categories of many common monads are categories of this kind. On one hand, this allows us to instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences. On the other hand, we can readily provide new weak behavioural equivalences for more complex behaviours, like those definable on presheaves, topological spaces, measurable spaces, etc.

This is joint work with Tomasz Brengos and Marino Miculan.

Up-to techniques for bisimulations with silent moves

Daniela Petrișan ²

Bisimulation is used in concurrency theory as a proof method for establishing behavioural equivalence of processes. Up-to techniques can be seen as a means of optimizing proofs by coinduction. For example, to establish that two processes are equivalent one can exhibit a smaller relation, which is not a bisimulation, but rather a bisimulation up to a certain technique, say ‘up-to contextual closure’. However, the up-to technique at issue has to be sound, in the sense that any bisimulation up-to should be included in a bisimulation.

In this talk, I will present a general coalgebraic framework for proving the soundness of a wide range of up-to techniques for coinductive unary predicates, as well as for bisimulations. The specific up-to techniques are obtained using liftings of functors to appropriate categories of relations or predicates. In the case of bisimulations with silent moves the situation is more complex. Even for simple examples like CCS, the weak transition system gives rise to a lax bialgebra, rather than a bialgebra. In order to prove that up-to context is a sound technique we have to account for this laxness. The flexibility and modularity of our approach, due in part to using a fibrational setting, pays off: I will show how to obtain such results by changing the base category to preorders.

This is joint work with Filippo Bonchi, Damien Pous and Jurriaan Rot.

Coalgebraic trace semantics via forgetful logics

Jurriaan Rot ^{3 4}

I will show how to use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata. If time permits, I will discuss connections to determinization procedures and Brzozowski’s minimization algorithm.

This is joint work with Bartek Klin.