{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:05:06Z","timestamp":1725573906093},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540216711"},{"type":"electronic","value":"9783540409038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-40903-8_16","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T10:37:38Z","timestamp":1294396658000},"page":"189-203","source":"Crossref","is-referenced-by-count":4,"title":["Control Synthesis for a\u00a0Smart Card Personalization System Using Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Biniam","family":"Gebremichael","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","first-page":"1272","volume-title":"International Conf. on Control Applications","author":"K. \u00c5kesson","year":"1999","unstructured":"\u00c5kesson, K., Fabian, M.: Implementing supervisory control for chemical batch processes. In: International Conf. on Control Applications, pp. 1272\u20131277. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"16_CR2","unstructured":"Albert, S.: Cybernetix case study \u2013 informal description. Technical report, Cybern\u00e9tix - LIF (2002), Available through http:\/\/ametist.cs.utwente.nl"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/70.481746","volume":"12","author":"B.A. Brandin","year":"1996","unstructured":"Brandin, B.A.: The real-time supervisory control of an experimental manufacturing cell. IEEE Transactions on Robotics and Automation\u00a012, 1\u201313 (1996)","journal-title":"IEEE Transactions on Robotics and Automation"},{"issue":"2","key":"16_CR4","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., Dill, D.L., Hwang, L.J.: Symbolic model checking 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"16_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4070-7","volume-title":"Introduction to Discrete Event Systems","author":"C.G. Cassandras","year":"1999","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"E.W. Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Communications ACM\u00a017, 643\u2013644 (1974)","journal-title":"Communications ACM"},{"key":"16_CR7","first-page":"280","volume-title":"Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA 1999)","author":"A. Fehnker","year":"1999","unstructured":"Fehnker, A.: Scheduling a steel plant with timed automata. In: Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA 1999), Hong Kong, China, pp. 280\u2013287. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Gebremichael, B., Vaandrager, F.: Control synthesis for a smart card personalization system using symbolic model checking. Technical Report NIIIR0312, Nijmegen Institute for Computing and Information Sciences, University of Nijmegen (2003)","DOI":"10.1007\/978-3-540-40903-8_16"},{"key":"16_CR9","unstructured":"Gunnarsson, J.: Symbolic Methods and Tools for Discrete Event Dynamic Systems. PhD thesis, Link\u00f6ping Studies in Science and Technology (1997)"},{"issue":"1","key":"16_CR10","first-page":"43","volume":"8","author":"T. Hune","year":"2001","unstructured":"Hune, T., Larsen, K.G., Pettersson, P.: Guided Synthesis of Control Programs using Uppaal. Nordic Journal of Computing\u00a08(1), 43\u201364 (2001)","journal-title":"Nordic Journal of Computing"},{"key":"16_CR11","unstructured":"Krilavicius, T., Usenko, Y.: Smart card personalisation machine in UPPAAL and \u03bcCRL (2003) (in preparation)"},{"key":"16_CR12","first-page":"1214","volume-title":"IEEE Trans. on Automatic Control","author":"Y. Li","year":"1993","unstructured":"Li, Y., Wonham, W.M.: Control of vector discrete-event systems I - the base model. In: IEEE Trans. on Automatic Control, vol.\u00a038, pp. 1214\u20131227. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"16_CR13","unstructured":"Mader, A.: Deriving schedules for the cybernetix case study (2003), Available through http:\/\/ametist.cs.utwente.nl"},{"key":"16_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-46430-1_29","volume-title":"Hybrid Systems: Computation and Control","author":"P. Niebert","year":"2000","unstructured":"Niebert, P., Yovine, S.: Computing optimal operation schemes fo multi batch operation of chemical plants. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 338\u2013351. Springer, Heidelberg (2000)"},{"key":"16_CR16","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. Proceedings of the IEEE\u00a077, 81\u201398 (1989)","journal-title":"Proceedings of the IEEE"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44829-2_1","volume-title":"Model Checking Software","author":"T. Ruys","year":"2003","unstructured":"Ruys, T.: Optimal Scheduling Using Branch and Bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 1\u201317. Springer, Heidelberg (2003)"},{"issue":"9","key":"16_CR18","doi-asserted-by":"publisher","first-page":"1555","DOI":"10.1109\/9.412626","volume":"40","author":"M. Sampath","year":"1995","unstructured":"Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete event systems. IEEE Transactions on Automatic Control\u00a040(9), 1555\u20131575 (1995)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Sreenivas, R.S., Krogh, B.H.: On condition\/event systems with discrete state realizations. In: Discrete Event Dynamic Systems. Theory and Applications 1, pp. 209\u2013236. Flumer Academic (1991)","DOI":"10.1007\/BF01805563"},{"key":"16_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020419","volume-title":"Introduction to Distributed Algorithms","author":"G. Tel","year":"1994","unstructured":"Tel, G.: Introduction to Distributed Algorithms. Cambridge University Press, Cambridge (1994)"},{"key":"16_CR21","unstructured":"Weiss, G.: Modeling smart-card personalization machine with LSCs. Research report, Weizmann (2003)"},{"key":"16_CR22","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1109\/9.280750","volume":"39","author":"W.M. Wonham","year":"1994","unstructured":"Wonham, W.M., Li, Y.: Control of vector discrete-event systems II \u2013 controller synthesis. IEEE Transactions on Autom. Control\u00a039, 512\u2013531 (1994)","journal-title":"IEEE Transactions on Autom. Control"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, Z., Wonham, W.M.: STCT: An efficient algorithm for supervisory control design. In: Symposium on Supervisory Control of Discrete Event Systems (2001)","DOI":"10.1007\/978-1-4757-6656-1_5"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40903-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T13:43:44Z","timestamp":1559915024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40903-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540216711","9783540409038"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40903-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}