Document Open Access Logo

Soundness in Negotiations

Authors Javier Esparza, Denis Kuperberg, Anca Muscholl, Igor Walukiewicz

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.12.pdf
  • Filesize: 0.51 MB
  • 13 pages

Document Identifiers

Author Details

Javier Esparza
Denis Kuperberg
Anca Muscholl
Igor Walukiewicz

Cite As Get BibTex

Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz. Soundness in Negotiations. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 12:1-12:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.12

Abstract

Negotiations are a formalism for describing multiparty distributed  cooperation. Alternatively, they can be seen as a model of   concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In a former paper, Esparza and Desel have shown that deciding soundness of a negotiation is PSPACE-complete, and in PTIME if the negotiation is deterministic. They have also provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open.
In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. 
In the second part we solve the open question of Esparza and Desel's paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.

Subject Classification

Keywords
  • Negotiations
  • workflows
  • soundness
  • verification
  • concurrency

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jörg Desel and Javier Esparza. Negotiations and Petri nets. In Int. Workshop on Petri Nets and Software Engineering (PNSE'15), volume 1372 of CEUR Workshop Proceedings, pages 41-57. CEUR-WS.org, 2015. Google Scholar
  2. Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995. Google Scholar
  3. Javier Esparza and Jörg Desel. On negotiation as concurrency primitive. In CONCUR, pages 440-454, 2013. Extended version in CoRR abs/1307.2145. Google Scholar
  4. Javier Esparza and Jörg Desel. On negotiation as concurrency primitive II: Deterministic cyclic negotiations. In FoSSaCS, pages 258-273, 2014. Extended version in CoRR abs/1403.4958. Google Scholar
  5. Javier Esparza and Jörg Desel. Negotiation programs. In Application and Theory of Petri Nets and Concurrency, volume 9115 of LNCS, pages 157-178. Springer, 2015. Google Scholar
  6. Javier Esparza and Philipp Hoffmann. Reduction rules for colored workflow nets. In FASE, volume 9633 of LNCS, pages 342-358. Springer, 2016. Google Scholar
  7. Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, and Karsten Wolf. Instantaneous soundness checking of industrial business process models. In Business Process Management, pages 278-293. Springer, 2009. Google Scholar
  8. Cédric Favre, Hagen Völzer, and Peter Müller. Diagnostic information for control-flow analysis of workflow graphs (a.k.a. free-choice workflow nets). In TACAS 2016, volume 9636 of LNCS, pages 463-479. Springer, 2016. Google Scholar
  9. Blaise Genest, Dietrich Kuske, and Anca Muscholl. A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf.&Comput., 204(6):920-956, 2006. Google Scholar
  10. Anca Muscholl. Automated synthesis of distributed controllers. In ICALP 2015, volume 9135 of LNCS, pages 11-27. Springer, 2015. Google Scholar
  11. Natalia Sidorova, Christian Stahl, and Nikola Trcka. Soundness verification for conceptual workflow nets with data: Early detection of errors with the most precision possible. Inf. Syst., 36(7):1026-1043, 2011. Google Scholar
  12. Wolfgang Thomas. Church’s problem and a tour through automata theory. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of LNCS, pages 635-655. Springer, 2008. Google Scholar
  13. Nikola Trcka, Wil M. P. van der Aalst, and Natalia Sidorova. Data-flow anti-patterns: Discovering data-flow errors in workflows. In Advanced Information Systems Engineering (CAiSE), volume 5565 of LNCS, pages 425-439. Springer, 2009. Google Scholar
  14. Wil M. P. van der Aalst. Business process management as the "Killer App" for Petri nets. Software &Systems Modeling, 14(2):685-691, 2015. Google Scholar
  15. Wil M.P. van der Aalst. The application of Petri nets to workflow management. J. Circuits, Syst. and Comput., 08(01):21-66, 1998. Google Scholar
  16. B. van Dongen, M. Jansen-Vullers, H.M.W. Verbeek, and Wil M. P. van der Aalst. Verification of the SAP reference models using EPC reduction, state-space analysis, and invariants. Computers in Industry, 58(6):578-601, 2007. Google Scholar
  17. W. Zielonka. Notes on finite asynchronous automata. RAIRO-Theoretical Informatics and Applications, 21:99-135, 1987. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact