{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:27:16Z","timestamp":1761964036164},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2004,3,1]],"date-time":"2004-03-01T00:00:00Z","timestamp":1078099200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2004,3]]},"DOI":"10.1007\/s10009-002-0104-3","type":"journal-article","created":{"date-parts":[[2004,3,19]],"date-time":"2004-03-19T13:53:20Z","timestamp":1079704400000},"page":"247-267","source":"Crossref","is-referenced-by-count":114,"title":["Directed explicit-state model checking in the validation of communication protocols"],"prefix":"10.1007","volume":"5","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Lluch-Lafuente","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,3,1]]},"reference":[{"key":"104_CR1","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Petterson, P., Romijn, J., Vaandrager, F.W.: Efficient guiding towards cost-imality in uppaal. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 2031. Springer, 2001","DOI":"10.1007\/3-540-45319-9_13"},{"key":"104_CR2","unstructured":"Bertoli, P., Cimatti, A., Roveri, M.: Heuristic search symbolic model checking = efficient conformant planning. In: International Joint Conference on Artificial Intelligence (IJCAI), 2001"},{"key":"104_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A.: \u03bccke - efficient \u03bc-calculus model checking. In: Computer Aided Verification (CAV), 1997, pp. 468\u2013471","DOI":"10.1007\/3-540-63166-6_50"},{"key":"104_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Design Automation Conference (DAC). ACM\/IEEE, 2000, pp. 29\u201334","DOI":"10.1145\/337292.337306"},{"key":"104_CR5","doi-asserted-by":"crossref","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM, 30(2): 323\u2013342, Apr 1983","DOI":"10.1145\/322374.322380"},{"key":"104_CR6","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, 2000"},{"key":"104_CR7","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Clarke, L.A., Osterweil, L.J.: The right algorithm at the right time: Comparing data flow analysis algorithms for finite s tate verification. In: 23rd International Conference on Software Engineering (ICSE). IEEE Computer Society, 2001, pp. 37\u201346","DOI":"10.1109\/ICSE.2001.919079"},{"key":"104_CR8","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. The MIT Press, 1990"},{"key":"104_CR9","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: A note on two problems in connection with graphs. Numerische Mathematik, 1: 269\u2013271, 1959","DOI":"10.1007\/BF01386390"},{"key":"104_CR10","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering (ICSE). IEEE Computer Society, 1999, pp. 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"104_CR11","unstructured":"Edelkamp, S.: Data Structures, and Learning Algorithms in State Space Search. PhD thesis, University of Freiburg, 1999. Infix."},{"key":"104_CR12","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: 8th International SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science 2057. Springer Verlag, 2001","DOI":"10.1007\/3-540-45139-0_5"},{"key":"104_CR13","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Protocol verification with heuristic search. In: AAAI Symposium on Model-based Validation of Intelligence, 2001"},{"key":"104_CR14","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Trail-directed model checking. In: Workshop on Software Model Checking, Electrical Notes in Theoretical Computer Science. Elsevier, 2001","DOI":"10.1007\/3-540-45139-0_5"},{"key":"104_CR15","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Reffel, F.: OBDDs in heuristic search. In: German Conference on Artificial Intelligence (KI), 1998, pp. 81\u201392","DOI":"10.1007\/BFb0095430"},{"key":"104_CR16","unstructured":"Edelkamp, S., Schr\u00f6dl, S.: Localizing A*. In: National Conference on Artificial Intelligence (AAAI), 2000, pp. 885\u2013890"},{"key":"104_CR17","doi-asserted-by":"crossref","unstructured":"Gouda, M.G.: Protocol verification made simple: a tutorial. Computer Networks and ISDN Systems, 25(9): 969\u2013980, 1993","DOI":"10.1016\/0169-7552(93)90094-K"},{"key":"104_CR18","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: Model checking java programs using structural heuristics. In: International Symposium on Software Testing and Analysis (ISSTA). ACM Press, 2002","DOI":"10.1145\/566172.566175"},{"key":"104_CR19","doi-asserted-by":"crossref","unstructured":"Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for heuristic determination of minimum path cost. IEEE Transactions on on Systems Science and Cybernetics, 4: 100\u2013107, 1968","DOI":"10.1109\/TSSC.1968.300136"},{"key":"104_CR20","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, 1990"},{"key":"104_CR21","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The model checker Spin. IEEE Transactions on Software Engineering, Special issue on Formal Methods in Software Practice, 23(5):279\u2013295, May 1997","DOI":"10.1109\/32.588521"},{"key":"104_CR22","unstructured":"Kamel, M., Leue, S.: Formalization and validation of the general inter-orb protocol (GIOP) using Promela and SPIN. In: Software Tools for Technology Transfer (STTT), 2: 394\u2013409, 2000"},{"key":"104_CR23","unstructured":"Kamel, M., Leue, S.: Vip: A visual editor and compiler for v-promela. In: 6th International Conference, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 1785. Springer, 2000, pp. 471\u2013486"},{"key":"104_CR24","doi-asserted-by":"crossref","unstructured":"Korf, R.E.: Depth-first iterative-deepening: An optimal admissible tree search. International Joint Conference on Artificial Intelligence (IJCAI), 27(1): 97\u2013109, 1985","DOI":"10.1016\/0004-3702(85)90084-0"},{"key":"104_CR25","doi-asserted-by":"crossref","unstructured":"Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. In: ACM SIGCOMM, 1987, pp. 126\u2013135","DOI":"10.1145\/55483.55496"},{"key":"104_CR26","doi-asserted-by":"crossref","unstructured":"Lluch-Lafuente, A., Leue, S., Edelkamp, S.: Partial order reduction in directed model checking. In: SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science, vol. 2318. Springer, 2002, pp. 112\u2013127","DOI":"10.1007\/3-540-46017-9_10"},{"key":"104_CR27","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"104_CR28","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Press, 1993","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"104_CR29","doi-asserted-by":"crossref","unstructured":"McVitie, D.G., Wilson, L.B.: The stable marriage problem. Communications of the ACM, 14(7): 486\u2013492, 1971","DOI":"10.1145\/362619.362631"},{"key":"104_CR30","unstructured":"Muller, D.E., Saoudi, A., Schnupp, P.E.: Alternating automata. The weak monadic theory of the tree, its complexity. In: Laurent Kott (ed.) International Colloquium on Automata, Languages and Programming. Springer, 1986, pp. 275\u2013283"},{"key":"104_CR31","doi-asserted-by":"crossref","unstructured":"Khurshid, S, Khurshid, P.: Exploring very large state spaces using genetic algorithms. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 2280. Springer, 2002, pp. 266\u2013280","DOI":"10.1007\/3-540-46002-0_19"},{"key":"104_CR32","unstructured":"Reffel, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: World Congress on Formal Methods. Springer, 1999, pp. 195\u2013211"},{"key":"104_CR33","doi-asserted-by":"crossref","unstructured":"Somenzi, F., Bloem, R.: Efficient buchi automata from LTL formulae. In: Computer Aided Verification, 2000","DOI":"10.1007\/10722167_21"},{"key":"104_CR34","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/s100090050042","volume":"2","author":"Visser,","year":"4","unstructured":"Visser, W., Barringer, H.: Practical CTL* model checking: Should SPIN be extended? Int J Softw Tools Technol Transfer 2(4): 350\u2013365, 2000","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"104_CR35","doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Design Automatin Conference (DAC). ACM\/IEEE, 1998, pp. 599\u2013604","DOI":"10.1145\/277044.277201"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0104-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0104-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0104-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0104-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:17Z","timestamp":1559100317000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0104-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":35,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["104"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0104-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,3]]}}}