{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:31Z","timestamp":1740108331026,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"3-5","license":[{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"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":["Acta Informatica"],"published-print":{"date-parts":[[2020,10]]},"DOI":"10.1007\/s00236-020-00367-6","type":"journal-article","created":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T15:04:01Z","timestamp":1588777441000},"page":"627-656","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["SMT-based generation of symbolic automata"],"prefix":"10.1007","volume":"57","author":[{"given":"Xudong","family":"Qin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7900-5271","authenticated-orcid":false,"given":"Simon","family":"Bliudze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5552-5993","authenticated-orcid":false,"given":"Eric","family":"Madelaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zechen","family":"Hou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuxin","family":"Deng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,5,6]]},"reference":[{"issue":"1\/2","key":"367_CR1","first-page":"29","volume":"8","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. JSAT 8(1\/2), 29\u201361 (2012)","journal-title":"JSAT"},{"key":"367_CR2","doi-asserted-by":"crossref","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of sat\/smt solvers to coq through proof witnesses. In: International Conference on Certified Programs and Proofs, pp. 135\u2013150. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-25379-9_12"},{"issue":"2","key":"367_CR3","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s00165-015-0349-8","volume":"18","author":"P Attie","year":"2016","unstructured":"Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Form. Asp. Comput. 18(2), 207\u2013231 (2016)","journal-title":"Form. Asp. Comput."},{"key":"367_CR4","doi-asserted-by":"crossref","unstructured":"Baldan, P., Bracciali, A., Bruni, R.: Bisimulation by unification. In: Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, vol. 2422, pp. 254\u2013270. Springer (2002)","DOI":"10.1007\/3-540-45719-4_18"},{"key":"367_CR5","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2015.05.011","volume":"109","author":"E Baranov","year":"2015","unstructured":"Baranov, E., Bliudze, S.: Offer semantics: achieving compositionality, flattening and full expressiveness for the glue operators in BIP. Sci. Comput. Program. 109, 2\u201335 (2015). https:\/\/doi.org\/10.1016\/j.scico.2015.05.011","journal-title":"Sci. Comput. Program."},{"key":"367_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: Cvc4. In: Computer Aided Verification, Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"367_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"issue":"3","key":"367_CR8","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011). https:\/\/doi.org\/10.1109\/MS.2011.27","journal-title":"IEEE Softw."},{"key":"367_CR9","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-22397-7_10","volume-title":"Coordination Models and Languages","author":"S Bliudze","year":"2019","unstructured":"Bliudze, S., Henrio, L., Madelaine, E.: Verification of concurrent design patterns with data. In: Riis Nielson, H., Tuosto, E. (eds.) Coordination Models and Languages, pp. 161\u2013181. Springer, Cham (2019)"},{"issue":"10","key":"367_CR10","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S Bliudze","year":"2008","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors\u2014structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008). https:\/\/doi.org\/10.1109\/TC.2008.26","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"367_CR11","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10703-010-0091-z","volume":"36","author":"S Bliudze","year":"2010","unstructured":"Bliudze, S., Sifakis, J.: Causal semantics for the algebra of connectors. Form. Methods Syst. Des. 36(2), 167\u2013194 (2010). https:\/\/doi.org\/10.1007\/s10703-010-0091-z","journal-title":"Form. Methods Syst. Des."},{"key":"367_CR12","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-44618-4_20","volume-title":"CONCUR 2000","author":"R Bruni","year":"2000","unstructured":"Bruni, R., de Frutos-Escrig, D., Mart\u00ed-Oliet, N., Montanari, U.: Bisimilarity congruences for open terms and term graphs via tile logic. In: Palamidessi, C. (ed.) CONCUR 2000, pp. 259\u2013274. Springer, Berlin (2000)"},{"key":"367_CR13","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes via array-based systems (extended version). CoRR arXiv:1806.11459 (2018)"},{"key":"367_CR14","first-page":"334","volume-title":"CAV","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV, pp. 334\u2013342. Springer, Cham (2014)"},{"key":"367_CR15","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification, pp. 510\u2013517. Springer, Cham (2016)"},{"key":"367_CR16","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. CoRR arXiv:1310.6847 (2013)","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"367_CR17","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/0304-3975(85)90093-3","volume":"37","author":"R De Simone","year":"1985","unstructured":"De Simone, R.: Higher-level synchronising devices in MEIJE-SCCS. Theor. Comput. Sci. 37, 245\u2013267 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"367_CR18","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1016\/j.scico.2011.03.007","volume":"78","author":"D D\u00e9harbe","year":"2013","unstructured":"D\u00e9harbe, D.: Integration of SMT-solvers in b and event-b development environments. Sci. Comput. Program. 78(3), 310\u2013326 (2013)","journal-title":"Sci. Comput. Program."},{"key":"367_CR19","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","volume":"94","author":"D D\u00e9harbe","year":"2014","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating smt solvers in rodin. Sci. Comput. Program. 94, 130\u2013143 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"367_CR20","first-page":"147","volume":"E\u20135","author":"Y Deng","year":"2001","unstructured":"Deng, Y., Fu, Y.: Algorithm for verifying strong open bisimulation in full $$\\pi $$ calculus. J. Shanghai Jiaotong Univ. E\u20135(2), 147\u2013152 (2001)","journal-title":"J. Shanghai Jiaotong Univ."},{"issue":"2","key":"367_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2579818","volume":"15","author":"Y Feng","year":"2014","unstructured":"Feng, Y., Deng, Y., Ying, M.: Symbolic bisimulation for quantum processes. ACM Trans. Comput. Log. 15(2), 1\u201332 (2014)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"367_CR22","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1), 63\u201392 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00102-X","journal-title":"Theor. Comput. Sci."},{"key":"367_CR23","doi-asserted-by":"publisher","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, 2008, pp. 67\u201382 (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_6","DOI":"10.1007\/978-3-540-71070-7_6"},{"issue":"2","key":"367_CR24","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M Hennessy","year":"1995","unstructured":"Hennessy, M., Lin, H.: Symbolic bisimulations. Theor. Comput. Sci. 138(2), 353\u2013389 (1995). https:\/\/doi.org\/10.1016\/0304-3975(94)00172-F","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"367_CR25","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0304-3975(97)00261-2","volume":"200","author":"M Hennessy","year":"1998","unstructured":"Hennessy, M., Rathke, J.: Bisimulations for a calculus of broadcasting systems. Theor. Comput. Sci. 200(1\u20132), 225\u2013260 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(97)00261-2","journal-title":"Theor. Comput. Sci."},{"key":"367_CR26","doi-asserted-by":"crossref","unstructured":"Henrio, L., Kulankhina, O., Liu, D., Madelaine, E.: Verifying the correct composition of distributed components: Formalisation and Tool. In: FOCLASA, no. 175 in EPTCS. Rome (2014). https:\/\/hal.inria.fr\/hal-01055370","DOI":"10.4204\/EPTCS.175.5"},{"key":"367_CR27","doi-asserted-by":"crossref","unstructured":"Henrio, L., Madelaine, E., Zhang, M.: pNets: an expressive model for parameterised networks of processes. In: 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP\u201915). IEEE (2015)","DOI":"10.1109\/PDP.2015.70"},{"key":"367_CR28","doi-asserted-by":"crossref","unstructured":"Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes. In: Formal Techniques for Distributed Objects, Components, and Systems (FORTE), vol. LNCS-9688. Heraklion, Greece (2016). https:\/\/hal.inria.fr\/hal-01432917","DOI":"10.1007\/978-3-319-39570-8_12"},{"key":"367_CR29","doi-asserted-by":"crossref","unstructured":"Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes \u2013 extended version. Rapport de recherche RR-8898, INRIA (2016)","DOI":"10.1007\/978-3-319-39570-8_12"},{"key":"367_CR30","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"367_CR31","unstructured":"ISO: Information Processing Systems\u2014Open Systems Interconnection\u2014LOTOS\u2014A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO\/IEC 8807, International Organisation for Standardization, Geneva, Switzerland (1989). citeseer.ist.psu.edu\/338220.html"},{"key":"367_CR32","doi-asserted-by":"publisher","unstructured":"Konnov, I.V., Kotek, T., Wang, Q., Veith, H., Bliudze, S., Sifakis, J.: Parameterized systems in BIP: design and model checking. In: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\u00e9bec City, Canada, LIPIcs, vol.\u00a059, pp. 30:1\u201330:16 (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.30","DOI":"10.4230\/LIPIcs.CONCUR.2016.30"},{"key":"367_CR33","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/0304-3975(87)90007-7","volume":"49","author":"KG Larsen","year":"1987","unstructured":"Larsen, K.G.: A context dependent equivalence between processes. Theor. Comput. Sci. 49, 184\u2013215 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"367_CR34","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1093\/logcom\/1.6.761","volume":"1","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Liu, X.: Compositionality through an operational semantics of contexts. J. Log. Comput. 1(6), 761\u2013795 (1991)","journal-title":"J. Log. Comput."},{"key":"367_CR35","doi-asserted-by":"crossref","unstructured":"Leifer, J.J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: The 11th International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 1877, pp. 243\u2013258. Springer (2000)","DOI":"10.1007\/3-540-44618-4_19"},{"key":"367_CR36","unstructured":"Li, Z.: Theories and algorithms for the verification of bisimulation equivalences in value-passing CCS and $$\\pi $$-calculus. Ph.D. thesis, Changsha Institute of Technology (1999)"},{"key":"367_CR37","doi-asserted-by":"crossref","unstructured":"Lin, H.: Symbolic transition graph with assignment. In: Montanari, U., Sassone, V. (eds.) Concur\u201996, LNCS, vol. 1119, pp. 50\u201365. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61604-7_47"},{"key":"367_CR38","unstructured":"Lin, H.: Model checking value-passing processes. In: 8th Asia-Pacific Software Engineering Conference (APSEC\u20192001). Macau (2001)"},{"key":"367_CR39","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Architecture diagrams: a graphical language for architecture style specification. In: Proceedings 9th Interaction and Concurrency Experience (ICE), EPTCS, vol. 223, pp. 83\u201397 (2016). https:\/\/doi.org\/10.4204\/EPTCS.223.6","DOI":"10.4204\/EPTCS.223.6"},{"key":"367_CR40","doi-asserted-by":"crossref","unstructured":"Mavridou, A., Stachtiari, E., Bliudze, S., Ivanov, A., Katsaros, P., Sifakis, J.: Architecture-based design: a satellite on-board software case study. In: 13th International Conference on Formal Aspects of Component Software (FACS 2016) (2016)","DOI":"10.1007\/978-3-319-57666-4_16"},{"issue":"3","key":"367_CR41","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R Milner","year":"1983","unstructured":"Milner, R.: Calculi for synchrony and asynchrony. TCS 25(3), 267\u2013310 (1983). https:\/\/doi.org\/10.1016\/0304-3975(83)90114-7","journal-title":"TCS"},{"key":"367_CR42","volume-title":"Communication and Concurrency. International Series in Computer Science","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989). SU Fisher Research 511\/24"},{"key":"367_CR43","volume-title":"Communicating and Mobile Systems\u2014the Pi-Calculus","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems\u2014the Pi-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"367_CR44","unstructured":"Qin, X., Bliudze, S., Madelaine, E., Zhang, M.: Using SMT engine to generate symbolic automata. In: 18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018). Electronic Communications of the EASST (2018)"},{"key":"367_CR45","unstructured":"Qin, X., Bliudze, S., Madelaine, E., Zhang, M.: Using SMT engine to generate Symbolic Automata\u2014Extended version. Rapport de recherche RR-9177, INRIA (2018)"},{"issue":"1\u20132","key":"367_CR46","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1006\/inco.1999.2818","volume":"156","author":"A Rensink","year":"2000","unstructured":"Rensink, A.: Bisimilarity of open terms. Inf. Comput. 156(1\u20132), 345\u2013385 (2000)","journal-title":"Inf. Comput."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00367-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00367-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00367-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,5]],"date-time":"2021-05-05T23:27:50Z","timestamp":1620257270000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00367-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,6]]},"references-count":46,"journal-issue":{"issue":"3-5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["367"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00367-6","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2020,5,6]]},"assertion":[{"value":"10 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 January 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}