2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017)
June 20, 2017 to June 23, 2017
Javier Esparza , Technical University of Munich, Germany
Anca Muscholl , University of Bordeaux, LaBRI, France
Igor Walukiewicz , CNRS, LaBRI, University of Bordeaux, France
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.
Petri nets, Synchronization, Algorithm design and analysis, Computational modeling, Analytical models, Concurrent computing, Unified modeling language
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.