{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:51Z","timestamp":1725456231359},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627814"},{"type":"electronic","value":"9783540685173"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0030626","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T01:10:41Z","timestamp":1133399441000},"page":"565-579","source":"Crossref","is-referenced-by-count":13,"title":["A compositional proof of a real-time mutual exclusion protocol"],"prefix":"10.1007","author":[{"given":"K\u00e5re J.","family":"Kristoffersen","sequence":"first","affiliation":[]},{"given":"Francois","family":"Laroussinie","sequence":"additional","affiliation":[]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,20]]},"reference":[{"issue":"2","key":"45_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. Automata for Modelling Real-Time Systems. Theoretical Computer Science, 126(2):183\u2013236, April 1994.","journal-title":"Theoretical Computer Science"},{"key":"45_CR2","doi-asserted-by":"crossref","unstructured":"H. R. Andersen. Partial Model Checking. In Proc. of LICS'95, 1995.","DOI":"10.1109\/LICS.1995.523274"},{"key":"45_CR3","unstructured":"Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal \u2014 A Tool Suite for Symbolic and Compositional Verification of Real-Time Systems. Presented at the 1st Workshop on Tools and Algorithms for the Construction and Analysis of Systems, May 1995."},{"key":"45_CR4","doi-asserted-by":"crossref","unstructured":"Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. In Proc. of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in Lecture Notes in Computer Science, pages 431\u2013434. Springer-Verlag, March 1996.","DOI":"10.1007\/3-540-61042-1_66"},{"key":"45_CR5","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1020 states and beyond. Logic in Computer Science, 1990."},{"key":"45_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetry in Temporal Logic Model Checking. 697, 1993. In Proc. of CAV'93.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"45_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Gr\u00fcmberg, and D. E. Long. Model Checking and Abstraction. Principles of Programming Languages, 1992.","DOI":"10.1145\/143165.143235"},{"key":"45_CR8","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, and S. Yovine. Verifying ET-LOTOS programs with KRONOS. In Proc. of 7th International Conference on Formal Description Techniques, 1994.","DOI":"10.1007\/978-0-387-34878-0_17"},{"key":"45_CR9","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. S. Jutla. Symmetry and Model Checking. 697, 1993. In Proc. of CAV'93.","DOI":"10.1007\/3-540-56922-7_38"},{"key":"45_CR10","doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper. A Partial Approach to Model Checking. Logic in Computer Science, 1991.","DOI":"10.1109\/LICS.1991.151664"},{"issue":"2","key":"45_CR11","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"Thomas. A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic Model Checking for Real-Time Systems. Information and Computation, 111(2):193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"45_CR12","doi-asserted-by":"crossref","unstructured":"Pei-Hsin Ho and Howard Wong-Toi. Automated Analysis of an Audio Control Protocol. In Proc. of CAV'95, volume 939 of Lecture Notes in Computer Science. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_64"},{"key":"45_CR13","doi-asserted-by":"crossref","unstructured":"F. Laroussinie and K.G. Larsen. Compositional Model Checking of Real Time Systems. In Proc. of CONCUR '95, Lecture Notes in Computer Science. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60218-6_3"},{"key":"45_CR14","doi-asserted-by":"crossref","unstructured":"F. Laroussinie, K.G. Larsen, and C. Weise. From Timed Automata to Logic \u2014 and Back. In Proc. of MFCS'95, Lecture Notes in Computer Sciencie, 1995. Also BRICS report series RS-95-2.","DOI":"10.1007\/3-540-60246-1_158"},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 76\u201387, December 1995.","DOI":"10.1109\/REAL.1995.495198"},{"key":"45_CR16","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, Lecture Notes in Computer Science. Springer-Verlag, October 1995.","DOI":"10.1007\/BFb0020977"},{"key":"45_CR17","doi-asserted-by":"crossref","unstructured":"F. Pagani. Partial orders and verification of real-time systems. Lecture Notes in Computer Science, (1135), 1996.","DOI":"10.1007\/3-540-61648-9_49"},{"key":"45_CR18","doi-asserted-by":"crossref","unstructured":"A. Valmari. A Stubborn Attack on State Explosion. Theoretical Computer Science, 3, 1990.","DOI":"10.1090\/dimacs\/003\/04"},{"key":"45_CR19","unstructured":"Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Proc. of the 7th International Conference on Formal Description Techniques, 1994."}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '97: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0030626","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T13:49:48Z","timestamp":1683294588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0030626"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627814","9783540685173"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0030626","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}