Open AccessCompleteness Results for Linear Logic on Petri Nets
Author(s) -
Uffe Engberg,
Glynn Winskel
Publication year - 1993
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v22i435.6752
Subject(s) - assertion , petri net , completeness (order theory) , impossibility , substructural logic , discrete mathematics , linear logic , higher order logic , mathematics , class (philosophy) , computer science , theoretical computer science , algorithm , programming language , description logic , artificial intelligence , mathematical analysis , political science , law
Completeness is shown for several versions of Girard's linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with $\otimes$, $-\!\circ$, \&, $\oplus$ and the exponential ! (''of course´´), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed.