{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:48:08Z","timestamp":1762458488231,"version":"3.32.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,7,6]],"date-time":"2006-07-06T00:00:00Z","timestamp":1152144000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,10,27]]},"DOI":"10.1007\/s10703-006-0006-1","type":"journal-article","created":{"date-parts":[[2006,7,6]],"date-time":"2006-07-06T04:43:25Z","timestamp":1152161005000},"page":"215-251","source":"Crossref","is-referenced-by-count":18,"title":["Question-guided stubborn set methods for state properties"],"prefix":"10.1007","volume":"29","author":[{"given":"L. M.","family":"Kristensen","sequence":"first","affiliation":[]},{"given":"K.","family":"Schmidt","sequence":"additional","affiliation":[]},{"given":"A.","family":"Valmari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,7,6]]},"reference":[{"key":"6_CR1","unstructured":"T. Andrews, S. Qadeer, S.K. Rajamani, J. Rehof, and Y. Xie,\u201cZing: A model checker for concurrent software,\u201d in Proceedings of Conference on Computer-Aided Verification , Vol. 3114 of Lecture Notes in Computer Science, 2004, pp. 484\u2013487."},{"key":"6_CR2","unstructured":"R. Bhattacharya, S. German, and G. Gopalakrishnan, \u201cA symbolic partial order reduction algorithm for rule based transition systems,\u201d Technical Report UUCS-03-028, School of Computing, University of Utah, 2003"},{"key":"6_CR3","unstructured":"E. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronisation skeletons using branching time temporal logic,\u201d in Proccedings of Workshop on Logic of Programs, Vol. 131 of Lecture Notes in Computer Science, 1981."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, M. Minna, and D. Peled, \u201cState Space Reduction using Partial Order Techniques,\u201d Int. J. Soft. Tools Technol. Trans., Vol. 2, No, 3, pp. 279\u2013287, 1999.","DOI":"10.1007\/s100090050035"},{"key":"6_CR5","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled, Model Checking, The MIT Press, 1999."},{"key":"6_CR6","unstructured":"F. Curbera, Y. Goland, J. Klein, F. Leymann, D. Roller, S. Thatte, and S. Weerawarana, \u201cBusiness process execution language for web services, Version 1.1,\u201d Technical report, BEA Systems, International Business Machines Corporation, Microsoft Corporation, 2003."},{"key":"6_CR7","unstructured":"J. Desel and W. Reisig, \u201cPlace\/Transition petri nets,\u201d in Lecture on Petri Nets I: Basic Models, Vol. 1491 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 122\u2013173."},{"key":"6_CR8","unstructured":"D.L. Dill, \u201cThe Mur\u03c6 verification system,\u201d in Proceedings of Conference on Computer-Aided Verification, Vol. 1102 of Lecture Notes in Computer Science 1996, pp. 390\u2013393."},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, Temporal and Modal Logic, Vol. B of Handbook of Theoretical Computer Science, Elsevier, Chapt. 16, pp. 995\u20131072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"R. Gerth, R. Kuiper, D. Peled, and W. Penczek, \u201cA Partial order approach to branching time logic model checking,\u201d in Proc. of 3rd Israel Symposium on the Theory of Computing and Systems, 1995, pp. 130\u2013140.","DOI":"10.1109\/ISTCS.1995.377038"},{"key":"6_CR11","unstructured":"A. Gibbons, Algorithmic Graph Theory. Cambridge University Press, 1985."},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"P. Godefroid, \u201cUsing partial orders to improve automatic verification methods,\u201d in Proceedings of CAV'90, Vol. 531 of Lecture Notes in Computer Science, 1990, pp. 175\u2013186.","DOI":"10.1090\/dimacs\/003\/21"},{"key":"6_CR13","unstructured":"P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, An Approach to the State-Explosion Problem, Vol. 1032 of Lecture Notes in Computer Science, Springer-Verlag, 1996."},{"key":"6_CR14","unstructured":"S. Hinz, K. Schmidt, and C. Stahl, \u201cTransforming BPEL to petri nets,\u201d in W. van der Aalst, B. Benatallah, F. Casati, and F. Curbera (Eds.), Proceedings of the Third International Conference on Business Process Management (BPM 2005), Vol. 3649 of Lecture Notes in Computer Science, Nancy, France, 2005, pp. 220\u2013235."},{"key":"6_CR15","unstructured":"G.J. Holzmann, The SPIN Model Checker, Addison-Wesley, 2003."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"I. Kokkarinen, A. Valmari, and D. Peled, \u201cRelaxed visibility enhances partial order reduction,\u201d Form. Method Syst. Des., Vol. 19, pp. 275\u2013289, 2001.","DOI":"10.1023\/A:1011202615884"},{"key":"6_CR17","unstructured":"L.M. Kristensen and A. Valmari, \u201cImproved question-guided stubborn set methods for state properties,\u201d in Proceedings of ICATPN'2000, vol. 1825 of Lecture Notes in Computer Science, 2000, pp. 282\u2013301."},{"key":"6_CR18","unstructured":"A. Lluch-Lafuente, S. Edelkamp, and S. Leue,\u201cPartial order reduction in directed model checking,\u201d in Proc. of 9th International SPIN Workshop on Model Checking of Software, Vol. 2318 of Lecture Notes in Computer Science, 2002, pp. 112\u2013127."},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"T. Murata, \u201cPetri Nets: Properties, analysis and application,\u201d in Proceedings of the IEEE, Vol. 77, No. 4. IEEE Computer Society 1989, pp. 541\u2013580.","DOI":"10.1109\/5.24143"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"D. Peled, \u201cAll from one, one for all: On model checking using representatives,\u201d in Proceedings of CAV'93, Vol. 697 of Lecture Notes in Computer Science, 1993, pp. 409\u2013423.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"D. Peled, \u201cCombining partial order reductions with on-the-fly model checking,\u201d Form. Method Syst. Des., Vol. 8, No. 1, pp. 39\u201364, 1996,.","DOI":"10.1007\/BF00121262"},{"key":"6_CR22","unstructured":"D. Peled, \u201cTen years of partial order reduction,\u201d in Proceedings of CAV'98, Vol. 1427 of Lecture Notes in Computer Science, 1998, pp. 17\u201328."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cA Temporal Logic of Concurrent Systems,\u201d Theor. Comp. Sci., Vol. 13, pp. 45\u201360, 1981.","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"J.P. Quielle, and J. Sifakis, \u201cSpecification and verification of concurrent systems in CESAR,\u201d in Proceedings of 5th International Symposium on Programming, Vol. 137 of Lecture Notes in Computer Science, 1982, pp. 337\u2013350.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare, Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"6_CR26","unstructured":"W. Reisig, Petri Nets, Vol. 4 of EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1985."},{"key":"6_CR27","unstructured":"K. Schmidt, \u201cStubborn sets for standard properties,\u201d in Proceedings of ICATPN'99, Vol. 1639 of Lecture Notes in Computer Science, 1999, pp. 46\u201365."},{"key":"6_CR28","unstructured":"K. Schmidt, \u201cLoLA: A low level analyser,\u201d in Proceedings of ICATPN'2000, Vol. 1825 of Lecture Notes in Computer Science, 2000, pp. 465\u2013474."},{"key":"6_CR29","unstructured":"K. Schmidt, \u201cLoLA tool homepage,\u201d 2003 http:\/\/www.informatik.hu-berlin.de\/~kschmidt\/lola.html ."},{"key":"6_CR30","unstructured":"C. Stahl, \u201cA petri net semantics for BPEL,\u201d Informatik-Berichte 188, Humboldt-Universitt zu Berlin, 2005."},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"C. Stahl, W. Reisig, and M. Krstic, \u201cHazard detection in a GALS Wrapper: A case study,\u201d in J. Desel and Y. Watanabe (Eds.), Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05), St. Malo, France, 2005, pp. 234\u2013243.","DOI":"10.1109\/ACSD.2005.20"},{"key":"6_CR32","unstructured":"A. Valmari, \u201cError detection by reduced reachability graph generation,\u201d in Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, 1988, pp. 95\u2013112."},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"A. Valmari, \u201cA stubborn attack on state explosion,\u201d in Proceedings of CAV'90, Vol. 531 of Lecture Notes in Computer Scienc, 1990, pp. 156\u2013165.","DOI":"10.1007\/BFb0023729"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"A. Valmari, \u201cStubborn sets for reduced state space generation,\u201d in G. Rozenberg (Ed.), Advances in Petri Nets '90, Vol. 483 of Lecture Notes in Computer Science, 1990, pp. 491\u2013515.","DOI":"10.1007\/3-540-53863-1_36"},{"key":"6_CR35","unstructured":"A. Valmari, \u201cState of the art report: Stubborn sets,\u201d Petri Net. Newsl., Vol. 46, pp. 6\u201314, 1994."},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"A. Valmari, \u201cStubborn set methods for process algebras,\u201d in Proceedings of POMIV'96, Workshop on Partial Order Methods in Verification, Vol. 29 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1997, pp. 213\u2013231.","DOI":"10.1090\/dimacs\/029\/12"},{"key":"6_CR37","unstructured":"A. Valmari, \u201cThe state explosion problem,\u201d in W. Reisig and G. Rozenberg (Eds.), Lectures on Petri Nets I: Basic Models, Vol. 1491 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 429\u2013528."},{"key":"6_CR38","unstructured":"R. van Glabbeek and W. Weijland, \u201cBranching time and abstraction in bisimulation semantics (Extended Abstract),\u201d in Proc. of IFIP International Conference on Information Processing, 1989, pp. 613\u2013618."},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"B. Vergauwen and J. Lewi, \u201cA linear local model checking algorithm for CTL,\u201d in Proceedings of CONCUR'93, Vol. 715 of Lecture Notes in Computer Science, 1993, pp. 447\u2013461.","DOI":"10.1007\/3-540-57208-2_31"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"P. Wolper and P. Godefroid, \u201cPartial order methods for temporal Verification,\u201d in Proceedings of CONCUR'93, Vol. 715 of Lecture Notes in Computer Science, 1993, pp. 233\u2013246.","DOI":"10.1007\/3-540-57208-2_17"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0006-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0006-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0006-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T19:49:55Z","timestamp":1736452195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0006-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,6]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,10,27]]}},"alternative-id":["6"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0006-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2006,7,6]]}}}