On linear logic planning and concurrency

We present an approach to linear logic planning where an explicit correspondence between partial order plans and multiplicative exponential linear logic proofs is established. This is performed by extracting partial order plans from sound and complete encodings of planning problems in multiplicative exponential linear logic. These partial order plans exhibit a non-interleaving behavioural concurrency semantics, i. e. , labelled event structures. Relying on this fact, we argue that this work is a crucial step for establishing a common language for concurrency and planning that will allow to carry techniques and methods between these two fields.

Authors

• Ozan Kahramanoğulları

Keywords

• Linear logic
• Planning
• Concurrency
• Petri nets
• Proof search