{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:39:19Z","timestamp":1725485959459},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414285"},{"type":"electronic","value":"9783540444640"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44464-5_14","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T19:34:00Z","timestamp":1181158440000},"page":"182-198","source":"Crossref","is-referenced-by-count":1,"title":["On Model Checking Synchronised Hardware Circuits"],"prefix":"10.1007","author":[{"given":"Martin","family":"Leucker","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,8]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"S. Bensalem, P. Caspi, C. Parent-Vigouroux, and C. Dumas. A methodology for proving control systems with Lustre and PVS. In Charles B. Weinstock and John Rushby, editors, Dependable Computing for Critical Applications\u20147, volume 12 of Dependable Computing and Fault Tolerant Systems, pages 89\u2013107, San Jose, CA, January 1999. IEEE Computer Society.","DOI":"10.1109\/DCFTS.1999.814291"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0304-3975(80)90069-9","volume":"10","author":"J. A. Brzozowski","year":"1980","unstructured":"J. A. Brzozowski and E. Leiss. On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science, 10:19\u201335, 1980.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"14_CR3","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A. K. Chandra","year":"1981","unstructured":"Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114\u2013133, January 1981. 198 Martin Leucker","journal-title":"Journal of the ACM"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. LUSTRE: A declarative language for programming synchronous systems. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, pages 178\u2013188, Munich, West Germany, January 21-23, 1987. ACM SIGACT-SIGPLAN, ACM Press.","DOI":"10.1145\/41625.41641"},{"key":"14_CR5","unstructured":"Volker Diekert and Yves M\u00e9tivier. Partial commutation and traces. Technical Report TR-1996-02, Universit\u00e4t Stuttgart, Fakult\u00e4t Informatik, Germany, March 1996."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.","DOI":"10.1142\/9789814261456"},{"key":"14_CR7","volume-title":"Tool Support for System Specification, Development, and Verification","author":"M. Lange","year":"1999","unstructured":"M. Lange, M. Leucker, T. Noll, and S. Tobies. Truth \u2014 a verification platform for concurrent systems. In Tool Support for System Specification, Development, and Verification, Advances in Computing Science. Springer-Verlag Wien New York, 1999."},{"issue":"3","key":"14_CR8","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25(3):267\u2013310, July 1983.","journal-title":"Theoretical Computer Science"},{"key":"14_CR9","unstructured":"R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989."},{"key":"14_CR10","unstructured":"Motorola, editor. The PowerPC (TM) 601 User\u2019s Manual. Motorola, 1993."},{"key":"14_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, 1992."},{"key":"14_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"CAV, Computer Aided Verification","author":"D. Peled","year":"1998","unstructured":"Doron Peled. Ten years of partial order reduction. In CAV, Computer Aided Verification, number 1427 in LNCS, pages 17\u201328, Vancouver, BC, Canada, 1998. Springer."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Doron Peled and Wojciech Penczek. Using asynchronous buchi automata for efficient model-checking of concurrent systems. In Protocol Specification Testing and Verification, pages 90\u2013100, Warsaw, Poland, 1995. Chapman & Hall.","DOI":"10.1007\/978-0-387-34892-6_20"},{"key":"14_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-71275-3","volume-title":"Petrinetze","author":"W. Reisig","year":"1986","unstructured":"Wolfgang Reisig. Petrinetze. Springer-Verlag, Berlin Heidelberg New York Tokyo, 2 edition, 1986.","edition":"2 edition"},{"key":"14_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1007\/3-540-65306-6_24","volume-title":"Distributed versions of linear time temporal logic: A trace perspective","author":"P. S. Thiagarajan","year":"1998","unstructured":"P. S. Thiagarajan and J. G. Henriksen. Distributed versions of linear time temporal logic: A trace perspective. Lecture Notes in Computer Science, 1492:643\u2013681, 1998."},{"key":"14_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-60218-6_33","volume-title":"A trace consistent subset of PTL","author":"P. S. Thiagarajan","year":"1995","unstructured":"P. S. Thiagarajan. A trace consistent subset of PTL. In Insup Lee and Scott A. Smolka, editors, CONCUR\u2019 95: Concurrency Theory, 6th International Conference, volume 962 of Lecture Notes in Computer Science, pages 438\u2013452, Philadelphia, Pennsylvania, 21-24 August 1995. Springer-Verlag."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133\u2013191. Elsevier Science Publishers B. V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"14_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"An Automata-Theoretic Approach to Linear Temporal Logic","author":"M. Y. Vardi","year":"1996","unstructured":"Moshe Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic, volume 1043 of Lecture Notes in Computer Science, pages 238\u2013266. Springer-Verlag Inc., New York, NY, USA, 1996."},{"key":"14_CR19","first-page":"99","volume":"21","author":"W. Zielonka","year":"1987","unstructured":"WiesMlaw Zielonka. Notes on finite asynchronous automata. R.A.I.R.O. \u2014 Informatique Th\u00e9orique et Applications, 21:99\u2013135, 1987.","journal-title":"R.A.I.R.O. \u2014 Informatique Th\u00e9orique et Applications"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44464-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:38:36Z","timestamp":1556465916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44464-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414285","9783540444640"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-44464-5_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}