{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:36:58Z","timestamp":1742391418758},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_7","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"67-81","source":"Crossref","is-referenced-by-count":13,"title":["Efficient Decompositional Model Checking for Regular Timing Diagrams"],"prefix":"10.1007","author":[{"given":"Nina","family":"Amla","sequence":"first","affiliation":[]},{"given":"E. Allen","family":"Emerson","sequence":"additional","affiliation":[]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"7_CR1","unstructured":"C. Antoine and B. Le Goff. Timing Diagrams for Writing and Checking Logical and Behavioral Properties of Integrated Systems. In Correct Hardware Design Methodologies. Elsevier Sciences Publishers, 1992."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"G. Borriello. Formalized Timing Diagrams. In EDAC92. IEEE Comput. Soc. Press, 1992.","DOI":"10.1109\/EDAC.1992.205958"},{"key":"7_CR3","unstructured":"R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS. In FMCAD, 1996."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"V. Cingel. A Graph-based Method for Timing Diagrams Representation and Verification. In Correct Hardware Design and Verification Methods. Springer Verlag, 1993.","DOI":"10.1007\/BFb0021710"},{"key":"7_CR5","unstructured":"E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In Workshop on Logics of Programs, volume 131. Springer Verlag, 1981."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic. ACM Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"7_CR7","volume-title":"Programming Concepts, Methods and Calculi","author":"W. Damm","year":"1994","unstructured":"W. Damm and J. Helbig. Linking Visual Formalisms: A Compositional proof System for Statecharts cased on Symbolic Timing Diagrams. In E. R. Olderog, editor, Programming Concepts, Methods and Calculi. Elsevier Science B. V. (North Holland), 1994."},{"key":"7_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Formal Development of Reactive Systems. Case Study Production Cell","author":"W. Damm","year":"1994","unstructured":"W. Damm, H. Hunger, P. Kelb, and R. Schl\u00f6r. Using Graphical Specification Languages and Symbolic Model Checking in the Verification of a Production Cell. In C. Lewerentz and T. Lindner, editors, Formal Development of Reactive Systems. Case Study Production Cell, LNCS 891. Springer Verlag, 1994."},{"key":"7_CR9","unstructured":"W. Damm, B. Josko, and Rainer Schl\u00f6r. Specification and Verification of VHDLbased System-level Hardware Designs. In Egon Borger, editor, Specificatio and Validation Methods. Oxford University Press, 1994."},{"key":"7_CR10","unstructured":"K. Feyerabend. Real-time Symbolic Timing Diagrams. Technical report, Department of Computer Science, Oldenburg University, September 1994."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"K. Feyerabend and B. Josko. A Visual Formalism for Real Time Requirement Specifications. In AMAST Workshop on Real-time systems and Concurrent and Distributed Software. Springer Verlag, 1997.","DOI":"10.1007\/3-540-63010-4_11"},{"key":"7_CR12","unstructured":"K. Feyerabend and R. Schl\u00f6r. Hardware synthesis from requirement specifications. In EURO-DAC'96 with EURO-VHDL'96. IEEE Computer Society Press, September 1996."},{"key":"7_CR13","unstructured":"K. Fisler. A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD thesis, Computer Science Department, Indiana University, August 1996."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"K. Fisler. Containment of Regular Languages in Non-Regular Timing Diagrams Languages is Decidable. In CAV. Springer Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_17"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"W. Grass, C. Grobe, S. Lenk, W. Tiedemann, C. D. Kloos, A. Marin, and T. Robles. Transformation of Timing Diagram Specifications into VHDL Code. In Conference on Hardware Description Languages, 1995.","DOI":"10.1109\/ASPDAC.1995.486384"},{"key":"7_CR16","unstructured":"J. Helbig, R. Schl\u00f6r, W. Damm, G. Doehmen, and P. Kelb. VHDL\/S-I ntegrating Statecharts, Timing diagrams, and VHDL. Microprocessing and Microprogramming, 1996."},{"key":"7_CR17","unstructured":"F. Jin and E. Cerny. Verification of Real-Time Controllers against Timing Diagram Specifications using Constraint Logic Programming. In IFIP EuroMICRO, 1998."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"K. Khordoc and E. Cerny. Semantics and Verification of Timing Diagrams with Linear Timing Constraints. ACM Transactions on Design Automation of Electronic Systems, 3(1), 1998.","DOI":"10.1145\/270580.270582"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer-aided verification of coordinating processes: the Automata-theoretic approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that Finite State Concurrent Programs satisfy their Linear Specifications. In POPL, 1985.","DOI":"10.1145\/318593.318622"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Specification and Verification of Concurrent Programs by \u2200-Automata. In POPL, 1987.","DOI":"10.1145\/41625.41626"},{"key":"7_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 5th International Symposium on Programming","author":"J. P. Queille","year":"1982","unstructured":"J. P. Queille and J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982."},{"key":"7_CR23","unstructured":"Y. S.. Ramakrishna, P. M. Melliar-Smith, L. E. Moser, L. K. Dillon, and G. Kutty. Really Visual Temporal Reasoning. In Real-Time Systems Symposium. IEEE Publishers, 1993."},{"key":"7_CR24","unstructured":"R. Schl\u00f6r. A Prover for VHDL-based Hardware Design. In Conference on Hardware Description Languages, 1995."},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"A. P. Sistla, M. Vardi, and P. Wolper. The Complementation Problem for B\u00fcchi Automata with Applications to Temporal Logic. TCS, 49, 1987.","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"E. M. Thurner. Proving System Properties by means of Trigger-Graph and Petri Nets. In EUROCAST. Springer Verlag, 1996.","DOI":"10.1007\/BFb0034752"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"W. D. Tiedemann. Bus Protocol Conversion: from Timing Diagrams to State Machines. In EUROCAST. Springer Verlag, 1992.","DOI":"10.1007\/BFb0021028"},{"key":"7_CR28","unstructured":"M. Vardi. Verification of Concurrent Programs. In POPL, 1987."},{"key":"7_CR29","unstructured":"M. Vardi and P. Wolper. An Automata-Theoretic approach to Automatic Program Verification. In LICS, 1986."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:01:02Z","timestamp":1558983662000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}