{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T15:35:20Z","timestamp":1786980920047,"version":"build-2736575974"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,1,25]],"date-time":"2024-01-25T00:00:00Z","timestamp":1706140800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,1,25]],"date-time":"2024-01-25T00:00:00Z","timestamp":1706140800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001652","name":"Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001652","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2024,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper addresses the verification of non-blockingness for modular discrete-event systems, i.e., discrete-event systems that are composed from component models. For such systems, the explicit construction of a monolithic representation turns out intractable for relevant applications, since such a construction in general is of exponential cost w.r.t. the number of components. One well established approach to circumvent the need for a monolithic representation for the verification task at hand is to alternate (a) the substitution of individual components by abstractions and (b) the composition of only a small number of strategically chosen components at a time. When successful, one ends up with a single moderately sized automaton which does not represent the overall behaviour in any detail but which does block if and only if the original modular system fails to be non-conflicting. This approach is referred to as\n                    <jats:italic>compositional verification<\/jats:italic>\n                    and originates from the field of process algebra with more recent adaptations to finite automata models. The main contribution of the present study is the development of a number of abstraction rules valid for compositional verification of non-conflictingness in the presence of global event priorities, i.e., where high priority events from one component possibly preempt events with lower priority of all components.\n                  <\/jats:p>","DOI":"10.1007\/s10626-024-00394-2","type":"journal-article","created":{"date-parts":[[2024,1,25]],"date-time":"2024-01-25T03:02:19Z","timestamp":1706151739000},"page":"125-161","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Compositional non-blockingness verification of finite automata with prioritised events"],"prefix":"10.1007","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-0396-2619","authenticated-orcid":false,"given":"Yiheng","family":"Tang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Moor","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,1,25]]},"reference":[{"key":"394_CR1","volume-title":"The Design and Analysis of Computer Algorithms","author":"AV Aho","year":"1974","unstructured":"Aho AV, Hopcroft JE, Ullman JD (1974) The Design and Analysis of Computer Algorithms. Addison-Wesley Publishing Company, Massachusetts, USA"},{"key":"394_CR2","doi-asserted-by":"crossref","unstructured":"Blech JO, Ould\u00a0Biha S (2011) Verification of PLC properties based on formal semantics in coq. In: Software engineering and formal methods, pp 58\u201373","DOI":"10.1007\/978-3-642-24690-6_6"},{"key":"394_CR3","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, New York, USA","edition":"2"},{"issue":"9","key":"394_CR4","doi-asserted-by":"publisher","first-page":"1426","DOI":"10.1016\/j.ic.2007.05.001","volume":"205","author":"R Cleaveland","year":"2007","unstructured":"Cleaveland R, L\u00fcttgen G, Natarajan V (2007) Priority and abstraction in process algebra. Inform Comput 205(9):1426\u20131458","journal-title":"Inform Comput"},{"key":"394_CR5","doi-asserted-by":"crossref","unstructured":"Fabian M, Hellgren A (1998) PLC-based implementation of supervisory control for discrete event systems. Proceedings of the 37th IEEE Conference on Decision and Control 3, 3305\u20133310","DOI":"10.1109\/CDC.1998.758209"},{"key":"394_CR6","doi-asserted-by":"publisher","first-page":"1914","DOI":"10.1137\/070695526","volume":"48","author":"H Flordal","year":"2009","unstructured":"Flordal H, Malik R (2009) Compositional verification in supervisory control. SIAM J Control Optim 48:1914\u20131938","journal-title":"SIAM J Control Optim"},{"key":"394_CR7","doi-asserted-by":"crossref","unstructured":"Flordal H, Malik R (2006) Modular nonblocking verification using conflict equivalence. In: 2006 8th International workshop on discrete event systems, pp 100\u2013106","DOI":"10.1109\/WODES.2006.1678415"},{"key":"394_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10626-021-00338-0","volume":"31","author":"M Goorden","year":"2021","unstructured":"Goorden M, Fabian M, van de Mortel-Fronczak J, Reniers M, Fokkink W, Rooda J (2021) Compositional coordinator synthesis of extended finite automata. Discrete Event Dynamic Syst 31:1\u201332","journal-title":"Discrete Event Dynamic Syst"},{"key":"394_CR9","doi-asserted-by":"crossref","unstructured":"Hering de Queiroz M, Cury J, Wonham W (2005) Multitasking supervisory control of discrete-event systems. Discrete Event Dynamic Syst 15:375\u2013395","DOI":"10.1007\/s10626-005-4058-y"},{"key":"394_CR10","unstructured":"L\u00fattgen G (1998) Pre-emptive modeling of concurrent and distributed systems. PhD thesis, Universit\u00e4t Passau"},{"key":"394_CR11","unstructured":"Malik P (2003) From supervisory control to nonblocking controllers for discrete event systems. PhD thesis, Universit\u00e4t Kaiserslautern"},{"key":"394_CR12","doi-asserted-by":"crossref","unstructured":"Malik R (2004) On the set of certain conflicts of a given language. IFAC Proceedings Volumes 37(18), 267\u2013272. 7th International Workshop on Discrete Event Systems (WODES\u201904), Reims, France, September 22-24 2004","DOI":"10.1016\/S1474-6670(17)30757-7"},{"key":"394_CR13","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10626-019-00305-w","volume":"30","author":"R Malik","year":"2020","unstructured":"Malik R, Ware S (2020) On the computation of counterexamples in compositional nonblocking verification. Discrete Event Dynamic Syst 30:301\u2013334","journal-title":"Discrete Event Dynamic Syst"},{"key":"394_CR14","doi-asserted-by":"crossref","unstructured":"Malik R, Streader D, Reeves S (2004) Fair testing revisited: a process-algebraic characterisation of conflicts. In: Automated technology for verification and analysis, pp 120\u2013134","DOI":"10.1007\/978-3-540-30476-0_14"},{"key":"394_CR15","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and Concurrency. Prentice-Hall Inc, USA"},{"key":"394_CR16","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10626-015-0217-y","volume":"26","author":"S Mohajerani","year":"2016","unstructured":"Mohajerani S, Malik R, Fabian M (2016) A framework for compositional nonblocking verification of extended finite-state machines. Discrete Event Dynamic Syst 26:33\u201384","journal-title":"Discrete Event Dynamic Syst"},{"key":"394_CR17","unstructured":"Moor T (2022) CompileDES: executable-code generation from synchronised libFAUDES automata. https:\/\/fgdes.tf.fau.de\/compiledes, Accessed 27 Jun 2022"},{"issue":"1","key":"394_CR18","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"RD Nicola","year":"1984","unstructured":"Nicola RD, Hennessy MCB (1984) Testing equivalences for processes. Theoret Comput Sci 34(1):83\u2013133","journal-title":"Theoret Comput Sci"},{"key":"394_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2015.05.010","volume":"113","author":"C Pilbrow","year":"2015","unstructured":"Pilbrow C, Malik R (2015) An algorithm for compositional nonblocking verification using special events. Sci Comput Program 113:119\u2013148","journal-title":"Sci Comput Program"},{"key":"394_CR20","first-page":"1","volume":"55","author":"Y Qamsane","year":"2016","unstructured":"Qamsane Y, Abdelouahed T, Philippot A (2016) A synthesis approach to distributed supervisory control design for manufacturing systems with Grafcet implementation. Int J Prod Res 55:1\u201321","journal-title":"Int J Prod Res"},{"key":"394_CR21","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P Ramadge","year":"1987","unstructured":"Ramadge P, Wonham W (1987) Supervisory control of a class of discrete event systems. SIAM J Control Optim 25:206\u2013230","journal-title":"SIAM J Control Optim"},{"key":"394_CR22","doi-asserted-by":"crossref","unstructured":"Schmidt K, de Queiroz MH, Cury JER (2007) Hierarchical and decentralized multitasking control of discrete event systems. In: 2007 46th IEEE conference on decision and control, pp 5936\u20135941","DOI":"10.1109\/CDC.2007.4434610"},{"issue":"6","key":"394_CR23","doi-asserted-by":"publisher","first-page":"968","DOI":"10.1016\/j.automatica.2010.02.025","volume":"46","author":"R Su","year":"2010","unstructured":"Su R, van Schuppen JH, Rooda JE, Hofkamp AT (2010) Nonconflict check by using sequential automaton abstractions based on weak observation equivalence. Automatica 46(6):968\u2013978","journal-title":"Automatica"},{"key":"394_CR24","doi-asserted-by":"crossref","unstructured":"Tang Y, Moor T (2022) Compositional verification of non-blockingness with prioritised events. 16th IFAC Workshop on Discrete Event Systems (WODES) 55(28), 236\u2013243","DOI":"10.1016\/j.ifacol.2022.10.348"},{"key":"394_CR25","doi-asserted-by":"crossref","unstructured":"Verbakel JJ, Vos de Wael MEW, van de Mortel-Fronczak JM, Fokkink WJ, Rooda JE (2022) Supervisory control of roadside units. IFAC-PapersOnLine 55(28), 79\u201386. 16th IFAC Workshop on Discrete Event Systems WODES 2022","DOI":"10.1016\/j.ifacol.2022.10.327"},{"key":"394_CR26","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s10626-012-0133-3","volume":"22","author":"S Ware","year":"2012","unstructured":"Ware S, Malik R (2012) Conflict-preserving abstraction of discrete event systems using annotated automata. Discrete Event Dynamic Systems 22:451\u2013477","journal-title":"Discrete Event Dynamic Systems"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-024-00394-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-024-00394-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-024-00394-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,15]],"date-time":"2024-02-15T04:13:20Z","timestamp":1707970400000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-024-00394-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,25]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["394"],"URL":"https:\/\/doi.org\/10.1007\/s10626-024-00394-2","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,25]]},"assertion":[{"value":"2 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 January 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 January 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of Interest"}}]}}