Approaches to the verification of multi-agent systems are typically based on games or transition systems defined in terms of states and actions. However such approaches often ignore a key aspect of multi-agent systems, namely that the agents’ actions require (and sometimes produce) resources. I will survey work on the verification of multi-agent systems that takes resources into account.
There is a very well-known relationship between session-based pi-calculi and linear logic, developed in a long and fruitful line of work initiated more than ten years ago by Caires and Pfenning. Perhaps less known, and certainly less developed, is the correspondence introduced a few years earlier by Honda and Laurent, and then Ehrhard and Laurent, in their work relating processes of (a certain variant of) the pi-calculus to (a certain variant of) proof nets. These two ways of bringing together concurrency and linear logic are RADICALly different (sorry I could not resist the pun): the first is session-based, synchronous, usually monadic on the pi-calculus side, and uses sequent calculus and unconstrained linear logic on the logical side. The second is not session-based, asynchronous, usually polyadic, uses polarized linear logic (or, rather, differential linear logic) and is more inspired by proof nets. This talk will focus on the lesser-known correnspondence, introducing the path from Honda and Laurent's original work to more recent results about intersection types in the pi-calculus, and will hopefully motivate discussion about whether any comparison at all is possible with the session-based approach.