Static Analysis of Deterministic Negotiations

• Published in: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Main Authors: Esparza, Javier, Muscholl, Anca, Walukiewicz, Igor
• Other Authors: Institut für Informatik (LRR-TUM), Technische Universität München München (TUM), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2017
• Subjects: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; Iceland
• Online Access: https://hal.archives-ouvertes.fr/hal-02397738; https://hal.archives-ouvertes.fr/hal-02397738/document; https://hal.archives-ouvertes.fr/hal-02397738/file/igw-lics17.pdf; https://doi.org/10.1109/LICS.2017.8005144

International audience 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. In this paper we generalize and explain these results. We extend the classical "meet-overall -paths" (MOP) formulation of static analysis problems to our concurrent setting, and introduce Mazurkiewicz-invariant analysis problems, which encompass the questions above and new ones. We show that any Mazurkiewicz-invariant analysis problem can be solved in PTIME for sound deterministic negotiations whenever it is in PTIME for sequential flow-graphs-even though the flow-graph of a deterministic negotiation diagram can be exponentially larger than the diagram itself. This gives a common explanation to the low-complexity of all the analysis questions studied so far. Finally, we show that classical gen/kill analyses are also an instance of our framework, and obtain a PTIME algorithm for detecting anti-patterns in free-choice workflow Petri nets. Our result is based on a novel decomposition theorem, of independent interest, showing that sound deterministic negotiation diagrams can be hierarchically decomposed into (possibly overlapping) smaller sound diagrams.