2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017)

Reykjavik, Iceland

June 20, 2017 to June 23, 2017

ISBN: 978-1-5090-3019-4

pp: 1-12

Javier Esparza , Technical University of Munich, Germany

Anca Muscholl , University of Bordeaux, LaBRI, France

Igor Walukiewicz , CNRS, LaBRI, University of Bordeaux, France

ABSTRACT

Negotiation diagrams are a model of concurrent computation akin to workflow Petri nets. Deterministic negotiation diagrams, equivalent to the much studied and used free-choice workflow Petri nets, are surprisingly amenable to verification. Soundness (a property close to deadlock-freedom) can be decided in PTIME. Further, other fundamental questions like computing summaries or the expected cost, can also be solved in PTIME for sound deterministic negotiation diagrams, while they are PSPACE-complete in the general case.

INDEX TERMS

Petri nets, Synchronization, Algorithm design and analysis, Computational modeling, Analytical models, Concurrent computing, Unified modeling language

CITATION

J. Esparza, A. Muscholl and I. Walukiewicz, "Static analysis of deterministic negotiations,"

*2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, Reykjavik, Iceland, 2017, pp. 1-12.

doi:10.1109/LICS.2017.8005144

CITATIONS