CoNeCo: Concurrency, Networks and Coinduction

NetKAT is a programming language that can be used to program network behaviour from a global point of view. Crucially, NetKAT allows the user to reason about the policy they wrote using straightforward algebraic laws, which accurately describe its semantics. As a matter of fact, this process can be automated quite efficiently using coinductive techniques.

However, NetKAT cannot express concurrency, that is, it cannot specify that a packet should be processed by multiple tables simultaneously, or perhaps even by multiple devices. The CoNeCo project aims to extend the mathematical foundation of NetKAT, known as Kleene algebra, with primitives for reasoning about concurrency. On this foundation, we hope to build a concurrent version of NetKAT, which enjoys the same benefits as NetKAT proper, including an accurate algebraic description, compilation to network configuration and an efficient (coinductive) decision procedure.

Soft Component Automata

Our world is driven more and more by programs that automate real-world tasks. As these programs make real-life decisions that have physical consequences for human beings, one looks to formal verification to be able to trust them.

In this project, we proposed an automata-based formalism for modeling an autonomous system, called Soft Component Automata (SCAs). These automata have two primary features. First, all transitions are endowed with a value that indicates the preference of the component to perform the action; if the highest-preference transition is unavailable, the component can fall back on transitions of lower preference. Second, SCAs can be composed using a number of operators; the semantics of their composed actions are brokered by a group-like structure superimposed on the action labels.

We then introduced an LTL-like logic for verification of SCAs, which was compatible with the compositional nature of the actions. In particular, this logic could answer queries about behaviour composable with a particular component, or about behaviour that subsumed that component's behaviour. A translation of this logic to Büchi automata ensures that the logic is also decidable. Later work looked at integrating SCAs with Reo, a language suitable for specifying and verifying inter-component interaction.