{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:36Z","timestamp":1771025796363,"version":"3.50.1"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T00:00:00Z","timestamp":1662940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T00:00:00Z","timestamp":1662940800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["POCI-01-0145-FEDER-016826"],"award-info":[{"award-number":["POCI-01-0145-FEDER-016826"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"DOI":"10.1007\/s10817-022-09642-2","type":"journal-article","created":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T19:02:41Z","timestamp":1663009361000},"page":"861-904","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Pardinus: A Temporal Relational Model Finder"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4817-948X","authenticated-orcid":false,"given":"Nuno","family":"Macedo","sequence":"first","affiliation":[]},{"given":"Julien","family":"Brunel","sequence":"additional","affiliation":[]},{"given":"David","family":"Chemouil","sequence":"additional","affiliation":[]},{"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,9,12]]},"reference":[{"key":"9642_CR1","doi-asserted-by":"crossref","unstructured":"Bagheri, H., Malek, S.: Titanium: efficient analysis of evolving Alloy specifications. In: SIGSOFT FSE, pp. 27\u201338. ACM (2016)","DOI":"10.1145\/2950290.2950337"},{"key":"9642_CR2","doi-asserted-by":"crossref","unstructured":"Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: TACAS, LNCS, vol. 2619, pp. 18\u201333. Springer (2003)","DOI":"10.1007\/3-540-36577-X_3"},{"key":"9642_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, LNCS, vol. 1579, pp. 193\u2013207. Springer (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"9642_CR4","unstructured":"Bozzano, M., Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: nuXmv 2.0.0 User Manual. FBK (2019). https:\/\/es.fbk.eu\/tools\/nuxmv\/downloads\/nuxmv-user-manual.pdf"},{"key":"9642_CR5","doi-asserted-by":"crossref","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The Electrum Analyzer: model checking relational first-order temporal specifications. In: ASE, pp. 884\u2013887. ACM (2018)","DOI":"10.1145\/3238147.3240475"},{"key":"9642_CR6","doi-asserted-by":"crossref","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: Simulation under arbitrary temporal logic constraints. In: F-IDE@FM, EPTCS, vol. 310, pp. 63\u201369 (2019)","DOI":"10.4204\/EPTCS.310.7"},{"key":"9642_CR7","doi-asserted-by":"crossref","unstructured":"Castillos, K.C., Waeselynck, H., Wiels, V.: Show me new counterexamples: a path-based approach. In: ICST, pp. 1\u201310. IEEE (2015)","DOI":"10.1109\/ICST.2015.7102606"},{"key":"9642_CR8","doi-asserted-by":"crossref","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: CAV, LNCS, vol. 8559, pp. 334\u2013342. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"9642_CR9","unstructured":"Cavada, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.6 User Manual. FBK-IRST (2010). http:\/\/nusmv.fbk.eu\/NuSMV\/userman\/v26\/nusmv.pdf"},{"issue":"5","key":"9642_CR10","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E Chang","year":"1979","unstructured":"Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979)","journal-title":"Commun. ACM"},{"key":"9642_CR11","doi-asserted-by":"crossref","unstructured":"Chang, F.S., Jackson, D.: Symbolic model checking of declarative relational models. In: ICSE, pp. 312\u2013320. ACM (2006)","DOI":"10.1145\/1134285.1134329"},{"issue":"5\u20136","key":"9642_CR12","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10009-007-0047-9","volume":"9","author":"M Chechik","year":"2007","unstructured":"Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 429\u2013445 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9642_CR13","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: CADE-19 Workshop on Model Computation (2003)"},{"key":"9642_CR14","doi-asserted-by":"crossref","unstructured":"Claris\u00f3, R., Cabot, J.: Diverse scenario exploration in model finders using graph kernels and clustering. In: ABZ, LNCS, vol. 12071. Springer (2020)","DOI":"10.1007\/978-3-030-48077-6_3"},{"key":"9642_CR15","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: KR, pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"9642_CR16","doi-asserted-by":"crossref","unstructured":"Cunha, A.: Bounded model checking of temporal formulas with Alloy. In: ABZ, LNCS, vol. 8477, pp. 303\u2013308. Springer (2014)","DOI":"10.1007\/978-3-662-43652-3_29"},{"key":"9642_CR17","doi-asserted-by":"crossref","unstructured":"Cunha, A., Macedo, N., Guimar\u00e3es, T.: Target oriented relational model finding. In: FASE, LNCS, vol. 8411, pp. 17\u201331. Springer (2014)","DOI":"10.1007\/978-3-642-54804-8_2"},{"key":"9642_CR18","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139236119","volume-title":"Temporal Logics in Computer Science: Finite-State Systems","author":"S Demri","year":"2016","unstructured":"Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (2016). https:\/\/doi.org\/10.1017\/CBO9781139236119"},{"key":"9642_CR19","unstructured":"Dominguez, A.L.J., Day, N.A.: Generating Multiple Diverse Counterexamples for an EFSM. Technical Report. CS-2013-06. University of Waterloo (2013)"},{"key":"9642_CR20","doi-asserted-by":"crossref","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: CAV, LNCS, vol. 2725, pp. 27\u201339. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_3"},{"key":"9642_CR21","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading Alloy with actions. In: ICSE, pp. 442\u2013451. ACM (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"9642_CR22","doi-asserted-by":"crossref","unstructured":"Ganov, S.R., Khurshid, S., Perry, D.E.: Annotations for Alloy: automated incremental analysis using domain specific solvers. In: ICFEM, LNCS, vol. 7635, pp. 414\u2013429. Springer (2012)","DOI":"10.1007\/978-3-642-34281-3_29"},{"key":"9642_CR23","unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V.H., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: ICACSIS, pp. 201\u2013206. IEEE (2011)"},{"issue":"5","key":"9642_CR24","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(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9642_CR25","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2016","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press, Cambridge (2016)","edition":"2"},{"key":"9642_CR26","unstructured":"Kromodimoeljo, S.: Controlling the generation of multiple counterexamples in LTL model checking. PhD Thesis, The University of Queensland (2014)"},{"issue":"3","key":"9642_CR27","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9642_CR28","volume-title":"Specifying Systems: The $$\\rm TLA^+$$ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The $$\\rm TLA^+$$ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"9642_CR29","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.J.: ProB: a model checker for B. In: FME, LNCS, vol. 2805, pp. 855\u2013874. Springer (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"9642_CR30","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: SIGSOFT FSE, pp. 373\u2013383. ACM (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"9642_CR31","unstructured":"Macedo, N., Cunha, A.: Alloy meets $${{\\rm TLA}}^{+}$$: an exploratory study. CoRR (2016).abs\/1603.03599"},{"key":"9642_CR32","doi-asserted-by":"crossref","unstructured":"Macedo, N., Cunha, A., Guimar\u00e3es, T.: Exploring scenario exploration. In: FASE, LNCS, vol. 9033, pp. 301\u2013315. Springer (2015)","DOI":"10.1007\/978-3-662-46675-9_20"},{"key":"9642_CR33","doi-asserted-by":"crossref","unstructured":"Macedo, N., Cunha, A., Pessoa, E.: Exploiting partial knowledge for efficient model analysis. In: ATVA, LNCS, vol. 10482, pp. 344\u2013362. Springer (2017)","DOI":"10.1007\/978-3-319-68167-2_23"},{"key":"9642_CR34","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"9642_CR35","doi-asserted-by":"crossref","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: CADE, LNCS, vol. 10395, pp. 148\u2013165. Springer (2017)","DOI":"10.1007\/978-3-319-63046-5_10"},{"key":"9642_CR36","doi-asserted-by":"crossref","unstructured":"Montaghami, V., Rayside, D.: Extending Alloy with partial instances. In: ABZ, LNCS, vol. 7316, pp. 122\u2013135. Springer (2012)","DOI":"10.1007\/978-3-642-30885-7_9"},{"key":"9642_CR37","doi-asserted-by":"crossref","unstructured":"Near, J.P., Jackson, D.: An imperative extension to Alloy. In: ASM, LNCS, vol. 5977, pp. 118\u2013131. Springer (2010)","DOI":"10.1007\/978-3-642-11811-1_10"},{"key":"9642_CR38","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE, pp. 232\u2013241. IEEE (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"issue":"1","key":"9642_CR39","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-009-0132-3","volume":"12","author":"D Plagge","year":"2010","unstructured":"Plagge, D., Leuschel, M.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Int. J. Softw. Tools Technol. Transf. 12(1), 9\u201321 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9642_CR40","doi-asserted-by":"crossref","unstructured":"Ponzio, P., Aguirre, N., Frias, M.F., Visser, W.: Field-exhaustive testing. In: SIGSOFT FSE, pp. 908\u2013919. ACM (2016)","DOI":"10.1145\/2950290.2950336"},{"key":"9642_CR41","doi-asserted-by":"crossref","unstructured":"Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: FM, LNCS, vol. 10951, pp. 568\u2013587. Springer (2018)","DOI":"10.1007\/978-3-319-95582-7_34"},{"key":"9642_CR42","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krstic, S.: Finite model finding in SMT. In: CAV, LNCS, vol. 8044, pp. 640\u2013655. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_42"},{"key":"9642_CR43","doi-asserted-by":"crossref","unstructured":"Rosner, N., Pombo, C.G.L., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F.: Parallel bounded verification of Alloy models by TranScoping. In: VSTTE, LNCS, vol. 8164, pp. 88\u2013107. Springer (2013)","DOI":"10.1007\/978-3-642-54108-7_5"},{"key":"9642_CR44","doi-asserted-by":"crossref","unstructured":"Rosner, N., Siddiqui, J.H., Aguirre, N., Khurshid, S., Frias, M.F.: Ranger: parallel analysis of Alloy models by range partitioning. In: ASE, pp. 147\u2013157. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693075"},{"issue":"2","key":"9642_CR45","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. STTT 12(2), 123\u2013137 (2010)","journal-title":"STTT"},{"key":"9642_CR46","doi-asserted-by":"crossref","unstructured":"Saeki, T., Ishikawa, F., Honiden, S.: Automatic generation of potentially pathological instances for validating Alloy models. In: ICFEM, LNCS, vol. 10009, pp. 41\u201356 (2016)","DOI":"10.1007\/978-3-319-47846-3_4"},{"key":"9642_CR47","doi-asserted-by":"crossref","unstructured":"Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: CADE, LNCS, vol. 9195, pp. 434\u2013449. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_30"},{"key":"9642_CR48","doi-asserted-by":"crossref","unstructured":"Serna, J., Day, N.A., Farheen, S.: DASH: a new language for declarative behavioural requirements with control state hierarchy. In: RE Workshops, pp. 64\u201368. IEEE Computer Society (2017)","DOI":"10.1109\/REW.2017.70"},{"key":"9642_CR49","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S1571-0653(04)00311-7","volume":"9","author":"I Shlyakhter","year":"2001","unstructured":"Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. Electron. Notes Discrete Math. 9, 19\u201335 (2001)","journal-title":"Electron. Notes Discrete Math."},{"key":"9642_CR50","doi-asserted-by":"crossref","unstructured":"Siegel, A., Santomauro, M., Dyer, T., Nelson, T., Krishnamurthi, S.: Prototyping formal methods tools: a protocol analysis case study. In: Protocols, Logic, and Strands: Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday, LNCS. Springer (2021).","DOI":"10.1007\/978-3-030-91631-2_22"},{"key":"9642_CR51","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Marinov, D., Khurshid, S.: Solution enumeration abstraction: a modeling idiom to enhance a lightweight formal method. In: ICFEM, LNCS, vol. 11852, pp. 336\u2013352. Springer (2019)","DOI":"10.1007\/978-3-030-32409-4_21"},{"key":"9642_CR52","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: ICST, pp. 264\u2013275. IEEE (2017)","DOI":"10.1109\/ICST.2017.31"},{"key":"9642_CR53","doi-asserted-by":"crossref","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: TACAS, LNCS, vol. 4424, pp. 632\u2013647. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"9642_CR54","doi-asserted-by":"crossref","unstructured":"Uzuncaova, E., Khurshid, S.: Constraint prioritization for efficient analysis of declarative models. In: FM, LNCS, vol. 5014, pp. 310\u2013325. Springer (2008)","DOI":"10.1007\/978-3-540-68237-0_22"},{"key":"9642_CR55","doi-asserted-by":"crossref","unstructured":"Vakili, A., Day, N.A.: Temporal logic model checking in Alloy. In: ABZ, LNCS, vol. 7316, pp. 150\u2013163. Springer (2012)","DOI":"10.1007\/978-3-642-30885-7_11"},{"key":"9642_CR56","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: IJCAI, pp. 298\u2013303. Morgan Kaufmann (1995)"},{"key":"9642_CR57","doi-asserted-by":"crossref","unstructured":"Zheng, G., Bagheri, H., Rothermel, G., Wang, J.: Platinum: reusing constraint solutions in bounded analysis of relational logic. In: FASE, LNCS, vol. 12076, pp. 29\u201352. Springer (2020)","DOI":"10.1007\/978-3-030-45234-6_2"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09642-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09642-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09642-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,3]],"date-time":"2024-10-03T18:25:42Z","timestamp":1727979942000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09642-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,12]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9642"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09642-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,12]]},"assertion":[{"value":"4 February 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 July 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 September 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}