{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T11:07:06Z","timestamp":1772795226022,"version":"3.50.1"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,2]]},"DOI":"10.1007\/s10703-025-00489-y","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T10:33:02Z","timestamp":1767868382000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A scalable anytime algorithm for learning fragments of linear temporal logic"],"prefix":"10.1007","volume":"68","author":[{"given":"Ritam","family":"Raha","sequence":"first","affiliation":[]},{"given":"Rajarshi","family":"Roy","sequence":"additional","affiliation":[]},{"given":"Nathana\u00ebl","family":"Fijalkow","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"489_CR1","doi-asserted-by":"publisher","unstructured":"Raha R, Roy R, Fijalkow N, Neider D (2022) Scalable anytime algorithms for learning fragments of linear temporal logic. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_14","DOI":"10.1007\/978-3-030-99524-9_14"},{"key":"489_CR2","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In Symposium on Foundations of Computer Science, SFCS. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"489_CR3","doi-asserted-by":"publisher","unstructured":"Giacomo GD, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In International Joint Conference on Artificial Intelligence, IJCAI. https:\/\/doi.org\/10.5555\/2540128.2540252","DOI":"10.5555\/2540128.2540252"},{"key":"489_CR4","doi-asserted-by":"crossref","unstructured":"Camacho A, McIlraith SA (2019) Learning interpretable models expressed in linear temporal logic. In International Conference on Automated Planning and Scheduling, ICAPS, vol 29. https:\/\/ojs.aaai.org\/index.php\/ICAPS\/article\/view\/3529","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"489_CR5","doi-asserted-by":"publisher","unstructured":"Roy R, Fisman D, Neider D (2020) Learning interpretable models in the property specification language. In International Joint Conference on Artificial Intelligence, IJCAI, pp 2213\u20132219). https:\/\/doi.org\/10.24963\/ijcai.2020\/306","DOI":"10.24963\/ijcai.2020\/306"},{"key":"489_CR6","unstructured":"Raha R (2023) Learning and verifying temporal specifications for cyber-physical systems. PhD thesis, https:\/\/hdl.handle.net\/10067\/1986580151162165141, University of Antwerp, Belgium"},{"key":"489_CR7","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2021.XVII.090","author":"K Grover","year":"2021","unstructured":"Grover K, Barbosa FS, Tumova J, Kret\u00ednsk\u00fd J (2021) Semantic abstraction-guided motion planning for LTL missions in unknown environments. Robot: Sci Syst XVII. https:\/\/doi.org\/10.15607\/RSS.2021.XVII.090","journal-title":"Robot: Sci Syst XVII"},{"key":"489_CR8","doi-asserted-by":"publisher","unstructured":"Ammons G, Bod\u00edk R, Larus JR (2002) Mining specifications. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL\u201902, New York, NY, USA, 4\u201316. Association for Computing Machinery, https:\/\/doi.org\/10.1145\/503272.503275","DOI":"10.1145\/503272.503275"},{"key":"489_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15187-3_13","author":"A Zeller","year":"2010","unstructured":"Zeller A (2010) Mining specifications: a roadmap. The Future Of Softw Eng. https:\/\/doi.org\/10.1007\/978-3-642-15187-3_13","journal-title":"The Future Of Softw Eng"},{"key":"489_CR10","doi-asserted-by":"publisher","unstructured":"Rozier KY (2016) Specification: the biggest bottleneck in formal methods and autonomy. In International Conference on Verified Software. Theories, Tools, and Experiments. Lecture Notes in Computer Science, vol 9971. pp 8\u201326). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2","DOI":"10.1007\/978-3-319-48869-1_2"},{"key":"489_CR11","doi-asserted-by":"publisher","unstructured":"Lemieux C, Park D, Beschastnikh I (2015) General LTL specification mining. In IEEE\/ACM International Conference on Automated Software Engineering. ASE\u201915, IEEE Computer Society, Los Alamitos, CA, USA, 81\u201392). https:\/\/doi.org\/10.1109\/ASE.2015.71","DOI":"10.1109\/ASE.2015.71"},{"key":"489_CR12","doi-asserted-by":"publisher","unstructured":"Lemieux C, Beschastnikh I (2015) Investigating program behavior using the texada LTL specifications miner. In IEEE\/ACM International Conference on Automated Software Engineering. ASE\u201915, IEEE Computer Society, Los Alamitos, CA, USA, 870\u2013875). https:\/\/doi.org\/10.1109\/ASE.2015.94","DOI":"10.1109\/ASE.2015.94"},{"key":"489_CR13","doi-asserted-by":"publisher","unstructured":"Valizadeh M, Fijalkow N, Berger M (2024) LTL learning on GPUs. In International Conference on Computer Aided Verification, CAV. Lecture Notes in Computer Science, vol 14683. https:\/\/doi.org\/10.1007\/978-3-031-65633-0_10","DOI":"10.1007\/978-3-031-65633-0_10"},{"key":"489_CR14","doi-asserted-by":"publisher","unstructured":"Christodorescu M, Jha S, Kruegel C (2007) Mining specifications of malicious behavior. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering. https:\/\/doi.org\/10.1145\/1287624.1287628","DOI":"10.1145\/1287624.1287628"},{"key":"489_CR15","doi-asserted-by":"publisher","unstructured":"Li Z, Zhou Y (2005) PR-miner: automatically extracting implicit programming rules and detecting violations in large software code. In European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering. https:\/\/doi.org\/10.1145\/1081706.1081755","DOI":"10.1145\/1081706.1081755"},{"key":"489_CR16","doi-asserted-by":"publisher","unstructured":"Ghosh S, Elenius D, Li W, Lincoln P, Shankar N, Steiner W (2016) Arsenal: automatic requirements specification extraction from natural language. In International Symposium on NASA Formal Methods. https:\/\/doi.org\/10.1007\/978-3-319-40648-0_4","DOI":"10.1007\/978-3-319-40648-0_4"},{"key":"489_CR17","unstructured":"Giannakopoulou D, Pressburger T, Mavridou A, Rhein J, Schumann J, Shi N (2020) Formal requirements elicitation with fret. In International Conference on Requirements Engineering: Foundation for Software Quality. https:\/\/ceur-ws.org\/Vol-2584\/PT-paper4.pdf"},{"key":"489_CR18","doi-asserted-by":"crossref","unstructured":"Lo D, Khoo S-C, Han J, Liu C (2017) Mining Software specifications: methodologies and applications, 1st edn edn. CRC Press, Inc, USA","DOI":"10.1201\/b10928-2"},{"key":"489_CR19","unstructured":"Li W (2013) Specification mining: new formalisms, algorithms and applications. PhD thesis, http:\/\/www.escholarship.org\/uc\/item\/4027r49r, University of California, Berkeley, USA"},{"key":"489_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/J.TCS.2015.02.046","volume":"587","author":"E Bartocci","year":"2015","unstructured":"Bartocci E, Bortolussi L, Nenzi L, Sanguinetti G (2015) System design of stochastic models using robustness of temporal properties. Theor Comput Sci 587:3\u201325. https:\/\/doi.org\/10.1016\/J.TCS.2015.02.046","journal-title":"Theor Comput Sci"},{"key":"489_CR21","doi-asserted-by":"publisher","unstructured":"Jones A, Kong Z, Belta C (2014) Anomaly detection in cyber-physical systems: a formal methods approach. In IEEE Conference on Decision and Control. https:\/\/doi.org\/10.1109\/CDC.2014.7039487","DOI":"10.1109\/CDC.2014.7039487"},{"key":"489_CR22","doi-asserted-by":"publisher","unstructured":"Kong Z, Jones A, Belta C (2017) Temporal logics for learning and detection of anomalous behavior 62:1210\u20131222. https:\/\/doi.org\/10.1109\/TAC.2016.2585083","DOI":"10.1109\/TAC.2016.2585083"},{"key":"489_CR23","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-29860-8_12","volume-title":"Runtime verification","author":"E Asarin","year":"2012","unstructured":"Asarin E, Donz\u00e9 A, Maler O, Nickovic D (2012) Parametric identification of temporal properties. In: Runtime verification. Springer, Berlin, Heidelberg, pp 147\u2013160"},{"key":"489_CR24","doi-asserted-by":"publisher","unstructured":"Yang H, Hoxha B, Fainekos GE (2012) Querying parametric temporal logic properties on embedded systems. In IFIP International Conference on Testing Software and Systems. Lecture Notes in Computer Science, vol 7641. https:\/\/doi.org\/10.1007\/978-3-642-34691-0_11","DOI":"10.1007\/978-3-642-34691-0_11"},{"issue":"11","key":"489_CR25","doi-asserted-by":"publisher","first-page":"1704","DOI":"10.1109\/TCAD.2015.2421907","volume":"34","author":"X Jin","year":"2015","unstructured":"Jin X, Donz\u00e9 A, Deshmukh JV, Seshia SA (2015) Mining requirements from closed-loop control models. IEEE Trans On Comput-Aided Des Of Integr Circuits And Syst 34(11):1704\u20131717. https:\/\/doi.org\/10.1109\/TCAD.2015.2421907","journal-title":"IEEE Trans On Comput-Aided Des Of Integr Circuits And Syst"},{"key":"489_CR26","doi-asserted-by":"crossref","unstructured":"Bombara G, Vasile CI, Penedo Alvarez F, Yasuoka H, Belta C (2016) A decision tree approach to data classification using signal temporal logic. Hybrid Syst: Computation And ControlHSCC\u201916)","DOI":"10.1145\/2883817.2883843"},{"key":"489_CR27","doi-asserted-by":"publisher","unstructured":"Bufo S, Bartocci E, Sanguinetti G, Borelli M, Lucangelo U, Bortolussi L (2014) Temporal logic based monitoring of assisted ventilation in intensive care patients. In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. https:\/\/doi.org\/10.1007\/978-3-662-45231-8_30","DOI":"10.1007\/978-3-662-45231-8_30"},{"key":"489_CR28","doi-asserted-by":"publisher","unstructured":"Bartocci E, Bortolussi L, Sanguinetti G (2014) Data-driven statistical learning of temporal logic properties. In International Conference on Formal Modeling and Analysis of Timed Systems. https:\/\/doi.org\/10.1007\/978-3-319-10512-3_3","DOI":"10.1007\/978-3-319-10512-3_3"},{"key":"489_CR29","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2020.XVI.097","author":"G Chou","year":"2020","unstructured":"Chou G, Ozay N, Berenson D (2020) Explaining multi-stage tasks by learning temporal logic formulas from suboptimal demonstrations. Robot: Sci Syst XVI. https:\/\/doi.org\/10.15607\/RSS.2020.XVI.097","journal-title":"Robot: Sci Syst XVI"},{"key":"489_CR30","doi-asserted-by":"publisher","first-page":"112086","DOI":"10.1016\/j.knosys.2024.112086","volume":"299","author":"M Lyu","year":"2024","unstructured":"Lyu M, Li F, Lee C-H, Chen C-H (2024) Valio: visual attention-based linear temporal logic method for explainable out-of-the-loop identification. Knowl-Based Syst 299:112086. https:\/\/doi.org\/10.1016\/j.knosys.2024.112086","journal-title":"Knowl-Based Syst"},{"key":"489_CR31","unstructured":"Icarte RT, Klassen TQ, Valenzano RA, McIlraith SA (2018) Teaching multiple tasks to an RL agent using LTL. In International Conference on Autonomous Agents and MultiAgent Systems. http:\/\/dl.acm.org\/citation.cfm?id=3237452"},{"key":"489_CR32","doi-asserted-by":"publisher","unstructured":"Camacho A, Chen O, Sanner S, McIlraith SA (2017) Non-markovian rewards expressed in LTL: guiding search via reward shaping. In International Symposium on Combinatorial Search. https:\/\/doi.org\/10.1609\/SOCS.V8I1.18421","DOI":"10.1609\/SOCS.V8I1.18421"},{"key":"489_CR33","doi-asserted-by":"publisher","unstructured":"Brafman RI, Giacomo GD, Patrizi F (2018) Ltlf\/Ldlf non-markovian rewards. In AAAI Conference on Artificial Intelligence. https:\/\/doi.org\/10.1609\/AAAI.V32I1.11572","DOI":"10.1609\/AAAI.V32I1.11572"},{"key":"489_CR34","unstructured":"Icarte RT, Klassen TQ, Valenzano RA, McIlraith SA (2018) Using reward machines for high-level task specification and decomposition in reinforcement learning. In International Conference on Machine Learning. http:\/\/proceedings.mlr.press\/v80\/icarte18a.html"},{"key":"489_CR35","doi-asserted-by":"publisher","unstructured":"Camacho A, Icarte RT, Klassen TQ, Valenzano RA, McIlraith SA (2019) LTL and beyond: formal languages for reward function specification in reinforcement learning. In International Joint Conference on Artificial Intelligence. https:\/\/doi.org\/10.24963\/IJCAI.2019\/840","DOI":"10.24963\/IJCAI.2019\/840"},{"key":"489_CR36","doi-asserted-by":"publisher","unstructured":"Murphy W, Holzer N, Koenig N, Cui L, Rothkopf R, Qiao F, Santolucito M (2024) Guiding LLM temporal logic generation with explicit separation of data and control. CoRr abs\/2406(7400). https:\/\/doi.org\/10.48550\/ARXIV.2406.07400","DOI":"10.48550\/ARXIV.2406.07400"},{"key":"489_CR37","doi-asserted-by":"publisher","unstructured":"Neider D, Gavran I (2018) Learning linear temporal properties. Formal Methods In Comput Aided Des. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603016","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"489_CR38","doi-asserted-by":"publisher","unstructured":"Arif MF, Larraz D, Echeverria M, Reynolds A, Chowdhury O, Tinelli C (2020) SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. Formal Methods In Comput Aided Des. https:\/\/doi.org\/10.34727\/2020\/ISBN.978-3-85448-042-6_16","DOI":"10.34727\/2020\/ISBN.978-3-85448-042-6_16"},{"key":"489_CR39","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-031-49299-0_3","volume-title":"Inductive logic programming","author":"A Ielo","year":"2023","unstructured":"Ielo A, Law M, Fionda V, Ricca F, De Giacomo G, Russo A (2023) Towards ILP-based LTLf passive learning. In: Inductive logic programming. Springer, Cham, pp 30\u201345"},{"key":"489_CR40","doi-asserted-by":"publisher","unstructured":"Jeppu N, Melham T, Kroening D, O\u2019Leary J (2020) Learning concise models from long execution traces. In ACM\/IEEE Design Automation Conference. DAC\u201920, pp 1\u20136). https:\/\/doi.org\/10.1109\/DAC18072.2020.9218613","DOI":"10.1109\/DAC18072.2020.9218613"},{"key":"489_CR41","doi-asserted-by":"crossref","unstructured":"Jeppu NY, Melham T, Kroening D (2022) Active learning of abstract system models from traces using model checking. In Conference & Exhibition on Design, Automation & Test in Europe. DATE\u201922, European Design and Automation Association, Leuven, BEL, 100\u2013103","DOI":"10.23919\/DATE54114.2022.9774595"},{"key":"489_CR42","doi-asserted-by":"publisher","unstructured":"Jeppu N, Melham T, Kroening D (2023) Enhancing active model learning with equivalence checking using simulation relations. Formal Methods In System Des. https:\/\/doi.org\/10.1007\/s10703-023-00433-y","DOI":"10.1007\/s10703-023-00433-y"},{"key":"489_CR43","unstructured":"Shah A, Kamath P, Shah JA, Li S (2018) Bayesian inference of temporal task specifications from demonstrations. In Annual Conference on Neural Information Processing Systems 2018, pp 3808\u20133817). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/13168e6a2e6c84b4b7de9390c0ef5ec5-Abstract.html"},{"key":"489_CR44","doi-asserted-by":"publisher","unstructured":"Kim J, Muise C, Shah A, Agarwal S, Shah J (2019) Bayesian inference of linear temporal logic specifications for contrastive explanations. In International Joint Conference on Artificial Intelligence. https:\/\/doi.org\/10.24963\/IJCAI.2019\/776","DOI":"10.24963\/IJCAI.2019\/776"},{"key":"489_CR45","doi-asserted-by":"publisher","unstructured":"Peng B, Liang P, Han T, Luo W, Du J, Wan H, Ye R, Zheng Y (2023) PURLTL: mining LTL specification from imperfect traces in testing. In IEEE\/ACM International Conference on Automated Software Engineering. ASE\u201923, IEEE Computer Society, Los Alamitos, CA, USA, 1766\u20131770). https:\/\/doi.org\/10.1109\/ASE56229.2023.00202","DOI":"10.1109\/ASE56229.2023.00202"},{"key":"489_CR46","doi-asserted-by":"publisher","unstructured":"Gupta A, Komp J, Rajput AS, Krishna S, Trivedi A, Varshney N (2024) Integrating explanations in learning LTL specifications from demonstrations. CoRr abs\/2404(2872). https:\/\/doi.org\/10.48550\/ARXIV.2404.02872","DOI":"10.48550\/ARXIV.2404.02872"},{"key":"489_CR47","doi-asserted-by":"publisher","unstructured":"Luo W, Liang P, Du J, Wan H, Peng B, Zhang D (2022) Bridging LTLf inference to GNN inference for learning LTLf formulae. AAAI Conf On Artif Intel 36(9):9849\u20139857. https:\/\/doi.org\/10.1609\/aaai.v36i9.21221","DOI":"10.1609\/aaai.v36i9.21221"},{"key":"489_CR48","doi-asserted-by":"publisher","unstructured":"Isik I, Gol EA, Cinbis RG (2024) Learning to estimate system specifications in linear temporal logic using transformers and mamba. CoRr abs\/2405(20917). https:\/\/doi.org\/10.48550\/ARXIV.2405.20917","DOI":"10.48550\/ARXIV.2405.20917"},{"key":"489_CR49","unstructured":"Fijalkow N, Lagarde G (2021) The complexity of learning linear temporal formulas from examples. In International Conference on Grammatical Inference, ICGI. https:\/\/proceedings.mlr.press\/v153\/fijalkow21a.html"},{"key":"489_CR50","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2312.16336","volume-title":"Learning temporal formulas from examples is hard","author":"C Mascle","year":"2023","unstructured":"Mascle C, Fijalkow N, Lagarde G (2023) Learning temporal formulas from examples is hard. https:\/\/doi.org\/10.48550\/arXiv.2312.16336"},{"key":"489_CR51","doi-asserted-by":"publisher","unstructured":"Baresi L, Kallehbasti MMP, Rossi M (2015) Efficient scalable verification of LTL specifications. In International Conference on Software Engineering, ICSE, pp 711\u2013721). https:\/\/doi.org\/10.1109\/ICSE.2015.84","DOI":"10.1109\/ICSE.2015.84"},{"key":"489_CR52","doi-asserted-by":"crossref","unstructured":"Flajolet P, Sedgewick R (2008) Analytic combinatorics. http:\/\/algo.inria.fr\/flajolet\/Publications\/AnaCombi\/anacombi.html","DOI":"10.1017\/CBO9780511801655"},{"key":"489_CR53","doi-asserted-by":"publisher","unstructured":"Dinur I, Steurer D (2014) Analytical approach to parallel repetition. In Symposium on Theory of Computing, STOC, pp 624\u2013633). https:\/\/doi.org\/10.1145\/2591796.2591884","DOI":"10.1145\/2591796.2591884"},{"key":"489_CR54","doi-asserted-by":"publisher","unstructured":"Raha R, Roy R, Fijalkow N, Neider D (2024) Scarlet: scalable anytime algorithms for learning fragments of linear temporal logic. J Open Source Softw 9(93):5052. https:\/\/doi.org\/10.21105\/JOSS.05052","DOI":"10.21105\/JOSS.05052"},{"key":"489_CR55","doi-asserted-by":"publisher","unstructured":"Neider D, Gavran I (2018) Learning linear temporal properties. Formal Methods In Comput Aided Des, FMCAD. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603016","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"489_CR56","doi-asserted-by":"publisher","unstructured":"Arif MF, Larraz D, Echeverria M, Reynolds A, Chowdhury O, Tinelli C (2020) SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. Formal Methods In Comput Aided Des, FMCAD. https:\/\/doi.org\/10.34727\/2020\/ISBN.978-3-85448-042-6_16","DOI":"10.34727\/2020\/ISBN.978-3-85448-042-6_16"},{"key":"489_CR57","doi-asserted-by":"publisher","unstructured":"Reynolds A, Barbosa H, N\u00f6tzli A, Barrett CW, Tinelli C: cvc 4sy: 2019) Smart and fast term enumeration for syntax-guided synthesis. Comput-Aided Verif, CAV. https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"489_CR58","doi-asserted-by":"publisher","unstructured":"Raha R, Roy R, Fijalkow N, Neider D (2022) Scarlet: scalable anytime algorithm for learning LTL. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.5890149","DOI":"10.5281\/zenodo.5890149"},{"key":"489_CR59","doi-asserted-by":"publisher","unstructured":"Henriksen JG, Jensen J, J\u00f8rgensen M, Klarlund N, Paige B, Rauhe T, Sandholm A (1995) Mona: monadic second-order logic in practice. Tools And Algoritms For The Construct And Anal Of Syst, TACAS. https:\/\/doi.org\/10.1007\/3-540-60630-0_5","DOI":"10.1007\/3-540-60630-0_5"},{"key":"489_CR60","doi-asserted-by":"publisher","unstructured":"Bernardi O, G (2010) O.: a linear algorithm for the random sampling from regular languages. Algorithmica 62:130\u2013145. https:\/\/doi.org\/10.1007\/s00453-010-9446-5","DOI":"10.1007\/s00453-010-9446-5"},{"key":"489_CR61","doi-asserted-by":"publisher","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In International Conference on Software Engineering, ICSE. https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"key":"489_CR62","doi-asserted-by":"publisher","unstructured":"Gaglione J, Neider D, Roy R, Topcu U, Xu Z (2022) Maxsat-based temporal logic inference from noisy data. Innovations In Syst And Softw Eng 18(3):427\u2013442. https:\/\/doi.org\/10.1007\/S11334-022-00444-8","DOI":"10.1007\/S11334-022-00444-8"},{"key":"489_CR63","doi-asserted-by":"publisher","unstructured":"Fainekos GE, Kress-Gazit H, Pappas GJ (2005) Temporal logic motion planning for mobile robots. In International Conference on Robotics and Automation, ICRA. https:\/\/doi.org\/10.1109\/ROBOT.2005.1570410","DOI":"10.1109\/ROBOT.2005.1570410"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00489-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00489-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00489-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T09:11:59Z","timestamp":1772788319000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00489-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":63,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2]]}},"alternative-id":["489"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00489-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"8 February 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declaration"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"2"}}