The Community for Technology Leaders
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
84 ms
(Ver 3.3 (11022016))