{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T13:27:42Z","timestamp":1749648462125},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s10009-021-00624-0","type":"journal-article","created":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T16:18:59Z","timestamp":1622564339000},"page":"601-614","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Comparing controlled system synthesis and suppression enforcement"],"prefix":"10.1007","volume":"23","author":[{"given":"Luca","family":"Aceto","sequence":"first","affiliation":[]},{"given":"Ian","family":"Cassar","sequence":"additional","affiliation":[]},{"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[]},{"given":"Anna","family":"Ing\u00f3lfsd\u00f3ttir","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,6,1]]},"reference":[{"key":"624_CR1","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(87)90065-X","volume":"53","author":"S Abramsky","year":"1987","unstructured":"Abramsky, S.: Observation equivalence as a testing equivalence. Theor. Comput. Sci. 53, 225\u2013241 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90065-X","journal-title":"Theor. Comput. Sci."},{"key":"624_CR2","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-49019-1_4","volume-title":"Foundations of Software Science and Computation Structures","author":"L Aceto","year":"1999","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: Testing Hennessy\u2013Milner Logic with Recursion. In: Thomas, W. (ed.) Foundations of Software Science and Computation Structures, pp. 41\u201355. Springer, Berlin (1999)"},{"key":"624_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems: Modelling, Specification and Verification","author":"L Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007)"},{"key":"624_CR4","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Kjartansson, S.\u00d6.: Determinizing monitors for HML with recursion. arXiv preprint (2016)"},{"key":"624_CR5","doi-asserted-by":"crossref","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: A framework for parameterized monitorability. In: Foundations of Software Science and Computation Structures, pp. 203\u2013220. Springer International Publishing, Cham (2018a)","DOI":"10.1007\/978-3-319-89366-2_11"},{"key":"624_CR6","doi-asserted-by":"publisher","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On runtime enforcement via suppressions. In: 29th International Conference on Concurrency Theory, CONCUR 2018, September 4\u20137, 2018, Beijing, China, pp. 34:1\u201334:17, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.34 (2018b)","DOI":"10.4230\/LIPIcs.CONCUR.2018.34"},{"key":"624_CR7","doi-asserted-by":"publisher","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc ACM Program Lang. 3(POPL):52:1\u201352:29, https:\/\/doi.org\/10.1145\/3290365 (2019a)","DOI":"10.1145\/3290365"},{"key":"624_CR8","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: Comparing controlled system synthesis and suppression enforcement. In: Runtime Verification, pp. 148\u2013164. Springer International Publishing, Cham (2019b)","DOI":"10.1007\/978-3-030-32079-9_9"},{"key":"624_CR9","doi-asserted-by":"crossref","unstructured":"Alur, R., \u010cern\u00fd, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, pp. 599\u2013610 (2011)","DOI":"10.1145\/1925844.1926454"},{"key":"624_CR10","unstructured":"Arnold, A., Walukiewicz, I.: Nondeterministic controllers of nondeterministic processes. In: Logic and Automata, Amsterdam University Press, Texts in Logic and Games, vol. 2, pp. 29\u201352 (2008)"},{"key":"624_CR11","doi-asserted-by":"crossref","unstructured":"Basile, D., ter\u00a0Beek, M.H., Pugliese, R.: Bridging the gap between supervisory control and coordination of services: synthesis of orchestrations and choreographies. In: COORDINATION 2019\u201421st International Conference on Coordination Models and Languages, (To appear) (2019)","DOI":"10.1007\/978-3-030-22397-7_8"},{"key":"624_CR12","doi-asserted-by":"crossref","unstructured":"Cassar, I., Francalanza, A., Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: A survey of runtime monitoring instrumentation techniques. In: PrePost2017, pp. 15\u201328 (2017)","DOI":"10.4204\/EPTCS.254.2"},{"key":"624_CR13","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press (1999)"},{"key":"624_CR14","doi-asserted-by":"crossref","unstructured":"Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Runtime Verfication (RV), pp. 172\u2013189. Springer International Publishing, Cham, LNCS (2017)","DOI":"10.1007\/978-3-319-67531-2_11"},{"key":"624_CR15","doi-asserted-by":"crossref","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 Proceedings Volumes, vol. 47(2), pp. 222 \u2013 227, 12th IFAC International Workshop on Discrete Event Systems (2014)","DOI":"10.3182\/20140514-3-FR-4046.00018"},{"key":"624_CR16","doi-asserted-by":"crossref","unstructured":"Erlingsson, U., Schneider, F.B.: Sasi enforcement of security policies: a retrospective. In: Proceedings of the 1999 Workshop on New Security Paradigms, ACM, New York, NY, USA, NSPW \u201999, pp. 87\u201395 (1999)","DOI":"10.1145\/335169.335201"},{"key":"624_CR17","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Marchand, H.: Runtime enforcement of k-step opacity. In: 52nd IEEE Conference on Decision and Control, pp. 7271\u20137278, https:\/\/doi.org\/10.1109\/CDC.2013.6761043(2013)","DOI":"10.1109\/CDC.2013.6761043"},{"issue":"3","key":"624_CR18","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone, Y., Fernandez, J.C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf. 14(3), 349 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"624_CR19","doi-asserted-by":"crossref","unstructured":"Francalanza, A.: A theory of monitors. In: International Conference on Foundations of Software Science and Computation Structures. Springer, pp. 145\u2013161 (2016)","DOI":"10.1007\/978-3-662-49630-5_9"},{"key":"624_CR20","unstructured":"Francalanza, A.: Consistently-detecting monitors. In: 28th International Conference on Concurrency Theory (CONCUR 2017), Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, Leibniz International Proceedings in Informatics (LIPIcs), vol. 85, pp. 8:1\u20138:19 (2017)"},{"key":"624_CR21","doi-asserted-by":"crossref","unstructured":"Francalanza, A., Aceto, L., Achilleos, A., Attard, D.P., Cassar, I., Della Monica, D., Ing\u00f3lfsd\u00f3ttir, A.: A foundation for runtime monitoring. In: Runtime Verification, pp. 8\u201329. Springer International Publishing, Cham (2017a)","DOI":"10.1007\/978-3-319-67531-2_2"},{"issue":"1","key":"624_CR22","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10703-017-0273-z","volume":"51","author":"A Francalanza","year":"2017","unstructured":"Francalanza, A., Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: Monitorability for the Hennessy\u2013Milner logic with recursion. Formal Methods Syst. Des. 51(1), 87\u2013116 (2017b)","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"624_CR23","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000). https:\/\/doi.org\/10.1007\/s100090050043","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"624_CR24","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/B:FORM.0000017721.39909.4b","volume":"24","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: An overview of the runtime verification tool java pathexplorer. Formal Methods Syst. Des. 24(2), 189\u2013215 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"624_CR25","doi-asserted-by":"crossref","unstructured":"Kejstov\u00e1, K., Ro\u010dkai, P., Barnat, J.: From model checking to runtime verification and back. In: RV, Springer (2017)","DOI":"10.1007\/978-3-319-67531-2_14"},{"issue":"2","key":"624_CR26","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10703-017-0276-9","volume":"51","author":"B K\u00f6nighofer","year":"2017","unstructured":"K\u00f6nighofer, B., Alshiekh, M., Bloem, R., Humphrey, L., K\u00f6nighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332\u2013361 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"624_CR27","doi-asserted-by":"crossref","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293\u2013303 (2009)","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"624_CR28","doi-asserted-by":"crossref","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1), 2\u201316 (2005)","DOI":"10.1007\/s10207-004-0046-8"},{"issue":"1","key":"624_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"624_CR30","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, New York, NY, USA, POPL \u201989, pp. 179\u2013190, https:\/\/doi.org\/10.1145\/75277.75293(1989)","DOI":"10.1145\/75277.75293"},{"issue":"1","key":"624_CR31","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"PJ Ramadge","year":"1987","unstructured":"Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206\u2013230 (1987)","journal-title":"SIAM J. Control Optim."},{"key":"624_CR32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195218","volume-title":"Elements of Automata Theory","author":"J Sakarovitch","year":"2009","unstructured":"Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, New York (2009)"},{"key":"624_CR33","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588","volume-title":"Introduction to Bisimulation and Coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)"},{"issue":"1","key":"624_CR34","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. (TISSEC) 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"issue":"1","key":"624_CR35","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10626-016-0231-8","volume":"27","author":"AC van Hulst","year":"2017","unstructured":"van Hulst, A.C., Reniers, M.A., Fokkink, W.J.: Maximally permissive controlled system synthesis for non-determinism and modal logic. Discrete Event Dyn. Syst. 27(1), 109\u2013142 (2017)","journal-title":"Discrete Event Dyn. Syst."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00624-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00624-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00624-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T14:08:50Z","timestamp":1634825330000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00624-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,1]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["624"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00624-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,1]]},"assertion":[{"value":"6 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}