{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T11:45:04Z","timestamp":1778327104582,"version":"3.51.4"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,11,18]],"date-time":"2016-11-18T00:00:00Z","timestamp":1479427200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s10009-016-0442-1","type":"journal-article","created":{"date-parts":[[2016,11,18]],"date-time":"2016-11-18T10:20:49Z","timestamp":1479464449000},"page":"35-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Exact finite-state machine identification from scenarios and temporal properties"],"prefix":"10.1007","volume":"20","author":[{"given":"Vladimir","family":"Ulyantsev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Buzhinsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anatoly","family":"Shalyto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,18]]},"reference":[{"key":"442_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Hardware and Software: Verification and Testing, pp. 75\u201391. Springer (2014)","DOI":"10.1007\/978-3-319-13338-6_7"},{"key":"442_CR2","doi-asserted-by":"crossref","unstructured":"Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of SAT-based model checking techniques in an industrial environment. In: Correct Hardware Design and Verification Methods, pp. 254\u2013268. Springer (2005)","DOI":"10.1007\/11560548_20"},{"key":"442_CR3","doi-asserted-by":"crossref","unstructured":"Beschastnikh, I., Brun, Y., Schneider, S., Sloan, M., Ernst, M.D.: Leveraging existing instrumentation to automatically infer invariant-constrained models. In: Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, pp. 267\u2013277. ACM (2011)","DOI":"10.1145\/2025113.2025151"},{"key":"442_CR4","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"issue":"5\u20136","key":"442_CR5","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-013-0287-9","volume":"15","author":"R Bodik","year":"2013","unstructured":"Bodik, R., Jobstmann, B.: Algorithmic program synthesis: introduction. Int. J. Software Tools Technol. Trans. 15(5\u20136), 397\u2013411 (2013)","journal-title":"Int. J. Software Tools Technol. Trans."},{"key":"442_CR6","doi-asserted-by":"crossref","unstructured":"Broy, M., Jonsson, B., Katoen, J.P., Leucker, M., Pretschner, A. (eds.): Model-based testing of reactive systems: advanced lectures. Lecture Notes in Computer Science, vol. 3472. Springer (2005)","DOI":"10.1007\/b137241"},{"key":"442_CR7","doi-asserted-by":"crossref","unstructured":"Cheng, C.H., Huang, C.H., Ruess, H., Stattelmann, S.: G4LTL-ST: Automatic generation of PLC programs. In: Computer Aided Verification, pp. 541\u2013549. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_36"},{"key":"442_CR8","doi-asserted-by":"crossref","unstructured":"Chivilikhin, D., Ulyantsev, V.: MuACOsm: a new mutation-based ant colony optimization algorithm for learning finite-state machines. In: Proceedings of the 15th Annual Conference on Genetic and Evolutionary Computation (GECCO), pp. 511\u2013518. ACM (2013)","DOI":"10.1145\/2463372.2463440"},{"key":"442_CR9","doi-asserted-by":"crossref","unstructured":"Chivilikhin, D., Ulyantsev, V., Shalyto, A.: Combining exact and metaheuristic techniques for learning extended finite-state machines from test scenarios and temporal properties. In: Proceedings of the 13th International Conference on Machine Learning and Applications (ICMLA), pp. 350\u2013355. IEEE (2014)","DOI":"10.1109\/ICMLA.2014.62"},{"key":"442_CR10","doi-asserted-by":"crossref","unstructured":"Chongstitvatana, P., Aporntewan, C.: Improving correctness of finite-state machine synthesis from multiple partial input\/output sequences. In: Proceedings of the 1st NASA\/DoD Workshop on Evolvable Hardware, pp. 262\u2013266. IEEE (1999)","DOI":"10.1109\/EH.1999.785463"},{"issue":"3","key":"442_CR11","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"4","author":"TS Chow","year":"1978","unstructured":"Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Software Eng. 4(3), 178\u2013187 (1978)","journal-title":"IEEE Trans. Software Eng."},{"key":"442_CR12","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT press, USA (1999)"},{"key":"442_CR13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1290.001.0001","volume-title":"Ant colony optimization","author":"M Dorigo","year":"2004","unstructured":"Dorigo, M., St\u00fctzle, T.: Ant colony optimization. MIT Press, USA (2004)"},{"key":"442_CR14","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A.: Manipulating LTL formulas using Spot 1.0. In: Automated technology for verification and analysis, pp. 442\u2013445. Springer (2013)","DOI":"10.1007\/978-3-319-02444-8_31"},{"issue":"4","key":"442_CR15","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comp. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comp. Sci."},{"key":"442_CR16","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Unbeast: Symbolic bounded synthesis. In: Abdulla, P., Leino, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 6605, pp. 272\u2013275. Springer, Berlin Heidelberg (2011)","DOI":"10.1007\/978-3-642-19835-9_25"},{"issue":"2","key":"442_CR17","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/s10703-011-0137-x","volume":"40","author":"R Ehlers","year":"2012","unstructured":"Ehlers, R.: Symbolic bounded synthesis. Formal Methods Syst. Design 40(2), 232\u2013262 (2012)","journal-title":"Formal Methods Syst. Design"},{"key":"442_CR18","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.F.: An antichain algorithm for LTL realizability. In: Computer Aided Verification, pp. 263\u2013277. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"442_CR19","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 219\u2013234. Springer (2012)","DOI":"10.1007\/978-3-642-27940-9_15"},{"issue":"5\u20136","key":"442_CR20","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Software Tools Technol. Trans. 15(5\u20136), 519\u2013539 (2013)","journal-title":"Int. J. Software Tools Technol. Trans."},{"issue":"3","key":"442_CR21","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1016\/S0019-9958(78)90562-4","volume":"37","author":"EM Gold","year":"1978","unstructured":"Gold, E.M.: Complexity of automaton identification from given data. Inform. Contr. 37(3), 302\u2013320 (1978)","journal-title":"Inform. Contr."},{"key":"442_CR22","doi-asserted-by":"crossref","unstructured":"Heule, M.J., Verwer, S.: Exact DFA identification using SAT solvers. In: Grammatical Inference: Theoretical Results and Applications, pp. 66\u201379. Springer (2010)","DOI":"10.1007\/978-3-642-15488-1_7"},{"issue":"4","key":"442_CR23","doi-asserted-by":"crossref","first-page":"825","DOI":"10.1007\/s10664-012-9222-z","volume":"18","author":"MJ Heule","year":"2013","unstructured":"Heule, M.J., Verwer, S.: Software model synthesis using satisfiability solvers. Empir. Software Eng. 18(4), 825\u2013856 (2013)","journal-title":"Empir. Software Eng."},{"key":"442_CR24","unstructured":"H\u00f6lldobler, S., Nguyen, V.H.: On SAT-encodings of the at-most-one constraint. In: Proceedings of the 12th International Workshop on Constraint Modelling and Reformulation, Uppsala, Sweden, pp. 16\u201320 (2013)"},{"issue":"3","key":"442_CR25","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.entcs.2006.12.020","volume":"174","author":"PB Jackson","year":"2007","unstructured":"Jackson, P.B., Sheridan, D.: A compact linear translation for bounded model checking. Electr. Notes Theor. Comp. Sci. 174(3), 17\u201330 (2007)","journal-title":"Electr. Notes Theor. Comp. Sci."},{"key":"442_CR26","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer Aided Design (FMCAD), pp. 117\u2013124. IEEE (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"442_CR27","doi-asserted-by":"crossref","unstructured":"Lang, K.J., Pearlmutter, B.A., Price, R.A.: Results of the Abbadingo One DFA learning competition and a new evidence-driven state merging algorithm. In: Grammatical Inference, pp. 1\u201312. Springer (1998)","DOI":"10.1007\/BFb0054059"},{"key":"442_CR28","doi-asserted-by":"crossref","unstructured":"Lo, D., Mariani, L., Pezz\u00e8, M.: Automatic steering of behavioral model inference. In: 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC-FSE), pp. 345\u2013354. ACM (2009)","DOI":"10.1145\/1595696.1595761"},{"key":"442_CR29","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Lecture Notes in Computer Science (to appear). Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_29"},{"key":"442_CR30","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3927.001.0001","volume-title":"An introduction to genetic algorithms","author":"M Mitchell","year":"1998","unstructured":"Mitchell, M.: An introduction to genetic algorithms. MIT press, USA (1998)"},{"key":"442_CR31","doi-asserted-by":"crossref","unstructured":"Ohmann, T., Herzberg, M., Fiss, S., Halbert, A., Palyart, M., Beschastnikh, I., Brun, Y.: Behavioral resource-aware model inference. In: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE), pp. 19\u201330. ACM (2014)","DOI":"10.1145\/2642937.2642988"},{"key":"442_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"442_CR33","unstructured":"Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992)"},{"key":"442_CR34","doi-asserted-by":"crossref","unstructured":"Tsarev, F., Egorov, K.: Finite state machine induction using genetic algorithm based on testing and model checking. In: 13th Annual Conference Companion on Genetic and Evolutionary Computation (GECCO), pp. 759\u2013762. ACM (2011)","DOI":"10.1145\/2001858.2002085"},{"key":"442_CR35","doi-asserted-by":"crossref","unstructured":"Ulyantsev, V., Tsarev, F.: Extended finite-state machine induction using SAT-solver. In: Proceedings of the 14th IFAC Symposium \u201cInformation Control Problems in Manufacturing (INCOM)\u201d, pp. 512\u2013517. IFAC (2012)","DOI":"10.3182\/20120523-3-RO-2023.00179"},{"key":"442_CR36","doi-asserted-by":"crossref","unstructured":"Ulyantsev, V., Zakirzyanov, I., Shalyto, A.: BFS-based symmetry breaking predicates for DFA identification. In: Language and Automata Theory and Applications, pp. 611\u2013622. Springer (2015)","DOI":"10.1007\/978-3-319-15579-1_48"},{"key":"442_CR37","unstructured":"Vyatkin, V.: IEC 61499 function blocks for embedded and distributed control systems design, Second ed. Instrumentation Society of America (2012)"},{"key":"442_CR38","doi-asserted-by":"crossref","unstructured":"Walkinshaw, N., Bogdanov, K.: Inferring finite-state models with temporal constraints. In: Proceedings of the 23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 248\u2013257. IEEE Computer Society (2008)","DOI":"10.1109\/ASE.2008.35"},{"issue":"3","key":"442_CR39","doi-asserted-by":"crossref","first-page":"811","DOI":"10.1007\/s10664-015-9367-7","volume":"21","author":"N Walkinshaw","year":"2016","unstructured":"Walkinshaw, N., Taylor, R., Derrick, J.: Inferring extended finite state machine models from software executions. Empir. Software Eng. 21(3), 811\u2013853 (2016)","journal-title":"Empir. Software Eng."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0442-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0442-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0442-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T18:44:16Z","timestamp":1749753856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0442-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,18]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["442"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0442-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,18]]}}}