Labelled Event Structure Semantics of Linear Logic Planning

Labelled event structures is a model of concurrency, where causality between actions is expressed by a partial order and the nondeterminism is expressed by a conflict relation on actions. We present a new approach to linear logic planning where computation is performed as cutfree proof search. We provide a labelled event structure semantics for the planning problems, and establish an explicit correspondence between the cut-free proofs of the planning problems and partial order plans that we extract from proofs. This results in a concurrency theoretic semantics of planning problems. As the underlying formalism, we employ the recently developed calculus of structures. This way, additional proof theoretical properties, that are not available in the sequent calculus presentation of linear logic, become available. We provide an implementation of our approach, and argue that this work is a crucial step for using the methods of concurrency for establishing a meaningful notion of plan equivalence