Dependency analysis

Maxime Gamboni

I will present a generic type system characterising two broad classes of pi-calculus properties ("existential" and "universal" properties). The type system uses dependency analysis to compose dependency statements produced by user-provided elementary rules into complex behavioural statements that describe the whole process. Types describe a process as an open system and are able to predict how the process behaviour will evolve when other components are added to it. Types form a Boolean algebra that naturally integrates choice and branching.