{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:38:16Z","timestamp":1762522696206,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T00:00:00Z","timestamp":1645574400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T00:00:00Z","timestamp":1645574400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100011688","name":"Electronic Components and Systems for European Leadership","doi-asserted-by":"publisher","award":["826452"],"award-info":[{"award-number":["826452"]}],"id":[{"id":"10.13039\/501100011688","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2022,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Supervisory controller synthesis is a means to compute correct-by-construction controllers for discrete event systems. As these systems and their requirements evolve over time, an updated supervisor needs to be computed each time an adaptation takes place. We consider the case that a supervisor has been synthesized for a given model, after which this model is (slightly) adapted. We investigate how we can make use of the previous synthesis result, in order to more efficiently compute the supervisor for the adapted model. We introduce model deltas as a means to describe the difference between pairs of models. Using the model deltas, a notion of atomic adaptations is introduced. For these atomic adaptations, algorithms are provided to compute the supervisor for the adapted model in a transformational manner from the previous synthesis result, rather than performing a completely new synthesis. These atomic adaptations can be iterated over, to transformationally compute a supervisor for model deltas that contain a number of atomic adaptations. To improve efficiency, it is shown how atomic adaptations can be grouped together based on their required computations and be processed at the same time. A running example is used to support the explanations on the functioning of the algorithms. The efficiency of the method is evaluated by means of both an academic and an industrial use case.<\/jats:p>","DOI":"10.1007\/s10626-021-00354-0","type":"journal-article","created":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T14:05:23Z","timestamp":1645625123000},"page":"317-358","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Transformational supervisor synthesis for evolving systems"],"prefix":"10.1007","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1628-8622","authenticated-orcid":false,"given":"Sander","family":"Thuijsman","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9283-4074","authenticated-orcid":false,"given":"Michel","family":"Reniers","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,2,23]]},"reference":[{"key":"354_CR1","unstructured":"Broadfoot GH, Hopcroft PJ (2003) Analytical software design. Technical report, Verum Consultants B.V."},{"key":"354_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras CG, Lafortune S (2008) Introduction to Discrete Event Systems, 2nd edn. Springer, Boston","edition":"2nd edn."},{"key":"354_CR3","doi-asserted-by":"crossref","unstructured":"Classen A, Heymans P, Schobbens PY, Legay A, Raskin JF (2010) Model checking lots of systems: Efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering, p 335\u2013344","DOI":"10.1145\/1806799.1806850"},{"issue":"6","key":"354_CR4","doi-asserted-by":"publisher","first-page":"2368","DOI":"10.1109\/TCST.2014.2303134","volume":"22","author":"Z Fei","year":"2014","unstructured":"Fei Z, Miremadi S, A\u0307kesson K, Lennartson B (2014) Efficient symbolic supervisor synthesis for extended finite automata. IEEE Trans Control Syst Technol 22(6):2368\u20132375","journal-title":"IEEE Trans Control Syst Technol"},{"issue":"4","key":"354_CR5","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10626-007-0018-z","volume":"17","author":"H Flordal","year":"2007","unstructured":"Flordal H, Malik R, Fabian M, \u00c5kesson K (2007) Compositional synthesis of maximally permissive supervisors using supervision equivalence. Discret Event Dyn Syst 17(4):475\u2013504","journal-title":"Discret Event Dyn Syst"},{"key":"354_CR6","doi-asserted-by":"crossref","unstructured":"Khan YI (2013) Optimizing verification of structurally evolving algebraic Petri nets. In: Proceedings of the 5th International Workshop Software Engineering for Resilient Systems, Lecture Notes in Computer Science, vol 8166, pp 64\u201378","DOI":"10.1007\/978-3-642-40894-6_6"},{"key":"354_CR7","volume-title":"Algorithm Design Addison-Wesley Longman Publishing Co.","author":"J Kleinberg","year":"2005","unstructured":"Kleinberg J, Tardos E (2005) Algorithm Design Addison-Wesley Longman Publishing Co. Inc., Boston"},{"key":"354_CR8","doi-asserted-by":"crossref","unstructured":"Krook J, Kianfar R, Fabian M (2020) Formal synthesis of safe stop tactical planners for an automated vehicle. In: Proceedings of the 15th IFAC Workshop on Discrete Event Systems, IFAC-PapersOnLine, vol 53, pp 445\u2013452","DOI":"10.1016\/j.ifacol.2021.04.059"},{"issue":"6","key":"354_CR9","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1109\/MC.2003.1204375","volume":"36","author":"C Larman","year":"2003","unstructured":"Larman C, Basili VR (2003) Iterative and incremental development: a brief history. Computer 36(6):47\u201356","journal-title":"Computer"},{"key":"354_CR10","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/BFb0017737","volume":"1149","author":"MM Lehman","year":"1996","unstructured":"Lehman MM (1996) Laws of software evolution revisited. Softw Process Technol Lect Notes Comput Sci 1149:108\u2013124","journal-title":"Softw Process Technol Lect Notes Comput Sci"},{"key":"354_CR11","doi-asserted-by":"crossref","unstructured":"Markovski J, van Beek D, Theunissen R, Jacobs K, Rooda J (2010) A state-based framework for supervisory control synthesis and verification. In: Proceedings of the 49th IEEE Conference on Decision and Control, pp 3481\u20133486","DOI":"10.1109\/CDC.2010.5717095"},{"issue":"3","key":"354_CR12","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, A\u0307kesson K (2011) Nonblocking and safe control of discrete-event systems modeled as extended finite automata. IEEE Trans Autom Sci Eng 8(3):560\u2013569","journal-title":"IEEE Trans Autom Sci Eng"},{"key":"354_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering: Foundations Principles and Techniques","author":"K Pohl","year":"2005","unstructured":"Pohl K, B\u00f6ckle G, van der Linden FJ (2005) Software Product Line Engineering: Foundations Principles and Techniques. Springer-Verlag, Berlin"},{"issue":"1","key":"354_CR14","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"PJ Ramadge","year":"1987","unstructured":"Ramadge PJ, Wonham WM (1987) Supervisory control of a class of discrete event processes. SIAM J Control Optim 25(1):206\u2013230","journal-title":"SIAM J Control Optim"},{"issue":"1","key":"354_CR15","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJ Ramadge","year":"1989","unstructured":"Ramadge PJ, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398","journal-title":"Proc IEEE"},{"key":"354_CR16","doi-asserted-by":"crossref","unstructured":"Rawlings BC, Christenson B, Wassick JM, Ydstie BE (2014) Supervisor synthesis to satisfy safety and reachability requirements in chemical process control. In: Proceedings of the 12th IFAC Workshop on Discrete Event Systems, IFAC Proceedings Volumes, vol 47, pp 195\u2013200","DOI":"10.3182\/20140514-3-FR-4046.00127"},{"key":"354_CR17","doi-asserted-by":"crossref","unstructured":"Reijnen FFH, Goorden MA, van de Mortel-Fronczak JM, Rooda JE (2020) Modeling for supervisor synthesis \u2013 a lock-bridge combination case study. Discret Event Dyna Syst 30(3):499\u2013532","DOI":"10.1007\/s10626-020-00314-0"},{"key":"354_CR18","doi-asserted-by":"crossref","unstructured":"Reniers MA, Thuijsman SB (2020) Supervisory control for dynamic feature configuration in product lines. In: Proceedings of the IEEE Forum on Specification and Design Languages, pp 1\u20138","DOI":"10.1109\/FDL50818.2020.9232937"},{"key":"354_CR19","doi-asserted-by":"crossref","unstructured":"Rosa M, Cury JER, Baldissera FL (2020) Supervisory control in construction robotics: in the quest for scalability and permissiveness. In: Proceedings of the 15th IFAC Workshop on Discrete Event Systems, IFAC-PapersOnLine, vol 53, pp 117\u2013122","DOI":"10.1016\/j.ifacol.2021.04.012"},{"issue":"5","key":"354_CR20","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/s10009-012-0253-y","volume":"14","author":"I Schaefer","year":"2012","unstructured":"Schaefer I, Rabiser R, Clarke D, Bettini L, Benavides D, Botterweck G, Pathak A, Trujillo S, Villela K (2012) Software diversity: state of the art and perspectives. Int J Softw Tools Technol Transfer 14(5):477\u2013495","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"1","key":"354_CR21","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/TASE.2013.2279692","volume":"11","author":"RJM Theunissen","year":"2014","unstructured":"Theunissen RJM, Petreczky M, Schiffelers RRH, van Beek DA, Rooda JE (2014) Application of supervisory control synthesis to a patient support table of a magnetic resonance imaging scanner. IEEE Trans Autom Sci Eng 11 (1):20\u201332","journal-title":"IEEE Trans Autom Sci Eng"},{"key":"354_CR22","doi-asserted-by":"crossref","unstructured":"Thuijsman SB, Reniers MA (2020) Transformational supervisor synthesis for evolving systems. In: Proceedings of the 15th IFAC Workshop on Discrete Event Systems, IFAC-PapersOnLine, vol 53, pp 309\u2013316","DOI":"10.1016\/j.ifacol.2021.04.030"},{"key":"354_CR23","unstructured":"Tijsse Claase RG (2020) Symbolic transformational supervisor synthesis. Master\u2019s thesis, Eindhoven University of Technology, Department of Mechanical Engineering"},{"key":"354_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77452-7","volume-title":"Supervisory Control of Discrete-Event Systems","author":"WM Wonham","year":"2019","unstructured":"Wonham WM, Cai K (2019) Supervisory Control of Discrete-Event Systems. Springer, Cham"},{"key":"354_CR25","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.arcontrol.2018.03.002","volume":"45","author":"WM Wonham","year":"2018","unstructured":"Wonham WM, Cai K, Rudie K (2018) Supervisory control of discrete-event systems: A brief history. IFAC Annu Rev Control 45:250\u2013256","journal-title":"IFAC Annu Rev Control"},{"key":"354_CR26","doi-asserted-by":"crossref","unstructured":"ter Beek MH, Reniers MA, de Vink EP (2016) Supervisory controller synthesis for product lines using CIF 3. In: Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Lecture Notes in Computer Science, vol 9952, pp 856\u2013873","DOI":"10.1007\/978-3-319-47166-2_59"},{"key":"354_CR27","doi-asserted-by":"crossref","unstructured":"ter Beek MH, de Vink EP (2014) Towards modular verification of software product lines with mCRL2. In: Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, Lecture Notes in Computer Science, vol 8802, pp 368\u2013385","DOI":"10.1007\/978-3-662-45234-9_26"},{"key":"354_CR28","doi-asserted-by":"crossref","unstructured":"van Beek DA, Fokkink WJ, Hendriks D, Hofkamp A, Markovski J, van de Mortel-Fronczak JM, Reniers MA (2014) CIf 3: Model-based engineering of supervisory controllers. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol 8413, pp 575\u2013580","DOI":"10.1007\/978-3-642-54862-8_48"},{"key":"354_CR29","doi-asserted-by":"crossref","unstructured":"van der Sanden LJ, Reniers MA, Geilen MCW, Basten AA, Jacobs J, Voeten JPM, Schiffelers RRH (2015) Modular model-based supervisory controller design for wafer logistics in lithography machines. In: Proceedings of the ACM\/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, pp 416\u2013425","DOI":"10.1109\/MODELS.2015.7338273"},{"key":"354_CR30","unstructured":"van der Schriek YIC (2018) Evaluation of supervisory control theory based on requirement evolution of LOPW. Master\u2019s thesis, Eindhoven University of Technology, Deptartment of Mechanical Engineering"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-021-00354-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-021-00354-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-021-00354-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T08:44:30Z","timestamp":1651740270000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-021-00354-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,23]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["354"],"URL":"https:\/\/doi.org\/10.1007\/s10626-021-00354-0","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2022,2,23]]},"assertion":[{"value":"8 January 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 October 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 February 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}