{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:42:49Z","timestamp":1740141769095,"version":"3.37.3"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:00:00Z","timestamp":1635724800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:00:00Z","timestamp":1635724800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Automated verification of distributed systems becomes very important in distributed computing. The graphical insight into the system in the early and late stages of the project is essential. In the design phase, the visual input helps to articulate the collaborative distributed components clearly. The formal verification gives evidence of correctness or malfunction, but in the latter case, graphical simulation of counterexample helps for better understanding design errors. For these purposes, we invented Distributed Autonomous and Asynchronous Automata (DA<jats:sup>3<\/jats:sup>), which have the same semantics as the formal verification base\u2014Integrated Model of Distributed Systems (IMDS). The IMDS model reflects the natural characteristics of distributed systems: unicasting, locality, autonomy, and asynchrony. Distributed automata have all of these features because they share the same semantics as IMDS. In formalism, the unified system definition has two views: the server view of the cooperating distributed nodes and the agent view of the migrating agents performing distributed computations. The automata have two formally equivalent forms that reflect two views: Server DA<jats:sup>3<\/jats:sup> for observing servers exchanging messages, and Agent DA<jats:sup>3<\/jats:sup> for tracking agents, which visit individual servers in their progress of distributed calculations. We present the DA<jats:sup>3<\/jats:sup> formulation based on the IMDS formalism and their application to design and verify distributed systems in the Dedan environment. DA<jats:sup>3<\/jats:sup> formalism is compared with other concepts of distributed automata known from the literature.<\/jats:p>","DOI":"10.1007\/s10270-021-00917-7","type":"journal-article","created":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T14:02:36Z","timestamp":1635775356000},"page":"363-398","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Graphic modeling in Distributed Autonomous and Asynchronous Automata (DA3)"],"prefix":"10.1007","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7532-362X","authenticated-orcid":false,"given":"Wiktor B.","family":"Daszczuk","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,1]]},"reference":[{"key":"917_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3390\/computers7040065","volume":"7","author":"WB Daszczuk","year":"2018","unstructured":"Daszczuk, W.B.: Specification and verification in integrated model of distributed systems (IMDS). MDPI Comput. 7, 1\u201326 (2018). https:\/\/doi.org\/10.3390\/computers7040065","journal-title":"MDPI Comput."},{"key":"917_CR2","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans. Softw. Eng."},{"key":"917_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"917_CR4","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2005.03.032","volume":"154","author":"I Lanese","year":"2006","unstructured":"Lanese, I., Montanari, U.: Hoare vs Milner: comparing synchronizations in a graphical framework with mobility. Electron. Notes Theor. Comput. Sci. 154, 55\u201372 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.03.032","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"917_CR5","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/spe.1006","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exp. 41, 133\u2013142 (2011). https:\/\/doi.org\/10.1002\/spe.1006","journal-title":"Softw. Pract. Exp."},{"key":"917_CR6","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/948176.948183","volume":"18","author":"D May","year":"1983","unstructured":"May, D.: OCCAM. ACM SIGPLAN Not. 18, 69\u201379 (1983). https:\/\/doi.org\/10.1145\/948176.948183","journal-title":"ACM SIGPLAN Not."},{"key":"917_CR7","unstructured":"Lutz, M.J.: Alloy, software engineering, and undergraduate education. In: ACM SIGSOFT First Alloy Workshop. Portland, Oregon, 6 Nov. pp. 1\u20132. ACM, New York, NY (2006)"},{"key":"917_CR8","doi-asserted-by":"publisher","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J.: Roby: Bandera: extracting finite-state models from Java source code. In: 22nd International Conference on Software Engineering\u2014ICSE \u201900, Limerick, Ireland, 9 June 2000. pp. 762\u2013765. IEEE (2000). https:\/\/doi.org\/10.1145\/337180.337625.","DOI":"10.1145\/337180.337625"},{"key":"917_CR9","unstructured":"Daszczuk, W.B., Bielecki, M., Michalski, J.: Rybu: imperative-style preprocessor for verification of distributed systems in the Dedan environment. In: KKIO\u201917\u2014Software Engineering Conference, Rzesz\u00f3w, Poland, 14\u201316 Sept. 2017. pp. 135\u2013150. Polish Information Processing Society (2017)."},{"key":"917_CR10","doi-asserted-by":"publisher","unstructured":"Jia, W., Zhou, W.: Distributed network systems. from concepts to implementations. NETA vol. 15, Springer, New York (2005). https:\/\/doi.org\/10.1007\/b102545.","DOI":"10.1007\/b102545"},{"key":"917_CR11","doi-asserted-by":"publisher","unstructured":"Dick, G., Yao, X.: Model representation and cooperative coevolution for finite-state machine evolution. In: 2014 IEEE Congress on Evolutionary Computation (CEC), Beijing, China, 6\u201311 July 2014. pp. 2700\u20132707. IEEE, New York, NY (2014). https:\/\/doi.org\/10.1109\/CEC.2014.6900622.","DOI":"10.1109\/CEC.2014.6900622"},{"key":"917_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/850657.850658","volume":"13","author":"HC Lauer","year":"1979","unstructured":"Lauer, H.C., Needham, R.M.: On the duality of operating system structures. ACM SIGOPS Oper. Syst. Rev. 13, 3\u201319 (1979). https:\/\/doi.org\/10.1145\/850657.850658","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"917_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-12835-7_8","volume-title":"Integrated Model of Distributed Systems","author":"WB Daszczuk","year":"2020","unstructured":"Daszczuk, W.B.: Distributed Autonomous and Asynchronous Automata (DA3). In: Kacprzyk, J. (ed.) Integrated Model of Distributed Systems, pp. 125\u2013137. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-12835-7_8"},{"key":"917_CR14","doi-asserted-by":"publisher","unstructured":"Ziadi, T., Helouet, L., Jezequel, J.-M.: Revisiting statechart synthesis with an algebraic approach. In: 26th International Conference on Software Engineering, Edinburgh, UK, 28 May 2004. pp. 242\u2013251. IEEE Comput. Soc (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317446.","DOI":"10.1109\/ICSE.2004.1317446"},{"key":"917_CR15","first-page":"751","volume":"17","author":"K Lodaya","year":"2006","unstructured":"Lodaya, K.: A regular viewpoint on processes and algebra. Acta Cybern. 17, 751\u2013763 (2006)","journal-title":"Acta Cybern."},{"key":"917_CR16","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, Cambridge (2009). https:\/\/doi.org\/10.1017\/CBO9781139195218"},{"key":"917_CR17","doi-asserted-by":"publisher","unstructured":"Phawade, R.: Kleene theorems for free choice automata over distributed alphabets. In: Koutny, M., Pomello, L., and Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency XIV, LNCS vol. 11790. pp. 146\u2013171. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-662-60651-3_6","DOI":"10.1007\/978-3-662-60651-3_6"},{"key":"917_CR18","doi-asserted-by":"publisher","unstructured":"Morales, L.E.M.: Specifying BPMN diagrams with Timed Automata: Proposal of some mapping rules. In: 9th Iberian Conference on Information Systems and Technologies (CISTI), Barcelona, Spain, 18\u201321 June 2014. pp. 1\u20136. IEEE (2014). https:\/\/doi.org\/10.1109\/CISTI.2014.6876897.","DOI":"10.1109\/CISTI.2014.6876897"},{"key":"917_CR19","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/s11390-013-1322-8","volume":"28","author":"Y Zhou","year":"2013","unstructured":"Zhou, Y., Baresi, L., Rossi, M.: Towards a formal semantics for UML\/MARTE state machines based on hierarchical timed automata. J. Comput. Sci. Technol. 28, 188\u2013202 (2013). https:\/\/doi.org\/10.1007\/s11390-013-1322-8","journal-title":"J. Comput. Sci. Technol."},{"key":"917_CR20","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbab","year":"2004","unstructured":"Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14, 329\u2013366 (2004). https:\/\/doi.org\/10.1017\/S0960129504004153","journal-title":"Math. Struct. Comput. Sci."},{"key":"917_CR21","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1142\/S0129054102001424","volume":"13","author":"C Mart\u00edn-Vide","year":"2002","unstructured":"Mart\u00edn-Vide, C., Mateescu, A., Mitrana, V.: Parallel finite automata systems communicating by states. Int. J. Found. Comput. Sci. 13, 733\u2013749 (2002). https:\/\/doi.org\/10.1142\/S0129054102001424","journal-title":"Int. J. Found. Comput. Sci."},{"key":"917_CR22","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0164-1212(94)90112-0","volume":"27","author":"PD Stotts","year":"1994","unstructured":"Stotts, P.D., Pugh, W.: Parallel finite automata for modeling concurrent software systems. J. Syst. Softw. 27, 27\u201343 (1994). https:\/\/doi.org\/10.1016\/0164-1212(94)90112-0","journal-title":"J. Syst. Softw."},{"key":"917_CR23","doi-asserted-by":"publisher","unstructured":"Poizat, P., Choppy, C., Royer, J.-C.: From informal requirements to COOP: a concurrent automata approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999\u2014Formal Methods, Toulouse, France, 20\u201324 Sept 1999, LNCS vol. 1709. pp. 939\u2013962. Springer, Berlin Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48118-4_1","DOI":"10.1007\/3-540-48118-4_1"},{"key":"917_CR24","unstructured":"Grosu, R., Rumpe, B.: Concurrent Timed Port Automata. Technical Report TUM-19533, TU Munich (1995)"},{"key":"917_CR25","unstructured":"Martin, O.B., Williams, B.C., Ingham, M.D.: Diagnosis as approximate belief state enumeration for probabilistic concurrent constraint automata. In: Cohn, A. (ed.) AAAI\u201905: Proceedings of the 20th national conference on Artificial intelligence, Pittsburgh, PA, 9\u201313 July 2005, Vol. 1. pp. 321\u2013326. AAAI Press, Palo Alto, CA (2005)."},{"key":"917_CR26","doi-asserted-by":"publisher","unstructured":"Mie\u015bcicki, J.: The use of model checking and the COSMA environment in the design of reactive systems. Ann. UMCS, Inform. Vol. AI. 4AI, 244\u2013253 (2006). https:\/\/doi.org\/10.17951\/ai.2006.4.1.244-253.","DOI":"10.17951\/ai.2006.4.1.244-253"},{"key":"917_CR27","doi-asserted-by":"publisher","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Automata, Languages and Programming. pp. 322\u2013335. Springer, Berlin\/Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032042","DOI":"10.1007\/BFb0032042"},{"key":"917_CR28","doi-asserted-by":"publisher","unstructured":"Lewerentz, C., Lindner, T. eds: Formal Development of Reactive Systems, LNCS 891. Springer, Berlin, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-58867-1.","DOI":"10.1007\/3-540-58867-1"},{"key":"917_CR29","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1109\/12.600823","volume":"46","author":"\u00d6 Babao\u011flu","year":"1997","unstructured":"Babao\u011flu, \u00d6., Bartoli, A., Dini, G.: Enriched view synchrony: a programming paradigm for partitionable asynchronous distributed systems. IEEE Trans. Comput. 46, 642\u2013658 (1997). https:\/\/doi.org\/10.1109\/12.600823","journal-title":"IEEE Trans. Comput."},{"key":"917_CR30","doi-asserted-by":"publisher","unstructured":"Quaglia, P., Walker, D.: On Synchronous and Asynchronous Mobile Processes. In: Tiuryn, J. (ed.) FoSSaCS 2000: Foundations of Software Science and Computation Structures, Berlin, Germany, March 25\u2013April 2, 2000, LNCS vol. 1784. pp. 283\u2013296. Springer, Berlin Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46432-8_19.","DOI":"10.1007\/3-540-46432-8_19"},{"key":"917_CR31","doi-asserted-by":"publisher","first-page":"931","DOI":"10.1016\/j.ic.2008.05.001","volume":"206","author":"D Gorla","year":"2008","unstructured":"Gorla, D.: Comparing communication primitives via their relative expressive power. Inf. Comput. 206, 931\u2013952 (2008). https:\/\/doi.org\/10.1016\/j.ic.2008.05.001","journal-title":"Inf. Comput."},{"key":"917_CR32","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1019263731139","volume":"1","author":"A Rowstron","year":"1998","unstructured":"Rowstron, A.: WCL: a co-ordination language for geographically distributed agents. World Wide Web. 1, 167\u2013179 (1998). https:\/\/doi.org\/10.1023\/A:1019263731139","journal-title":"World Wide Web."},{"key":"917_CR33","doi-asserted-by":"publisher","first-page":"579","DOI":"10.3166\/ejc.17.579-602","volume":"17","author":"JH van Schuppen","year":"2011","unstructured":"van Schuppen, J.H., Boutin, O., Kempker, P.L., Komenda, J., Masopust, T., Pambakian, N., Ran, A.C.M.: Control of distributed systems: tutorial and overview. Eur. J. Control. 17, 579\u2013602 (2011). https:\/\/doi.org\/10.3166\/ejc.17.579-602","journal-title":"Eur. J. Control."},{"key":"917_CR34","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1051\/ita\/1987210200991","volume":"21","author":"W Zielonka","year":"1987","unstructured":"Zielonka, W.: Notes on finite asynchronous automata. RAIRO Theor. Informatics Appl. 21, 99\u2013135 (1987). https:\/\/doi.org\/10.1051\/ita\/1987210200991","journal-title":"RAIRO Theor. Informatics Appl."},{"key":"917_CR35","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S1571-0661(05)80627-9","volume":"28","author":"P Krishnan","year":"2000","unstructured":"Krishnan, P.: Distributed timed automata. Electron. Notes Theor. Comput. Sci. 28, 5\u201321 (2000). https:\/\/doi.org\/10.1016\/S1571-0661(05)80627-9","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"917_CR36","doi-asserted-by":"publisher","unstructured":"Muscholl, A.: Automated synthesis of distributed controllers. In: Automata, Languages, and Programming\u201442nd International Colloquium, {ICALP} 2015, Kyoto, Japan, 6\u201310 July 2015, Part {II}. pp. 11\u201327 (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_2","DOI":"10.1007\/978-3-662-47666-6_2"},{"key":"917_CR37","doi-asserted-by":"publisher","unstructured":"Diekert, V., Muscholl, A.: On distributed monitoring of asynchronous systems. In: 19th International Workshop on Logic, Language, Information and Computation, WoLLIC 2012, Buenos Aires, Argentina, 3\u20136 Sept. 2012. pp. 70\u201384. Springer, Berlin Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32621-9_5","DOI":"10.1007\/978-3-642-32621-9_5"},{"key":"917_CR38","doi-asserted-by":"publisher","unstructured":"Mukund, M.: Automata on distributed alphabets. In: Modern Applications of Automata Theory. pp. 257\u2013288. Co-Published with Indian Institute of Science (IISc), Bangalore, India (2012). https:\/\/doi.org\/10.1142\/9789814271059_0009.","DOI":"10.1142\/9789814271059_0009"},{"key":"917_CR39","doi-asserted-by":"publisher","unstructured":"Sandholm, A.B., Schwartzbach, M.I.: Distributed Safety Controllers for Web Services. BRICS Rep. Ser. 4, (1997). https:\/\/doi.org\/10.7146\/brics.v4i47.19268.","DOI":"10.7146\/brics.v4i47.19268"},{"key":"917_CR40","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s13389-019-00216-4","volume":"9","author":"C Baumann","year":"2019","unstructured":"Baumann, C., Schwarz, O., Dam, M.: On the verification of system-level information flow properties for virtualized execution platforms. J. Cryptogr. Eng. 9, 243\u2013261 (2019). https:\/\/doi.org\/10.1007\/s13389-019-00216-4","journal-title":"J. Cryptogr. Eng."},{"key":"917_CR41","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10703-017-0282-y","volume":"53","author":"B Bollig","year":"2018","unstructured":"Bollig, B., Grindei, M.-L., Habermehl, P.: Realizability of concurrent recursive programs. Form. Methods Syst. Des. 53, 339\u2013362 (2018). https:\/\/doi.org\/10.1007\/s10703-017-0282-y","journal-title":"Form. Methods Syst. Des."},{"key":"917_CR42","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.10.015","volume":"135","author":"L Brim","year":"2006","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: How to order vertices for distributed LTL model-checking based on accepting predecessors. Electron. Notes Theor. Comput. Sci. 135, 3\u201318 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.10.015","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"917_CR43","doi-asserted-by":"publisher","unstructured":"Bollig, B., Leucker, M.: Message-passing automata are expressively equivalent to EMSO logic. In: 15th International Conference CONCUR 2004 - Concurrency Theory, London, UK, 31 Aug. - 3 Sept. 2004. pp. 146\u2013160. Springer, Berlin Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_10.","DOI":"10.1007\/978-3-540-28644-8_10"},{"key":"917_CR44","doi-asserted-by":"publisher","unstructured":"Bollig, B., Leucker, M.: A hierarchy of implementable MSC languages. In: Formal Techniques for Networked and Distributed Systems - FORTE 2005, Taipei, Taiwan, 2\u20135 Oct. 2005. pp. 53\u201367. Springer, Berlin Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562436_6","DOI":"10.1007\/11562436_6"},{"key":"917_CR45","doi-asserted-by":"publisher","unstructured":"Reiter, F.: Asynchronous distributed automata: a characterization of the modal mu-fragment. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl, A. (eds.) 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), Warsaw, Poland, 10\u201314 July 2017. pp. 100:1\u2013100:14. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.100","DOI":"10.4230\/LIPIcs.ICALP.2017.100"},{"key":"917_CR46","doi-asserted-by":"publisher","first-page":"59","DOI":"10.4204\/EPTCS.3.5","volume":"3","author":"MS Balan","year":"2009","unstructured":"Balan, M.S.: Serializing the parallelism in parallel communicating pushdown automata systems. Electron. Proc. Theor. Comput. Sci. 3, 59\u201368 (2009). https:\/\/doi.org\/10.4204\/EPTCS.3.5","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"917_CR47","doi-asserted-by":"publisher","first-page":"74","DOI":"10.4204\/EPTCS.161.9","volume":"161","author":"C Enea","year":"2014","unstructured":"Enea, C., Habermehl, P., Inverso, O., Parlato, G.: On the path-width of integer linear programming. Electron. Proc. Theor. Comput. Sci. 161, 74\u201387 (2014). https:\/\/doi.org\/10.4204\/EPTCS.161.9","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"917_CR48","doi-asserted-by":"publisher","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL \u201911, Austin, TX, 26\u201328 Jan. 2011. pp. 283\u2013294. ACM Press, New York, NY (2011). https:\/\/doi.org\/10.1145\/1926385.1926419.","DOI":"10.1145\/1926385.1926419"},{"key":"917_CR49","unstructured":"Liu, T.: Computation in the wild: reconsidering dynamic systems in light of irregularity. http:\/\/cs.williams.edu\/~bailey\/Li16.pdf (2016)"},{"key":"917_CR50","doi-asserted-by":"publisher","unstructured":"Kutrib, M., Malcher, A.: Iterative arrays with finite inter-cell communication. In: Castillo-Ramirez, A., de Oliveira, P.P.B. (eds.) AUTOMATA 2019: Cellular Automata and Discrete Complex Systems, Guadalajara, Mexico, 26\u201328 June 2019. pp. 35\u201347. Springer, Cham, Switzerland (2019). https:\/\/doi.org\/10.1007\/978-3-030-20981-0_3.","DOI":"10.1007\/978-3-030-20981-0_3"},{"key":"917_CR51","doi-asserted-by":"publisher","unstructured":"Beeck, M.: A comparison of Statecharts variants. In: FTRTFT 1994: Formal Techniques in Real-Time and Fault-Tolerant Systems, L\u00fcbeck, Germany, 19\u201323 Sept. 1994, LNCS vol. 863. pp. 128\u2013148. Springer, Berlin Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58468-4_163","DOI":"10.1007\/3-540-58468-4_163"},{"key":"917_CR52","doi-asserted-by":"publisher","first-page":"494","DOI":"10.3217\/jucs-005-09-0494","volume":"5","author":"T Balanescu","year":"1999","unstructured":"Balanescu, T., Cowling, A.J., Georgescu, H., Gheorghe, M., Holcombe, M., Vertan, C.: Communicating stream X-machines systems are no more than X-machines. J. Univers. Comput. Sci. 5, 494\u2013507 (1999). https:\/\/doi.org\/10.3217\/jucs-005-09-0494","journal-title":"J. Univers. Comput. Sci."},{"key":"917_CR53","doi-asserted-by":"publisher","unstructured":"Olson, A.G., Evans, B.L.: Deadlock detection for distributed process networks. In: ICASSP \u201905. IEEE International Conference on Acoustics, Speech, and Signal Processing, Philadelphia, PA, 18\u201323 March 2005, Vol. V. pp. 73\u201376. IEEE, New York, NY (2005). https:\/\/doi.org\/10.1109\/ICASSP.2005.1416243.","DOI":"10.1109\/ICASSP.2005.1416243"},{"key":"917_CR54","doi-asserted-by":"publisher","unstructured":"Reniers, M.A., Willemse, T.A.C.: Folk theorems on the correspondence between state-based and event-based systems. In: 37th Conference on Current Trends in Theory and Practice of Computer Science, Nov\u00fd Smokovec, Slovakia, 22\u201328 Jan. 2011, LNCS vol. 6543. pp. 494\u2013505. Springer, Berlin Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18381-2_41","DOI":"10.1007\/978-3-642-18381-2_41"},{"key":"917_CR55","doi-asserted-by":"publisher","first-page":"245","DOI":"10.3233\/FI-2000-43123413","volume":"43","author":"W Penczek","year":"2000","unstructured":"Penczek, W., Szreter, M., Gerth, R., Kuiper, R.: Improving partial order reductions for universal branching time properties. Fundam. Informaticae. 43, 245\u2013267 (2000). https:\/\/doi.org\/10.3233\/FI-2000-43123413","journal-title":"Fundam. Informaticae."},{"key":"917_CR56","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"917_CR57","doi-asserted-by":"publisher","unstructured":"Daszczuk, W.B.: Deadlock detection examples: the Dedan environment at work. In: Integrated Model of Distributed Systems. pp. 53\u201385. Springer Nature, Cham, Switzerland (2020). https:\/\/doi.org\/10.1007\/978-3-030-12835-7_5","DOI":"10.1007\/978-3-030-12835-7_5"},{"key":"917_CR58","doi-asserted-by":"publisher","unstructured":"Daszczuk, W.B.: Asynchronous specification of production cell benchmark in integrated model of distributed systems. In: Bembenik, R., Skonieczny, L., Protaziuk, G., Kryszkiewicz, M., Rybinski, H. (eds.) 23rd International Symposium on Methodologies for Intelligent Systems, ISMIS 2017, Warsaw, Poland, 26\u201329 June 2017, Studies in Big Data, vol. 40. pp. 115\u2013129. Springer International Publishing, Cham, Switzerland (2019). https:\/\/doi.org\/10.1007\/978-3-319-77604-0_9","DOI":"10.1007\/978-3-319-77604-0_9"},{"key":"917_CR59","first-page":"1294","volume":"17","author":"B Czejdo","year":"2016","unstructured":"Czejdo, B., Bhattacharya, S., Baszun, M., Daszczuk, W.B.: Improving resilience of autonomous moving platforms by real-time analysis of their cooperation. Autobusy-TEST 17, 1294\u20131301 (2016)","journal-title":"Autobusy-TEST"},{"key":"917_CR60","doi-asserted-by":"publisher","unstructured":"Daszczuk, W.B.: Fairness in temporal verification of distributed systems. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds.) 13th International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, 2\u20136 July 2018, Brun\u00f3w, Poland, AISC vol.761. pp. 135\u2013150. Springer International Publishing, Cham, Switzerland (2019). https:\/\/doi.org\/10.1007\/978-3-319-91446-6_14","DOI":"10.1007\/978-3-319-91446-6_14"},{"key":"917_CR61","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3390\/s21134541","volume":"21","author":"WB Daszczuk","year":"2021","unstructured":"Daszczuk, W.B.: Static and dynamic verification of space systems using asynchronous observer agents. Sensors. 21, 1\u201324 (2021). https:\/\/doi.org\/10.3390\/s21134541","journal-title":"Sensors."},{"key":"917_CR62","doi-asserted-by":"publisher","unstructured":"Lutz, M.J.: Modeling software the Alloy way. In: 2013 IEEE Frontiers in Education Conference (FIE), Oklahoma City, OK, 23\u201326 Oct. 2013. p. 3. IEEE (2013). https:\/\/doi.org\/10.1109\/FIE.2013.6684771","DOI":"10.1109\/FIE.2013.6684771"},{"key":"917_CR63","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4236\/jcc.2015.37001","volume":"3","author":"MH Abdul-Hussin","year":"2015","unstructured":"Abdul-Hussin, M.H.: Elementary siphons of petri nets and deadlock control in FMS. J. Comput. Commun. 3, 1\u201312 (2015). https:\/\/doi.org\/10.4236\/jcc.2015.37001","journal-title":"J. Comput. Commun."},{"key":"917_CR64","doi-asserted-by":"publisher","unstructured":"Daszczuk, W.B.: Timed IMDS. In: Integrated Model of Distributed Systems. pp. 161\u2013192. Springer Nature, Cham, Switzerland (2020). https:\/\/doi.org\/10.1007\/978-3-030-12835-7_10","DOI":"10.1007\/978-3-030-12835-7_10"},{"key":"917_CR65","doi-asserted-by":"publisher","unstructured":"Daszczuk, W.B.: 2-Vagabonds: non-exhaustive verification algorithm. In: Integrated Model of Distributed Systems. pp. 193\u2013218. Springer, Cham, Switzerland (2020). https:\/\/doi.org\/10.1007\/978-3-030-12835-7_11","DOI":"10.1007\/978-3-030-12835-7_11"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-021-00917-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-021-00917-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-021-00917-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,16]],"date-time":"2022-02-16T06:10:46Z","timestamp":1644991846000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-021-00917-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,1]]},"references-count":65,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["917"],"URL":"https:\/\/doi.org\/10.1007\/s10270-021-00917-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2021,11,1]]},"assertion":[{"value":"23 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 July 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 July 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 November 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The author declares no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}