Linear process algebra

Abstract

A linear process is a system of events and states related by an inner product, on which are defined the behaviorally motivated operations of tensor product or orthocurrence, sum or concurrence, sequence, and choice. Linear process algebra or LPA is the theory of this framework. LPA resembles Girard's linear logic with the differences attributable to its focus on behavior instead of proof. As with MLL the multiplicative part can be construed via the Curry-Howard isomorphism as an enrichment of Boolean algebra. The additives cater for independent concurrency or parallel play. The traditional sequential operations of sequence and choice exploit process-specific state information catering for notions of transition and cancellation. © 2011 Springer-Verlag.