{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:25:25Z","timestamp":1745987125280,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642371684"},{"type":"electronic","value":"9783642371691"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37169-1_29","type":"book-chapter","created":{"date-parts":[[2013,3,26]],"date-time":"2013-03-26T14:03:46Z","timestamp":1364306626000},"page":"295-304","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Liveness in Supervised Systems Using UPPAAL and mCRL2"],"prefix":"10.1007","author":[{"given":"Jasen","family":"Markovski","sequence":"first","affiliation":[]},{"given":"M. A.","family":"Reniers","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Akesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica - an integrated environment for verification, synthesis and simulation of discrete event systems. In: Proceedings of WODES 2006, pp. 384\u2013385. IEEE (2006)","DOI":"10.1109\/WODES.2006.382401"},{"key":"29_CR2","unstructured":"Baeten, J.C.M., van de Mortel-Fronczak, J.M., Rooda, J.E.: Integration of Supervisory Control Synthesis in Model-Based Systems Engineering. In: Proceedings of ETAI\/COSY 2011, pp. 167\u2013178. IEEE (2011)"},{"issue":"3","key":"29_CR3","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1109\/TCST.2004.824795","volume":"12","author":"B.A. Brandin","year":"2004","unstructured":"Brandin, B.A., Malik, R., Malik, P.: Incremental verification and synthesis of discrete-event systems guided by counter examples. IEEE Transactions on Control Systems Technology\u00a012(3), 387\u2013401 (2004)","journal-title":"IEEE Transactions on Control Systems Technology"},{"key":"29_CR4","unstructured":"Cassandras, C., Lafortune, S.: Introduction to discrete event systems. Kluwer Academic Publishers (2004)"},{"issue":"2","key":"29_CR5","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 System\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and System"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N.R., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of live behaviour models. In: Proceedings of SIGSOFT 2010, pp. 77\u201386. ACM (2010)","DOI":"10.1145\/1882291.1882305"},{"key":"29_CR7","unstructured":"Groote, J.F., Mathijssen, A.H.J., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.J.: Analysis of distributed systems with mCRL2. In: Process Algebra for Parallel and Distributed Processing, pp. 99\u2013128. Chapman & Hall (2009)"},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Reniers, M.A.: Algebraic process verification. In: Handbook of Process Algebra, ch.\u00a017, pp. 1151\u20131208. Elsevier (2001)","DOI":"10.1016\/B978-044482830-9\/50035-7"},{"issue":"6","key":"29_CR9","doi-asserted-by":"publisher","first-page":"2079","DOI":"10.1137\/S0363012902409982","volume":"44","author":"S. Jiang","year":"2006","unstructured":"Jiang, S., Kumar, R.: Supervisory control of discrete event systems with CTL* temporal logic specifications. SIAM Journal on Control and Optimization\u00a044(6), 2079\u20132103 (2006)","journal-title":"SIAM Journal on Control and Optimization"},{"issue":"1-2","key":"29_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"6","key":"29_CR11","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/52.60589","volume":"7","author":"N. Leveson","year":"1990","unstructured":"Leveson, N.: The challenge of building process-control software. IEEE Software\u00a07(6), 55\u201362 (1990)","journal-title":"IEEE Software"},{"key":"29_CR12","unstructured":"Markovski, J.: Supremica2{UPPAAL, mCRL2} and demo models (2012), http:\/\/sites.google.com\/site\/jasenmarkovski"},{"key":"29_CR13","unstructured":"Markovski, J., Jacobs, K.G.M., van Beek, D.A., Somers, L.J.A.M., Rooda, J.E.: Coordination of resources using generalized state-based requirements. In: Proceedings of WODES 2010, pp. 300\u2013305. IFAC (2010)"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Markovski, J., Reniers, M.A.: An integrated state- and event-based framework for verifying liveness in supervised systems. In: Proceedings of ICARCV 2012. IEEE (2012) (to appear)","DOI":"10.1109\/ICARCV.2012.6485166"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2006)"},{"issue":"1","key":"29_CR16","doi-asserted-by":"publisher","first-page":"206","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 Journal on Control and Optimization\u00a025(1), 206\u2013230 (1987)","journal-title":"SIAM Journal on Control and Optimization"},{"issue":"3","key":"29_CR17","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1109\/TASE.2006.881904","volume":"4","author":"K.T. Seow","year":"2007","unstructured":"Seow, K.T.: Integrating temporal logic as a state-based specification language for discrete-event control design in finite automata. IEEE Transactions on Automation Science and Engineering\u00a04(3), 451\u2013464 (2007)","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Song, R., Leduc, R.: Symbolic synthesis and verification of hierarchical interface-based supervisory control. In: Proceedings of WODES 2006, pp. 419\u2013426. IEEE (2006)","DOI":"10.1109\/WODES.2006.382510"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Voronov, A., Akesson, K.: Verification of process operations using model checking. In: Proceedings of CASE 2009, pp. 415\u2013420. IEEE (2009)","DOI":"10.1109\/COASE.2009.5234103"},{"issue":"2","key":"29_CR20","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1145\/1067915.1067920","volume":"4","author":"R. Ziller","year":"2005","unstructured":"Ziller, R., Schneider, K.: Combining supervisor synthesis and model checking. ACM Transactions on Embedded Computing Systems\u00a04(2), 331\u2013362 (2005)","journal-title":"ACM Transactions on Embedded Computing Systems"}],"container-title":["Advances in Intelligent Systems and Computing","ICT Innovations 2012"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37169-1_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T02:06:52Z","timestamp":1745978812000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-37169-1_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642371684","9783642371691"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37169-1_29","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2013]]}}}