{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:10:20Z","timestamp":1725466220873},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054268","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"302-316","source":"Crossref","is-referenced-by-count":0,"title":["Automated deduction of finite-state control programs for reactive systems"],"prefix":"10.1007","author":[{"given":"Robi","family":"Malik","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"issue":"2","key":"29_CR1","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L.: Symbolic model checking: 1020 states and beyond. Information and Computing 98 (2), 142\u2013170, 1992.","journal-title":"Information and Computing"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Burch, J. R., Clarke, E. M., Long, D. E., McMillan, K. E., Dill, D. L.: Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and systems 13 (4), 1994.","DOI":"10.1109\/43.275352"},{"issue":"9","key":"29_CR3","doi-asserted-by":"publisher","first-page":"1270","DOI":"10.1109\/5.97297","volume":"79","author":"A. Benveniste","year":"1991","unstructured":"Benveniste, A., Berry, G.: The synchronous approach to reactive and real-time systems. Proc. IEEE 79 (9), 1270\u20131282, 1991.","journal-title":"Proc. IEEE"},{"issue":"7","key":"29_CR4","doi-asserted-by":"publisher","first-page":"1040","DOI":"10.1109\/9.231459","volume":"38","author":"S. Balemi","year":"1993","unstructured":"Balemi, S., Hoffmann, G. J., Gyugyi, P., Wong-Toi, H., Franklin, G. F.: Supervisory control of a rapid thermal multiprocessor. IEEE Transactions on Automatic Control 38 (7), 1040\u20131059, 1993.","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"8","key":"29_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp. 35 (8), 677\u2013691, 1986.","journal-title":"IEEE Trans. Comp."},{"issue":"2","key":"29_CR6","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 8 (2), 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR7","unstructured":"Dutertre, B., Le Borgne, M.: Control of polynomial dynamical systems: an example. Tech. Report 2193, INRIA, 1994."},{"key":"29_CR8","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson","year":"1982","unstructured":"Emerson, E. A., Clarke, E. M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241\u2013266, 1982.","journal-title":"Science of Computer Programming"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Fisher, M.: A normal form for first-order temporal formulae. Proc. 9th International Conference in Automated Deduction, CADE-9, 371\u2013384, Springer, 1992.","DOI":"10.1007\/3-540-55602-8_178"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Fisher, M., Owens, R.: An introduction to executable modal and temporal logics. Proc. IJCAI Workshop on Executable Modal and Temporal Logics, 1\u201320, Springer, 1993.","DOI":"10.1007\/3-540-58976-7_1"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer, 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and Models of Concurrent Systems, ed. K. R. Apt, NATO ASI Series, vol. 13, 477\u2013498, Springer, 1985.","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Lloyd, J. W.: Foundations of Logic Programming. Springer, 1984.","DOI":"10.1007\/978-3-642-96826-6"},{"key":"29_CR14","unstructured":"Malik, R., Mayer, O.: Eine Fixpunkt-Semantik f\u00fcr temporal stratifizierte Programme. Interner Bericht, FB Informatik, Universit\u00c4t Kaiserslautern, 1994."},{"key":"29_CR15","series-title":"Dissertation, FB Informatik, Universit\u00c4t Kaiserslautern, 1997","volume-title":"Automatische Synthese diskreter Steuerungen aus logischen Spezifikationen","author":"R. Malik","year":"1998","unstructured":"Malik, R.: Automatische Synthese diskreter Steuerungen aus logischen Spezifikationen. Shaker Verlag, Aachen, 1998; also available as: Dissertation, FB Informatik, Universit\u00c4t Kaiserslautern, 1997."},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems \u2014 Specification. Springer 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems \u2014 Safety. Springer, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. Proc. Logics of Programs, 253\u2013281, 1981.","DOI":"10.1007\/BFb0025786"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K. L.: Symbolic Model Checking. Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"29_CR20","series-title":"Advanced Software Development Series","volume-title":"Temporal logic for real-time systems","author":"J. Ostroff","year":"1989","unstructured":"Ostroff, J.: Temporal logic for real-time systems. Research Studies Press Ltd., Advanced Software Development Series, Taunton, Somerset, 1989."},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. Proc. 16th ACM Symp. on Principles of Programming Languages POPL '89, 1989.","DOI":"10.1145\/75277.75293"},{"issue":"1","key":"29_CR22","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"P. J. G. Ramadge","year":"1989","unstructured":"Ramadge, P. J. G., Wonham, W. M.: The control of discrete event systems. Proc. IEEE 77 (1), 81\u201398, 1989.","journal-title":"Proc. IEEE"},{"issue":"5","key":"29_CR23","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1145\/123041.123062","volume":"16","author":"C. Ratel","year":"1991","unstructured":"Ratel, C., Halbwachs, N., Raymond, P.: Programming and verifying critical systems by means of the synchronous data-flow language Lustre. Software Engineering Notes 16 (5), 112\u2013119, 1991.","journal-title":"Software Engineering Notes"},{"key":"29_CR24","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285\u2013309, 1955.","journal-title":"Pacific J. Math."},{"issue":"3","key":"29_CR25","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1137\/0325036","volume":"25","author":"W. M. Wonham","year":"1987","unstructured":"Wonham, W. M., Ramadge, P. J.: On the supremal controllable sublanguage of a given language. SIAM J. Control and Optimization 25 (3), 637\u2013650, 1987.","journal-title":"SIAM J. Control and Optimization"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T06:45:36Z","timestamp":1555656336000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054268"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0054268","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}