Process algebras provide convenient languages for representing concurrent computation, and they have been used successfully to model complex systems such as security protocols. However, their naive interleaving semantics gives rise to exponentially many states that are essentially the same. This is problematic, for instance, when model-checking security protocols. We solve this problem on a large fragment of the applied pi-calculus by providing reduced transition systems that optimally eliminate redundant traces, and which are still adequate for on-the-fly model-checking of reachability and (in the action-deterministic case) trace equivalence properties.

Technically, we rely on basic trace theory but also on focusing from proof theory.

(Joint work with Baelde & Delaune.)