The Mays and Musts of Concurrent Strategies
Simon Castellan (CELTIQUE, IRISA), Pierre Clairambault (LIP, PLUME),, Glynn Winskel

TL;DR
This paper extends the theory of concurrent strategies based on event structures to better capture 'may' and 'must' testing behaviors, addressing limitations in their composition and providing new characterizations of behavioral equivalences.
Contribution
It introduces extensions to the bicategory of strategies to incorporate 'may' and 'must' testing, enabling better analysis of deadlocks and divergences in concurrent systems.
Findings
Extended strategies with neutral moves lose identities in composition.
Strategies with stopping configurations form a bicategory.
Characterizations of 'may' and 'must' equivalences and preorders are provided.
Abstract
Concurrent strategies based on event structures are examined from the viewpoint of 'may' and 'must' testing in traditional process calculi. In their pure form concurrent strategies fail to expose the deadlocks and divergences that can arise in their composition. This motivates an extension of the bicategory of concurrent strategies to treat the 'may' and 'must' behaviour of strategies under testing. One extension adjoins neutral moves to strategies but in so doing loses identities w.r.t. composition. This in turn motivates another extension in which concurrent strategies are accompanied by stopping configurations; the ensuing stopping strategies inherit the structure of a bicategory from that of strategies. The technical developments converge in providing characterisations of the 'may' and 'must' equivalences and preorders on strategies.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
