{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:22:04Z","timestamp":1762521724110,"version":"3.40.5"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319133379"},{"type":"electronic","value":"9783319133386"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-13338-6_19","type":"book-chapter","created":{"date-parts":[[2014,11,3]],"date-time":"2014-11-03T03:35:45Z","timestamp":1414985745000},"page":"252-266","source":"Crossref","is-referenced-by-count":10,"title":["Supervisory Control of Discrete-Event Systems via IC3"],"prefix":"10.1007","author":[{"given":"Mohammad Reza","family":"Shoaei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Lennartson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","first-page":"384","volume-title":"8th Int. Work. Discret. Event Syst.","author":"K. \u00c5kesson","year":"2006","unstructured":"\u00c5kesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica - An integrated environment for verification, synthesis and simulation of discrete event systems. In: 8th Int. Work. Discret. Event Syst., pp. 384\u2013385. Ann Arbor, MI (2006)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"19_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete Event Systems","author":"C.G. Cassandras","year":"2008","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer US, Boston (2008)","edition":"2"},{"key":"19_CR5","unstructured":"Chen, Y.L., Lin, F.: Modeling of discrete event systems using finite state machines with parameters. In: IEEE Int. Conf. Control Appl. Conf. Proc., pp. 941\u2013946 (2000)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 277\u2013293. Springer, Heidelberg (2012)"},{"issue":"4","key":"19_CR7","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10626-009-0081-8","volume":"19","author":"K. Claessen","year":"2009","unstructured":"Claessen, K., Een, N., Sheeran, M., S\u00f6rensson, N., Voronov, A., \u00c5kesson, K.: SAT-Solving in Practice, with a Tutorial Example from Supervisory Control. Discret. Event Dyn. Syst.\u00a019(4), 495\u2013524 (2009)","journal-title":"Discret. Event Dyn. Syst."},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"19_CR9","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Form. Methods Comput. Des., pp. 125\u2013134 (2011)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Fei, Z., Miremadi, S., \u00c5kesson, K., Lennartson, B.: A symbolic approach to large-scale discrete event systems modeled as finite automata with variables. In: 2012 IEEE Int. Conf. Autom. Sci. Eng., pp. 502\u2013507. IEEE (2012)","DOI":"10.1109\/CoASE.2012.6386479"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-642-31424-7_38","volume-title":"Computer Aided Verification","author":"Z. Hassan","year":"2012","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Incremental, Inductive CTL Model Checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 532\u2013547. Springer, Heidelberg (2012)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. ACM SIGPLAN Not., 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K. Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-14203-1_16","volume-title":"Automated Reasoning","author":"K. Hoder","year":"2010","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination in vampire. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 188\u2013195. Springer, Heidelberg (2010)"},{"key":"19_CR15","unstructured":"Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Series in Computer Science,Education. Pearson Education India (2007)"},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1109\/9.250512","volume":"38","author":"R. Kumar","year":"1993","unstructured":"Kumar, R., Garg, V., Marcus, S.: Predicates and predicate transformers for supervisory control of discrete event dynamical systems. IEEE Trans. Automat. Contr.\u00a038(2), 232\u2013247 (1993)","journal-title":"IEEE Trans. Automat. Contr."},{"issue":"9","key":"19_CR17","doi-asserted-by":"publisher","first-page":"1336","DOI":"10.1109\/TAC.2005.854612","volume":"50","author":"R. Leduc","year":"2005","unstructured":"Leduc, R., Lawford, M., Wonham, W.M.: Hierarchical interface-based supervisory control-part II: parallel case. IEEE Trans. Automat. Contr.\u00a050(9), 1336\u20131348 (2005)","journal-title":"IEEE Trans. Automat. Contr."},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Miremadi, S., \u00c5kesson, K., Fabian, M., Vahidi, A.: Solving two supervisory control benchmark problems using Supremica. In: 9th Int. Work. Discret. Event Syst., pp. 131\u2013136 (2008)","DOI":"10.1109\/WODES.2008.4605934"},{"issue":"6","key":"19_CR21","doi-asserted-by":"publisher","first-page":"1421","DOI":"10.1109\/TCST.2011.2167150","volume":"20","author":"S. Miremadi","year":"2012","unstructured":"Miremadi, S., Lennartson, B., \u00c5kesson, K.: A BDD-Based Approach for Modeling Plant and Supervisor by Extended Finite Automata. IEEE Trans. Control Syst. Technol.\u00a020(6), 1421\u20131435 (2012)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-38613-8_13","volume-title":"Integrated Formal Methods","author":"A. Morgenstern","year":"2013","unstructured":"Morgenstern, A., Gesell, M., Schneider, K.: Solving games using incremental induction. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 177\u2013191. Springer, Heidelberg (2013)"},{"issue":"3","key":"19_CR23","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1109\/TASE.2011.2124457","volume":"8","author":"L. Ouedraogo","year":"2011","unstructured":"Ouedraogo, L., Kumar, R., Malik, R., \u00c5kesson, K.: Nonblocking and Safe Control of Discrete-Event Systems Modeled as Extended Finite Automata. IEEE Trans. Autom. Sci. Eng.\u00a08(3), 560\u2013569 (2011)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"5","key":"19_CR24","doi-asserted-by":"publisher","first-page":"1202","DOI":"10.1137\/0325066","volume":"25","author":"P.J. Ramadge","year":"1987","unstructured":"Ramadge, P.J., Wonham, W.M.: Modular Feedback Logic for Discrete Event Systems. SIAM J. Control Optim.\u00a025(5), 1202\u20131218 (1987)","journal-title":"SIAM J. Control Optim."},{"issue":"1","key":"19_CR25","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1137\/0325013","volume":"25","author":"P.J. Ramadge","year":"1987","unstructured":"Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim.\u00a025(1), 635\u2013650 (1987)","journal-title":"SIAM J. Control Optim."},{"issue":"1","key":"19_CR26","first-page":"81","volume":"77","author":"P.J. Ramadge","year":"1989","unstructured":"Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proc. IEEE, Spec. Issue Discret. Event Dyn. Syst.\u00a077(1), 81\u201398 (1989)","journal-title":"Proc. IEEE, Spec. Issue Discret. Event Dyn. Syst."},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Skoldstam, M., \u00c5kesson, K., Fabian, M.: Modeling of discrete event systems using finite automata with variables. In: 46th IEEE Conf. Decis. Control, pp. 3387\u20133392 (2007)","DOI":"10.1109\/CDC.2007.4434894"},{"key":"19_CR29","unstructured":"Somenzi, F., Bradley, A.R.: IC3: where monolithic and incremental meet. In: Form. Methods Comput. Des., pp. 3\u20138 (2011)"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Yang, Y., Gohari, P.: Embedded supervisory control of discrete-event systems. In: Int. Conf. Autom. Sci. Eng., pp. 410\u2013415 (2005)","DOI":"10.1109\/COASE.2005.1506804"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-13338-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T04:21:30Z","timestamp":1746505290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-13338-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319133379","9783319133386"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-13338-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}