TY - GEN
T1 - Static analysis of deterministic negotiations
AU - Esparza, Javier
AU - Muscholl, Anca
AU - Walukiewicz, Igor
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/8/8
Y1 - 2017/8/8
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85034063161&partnerID=8YFLogxK
U2 - 10.1109/LICS.2017.8005144
DO - 10.1109/LICS.2017.8005144
M3 - Conference contribution
AN - SCOPUS:85034063161
T3 - Proceedings - Symposium on Logic in Computer Science
BT - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
Y2 - 20 June 2017 through 23 June 2017
ER -