{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:51:40Z","timestamp":1757544700684,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031637896"},{"type":"electronic","value":"9783031637902"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-63790-2_4","type":"book-chapter","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T14:03:41Z","timestamp":1718892221000},"page":"61-79","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Alloy Goes Fuzzy"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6918-5558","authenticated-orcid":false,"given":"Pedro","family":"Silva","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2714-8027","authenticated-orcid":false,"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4817-948X","authenticated-orcid":false,"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0196-4229","authenticated-orcid":false,"given":"Jos\u00e9 N.","family":"Oliveira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,21]]},"reference":[{"key":"4_CR1","first-page":"76","volume":"3","author":"O Adil","year":"2015","unstructured":"Adil, O., Ali, A., Sumait, B.: Comparison between the effects of different types of membership functions on fuzzy logic controller performance. Int. J. Emerging Eng. Res. Technol. 3, 76\u201383 (2015)","journal-title":"Int. J. Emerging Eng. Res. Technol."},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Ahmad, K., Mesiarova, A.: Choosing t-norms and t-conorms for fuzzy controllers, vol.\u00a02, pp. 641\u2013646 (2007). https:\/\/doi.org\/10.1109\/FSKD.2007.216","DOI":"10.1109\/FSKD.2007.216"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Bofill, M., Many\u00e0, F., Villaret, M.: Building automated theorem provers for infinitely-valued logics with satisfiability modulo theory solvers. In: 2012 IEEE 42nd International Symposium on Multiple-Valued Logic, pp. 25\u201330 (2012). https:\/\/doi.org\/10.1109\/ISMVL.2012.63","DOI":"10.1109\/ISMVL.2012.63"},{"key":"4_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). http:\/\/www.SMT-LIB.org"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Bofill, M., Moreno, G., V\u00e1zquez P\u00e9rez-\u00cd\u00f1igo, C., Villaret, M.: Automatic proving of fuzzy formulae with fuzzy logic programming and SMT. In: Proceedings of XIII Spanish Conference on Programming and Languages, PROLE 2013 (2014). https:\/\/doi.org\/10.14279\/tuj.eceasst.64.991.974","DOI":"10.14279\/tuj.eceasst.64.991.974"},{"issue":"17","key":"4_CR7","doi-asserted-by":"publisher","first-page":"3652","DOI":"10.1016\/J.INS.2011.04.030","volume":"181","author":"T Chen","year":"2011","unstructured":"Chen, T.: A comparative analysis of score functions for multiple criteria decision making in intuitionistic fuzzy settings. Inf. Sci. 181(17), 3652\u20133676 (2011). https:\/\/doi.org\/10.1016\/J.INS.2011.04.030","journal-title":"Inf. Sci."},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"issue":"2","key":"4_CR9","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/S0165-0114(98)00235-8","volume":"117","author":"SK De","year":"2001","unstructured":"De, S.K., Biswas, R., Roy, A.R.: An application of intuitionistic fuzzy sets in medical diagnosis. Fuzzy Sets Syst. 117(2), 209\u2013213 (2001)","journal-title":"Fuzzy Sets Syst."},{"key":"4_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-642-02282-1_38","volume-title":"Fuzzy Logic and Applications","author":"G Della Penna","year":"2009","unstructured":"Della Penna, G., Intrigila, B., Magazzeni, D.: Evaluating fuzzy controller robustness using model checking. In: Di Ges\u00f9, V., Pal, S.K., Petrosino, A. (eds.) WILF 2009. LNCS, pp. 303\u2013311. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02282-1_38"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Ebrahimi, M., Sotudeh, G., Movaghar, A.: Symbolic checking of fuzzy CTL on fuzzy program graph. Acta Informatica 56 (2019).https:\/\/doi.org\/10.1007\/s00236-018-0311-3","DOI":"10.1007\/s00236-018-0311-3"},{"issue":"9","key":"4_CR13","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019). https:\/\/doi.org\/10.1145\/3338843","journal-title":"Commun. ACM"},{"key":"4_CR14","unstructured":"Jang, J., Gulley.: Matlab: fuzzy logic toolbox user\u2019s guide. the math-works, inc., natick, 19-127 (1997)"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Kiszka, J.B., Kocha\u0144ska, M.E., Sliwi\u0144ska, D.S.: The influence of some fuzzy implication operators on the accuracy of a fuzzy model-part i. Fuzzy Sets Syst. 15(2), 111\u2013128 (1985).https:\/\/doi.org\/10.1016\/0165-0114(85)90041-7, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0165011485900417","DOI":"10.1016\/0165-0114(85)90041-7"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Kiszka, J.B., Kocha\u0144ska, M.E., Sliwi\u0144ska, D.S.: The influence of some fuzzy implication operators on the accuracy of a fuzzy model-part ii. Fuzzy Sets Syst. 15(3), 223\u2013240 (1985).https:\/\/doi.org\/10.1016\/0165-0114(85)90016-8, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0165011485900168","DOI":"10.1016\/0165-0114(85)90016-8"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Kumar, S., Gangwal, C.: A study of fuzzy relation and its application in medical diagnosis. Asian Res. J. Math. 6\u201311 (2021).https:\/\/doi.org\/10.9734\/arjom\/2021\/v17i430289","DOI":"10.9734\/arjom\/2021\/v17i430289"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.fss.2017.03.012","volume":"320","author":"Y Li","year":"2017","unstructured":"Li, Y.: Quantitative model checking of linear-time properties based on generalized possibility measures. Fuzzy Sets Syst. 320, 17\u201339 (2017)","journal-title":"Fuzzy Sets Syst."},{"issue":"5","key":"4_CR19","doi-asserted-by":"publisher","first-page":"842","DOI":"10.1109\/TFUZZ.2012.2232298","volume":"21","author":"Y Li","year":"2013","unstructured":"Li, Y., Li, L.: Model checking of linear-time properties based on possibility measure. IEEE Trans. Fuzzy Syst. 21(5), 842\u2013854 (2013)","journal-title":"IEEE Trans. Fuzzy Syst."},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1016\/j.fss.2014.03.009","volume":"262","author":"Y Li","year":"2015","unstructured":"Li, Y., Li, Y., Ma, Z.: Computation tree logic model checking based on possibility measures. Fuzzy Sets Syst. 262, 44\u201359 (2015)","journal-title":"Fuzzy Sets Syst."},{"issue":"6","key":"4_CR21","doi-asserted-by":"publisher","first-page":"2034","DOI":"10.1109\/TFUZZ.2015.2396537","volume":"23","author":"Y Li","year":"2015","unstructured":"Li, Y., Ma, Z.: Quantitative computation tree logic model checking based on generalized possibility measures. IEEE Trans. Fuzzy Syst. 23(6), 2034\u20132047 (2015)","journal-title":"IEEE Trans. Fuzzy Syst."},{"issue":"7","key":"4_CR22","doi-asserted-by":"publisher","first-page":"1899","DOI":"10.1109\/TFUZZ.2020.2988848","volume":"29","author":"Y Li","year":"2021","unstructured":"Li, Y., Wei, J.: Possibilistic fuzzy linear temporal logic and its model checking. IEEE Trans. Fuzzy Syst. 29(7), 1899\u20131913 (2021). https:\/\/doi.org\/10.1109\/TFUZZ.2020.2988848","journal-title":"IEEE Trans. Fuzzy Syst."},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Ma, Z., Li, Z., Li, W., Gao, Y., Li, X.: Model checking fuzzy computation tree logic based on fuzzy decision processes with cost. Entropy 24(9) (2022). https:\/\/doi.org\/10.3390\/e24091183, https:\/\/www.mdpi.com\/1099-4300\/24\/9\/1183","DOI":"10.3390\/e24091183"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Mamdani, E., Assilian, S.: An experiment in linguistic synthesis with a fuzzy logic controller. Int. J. Man-Mach. Stud. 7(1), 1\u201313 (1975). https:\/\/doi.org\/10.1016\/S0020-7373(75)80002-2, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0020737375800022","DOI":"10.1016\/S0020-7373(75)80002-2"},{"key":"4_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Pan, H., Li, Y., Cao, Y., Ma, Z.: Model checking fuzzy computation tree logic. Fuzzy Sets and Systems 262, 60\u201377 (2015).https:\/\/doi.org\/10.1016\/j.fss.2014.07.008, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0165011414003157. theme: Logic and Computer Science","DOI":"10.1016\/j.fss.2014.07.008"},{"key":"4_CR27","unstructured":"Rada-Vilela, J.: The fuzzylite libraries for fuzzy logic control (2018). https:\/\/fuzzylite.com\/"},{"key":"4_CR28","unstructured":"Reznik, L.: Fuzzy controllers handbook: how to design them, how they work. Elsevier (1997)"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Sanchez, E.: Solutions in composite fuzzy relation equations: application to medical diagnosis in brouwerian logic. In: Dubois, D., Prade, H., Yager, R.R. (eds.) Readings in Fuzzy Sets for Intelligent Systems, pp. 159\u2013165. Morgan Kaufmann (1993). https:\/\/doi.org\/10.1016\/B978-1-4832-1450-4.50017-1, https:\/\/www.sciencedirect.com\/science\/article\/pii\/B9781483214504500171","DOI":"10.1016\/B978-1-4832-1450-4.50017-1"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Silva, P., Oliveira, J.N., Macedo, N., Cunha, A.: Quantitative relational modelling with QAlloy. In: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 885\u2013896. ESEC\/FSE 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3540250.3549154","DOI":"10.1145\/3540250.3549154"},{"issue":"2","key":"4_CR31","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s00165-014-0318-7","volume":"27","author":"G Sotudeh","year":"2015","unstructured":"Sotudeh, G., Movaghar, A.: Abstraction and approximation in fuzzy temporal logics and models. Formal Aspects Comput. 27(2), 309\u2013334 (2015)","journal-title":"Formal Aspects Comput."},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Takagi, T., Sugeno, M.: Fuzzy identification of systems and its applications to modeling and control. IEEE Trans. Syst. Man, Cybern. SMC-15(1), 116\u2013132 (1985). https:\/\/doi.org\/10.1109\/TSMC.1985.6313399","DOI":"10.1109\/TSMC.1985.6313399"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"Tamura, S., Higuchi, S., Tanaka, K.: Pattern classification based on fuzzy relations. IEEE Trans. Syst. Man, Cybern. SMC-1(1), 61\u201366 (1971). https:\/\/doi.org\/10.1109\/TSMC.1971.5408605","DOI":"10.1109\/TSMC.1971.5408605"},{"key":"4_CR34","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Tronci, E., et al.: A model checking technique for the verification of fuzzy control systems. In: International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce (CIMCA-IAWTIC 2006), vol.\u00a01, pp. 536\u2013542 (2005). https:\/\/doi.org\/10.1109\/CIMCA.2005.1631319","DOI":"10.1109\/CIMCA.2005.1631319"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Vidal, A.: MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions. Inf. Sci. 372, 709\u2013730 (2016). https:\/\/doi.org\/10.1016\/j.ins.2016.08.072, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0020025516306491","DOI":"10.1016\/j.ins.2016.08.072"},{"key":"4_CR37","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1007\/978-3-642-33362-0_53","volume-title":"Scalable Uncertainty Management","author":"A Vidal","year":"2012","unstructured":"Vidal, A., Bou, F., Godo, L.: An SMT-based solver for continuous t-norm based logics. In: H\u00fcllermeier, E., Link, S., Fober, T., Seeger, B. (eds.) SUM 2012. LNCS, vol. 7520, pp. 633\u2013640. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33362-0_53"},{"key":"4_CR38","series-title":"Trends in Logic","volume-title":"Goguen Categories\u2013A Categorical Approach to L-Fuzzy Relations","author":"M Winter","year":"2007","unstructured":"Winter, M.: Goguen Categories\u2013A Categorical Approach to L-Fuzzy Relations. Trends in Logic, vol. 25. Springer, Dordrecht (2007)"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Zadeh, L.: Fuzzy sets. Inf. Control 8(3), 338\u2013353 (1965). https:\/\/doi.org\/10.1016\/S0019-9958(65)90241-X, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S001999586590241X","DOI":"10.1016\/S0019-9958(65)90241-X"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Zhao, S., Li, Z., Chen, Z., Wang, J.: Symbolic verification of fuzzy logic models, pp. 1787\u20131789 (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00087","DOI":"10.1109\/ASE56229.2023.00087"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63790-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T08:07:19Z","timestamp":1725523639000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63790-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031637896","9783031637902"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63790-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"21 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author(s) has no competing interests to declare that are relevant to the content of this manuscript.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergamo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}