{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:03:32Z","timestamp":1773615812209,"version":"3.50.1"},"reference-count":14,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"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":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.3103\/s0146411620070135","type":"journal-article","created":{"date-parts":[[2021,2,8]],"date-time":"2021-02-08T12:46:46Z","timestamp":1612788406000},"page":"630-644","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of Three-Valued Digital Waveforms"],"prefix":"10.3103","volume":"54","author":[{"given":"N. Yu.","family":"Kutsak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V. V.","family":"Podymov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2021,2,8]]},"reference":[{"key":"7280_CR1","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C. and Katoen, J.P., Principles of Model Checking, Cambridge: The MIT Press, 2008."},{"key":"7280_CR2","volume-title":"Digital Design and Computer Architecture","author":"S. Harris","year":"2012","unstructured":"Harris, S. and Harris, D., Digital Design and Computer Architecture, San Francisco: Morgan Kaufmann Publishers Inc., 2012, 2nd ed."},{"key":"7280_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58940-9","volume-title":"Algorithms and Data Structures in VLSI Design: OBDD \u2013 Foundations and Applications","author":"C. Meinel","year":"1998","unstructured":"Meinel, C. and Theobald, T., Algorithms and Data Structures in VLSI Design: OBDD \u2013 Foundations and Applications, Berlin: Springer-Verlag, 1998."},{"key":"7280_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C. Kern","year":"1999","unstructured":"Kern, C. and Greenstreet, M.R., Formal verification in hardware design: A survey, ACM Trans. Des. Autom. Electron. Syst., 1999, vol. 4, no. 2, pp. 123\u2013193.","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"7280_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03809-3","volume-title":"Introduction to Formal Hardware Verification","author":"T. Kropf","year":"1999","unstructured":"Kropf, T., Introduction to Formal Hardware Verification, Berlin: Springer-Verlag, 1999."},{"key":"7280_CR6","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0023717","volume":"531","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E. and Seger, C.J.H., Formal verification of digital circuits using symbolic ternary system models, Lect. Notes Comput. Sci., 1991, vol. 531, pp. 33\u201343.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7280_CR7","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-35632-2_24","volume":"7687","author":"K. Baldor","year":"2013","unstructured":"Baldor, K. and Niu, J., Monitoring dense-time, continuous-semantics, metric temporal logic, Lect. Notes Comput. Sci., 2013, vol. 7687, pp. 245\u2013259.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7280_CR8","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s00236-017-0295-4","volume":"55","author":"D. Basin","year":"2018","unstructured":"Basin, D., Klaedtke, F., and Z\u0103linescu, E., Algorithms for monitoring real-time properties, Acta Inf., 2018, vol.\u00a055, no. 4, pp. 309\u2013338.","journal-title":"Acta Inf."},{"key":"7280_CR9","unstructured":"Yablonsky, S.V., Vvedenie v diskretnuyu matematiku (Introduction to Discrete Mathematics), Moscow: Nauka, 1986."},{"key":"7280_CR10","doi-asserted-by":"publisher","first-page":"150","DOI":"10.2307\/2267778","volume":"3","author":"S.C. Kleene","year":"1938","unstructured":"Kleene, S.C., On notation for ordinal numbers, J. Symbolic Logic, 1938, vol. 3, no. 4, pp. 150\u2013155.","journal-title":"J. Symbolic Logic"},{"key":"7280_CR11","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C., Introduction to Metamathematics, Amsterdam: North-Holland Pub. Co., 1952."},{"key":"7280_CR12","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume":"1633","author":"G. Bruns","year":"1991","unstructured":"Bruns, G. and Godefroid, P., Model checking partial state spaces with 3-valued temporal logics, Lect. Notes Comput. Sci., 1991, vol. 1633, pp. 274\u2013287.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7280_CR13","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-45139-0_3","volume":"2057","author":"M. Chechik","year":"2001","unstructured":"Chechik, M., Devereux, B., and Gurfinkel, A., Model-checking infinite state-space systems with fine-grained abstractions using SPIN, Lect. Notes Comput. Sci., 2001, vol. 2057, pp. 16\u201336.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7280_CR14","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., and Schnoebelen, P., Temporal logic with forgettable past, Proceedings of the 17th\u00a0Annual IEEE Symposium on Logic in Computer Science, Washington, DC, 2002, pp. 383\u2013392.","DOI":"10.1109\/LICS.2002.1029846"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411620070135.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411620070135","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411620070135.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:04:59Z","timestamp":1773612299000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411620070135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12]]},"references-count":14,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["7280"],"URL":"https:\/\/doi.org\/10.3103\/s0146411620070135","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12]]},"assertion":[{"value":"28 June 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 September 2019","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 September 2019","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}