{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171935},"publisher-location":"Berlin\/Heidelberg","reference-count":28,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540566627"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0024669","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T05:09:15Z","timestamp":1132722555000},"page":"597-616","source":"Crossref","is-referenced-by-count":22,"title":["Putting advanced reachability analysis techniques together: The \u201cARA\u201d tool"],"prefix":"10.1007","author":[{"given":"Antti","family":"Valmari","sequence":"first","affiliation":[]},{"given":"Jukka","family":"Kemppainen","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Clegg","sequence":"additional","affiliation":[]},{"given":"Mikko","family":"Levanto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"36_CR1","unstructured":"Bergstra, J. A. & Klop, J. W. & Olderog, E.-R.: Failures without Chaos: A New Process Semantics for Fair Abstraction. Formal Description of Programming Concepts III, North-Holland 1987, pp. 77\u2013103."},{"key":"36_CR2","unstructured":"Bochmann, G. v.: Usage of Protocol Development Tools: The Results of a Survey. Proceedings of the 7th International IFIP WG 6.1 Symposium on Protocol Specification, Testing and Verification (1987), North-Holland 1988."},{"key":"36_CR3","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LO-TOS. Computer Networks and ISDN Systems 14 1987 pp. 25\u201359. Also: The Formal Description Technique LOTOS, North-Holland 1989, pp. 23\u201373.","journal-title":"Computer Networks and ISDN Systems"},{"issue":"3","key":"36_CR4","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S. D. Brookes","year":"1984","unstructured":"Brookes, S. D. & Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating Sequential Processes. Journal of the ACM 31 (3) 1984 pp. 560\u2013599.","journal-title":"Journal of the ACM"},{"key":"36_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M. & Emerson, E. A. & Sistla, A. P.: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, vol 8, 1986, pp. 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Cleaveland, R. & Parrow, J. & Steffen, B.: The Concurrency Workbench. Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 24\u201337.","DOI":"10.1007\/3-540-52148-8_3"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Feldbrugge, F. & Jensen, K.: Petri Net Tool Overview 1986. Advances in Petri Nets 1986, Part II, Lecture Notes in Computer Science 255, Springer-Verlag 1987, pp. 20\u201361.","DOI":"10.1007\/3-540-17906-2_21"},{"key":"36_CR8","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","volume":"13","author":"J.-C Fernandez","year":"1989\/90","unstructured":"Fernandez, J.-C: An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming 13 (1989\/90) pp. 219\u2013236.","journal-title":"Science of Computer Programming"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C. & Mounier, L.: A Tool Set for Deciding Behavioural Equivalences. Proceedings of CONCUR '91, Lecture Notes in Computer Science 527, Springer-Verlag 1991, pp. 23\u201342.","DOI":"10.1007\/3-540-54430-5_78"},{"key":"36_CR10","doi-asserted-by":"crossref","unstructured":"Graf, S. & Steffen, B.: Compositional Minimization of Finite-State Processes. In: Computer-Aided Verification '90 (Proceedings of a workshop), AMS DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol 3, American Mathematical Society 1991, pp. 57\u201373.","DOI":"10.1090\/dimacs\/003\/06"},{"key":"36_CR11","unstructured":"Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p."},{"key":"36_CR12","unstructured":"ISO 8807 International Standard: Information processing systems \u2014 Open Systems Interconnection \u2014 LOTOS \u2014 A formal description technique based on the temporal ordering of observational behaviour. International Organization for Standardization, 1989, 142 p."},{"key":"36_CR13","doi-asserted-by":"crossref","unstructured":"Kaivola, R. & Valmari, A.: Using Truth-Preserving Reductions to Improve the Clarity of Kripke Models. Proceedings of CONCUR '91, Lecture Notes in Computer Science 527, Springer-Verlag 1991, pp. 361\u2013375.","DOI":"10.1007\/3-540-54430-5_100"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Kaivola, R. & Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-Less Linear Temporal Logic. Proceedings of CONCUR '92, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207\u2013221.","DOI":"10.1007\/BFb0084793"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O. & Pnueli, A.: Checking that Finite State Concurrent Programs Satisfy their Linear Specification. Tenth ACM Symposium on Principles of Programming Languages, 1984, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"36_CR16","unstructured":"Madelaine, E. & Vergamini, D.: AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. Formal Description Techniques II (Proceedings of FORTE '89), North-Holland 1990, pp. 61\u201366."},{"key":"36_CR17","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p."},{"key":"36_CR18","unstructured":"Petri Net Newsletter 41, Special Volume: Petri Net Tools Overview 92. Gesellschaft f\u00fcr Informatik, Bonn, Germany, April 1992, 43 p."},{"key":"36_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. Current Trends in Concurrency, Lecture Notes in Computer Science 224, Springer-Verlag 1985, pp. 510\u2013584.","DOI":"10.1007\/BFb0027047"},{"key":"36_CR20","unstructured":"Valmari, A.: Error Detection by Reduced Reachability Graph Generation. Proceedings of the Ninth European Workshop on Application and Theory of Petri Nets, Venice, Italy 1988, pp. 95\u2013112."},{"key":"36_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0165-6074(88)90016-6","volume":"24","author":"A. Valmari","year":"1988","unstructured":"Valmari, A.: PC-Rimst \u2014 A Tool for Validating Concurrent Program Designs. Micro-processing and Microprogramming 24 (1988) 1\u20135 (Proceedings of the Euromicro '88), pp. 809\u2013818.","journal-title":"Micro-processing and Microprogramming"},{"key":"36_CR22","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491\u2013515. (An earlier version appeared in Proceedings of the Tenth International Conference on Application and Theory of Petri Nets, Bonn, FRG 1989, Vol. II pp. 1\u201322.)","DOI":"10.1007\/3-540-53863-1_36"},{"key":"36_CR23","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods is System Design, 1: 297\u2013322 (1992). (Earlier version appeared in Proceedings of the Workshop on Computer-Aided Verification 1990.)","journal-title":"Formal Methods is System Design"},{"key":"36_CR24","unstructured":"Valmari, A.: Compositional State Space Generation. University of Helsinki, Department of Computer Science, Report A-1991\u20135, Helsinki, Finland 1991. 30 p. (An earlier version appeared in Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France 1990, pp. 43\u201362.)"},{"key":"36_CR25","doi-asserted-by":"crossref","unstructured":"Valmari, A. et Clegg, M.: Reduced Labelled Transition Systems Save Verification Effort. Proceedings of CONCUR '91, Lecture Notes in Computer Science 527, Springer-Verlag 1991, pp. 526\u2013540.","DOI":"10.1007\/3-540-54430-5_111"},{"key":"36_CR26","unstructured":"Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. Protocol Specification, Testing and Verification XI (Proceedings of the 11th International IFIP Symposium), North-Holland 1991, pp. 3\u201318."},{"key":"36_CR27","volume-title":"Report A-1992-4","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. University of Helsinki, Department of Computer Science, Report A-1992-4, Helsinki, Finland 1992. 57 p."},{"key":"36_CR28","unstructured":"Wheeler, G. R. & Valmari, A. & Billington, J.: Baby TORAS Eats Philosophers but Thinks about Solitaire. Proceedings of the Fifth Australian Software Engineering Conference, Sydney, Australia 1990, pp. 283\u2013288."}],"container-title":["Lecture Notes in Computer Science","FME '93: Industrial-Strength Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0024669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:54:07Z","timestamp":1586566447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0024669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540566627"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/bfb0024669","relation":{},"subject":[]}}