Laboratoire d'informatique de l'École polytechnique

Talk by Georg Struth: «Generalised Kripke Semantics for Concurrent Quantales»

Speaker: Georg Struth
Location: Room Grace Hopper
Date: Mon, 14 Jan 2019, 15:00-16:00

For the next seminar of the Cosynus team, we will have the pleasure of welcoming Georg Struth.

Abstract: I present ongoing work on a new technique for constructing models of concurrent quantales (and concurrent Kleene algebras). It is inspired by modal correspondence theory for substructural logics and the duality between boolean algebras with operators and relational structures. In our case, frame conditions are given by ternary relations. The operations of concurrent quantales arise as binary modalities---in fact as convolution operations---over quantale-valued functions, parametrised by the ternary frames. The main result so far is a correspondence between concurrent quantales and frame conditions. A first example constructs concurrent quantales and Kleene algebras of weighted shuffle languages from word-level concatenations and shuffles. The second one obtains concurrent quantales of graphs (or graph types) by lifting from the operations of complete join and disjoint union on graphs. Concurrent quantales of pomset languages arise as special cases. Similar constructions in separation logic or interval temporal logics illustrate the universality of the approach, if time permits. Joint work with James Cranch, Simon Doherty, Brijesh Dongol and Ian Hayes