Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, December 11, 2006 - 4:30pm

Iliano Cervesato

Carnegie Mellon University - Qatar

Location

University of Pennsylvania

DRL 4C8

We present a revisited semantics for multiset rewriting founded on the left sequent rules of linear logic in its DILL presentation. The resulting interpretation is extended with a majority of linear connectives into the language of omega-multisets. It drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication and more. The cut rules introduce finite auxiliary rewriting chains and are admissible. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. A simple translation maps process constructors of the asynchronous pi-calculus to rewrite operators, while the structural equivalence correspond directly to logically-motivated structural properties of omega-multisets (with one exception). The language of omega-multisets forms the basis for the security protocol specification language MSR 3. With relations to both multiset rewriting and process algebra, it supports specifications that are process-based, state-based, or of a mixed nature. Additionally, its logical underpinning makes it an ideal common ground for systematic comparisons among protocol specification languages, a task currently done in an ad-hoc manner.