An approach to innocent strategies as graphs

This paper proposes an approach for extending to graphs the close relation between proofs and innocent strategies. We work in the setting of L-nets, introduced by Faggian and Maurel as a game model of concurrent interaction. We show how L-nets satisfying an additional condition, which we call LS-nets, can be sequentialized into traditional tree-like strategies. Conversely, sequential strategies can be relaxed into more asynchronous ones.We develop an algebra of constructors and destructors that serve to build and decompose graph strategies, and to describe a class of minimally sequential graph strategies, which can be seen as an abstract kind of multiplicative–additive proof nets.