{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:49:12Z","timestamp":1742914152615,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319899596"},{"type":"electronic","value":"9783319899602"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89960-2_19","type":"book-chapter","created":{"date-parts":[[2018,4,11]],"date-time":"2018-04-11T14:14:43Z","timestamp":1523456083000},"page":"344-361","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["From Natural Projection to Partial Model Checking and Back"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9385-3998","authenticated-orcid":false,"given":"Gabriele","family":"Costa","sequence":"first","affiliation":[]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[]},{"given":"Chiara","family":"Bodei","sequence":"additional","affiliation":[]},{"given":"Pierpaolo","family":"Degano","sequence":"additional","affiliation":[]},{"given":"Letterio","family":"Galletta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,12]]},"reference":[{"key":"19_CR1","unstructured":"Andersen, H.R.: Partial model checking (extended abstract). In: Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 398\u2013407. IEEE Computer Society Press (1995)"},{"key":"19_CR2","unstructured":"Andersen, H.R., Lind-Nielsen, J.: MuDiv: a tool for partial model checking. Demo Presentation at CONCUR (1996)"},{"issue":"3","key":"19_CR3","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/s100090050032","volume":"2","author":"HR Andersen","year":"1999","unstructured":"Andersen, H.R., Lind-Nielsen, J.: Partial model checking of modal equations: a survey. Int. J. Softw. Tools Technol. Transf. 2(3), 242\u2013259 (1999)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"303","key":"19_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/S0304-3975(02)00442-5","volume":"1","author":"A Arnold","year":"2003","unstructured":"Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. Theor. Comput. Sci. 1(303), 7\u201334 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1017\/S0960129514000309","volume":"26","author":"JCM Baeten","year":"2016","unstructured":"Baeten, J.C.M., Luttik, B., Muller, T., Van Tilburg, P.: Expressiveness modulo bisimilarity of regular expressions with parallel composition. Mathe. Struct. Comput. Sci. 26, 933\u2013968 (2016)","journal-title":"Mathe. Struct. Comput. Sci."},{"key":"19_CR6","unstructured":"Basu, S., Kumar, R.: Quotient-based approach to control of nondeterministic discrete-event systems with $$\\mu $$ \u03bc -calculus specification (2006). http:\/\/home.eng.iastate.edu\/~rkumar\/PUBS\/acc06-muctrl.pdf"},{"key":"19_CR7","unstructured":"Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Foundations of Computer Security, Copenhagen, Denmark, July 2002"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/S1570-2464(07)80015-2","volume-title":"Handbook of Modal Logic","author":"Julian Bradfield","year":"2007","unstructured":"Bradfield, J., Stirling, C.: Modal Mu-calculi. In: Handbook of Modal Logic, vol. 3. Elsevier Science (2006)"},{"key":"19_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4070-7","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"1999","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer, Boston (1999)"},{"key":"19_CR10","unstructured":"Open Fog Consortium: Out of the Fog: Use Case Scenarios. Supply Chain, High-Scale Drone Package Delivery, July 2016. https:\/\/www.openfogconsortium.org\/wp-content\/uploads\/OpenFog-Transportation-Drone-Delivery-Use-Case.pdf . Accessed Jan 2017"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Costa, G., Basin, D., Bodei, C., Degano, P., Galletta, L.: Pests: Partial evaluator of simple transition systems. GitHub, February 2018. https:\/\/github.com\/SCPTeam\/pests , https:\/\/doi.org\/10.6084\/m9.figshare.5918707.v1","DOI":"10.6084\/m9.figshare.5918707.v1"},{"issue":"2","key":"19_CR12","doi-asserted-by":"publisher","first-page":"222","DOI":"10.3182\/20140514-3-FR-4046.00018","volume":"47","author":"R Ehlers","year":"2014","unstructured":"Ehlers, R., Lafortune, S., Tripakis, S., Vardi, M.: Bridging the gap between supervisory control and reactive synthesis: case of full observation and centralized control. IFAC Proc. Volumes 47(2), 222\u2013227 (2014)","journal-title":"IFAC Proc. Volumes"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Feng, L., Wonham, W.M.: TCT: a computation tool for supervisory control synthesis. In: Proceedings of 2006 8th International Workshop on Discrete Event Systems, pp. 388\u2013389 (2006)","DOI":"10.1109\/WODES.2006.382399"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10626-008-0054-3","volume":"20","author":"L Feng","year":"2010","unstructured":"Feng, L., Wonham, W.M.: On the computation of natural observers in discrete-event systems. Discret. Event Dyn. Syst. 20(1), 63\u2013102 (2010)","journal-title":"Discret. Event Dyn. Syst."},{"issue":"2","key":"19_CR15","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s10626-006-0008-6","volume":"17","author":"G Feuillade","year":"2007","unstructured":"Feuillade, G., Pinchinat, S.: Modal specifications for the control theory of discrete event systems. Discret. Event Dyn. Syst. 17(2), 211\u2013232 (2007)","journal-title":"Discret. Event Dyn. Syst."},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/3-540-45789-5_32","volume-title":"Static Analysis","author":"R Giacobazzi","year":"2002","unstructured":"Giacobazzi, R., Ranzato, F.: States vs. traces in model checking by abstract interpretation. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 461\u2013476. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45789-5_32"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Gromyko, A., Pistore, M., Traverso, P.: A tool for controller synthesis via symbolic model checking. In: 8th International Workshop on Discrete Event Systems, pp. 475\u2013476, July 2006","DOI":"10.1109\/WODES.2006.382523"},{"key":"19_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. The MIT Press, Cambridge (2014)"},{"key":"19_CR19","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"2006","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley Longman Publishing Co., Inc., Boston (2006)","edition":"3"},{"issue":"6","key":"19_CR20","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 $$^*$$ \u2217 temporal logic specifications. SIAM J. Control Optim. 44(6), 2079\u20132103 (2006)","journal-title":"SIAM J. Control Optim."},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.tcs.2012.04.009","volume":"449","author":"G Jir\u00e1skov\u00e1","year":"2012","unstructured":"Jir\u00e1skov\u00e1, G., Masopust, T.: On a structural property in the state complexity of projected regular languages. Theoret. Comput. Sci. 449, 93\u2013105 (2012)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-28756-5_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Lang","year":"2012","unstructured":"Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and boolean equation systems. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 141\u2013156. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_11"},{"issue":"3","key":"19_CR24","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0020-0255(88)90002-3","volume":"44","author":"F Lin","year":"1988","unstructured":"Lin, F., Wonham, W.M.: Decentralized supervisory control of discrete-event systems. Inf. Sci. 44(3), 199\u2013224 (1988)","journal-title":"Inf. Sci."},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Martinelli, F., Matteucci, I.: Synthesis of local controller programs for enforcing global security properties. In: 3rd International Conference on Availability, Reliability and Security (ARES), pp. 1120\u20131127, March 2008","DOI":"10.1109\/ARES.2008.196"},{"issue":"8","key":"19_CR26","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1002\/stvr.441","volume":"22","author":"F Martinelli","year":"2012","unstructured":"Martinelli, F., Matteucci, I.: A framework for automatic generation of security controller. Softw. Test. Verif. Reliab. 22(8), 563\u2013582 (2012)","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"1","key":"19_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/357195.357196","volume":"5","author":"P Merlin","year":"1983","unstructured":"Merlin, P., Bochmann, G.V.: On the construction of submodule specifications and communication protocols. ACM Trans. Program. Lang. Syst. (TOPLAS) 5(1), 1\u201325 (1983)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Moor, T., Schmidt, K., Perk, S.: libFAUDES \u2013 an open source C++ library for discrete event systems. In: 9th International Workshop on Discrete Event Systems, pp. 125\u2013130, May 2008","DOI":"10.1109\/WODES.2008.4605933"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1007\/978-3-540-45138-9_58","volume-title":"Mathematical Foundations of Computer Science 2003","author":"S Riedweg","year":"2003","unstructured":"Riedweg, S., Pinchinat, S.: Quantified Mu-calculus for control synthesis. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 642\u2013651. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45138-9_58"},{"key":"19_CR30","unstructured":"Rudie, K., Grigorov, L.: Integrated Discrete-Event Systems (IDES), Department of Electrical and Computer Engineering, Queen\u2019s University in Kingston, ON, Canada. https:\/\/qshare.queensu.ca\/Users01\/rudie\/www\/software.html . Accessed Feb 2017"},{"issue":"12","key":"19_CR31","doi-asserted-by":"publisher","first-page":"1923","DOI":"10.1109\/TAC.2005.860291","volume":"50","author":"R Su","year":"2005","unstructured":"Su, R., Wonham, W.M.: Global and local consistencies in distributed fault diagnosis for discrete-event systems. IEEE Trans. Autom. Control 50(12), 1923\u20131935 (2005)","journal-title":"IEEE Trans. Autom. Control"},{"key":"19_CR32","unstructured":"Wong, K.C.: On the complexity of projections of discrete-event systems. In: Proceedings of IEEE Workshop on Discrete Event Systems, pp. 201\u2013208 (1998)"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Wonham, W.M.: Supervisory control of discrete-event systems, Department of Electrical and Computer Engineering. University of Toronto, ON, Canada. http:\/\/www.control.toronto.edu\/DES . Accessed Feb 2017","DOI":"10.1007\/978-3-319-77452-7_9"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Wonham, W.M., Ramadge, P.J.: On the supremal controllable sublanguage of a given language. In: Proceedings of the 23rd IEEE Conference on Decision and Control, pp. 1073\u20131080, December 1984","DOI":"10.1109\/CDC.1984.272178"},{"issue":"1","key":"19_CR35","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/BF02551233","volume":"1","author":"WM Wonham","year":"1988","unstructured":"Wonham, W.M., Ramadge, P.J.: Modular supervisory control of discrete-event systems. Math. Control Signals Syst. 1(1), 13\u201330 (1988)","journal-title":"Math. Control Signals Syst."},{"issue":"2","key":"19_CR36","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 Trans. Embed. Comput. Syst. 4(2), 331\u2013362 (2005)","journal-title":"ACM Trans. Embed. Comput. Syst."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89960-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,5]],"date-time":"2024-07-05T22:33:02Z","timestamp":1720218782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89960-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899596","9783319899602"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89960-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"12 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}