{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:40:56Z","timestamp":1773654056830,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540412199","type":"print"},{"value":"9783540409229","type":"electronic"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_13","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:41:36Z","timestamp":1196329296000},"page":"217-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Executable Protocol Specification in ESL"],"prefix":"10.1007","author":[{"given":"E.","family":"Clarke","sequence":"first","affiliation":[]},{"given":"S.","family":"German","sequence":"additional","affiliation":[]},{"given":"Y.","family":"Lu","sequence":"additional","affiliation":[]},{"given":"H.","family":"Veith","sequence":"additional","affiliation":[]},{"given":"D.","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/10722167_40","volume-title":"CAV 00: Computer-Aided Verification","author":"Y. Abarbanel","year":"2000","unstructured":"Y. Abarbanel, I. Beer, L. Gluhovsky, S. Keidar and Y. Wolfsthal,\u201cFoCs-AutomaticGeneration of Simulation Checkers from Formal Specifications\u201d, CAV 00: Computer-Aided Verification, Lecture Notes in Computer Science 1855, 538\u2013542. Springer-Verlag, 2000."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Reactive Modules, Proceedings of the 11th Annual Symposium on Logic in Computer Science, 207\u2013218. IEEE Computer Society Press, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Proc. 38th IEEE Symposium on Foundations of Computer Science, 100\u2013109, 1997.","DOI":"10.1109\/SFCS.1997.646098"},{"key":"13_CR4","unstructured":"R. E. Bryant, P. Chauhan, E. M. Clarke, A. Goel. A Theory of Consistency for Modular Synchronous Systems. Formal Methods in Computer-Aided Design, 2000"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"P. Chauhan, E. Clarke, Y. Lu, and D. Wang. Verifying IP-Core based System-On-Chip Designs. In Proceedings of the IEEE ASIC Conference, 27\u201331, 1999.","DOI":"10.1109\/ASIC.1999.806467"},{"key":"13_CR6","unstructured":"T. Cormen, C. Leiserson, and R. Rivest. Introduction to Algorithm. MIT Press, 1990."},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Synthesis of synchronization skeletons for branching time temporal logic","author":"E. Clarke","year":"1981","unstructured":"E. Clarke and E. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. Logic of Programs: Workshop, Yorktown Heights, NY, May 1981 Lecture Notes in Computer Science, Vol. 131, Springer-Verlag. 1981."},{"key":"13_CR8","first-page":"241","volume":"2","author":"E. Emerson","year":"1982","unstructured":"E. Emerson and E. Clarke.Using branching time temporal logic to synthesize synchronization skeletons. In Science of Computer Programming, Vol 2, 241\u2013266. 1982.","journal-title":"Using branching time temporal logic to synthesize synchronization skeletons"},{"key":"13_CR9","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking.MIT Publishers, 1999."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"David Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independentCircuits. MIT Press, 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"13_CR11","unstructured":"M. Fujita and S. Kono. Synthesis of Controllers from Interval Temporal Logic Specification. InternationalWorkshop on Logic Synthesis,May, 1993."},{"key":"13_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-51803-7_36","volume-title":"Temporal Logic in Specification","author":"D. Gabbay","year":"1989","unstructured":"D. Gabbay. The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In B. Banieqbal, B. Barringer, and A. Pnueli, editors, Temporal Logic in Specification,Vol. 398, 409\u2013448. Springer Verlag, LNCS 398, 1989."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"13_CR14","unstructured":"N. Halbwachs, J.-C. Fernandez, and A. Bouajjanni. An executable temporal logic to express safety properties and its connection with the language Lustre. In Sixth International Symp. on Lucid and Intensional Programming, ISLIP\u201993, Quebec City, Canada, April 1993. Universit\u2019e Laval."},{"issue":"3","key":"13_CR15","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872\u2013923,March 1994.","journal-title":"ACM TOPLAS"},{"issue":"1","key":"13_CR16","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Z. Manna, P. Wolper: Synthesis of Communicating Processes from Temporal Logic Specifications, ACM TOPLAS, Vol.6, N.1, Jan. 1984, 68\u201393.","journal-title":"ACM TOPLAS"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"B. Moszkowski. Executing temporal logic programs. Cambridge University Press, 1986.","DOI":"10.1007\/3-540-15670-4_6"},{"key":"13_CR19","unstructured":"PCI Special Interest Group. PCI Local Bus Specification Rev 2.2. Dec. 1998."},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"J. Yuan, K. Shultz, C. Pixley, and H. Miller. Modeling Design Constraints and Biasing in Simulation Using BDDs. In International Conference on Computer-Aided Design. 584\u2013589, November 7-11, 1999","DOI":"10.1109\/ICCAD.1999.810715"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"A. Seawright, and F. Brewer. Synthesis from Production-Based Specifications. In Proceedings of the 29th ACM\/IEEE Design Automation Conference, 194\u2013199, 1992.","DOI":"10.1109\/DAC.1992.227837"},{"key":"13_CR22","unstructured":"X. Shen, and Arvind. Design and Verification of Speculative Processors. In Proceedings of the Workshop on Formal Techniques for Hardware and Hardware-like Systems, June 1998, Marstrand, Sweden."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"K. Shimizu, D. Dill, and A. Hu. Monitor Based Formal Specification of PCI. FormalMethods in Computer-Aided Design, 2000.","DOI":"10.1007\/3-540-40922-X_21"},{"key":"13_CR24","unstructured":"K. Shimizu. http:\/\/radish.stanford.edu\/pci"},{"key":"13_CR25","unstructured":"M. Sipser. Introduction to the Theory of Computation. PWS Publishing Company. 1997."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:23:58Z","timestamp":1737591838000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}