{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T05:13:16Z","timestamp":1718341996402},"reference-count":112,"publisher":"Oxford University Press (OUP)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Computer Journal"],"DOI":"10.1093\/comjnl\/bxw099","type":"journal-article","created":{"date-parts":[[2016,11,16]],"date-time":"2016-11-16T20:05:49Z","timestamp":1479326749000},"source":"Crossref","is-referenced-by-count":9,"title":["Communication and Resource Deadlock Analysis Using IMDS Formalism and Model Checking"],"prefix":"10.1093","author":[{"given":"Wiktor B.","family":"Daszczuk","sequence":"first","affiliation":[]}],"member":"286","published-online":{"date-parts":[[2016,12,20]]},"reference":[{"key":"2016122017200672000_bxw099v1.1","unstructured":"Jia, W. and Zhou, W. (2005) Distributed Network Systems. From Concepts to Implementations (Network Theory and Applications), Springer, New York. ISBN: 978-0-387-23839-5."},{"key":"2016122017200672000_bxw099v1.2","first-page":"261","article-title":"Communication dualism in distributed systems with Petri Net Interpretation","volume":"18","author":"Chrobot","year":"2006","journal-title":"Theor. Appl. Inform."},{"key":"2016122017200672000_bxw099v1.3","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/356603.356607","article-title":"Some deadlock properties of computer systems","volume":"3","author":"Holt","year":"1972","journal-title":"ACM Comput. Surv."},{"key":"2016122017200672000_bxw099v1.4","doi-asserted-by":"crossref","unstructured":"Reniers, M.A. and Willemse T.A.C. (2011) Folk Theorems on the Correspondence between State-Based and Event-Based Systems. 37th Conf. Current Trends in Theory and Practice of Computer Science, Novy Smokovec, Slovakia, January 22\u201328, pp. 494\u2013505. Springer, Berlin Heidelberg. DOI 10.1007\/978-3-642-18381-2_41.","DOI":"10.1007\/978-3-642-18381-2_41"},{"key":"2016122017200672000_bxw099v1.5","doi-asserted-by":"publisher","DOI":"10.1145\/214451.214456"},{"key":"2016122017200672000_bxw099v1.6","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1145\/357360.357365","article-title":"Distributed deadlock detection","volume":"1","author":"Chandy","year":"1983","journal-title":"ACM Trans. Comput. Syst."},{"key":"2016122017200672000_bxw099v1.7","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/15833.15837","article-title":"A survey of distributed deadlock detection algorithms","volume":"15","author":"Elmagarmid","year":"1986","journal-title":"ACM SIGMOD Rec."},{"key":"2016122017200672000_bxw099v1.8","doi-asserted-by":"crossref","unstructured":"Mitchell, D.P. and Merritt, M.J. (1984) A Distributed Algorithm for Deadlock Detection and Resolution. Third Annual ACM Symposium on Principles of Distributed Computing\u2014PODC \u201884, Vancouver, Canada, August 27\u201329, pp. 282\u2013284. ACM Press, New York, NY. DOI 10.1145\/800222.806755","DOI":"10.1145\/800222.806755"},{"key":"2016122017200672000_bxw099v1.9","doi-asserted-by":"crossref","unstructured":"Agarwal, R. and Stoller, S.D. (2006) Run-Time Detection of Potential Deadlocks for Programs with Locks, Semaphores, and Condition Variables. Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD-IV), ISSTA, Portland, ME, July 17\u201320, pp. 51\u201359. ACM Press, New York, NY. DOI 10.1145\/1147403.1147413","DOI":"10.1145\/1147403.1147413"},{"key":"2016122017200672000_bxw099v1.10","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1145\/45075.46163","article-title":"Deadlock detection in distributed databases","volume":"19","author":"Knapp","year":"1987","journal-title":"ACM Comput. Surv."},{"key":"2016122017200672000_bxw099v1.11","doi-asserted-by":"crossref","unstructured":"Zhou, J. , Chen, X. , Dai, H. , Cao, J. and Chen, D. (2004 ) M-Guard: A New Distributed Deadlock Detection Algorithm Based on Mobile Agent Technology. 2nd Int. Conf. Parall. Distributed Processing and Applications ISPA'04, Hong Kong, China, December 13\u201315, pp. 75\u201384. Springer, Berlin Heidelberg. DOI 10.1007\/978-3-540-30566-8_13","DOI":"10.1007\/978-3-540-30566-8_13"},{"key":"2016122017200672000_bxw099v1.12","doi-asserted-by":"crossref","unstructured":"Hilbrich, T. , de Supinski, B.R. , Schulz, M. and M\u00fcller, M.S. (2009) A Graph Based Approach for MPI Deadlock Detection. 23rd International Conference on Supercomputing\u2014ICS \u201809, Yorktown Heights, NY, June 8\u201312, pp. 296\u2013305. ACM Press, New York, NY. DOI 10.1145\/1542275.1542319","DOI":"10.1145\/1542275.1542319"},{"key":"2016122017200672000_bxw099v1.13","doi-asserted-by":"crossref","unstructured":"Hilbrich, T. , de Supinski, B.R. , Nagel, W.E. , Protze, J. , Baier, C. and M\u00fcller, M.S. (2013) Distributed Wait State Tracking for Runtime MPI Deadlock Detection. Int. Conf. High Performance Computing, Networking, Storage and Analysis - SC \u201813, Denver, CO, November 17\u201321, pp. 1\u201312. ACM Press, New York, NY. DOI 10.1145\/2503210.2503237","DOI":"10.1145\/2503210.2503237"},{"key":"2016122017200672000_bxw099v1.14","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1109\/TSE.1986.6312900","article-title":"A distributed scheme for detecting communication deadlocks","volume":"SE-12","author":"Natarajan","year":"1986","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2016122017200672000_bxw099v1.15","doi-asserted-by":"crossref","unstructured":"Hosseini, R. and Haghighat, A. (2005) An Improved Algorithm for Deadlock Detection and Resolution in Mobile Agent Systems. Int. Conf. Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce (CIMCA-IAWTIC'06), Vienna, Austria, November 28\u201330, Vol. 2, pp. 1037\u20131042. IEEE, New York, NY. DOI 10.1109\/CIMCA.2005.1631606","DOI":"10.1109\/CIMCA.2005.1631606"},{"key":"2016122017200672000_bxw099v1.16","doi-asserted-by":"crossref","unstructured":"Allen, G.E. , Zucknick, P.E. and Evans, B.L. (2007) A Distributed Deadlock Detection and Resolution Algorithm for Process Networks. 2007 IEEE Int. Conf. Acoustics, Speech and Signal Processing\u2014ICASSP \u201807, April 15\u201320, Honolulu, HI, Vol.2, pp. II-33-II-36. IEEE, New York, NY. DOI 10.1109\/ICASSP.2007.366165","DOI":"10.1109\/ICASSP.2007.366165"},{"key":"2016122017200672000_bxw099v1.17","doi-asserted-by":"crossref","unstructured":"Olson, A. and Evans, B. (2005) Deadlock Detection For Distributed Process Networks. IEEE Int. Conf. Acoustics, Speech, and Signal Processing, ICASSP'05, Philadelphia, PA, March 18\u201323, Vol.V, pp. 73\u201376. IEEE, New York, NY. DOI 10.1109\/ICASSP.2005.1416243","DOI":"10.1109\/ICASSP.2005.1416243"},{"key":"2016122017200672000_bxw099v1.18","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1109\/2.43525","article-title":"Deadlock detection in distributed systems","volume":"22","author":"Singhal","year":"1989","journal-title":"Computer"},{"key":"2016122017200672000_bxw099v1.19","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/32.21721","article-title":"A modified priority based probe algorithm for distributed deadlock detection and resolution","volume":"15","author":"Choudhary","year":"1989","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2016122017200672000_bxw099v1.20","doi-asserted-by":"crossref","unstructured":"Yeung, C.-F. , Huang, S.-L. , Lam, K.-Y. and Law, C.-K. (1994) A New Distributed Deadlock Detection Algorithm for Distributed Database Systems. IEEE Region 10\u2019s 9th Annual Int. Conf.: \u2018Frontiers of Comput. Technol.\u2019, TENCON'94, Singapore, August 22\u201326, Vol. 1, pp. 506\u2013510. IEEE, New York, NY. DOI 10.1109\/TENCON.1994.369249","DOI":"10.1109\/TENCON.1994.369249"},{"key":"2016122017200672000_bxw099v1.21","doi-asserted-by":"crossref","unstructured":"Park, Y. and Scheuermann, P. (1991) A Deadlock Detection and Resolution Algorithm for Sequential Transaction Processing with Multiple Lock Modes. 15th Annual Int. Comput. Software & Applications Conf., Tokyo, Japan, September 11\u201313, pp. 70\u201377. IEEE Computer Society Press, New York, NY. DOI 10.1109\/CMPSAC.1991.170154","DOI":"10.1109\/CMPSAC.1991.170154"},{"key":"2016122017200672000_bxw099v1.22","first-page":"17","article-title":"Analysis of deadlock detection and resolution techniques in distributed database environment","volume":"2","author":"Grover","year":"2013","journal-title":"Int. J. Comput. Eng. Sci."},{"key":"2016122017200672000_bxw099v1.23","unstructured":"Li, T. , Ellis, C.S. , Lebeck, A.R. and Sorin, D.J. (2005) Pulse: A Dynamic Deadlock Detection Mechanism Using Speculative Execution. USENIX Annual Technical Conference, Berkeley, CA, pp. 31\u201344. USENIX, Berkeley, CA. https:\/\/usenix.org\/legacy\/publications\/library\/proceedings\/usenix05\/tech\/general\/full_papers\/li\/li.pdf (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.24","doi-asserted-by":"crossref","unstructured":"Huang, S.-T. (1989) Detecting Termination of Distributed Computations by External Agents. 9th International Conference on Distributed Computing Systems, Newport Beach, CA, June 5\u20139, pp. 79-84. IEEE Comput. Soc. Press, New York, NY. DOI 10.1109\/ICDCS.1989.37933","DOI":"10.1109\/ICDCS.1989.37933"},{"key":"2016122017200672000_bxw099v1.25","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0020-0190(89)90212-3","article-title":"Global quiescence detection based on credit distribution and recovery","volume":"30","author":"Mattern","year":"1989","journal-title":"Inf. Process. Lett."},{"key":"2016122017200672000_bxw099v1.26","unstructured":"Peri, S. and Mittal, N. (2004) On Termination Detection in an Asynchronous Distributed System. 17th ISCA Int. Conf. Parall. Distrib. Comput. Systems (PDCS), San Francisco, CA, September 15\u201317, pp. 209\u2013215. International Society for Computers and Their Applications, Cary, North Carolina http:\/\/www.iith.ac.in\/~sathya_p\/index_files\/PDCS-Transtd.pdf (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.27","unstructured":"Clarke, E. , Grumberg, O. and Peled, D. (1999) Model Checking, MIT Press, Cambridge, MA. ISBN:0-262-03270-8."},{"key":"2016122017200672000_bxw099v1.28","doi-asserted-by":"crossref","unstructured":"Bensalem, S. , Griesmayer, A. , Legay, A. , Nguyen, T.H. and Peled, D. (2011) Efficient Deadlock Detection for Concurrent Systems. 9th ACM\/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, July 11\u201313, Cambridge, UK, pp. 119\u2013129. IEEE, New York, NY. DOI 10.1109\/MEMCOD.2011.5970518","DOI":"10.1109\/MEMCOD.2011.5970518"},{"key":"2016122017200672000_bxw099v1.29","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1646353.1646372","article-title":"Software model checking takes off","volume":"53","author":"Miller","year":"2010","journal-title":"Commun. ACM"},{"key":"2016122017200672000_bxw099v1.30","doi-asserted-by":"crossref","unstructured":"Kaveh, N. (2000) Using Model Checking to Detect Deadlocks in Distributed Object Systems. In Emmerich, W. and Tai, S. (eds.) 2nd International Workshop on Distributed Objects, Davis, CA, November 2\u20133, LNCS vol. 1999 , 116\u2013128. Springer, London, UK. DOI 10.1007\/3-540-45254-0_11.","DOI":"10.1007\/3-540-45254-0_11"},{"key":"2016122017200672000_bxw099v1.31","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J. (1995) Tutorial: Proving Properties of Concurrent Systems with SPIN. 6th International Conference on Concurrency Theory, CONCUR'95, Philadelphia, PA, August 21\u201324, pp. 453\u2013455. Springer, Berlin Heidelberg. DOI 10.1007\/3-540-60218-6_34","DOI":"10.1007\/3-540-60218-6_34"},{"key":"2016122017200672000_bxw099v1.32","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1109\/32.489078","article-title":"Evaluating deadlock detection methods for concurrent software","volume":"22","author":"Corbett","year":"1996","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2016122017200672000_bxw099v1.33","unstructured":"Puhakka, A. and Valmari, A. (2000) Livelocks, Fairness and Protocol Verification. 16th World Conf. on Software: Theory and Practice, Beijing, China, August 21\u201325, IFIP, pp. 471\u2013479. International Federation for Information Processing, Laxenburg, Austria. http:\/\/www.cs.tut.fi\/ohj\/VARG\/publications\/00-3.ps (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.34","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"2016122017200672000_bxw099v1.35","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","article-title":"Model checking JAVA programs using JAVA PathFinder","volume":"2","author":"Havelund","year":"2000","journal-title":"Int. J. Softw. Tool. Technol. Transf. (STTT)"},{"key":"2016122017200672000_bxw099v1.36","unstructured":"Magee, J. and Kramer, J. (1999) Concurrency: Models and Programs - From Finite State Models to Java Programs, John Wiley, Chichester. ISBN 0470093552."},{"key":"2016122017200672000_bxw099v1.37","doi-asserted-by":"crossref","unstructured":"Cho, J. , Yoo, J. and Cha, S. (2006) NuEditor - A Tool Suite for Specification and Verification of NuSCR. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), LNCS 3647, 19\u201328. Springer, Berlin Heidelberg. DOI 10.1007\/11668855_2.","DOI":"10.1007\/11668855_2"},{"key":"2016122017200672000_bxw099v1.38","doi-asserted-by":"crossref","unstructured":"Royer, J. (2001) Formal Specification and Temporal Proof Techniques for Mixed Systems. 15th Int. Parall. Distrib. Processing Symposium. IPDPS 2001, San Francisco, CA, pp. 1542\u20131551. IEEE Comput. Soc., New York, NY. DOI 10.1109\/IPDPS.2001.925139","DOI":"10.1109\/IPDPS.2001.925139"},{"key":"2016122017200672000_bxw099v1.39","unstructured":"Perna, J. and George, C. (2006) Model Checking RAISE Specifications. Technical Report. United Nations University. http:\/\/i.unu.edu\/media\/unu.edu\/publication\/1550\/report331.pdf (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.40","unstructured":"Mazuelo, C.L. (2008) Automatic model checking of UML models. Master's Thesis. Universitat Berlin. http:\/\/www.iam.unibe.ch\/tilpub\/2008\/lar08.pdf (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.41","doi-asserted-by":"crossref","unstructured":"Berard, B. , Bidoit, M. , Finkel, A. , Laroussinie, F. , Petit, A. , Petrucci, L. and Schnoebelen, P. (2001) Systems and Software Verification. In Model-Checking Techniques and Tools, Springer, Berlin Heidelberg. ISBN 978-3-662-04558-9.","DOI":"10.1007\/978-3-662-04558-9"},{"key":"2016122017200672000_bxw099v1.42","doi-asserted-by":"crossref","unstructured":"Kokash, N. and Arbab, F. (2008) Formal Behavioral Modeling and Compliance Analysis for Service-oriented Systems. In de Boer, F. S. (ed.), Formal Methods for Components and Objects - 7th International Symposium, FMCO 2008, Sophia Antipolis, France, October 21\u201323, LNCS 5751, pp. 21\u201341. Springer, Berlin Heidelberg. DOI 10.1007\/978-3-642-04167-9_2.","DOI":"10.1007\/978-3-642-04167-9_2"},{"key":"2016122017200672000_bxw099v1.43","unstructured":"Arcaini, P. , Gargantini, A. and Riccobene, E. AsmetaSMV: A Model Checker for AsmetaL Models\u2014Tutorial. Technical Report TR120. DTI Univ. of Milan. https:\/\/air.unimi.it\/retrieve\/handle\/2434\/69105\/96882\/Tutorial_AsmetaSMV.pdf (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.44","doi-asserted-by":"crossref","unstructured":"Corbett, J.C. (1994) An Empirical Evaluation of Three Methods for Deadlock Analysis of Ada Tasking Programs. International Symposium on Software Testing and Analysis, ISSTA'94, Seattle, WA, August 17\u201319, pp. 204\u2013215. ACM Press, New York, NY. DOI 10.1145\/186258.187206","DOI":"10.1145\/186258.187206"},{"key":"2016122017200672000_bxw099v1.45","unstructured":"Milner, R. (1984) A Calculus of Communicating Systems, Springer, Berlin Heidelberg. ISBN 0387102353."},{"key":"2016122017200672000_bxw099v1.46","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/S0167-6423(97)00017-8","article-title":"State space reduction by non-standard semantics for deadlock analysis","volume":"30","author":"De Francesco","year":"1998","journal-title":"Sci. Comput. Progr."},{"key":"2016122017200672000_bxw099v1.47","doi-asserted-by":"crossref","unstructured":"Shi, L. and Liu, Y. (2010) Modeling and Verification of Transmission Protocols: A Case Study on CSMA\/CD Protocol. SSIRI-C 2010 - 4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion, Singapore, June 9\u201311, pp. 143\u2013149. IEEE Computer Society, Washington, DC. DOI 10.1109\/SSIRI-C.2010.33","DOI":"10.1109\/SSIRI-C.2010.33"},{"key":"2016122017200672000_bxw099v1.48","doi-asserted-by":"crossref","unstructured":"Hiraishi, H. (2000) Verification of Deadlock Free Property of High Level Robot Control. Ninth Asian Test Symposium ATS 2000, Taipei, December 4\u20136, pp. 198\u2013203. IEEE Computer Society, New York, NY. DOI 10.1109\/ATS.2000.893625","DOI":"10.1109\/ATS.2000.893625"},{"key":"2016122017200672000_bxw099v1.49","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","article-title":"Formal verification in hardware design: a survey","volume":"4","author":"Kern","year":"1999","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"2016122017200672000_bxw099v1.50","doi-asserted-by":"crossref","unstructured":"Havelund, K. and Skakkebaek, J.U. (1999) Applying Model Checking in Java Verification 5th and 6th Int. SPIN Workshops, Trento, Italy, July 5, Toulouse, France, September 21 and 24, pp. 216\u2013231. Springer, London, UK. DOI 10.1007\/3-540-48234-2_17","DOI":"10.1007\/3-540-48234-2_17"},{"key":"2016122017200672000_bxw099v1.51","doi-asserted-by":"crossref","unstructured":"Chang, F.S.-H. and Jackson, D. (2006) Symbolic Model Checking of Declarative Relational Models. 28th Int. Conf. Softw. Engg - ICSE \u201806, Shanghai, China, May 20\u201328, pp. 312\u2013320. ACM Press, New York, NY. DOI 10.1145\/1134285.1134329","DOI":"10.1145\/1134285.1134329"},{"key":"2016122017200672000_bxw099v1.52","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/j.entcs.2008.11.014","article-title":"A case study in parallel verification of component-based systems","volume":"220","author":"Benes","year":"2008","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"2016122017200672000_bxw099v1.53","doi-asserted-by":"crossref","unstructured":"Cordeiro, L. (2010) SMT-based Bounded Model Checking for Multi-threaded Software in Embedded Systems. In 32nd ACM\/IEEE Int. Conf. Softw. Engg, ICSE'10, Cape Town, RSA, May 2\u20138, Vol. 2, pp. 373\u2013376. ACM Press, New York, NY. DOI 10.1145\/1810295.1810396","DOI":"10.1145\/1810295.1810396"},{"key":"2016122017200672000_bxw099v1.54","doi-asserted-by":"crossref","unstructured":"Inverso, O. , Nguyen, T.L. , Fischer, B. , La Torre, S. and Parlato, G. (2015) Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs. 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), Lincoln, NE, November 9\u201313, pp. 807\u2013812. IEEE, New York, NY. DOI 10.1109\/ASE.2015.108","DOI":"10.1109\/ASE.2015.108"},{"key":"2016122017200672000_bxw099v1.55","doi-asserted-by":"crossref","first-page":"32","DOI":"10.4204\/EPTCS.181.3","article-title":"Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model","volume":"181","author":"Heussner","year":"2015","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"2016122017200672000_bxw099v1.56","unstructured":"Yang, Y. , Chen, X. and Gopalakrishnan, G. (2008) Inspect: A Runtime Model Checker for Multithreaded C Programs, Report UUCS-08-004, University of Utah, Salt Lake City, UT. http:\/\/www.cs.utah.edu\/docs\/techreports\/2008\/pdf\/UUCS-08-004.pdf (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.57","first-page":"1","article-title":"Synthesis of large dynamic concurrent programs from dynamic specifications","volume":"47","author":"Attie","year":"2015","journal-title":"Form. Method. Syst. Des."},{"key":"2016122017200672000_bxw099v1.58","doi-asserted-by":"crossref","first-page":"2024","DOI":"10.1109\/TAC.2014.2315311","article-title":"Weak invariant simulation and its application to analysis of parameterized networks","volume":"59","author":"Zibaeenejad","year":"2014","journal-title":"IEEE Trans. Autom. Control"},{"key":"2016122017200672000_bxw099v1.59","unstructured":"Baier, C. and Katoen, J.-P. (2008) Principles of Model Checking, MIT Press, Cambridge, MA. ISBN:9780262026499."},{"key":"2016122017200672000_bxw099v1.60","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1016\/j.datak.2011.01.004","article-title":"Analysis on demand: instantaneous soundness checking of industrial business process models","volume":"70","author":"Fahland","year":"2011","journal-title":"Data Knowl. Eng."},{"key":"2016122017200672000_bxw099v1.61","unstructured":"Joosten, S.J.C. , Julien, F.V. and Schmaltz, J. (2014) WickedXmas: Designing and Verifying On-chip Communication Fabrics. 3rd International Workshop on Design and Implementation of Formal Tools and Systems, DIFTS'14, Lausanne, Switzerland, October 20, pp. 1\u20138. Technische Universiteit Eindhoven, The Netherlands https:\/\/pure.tue.nl\/ws\/files\/3916267\/889737443709527.pdf (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.62","unstructured":"Martens, M. (2009) Establishing properties of interaction systems. PhD Thesis, University of Mannheim, Germany. http:\/\/ub-madoc.bib.uni-mannheim.de\/2629\/1\/DrArbeitMyThesis.pdf (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.63","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1145\/201024.201038","article-title":"Application and experimental evaluation of state space reduction methods for deadlock analysis in Ada","volume":"3","author":"Duri","year":"1994","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"2016122017200672000_bxw099v1.64","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Pnueli, A. (1992) The Temporal Logic of Reactive and Concurrent Systems, Springer, New York, NY. ISBN:978-1-4612-6950-2 DOI 10.1007\/978-1-4612-0931-7.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"2016122017200672000_bxw099v1.65","unstructured":"Yoneda, T. and Schlingloff, H. (1992) On Model Checking for Petri Nets and a Linear Time Temporal Logic. IEICE FTS'92 workshop, Kyoto, Japan, June 1992. https:\/\/www2.informatik.hu-berlin.de\/~hs\/Publikationen\/1992_IEICE-FTS_Yoneda-Schlingloff_Model-Checking-for-Petri-Nets-and-Linear-Temporal-Logic-using-Partial-Orders.pdf (accessed July 7, 2016)"},{"key":"2016122017200672000_bxw099v1.66","unstructured":"Liu, S. (2014) Formal Modeling and Analysis Techniques for High Level Petri Nets. PhD Thesis, Florida International University, Miami, FL. http:\/\/digitalcommons.fiu.edu\/cgi\/viewcontent.cgi?article=2592&context=etd (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.67","doi-asserted-by":"crossref","first-page":"426","DOI":"10.4156\/jdcta.vol6.issue21.48","article-title":"A literature review of deadlock prevention policy based on Petri Nets for automated manufacturing systems","volume":"6","author":"Guan","year":"2012","journal-title":"Int. J. Digit. Content Technol. Appl."},{"key":"2016122017200672000_bxw099v1.68","unstructured":"Godefroid, P. and Wolper, P. (1991) Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. 3rd Int. Workshop, CAV \u201891, Aalborg, Denmark, July 1\u20134, LNCS 575, pp. 332\u2013342. Springer, Berlin Heidelberg. DOI 10.1007\/3-540-55179-4_32"},{"key":"2016122017200672000_bxw099v1.69","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/FI-2000-43123413","article-title":"Improving partial order reductions for universal branching time properties","volume":"43","author":"Penczek","year":"2000","journal-title":"Fundam. Inform."},{"key":"2016122017200672000_bxw099v1.70","unstructured":"Gerth, R. , Kuiper, R. , Penczek, W. and Szreter, M. (1999) Partial Order Reductions Preserving Simulations. Concurrency Specification and Programming (CS&P), Warsaw, Poland, September 28\u201330, pp. 153\u2013171. http:\/\/www.ipipan.waw.pl\/~penczek\/WPenczek\/papersPS\/CSP99.ps.gz (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.71","unstructured":"Daszczuk, W.B. (2003) Verification of temporal properties in concurrent systems. PhD thesis, Warsaw University of Technology. DOI 10.13140\/RG.2.1.2779.6565"},{"key":"2016122017200672000_bxw099v1.72","first-page":"6","article-title":"State of the art report: STUBBORN SETS","volume":"46","author":"Valmari","year":"1994","journal-title":"Petri Net Newsl."},{"key":"2016122017200672000_bxw099v1.73","doi-asserted-by":"crossref","unstructured":"Valmari, A. and Hansen, H. (2010) Can Stubborn Sets be Optimal? In 31st Int. Conf., PETRI NETS 2010, Braga, Portugal, June 21\u201325, pp. 43\u201362. DOI 10.1007\/978-3-642-13675-7_5 (accessed May 12, 2016)","DOI":"10.1007\/978-3-642-13675-7_5"},{"key":"2016122017200672000_bxw099v1.74","doi-asserted-by":"publisher","DOI":"10.1109\/70.650158"},{"key":"2016122017200672000_bxw099v1.75","unstructured":"Tricas, F. , Colom, J.M. and Merelo, J.J. (2014) Computing Minimal Siphons in Petri Net Models of Resource Allocation Systems: An Evolutionary Approach. CEUR Workshop Proceedings, Petri Nets and Software Engineering, Tunis, Tunisia, June 23\u201324, pp. 307\u2013322. Univesit\u00e4t Hamburg, Germany http:\/\/ceur-ws.org\/Vol-1160\/paper18.pdf (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.76","first-page":"113","article-title":"Detection of deadlocks and traps in Petri Nets by means of Thelen's Prime Implicant Method","volume":"14","author":"Wegrzyn","year":"2004","journal-title":"Int. J. Ajppl. Math. Comput. Sci."},{"key":"2016122017200672000_bxw099v1.77","doi-asserted-by":"crossref","unstructured":"Tricas, F. , Garcia-Valles, F. , Colom, J.M. and Ezpeleta, J. A Petri Net structure- based deadlock prevention solution for sequential resource allocation systems 2005 IEEE Int. Conf. Robotics Automation, Barcelona, Spain, April 18\u201322, pp. 271\u2013277. DOI 10.1109\/ROBOT.2005.1570131.","DOI":"10.1109\/ROBOT.2005.1570131"},{"key":"2016122017200672000_bxw099v1.78","doi-asserted-by":"crossref","unstructured":"Bertino, E. , Chiola, G. and Mancini, L.V. (1998) Deadlock Detection in the Face of Transaction and Data Dependencies. 19th Int. Conf. ICATPN'98, 22\u201326 June 1998, Lisbon, Portugal, pp. 266\u2013285. Springer, Berlin Heidelberg. DOI 10.1007\/3-540-69108-1_15.","DOI":"10.1007\/3-540-69108-1_15"},{"key":"2016122017200672000_bxw099v1.79","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1145\/858344.858348","article-title":"A deadlock detection and recovery algorithm using the formalism of a directed graph matrix","volume":"23","author":"Leibfried","year":"1989","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"2016122017200672000_bxw099v1.80","doi-asserted-by":"crossref","unstructured":"Ni, Q. , Sun, W. and Ma, S. (2009) Deadlock Detection Based on Resource Allocation Graph. 5th Int. Conf. Inform. Assurance Security, Xian, China, August 18\u201320, pp. 135\u2013138. IEEE, New York, NY. DOI 10.1109\/IAS.2009.64.","DOI":"10.1109\/IAS.2009.64"},{"key":"2016122017200672000_bxw099v1.81","doi-asserted-by":"crossref","unstructured":"Nguyen, H.H.C. , Le, V.S. and Nguyen, T.T. (2014) Algorithmic Approach to Deadlock Detection for Resource Allocation in Heterogeneous Platforms. In Int. Conf. Smart Comput., Hong Kong, November 3\u20135, pp. 97\u2013103. IEEE, New York, NY. DOI 10.1109\/SMARTCOMP.2014.7043845.","DOI":"10.1109\/SMARTCOMP.2014.7043845"},{"key":"2016122017200672000_bxw099v1.82","doi-asserted-by":"crossref","unstructured":"Petrovic, T. , Bogdan, S. and Sindicic, I. (2009) Determination of Circular Waits in Multiple-reentrant Flowlines Based on Machine-job Incidence Matrix. European Control Conference (ECC) 2009, Budapest, Hungary, August 23\u201326, pp. 4463\u20134468. IEEE, New York, NY. http:\/\/ieeexplore.ieee.org\/stamp\/stamp.jsp?arnumber=7075103 (accessed July 7, 2016).","DOI":"10.23919\/ECC.2009.7075103"},{"key":"2016122017200672000_bxw099v1.83","doi-asserted-by":"crossref","unstructured":"Kaveh, N. and Emmerich, W. (2001) Deadlock Detection in Distribution Object Systems. 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering - ESEC\/FSE-9, Vienna, Austria, September 10\u201314, pp. 44\u201351. ACM Press, New York, NY. DOI 10.1145\/503209.503216.","DOI":"10.1145\/503209.503216"},{"key":"2016122017200672000_bxw099v1.84","unstructured":"Karatkevich, A. and Grobelna, I. (2014) Deadlock Detection in Petri nets: One Trace for One Deadlock? 2014 7th Int. Conf. Hum. Syst. Interactions (HSI), Costa da Caparica, Lisbon, Portugal, June 16\u201318, pp. 227\u2013231. IEEE, New York, NY. DOI 10.1109\/HSI.2014.6860480."},{"key":"2016122017200672000_bxw099v1.85","doi-asserted-by":"crossref","unstructured":"Karacali, B. , Tai K.-C. and Vouk, M. (2000) Deadlock Detection of EFSMs Using Simultaneous Reachability Analysis. Int. Conf. Dependable Systems and Netw., DSN 2000, New York, NY, June 25\u201328, pp. 315\u2013324. IEEE Computer Society, New York, NY. DOI 10.1109\/ICDSN.2000.857555.","DOI":"10.1109\/ICDSN.2000.857555"},{"key":"2016122017200672000_bxw099v1.86","doi-asserted-by":"crossref","unstructured":"Geilen, M. and Basten, T. (2003) Requirements on the Execution of Kahn Process Networks. ESOP'03 the 12th European Symposium on Programming, Warsaw, Poland, April 7\u201311, LNCS 2618, pp. 319\u2013334. Springer, Berlin Heidelberg. DOI 10.1007\/3-540-36575-3_22.","DOI":"10.1007\/3-540-36575-3_22"},{"key":"2016122017200672000_bxw099v1.87","unstructured":"Longley, D. and Shain, M. (1986) Dictionary of Information Technology, Macmillan Press, London. ISBN 0-19-520519-7."},{"key":"2016122017200672000_bxw099v1.88","unstructured":"Masticola, S. and Ryder, B. (1990) Static Infinite Wait Anomaly Detection in Polynomial Time. 1990 Int. Conf. Parall. Process., Urbana-Champaign, IL, August 13\u201317, Vol. 2, pp. 78\u201387. Penn State University Press, University Park, PA. ISBN: 978-0-271-00728-1, Vol. 2: Software"},{"key":"2016122017200672000_bxw099v1.89","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/356586.356588","article-title":"System deadlocks","volume":"3","author":"Coffman","year":"1971","journal-title":"ACM Comput. Surv."},{"key":"2016122017200672000_bxw099v1.90","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1109\/MC.1980.1653786","article-title":"The deadlock problem: an overview","volume":"13","author":"Isloor","year":"1980","journal-title":"Computer"},{"key":"2016122017200672000_bxw099v1.91","doi-asserted-by":"crossref","unstructured":"Huang, C.-M. and Huang, D.-T. (1993) A Backward Protocol Verification Method. TENCON \u201893. IEEE Region 10 Int. Conf. Comput., Commun. Autom., Beijing, China, October 19\u201321, Vol. 1, pp. 515\u2013518. IEEE, New York, NY. DOI 10.1109\/TENCON.1993.320039","DOI":"10.1109\/TENCON.1993.320039"},{"key":"2016122017200672000_bxw099v1.92","unstructured":"Sharma, N.K. and Bhargava, B. (1987) A Robust Distributed Termination Detection Algorithm, Report 87\u2013726, Purdue University Press, West Lafayette, IN. http:\/\/docs.lib.purdue.edu\/cgi\/viewcontent.cgi?article=1626&context=cstech (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.93","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0020-0190(80)90021-6","article-title":"Termination detection for diffusing computations","volume":"11","author":"Dijkstra","year":"1980","journal-title":"Inf. Process. Lett."},{"key":"2016122017200672000_bxw099v1.94","doi-asserted-by":"crossref","unstructured":"Kumar, D. (1985). A Class of Termination Detection Algorithms for Distributed Computations. Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, December 16\u201318, pp. 73\u2013100. Springer, Berlin Heidelberg. DOI 10.1007\/3-540-16042-6_4.","DOI":"10.1007\/3-540-16042-6_4"},{"key":"2016122017200672000_bxw099v1.95","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF01782776","article-title":"Algorithms for distributed termination detection","volume":"2","author":"Mattern","year":"1987","journal-title":"Distrib. Comput."},{"key":"2016122017200672000_bxw099v1.96","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0164-1212(98)10034-1","article-title":"A taxonomy of distributed termination detection algorithms","volume":"43","author":"Matocha","year":"1998","journal-title":"J. Syst. Softw."},{"key":"2016122017200672000_bxw099v1.97","doi-asserted-by":"crossref","unstructured":"Chalopin, J. , Godard, E. , Metivier, Y. and Tel, G. (2007) About the Termination Detection in the Asynchronous Message Passing Model. 33rd Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, January 20\u201326, pp. 200\u2013211. Springer, Berlin Heidelberg. DOI 10.1007\/978-3-540-69507-3_16.","DOI":"10.1007\/978-3-540-69507-3_16"},{"key":"2016122017200672000_bxw099v1.98","doi-asserted-by":"crossref","unstructured":"Kshemkalyani, A.D. and Mukesh, S. (2008) Distributed Computing. Principles, Algorithms, and Systems, Cambridge University Press, Cambridge, UK. ISBN: 978-0-521-87634-6.","DOI":"10.1017\/CBO9780511805318"},{"key":"2016122017200672000_bxw099v1.99","unstructured":"Ma, G. (2007) Model checking support for CoreASM: model checking distributed abstract state machines using Spin, MSc Thesis. Simon Fraser University, Burnaby, Canada. http:\/\/summit.sfu.ca\/system\/files\/iritems1\/8056\/etd2938.pdf (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.100","doi-asserted-by":"crossref","unstructured":"Ray, I. and Ray, I. (2001) Detecting Termination of Active Database Rules Using Symbolic Model Checking. 5th East European Conference on Advances in Databases and Information Systems, ADBIS \u201801, Vilnius, Lithuania, September 25\u201328, pp. 266\u2013279. Springer, London, UK. DOI 10.1007\/3-540-44803-9_21.","DOI":"10.1007\/3-540-44803-9_21"},{"key":"2016122017200672000_bxw099v1.101","unstructured":"Garanina, N.O. and Bodin, E.V. (2014) Distributed Termination Detection by Counting Agent. 23th International Workshop on Concurrency, Specification and Programming, CS&P 2014, Chemnitz, Germany, 29 September\u20131 October 2014, pp. 69\u201379. Humboldt University, Berlin, Germany. http:\/\/ceur-ws.org\/Vol-1269\/paper69.pdf (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.102","unstructured":"Podelski, A. and Rybalchenko, A. (2003) Software Model Checking of Liveness Properties via Transition Invariants, Technical Report, Max Planck Institite fur Informatik, 2003."},{"key":"2016122017200672000_bxw099v1.103","doi-asserted-by":"crossref","unstructured":"Glabbeek, R.J. and Goltz, U. (1990) Equivalences and Refinement. LITP Spring School on Theoretical Computer Science La Roche Posay, France, April 23\u201327, LNCS 469, pp. 309\u2013333. Springer, Berlin Heidelberg. DOI 10.1007\/3-540-53479-2 13.","DOI":"10.1007\/3-540-53479-2"},{"key":"2016122017200672000_bxw099v1.104","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","article-title":"NUSMV: A new symbolic model checker","volume":"2","author":"Cimatti","year":"2000","journal-title":"Int. J. Softw. Tool. Technol. Transf."},{"key":"2016122017200672000_bxw099v1.105","first-page":"1294","article-title":"Improving resilience of autonomous moving platforms by real time analysis of their cooperation","volume":"2016","author":"Czejdo","year":"2016","journal-title":"Autobusy-TEST"},{"key":"2016122017200672000_bxw099v1.106","unstructured":"Dedan Examples , http:\/\/staff.ii.pw.edu.pl\/dedan\/files\/examples.zip (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.107","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.ic.2005.07.004","article-title":"Using heuristic search for finding deadlocks in concurrent systems","volume":"202","author":"Gradara","year":"2005","journal-title":"Inf. Comput."},{"key":"2016122017200672000_bxw099v1.108","doi-asserted-by":"crossref","first-page":"1397","DOI":"10.1016\/j.jcss.2006.03.003","article-title":"DELFIN+: An efficient deadlock detection tool for CCS processes","volume":"72","author":"Gradara","year":"2006","journal-title":"J. Comput. Syst. Sci."},{"key":"2016122017200672000_bxw099v1.109","doi-asserted-by":"crossref","unstructured":"Cheng, A. (1995) Complexity Results For Model Checking. BRICS Report RS- 95-18. University of Aarhus, Denmark. http:\/\/ojs.statsbiblioteket.dk\/index.php\/brics\/article\/view\/19920\/17574 (accessed September 21, 2016).","DOI":"10.7146\/brics.v2i18.19920"},{"key":"2016122017200672000_bxw099v1.110","unstructured":"Dedan , http:\/\/staff.ii.pw.edu.pl\/dedan\/files\/DedAn.zip (accessed July 7, 2016)."},{"key":"2016122017200672000_bxw099v1.111","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"2016122017200672000_bxw099v1.112","doi-asserted-by":"crossref","unstructured":"Krystosik, A. (2006) Embedded Systems Modeling Language. 2006 Int. Conf. Dependab. Comput. Syst., DepCos-RELCOMEX \u201806, Szklarska Poreba, Poland, May 25\u201327, pp. 27\u201334. Springer, Berlin Heidelberg. DOI 10.1109\/DEPCOS-RELCOMEX.2006.21.","DOI":"10.1109\/DEPCOS-RELCOMEX.2006.21"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/article-pdf\/60\/5\/729\/14011406\/bxw099.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,27]],"date-time":"2020-09-27T09:48:01Z","timestamp":1601200081000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article-lookup\/doi\/10.1093\/comjnl\/bxw099"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,20]]},"references-count":112,"alternative-id":["10.1093\/comjnl\/bxw099"],"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxw099","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"value":"0010-4620","type":"print"},{"value":"1460-2067","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,20]]}}}