{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:00:01Z","timestamp":1773615601476,"version":"3.50.1"},"reference-count":23,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"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":[[2021,12]]},"DOI":"10.3103\/s0146411621070038","type":"journal-article","created":{"date-parts":[[2022,2,1]],"date-time":"2022-02-01T09:15:43Z","timestamp":1643706943000},"page":"763-775","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["A Temporal Logic for Programmable Logic Controllers"],"prefix":"10.3103","volume":"55","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9734-3808","authenticated-orcid":false,"given":"N. O.","family":"Garanina","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9574-128X","authenticated-orcid":false,"given":"I. S.","family":"Anureev","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8198-3197","authenticated-orcid":false,"given":"V. E.","family":"Zyubin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5183-9736","authenticated-orcid":false,"given":"S. M.","family":"Staroletov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9148-946X","authenticated-orcid":false,"given":"T. V.","family":"Liakh","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7468-0411","authenticated-orcid":false,"given":"A. S.","family":"Rozov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3857-9380","authenticated-orcid":false,"given":"S. P.","family":"Gorlatch","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2022,2,1]]},"reference":[{"key":"7403_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.18255\/1818-1015-2019-4-475-487","volume":"26","author":"I. Anureev","year":"2019","unstructured":"Anureev, I., Operational semantics of annotated Reflex programs, Model. Anal. Inf. Sist., 2019, vol. 26, no. 6, pp. 181\u2013192.","journal-title":"Model. Anal. Inf. Sist."},{"key":"7403_CR2","doi-asserted-by":"crossref","unstructured":"Anureev, I., Garanina, N., Liakh, T., Rozov, A., and Zyubin, V., Towards safe cyber-physical systems: The Reflex language and its transformational semantics, IEEE International Siberian Conference on Control and Communications, IEEE, 2019, pp. 18\u201320.","DOI":"10.1109\/SIBCON.2019.8729633"},{"key":"7403_CR3","volume-title":"Verification and optimization of a PLC control schedule, SPIN 2000 \u2013 SPIN Model Checking and Software Verification","author":"E. Brinksma","year":"2000","unstructured":"Brinksma, E. and Mader, A., Verification and optimization of a PLC control schedule, SPIN 2000 \u2013 SPIN Model Checking and Software Verification, Springer, 2000, pp. 73\u201392."},{"key":"7403_CR4","doi-asserted-by":"crossref","unstructured":"Gourcuff, V., de Smet, O., and Faure, J.-M., Improving large-sized PLC programs verification using abstractions, IFAC Proc. Vol., 2008, vol. 41, no. 2, pp. 5101\u20135106.","DOI":"10.3182\/20080706-5-KR-1001.00857"},{"key":"7403_CR5","series-title":"A classification of PLC models and applications","volume-title":"Discrete Event Systems","author":"A. Mader","year":"2000","unstructured":"Mader, A., A classification of PLC models and applications, in Discrete Event Systems, Springer, 2000, pp. 239\u2013246."},{"key":"7403_CR6","doi-asserted-by":"crossref","unstructured":"Wan, H., Chen, G., Song, X., and Gu, M., Formalization and verification of PLC timers in Coq, Proc. of 33rd Annual IEEE International Computer Software and Applications Conference, IEEE, 2009, pp. 315\u2013323.","DOI":"10.1109\/COMPSAC.2009.49"},{"key":"7403_CR7","doi-asserted-by":"crossref","unstructured":"Yoo, J., Cha, S., and Jee, E., A verification framework for FBD based software in nuclear power plants, Proc. of 15th Asia-Pacific Software Engineering Conference, IEEE, 2008, pp. 385\u2013392.","DOI":"10.1109\/APSEC.2008.26"},{"key":"7403_CR8","first-page":"25","volume":"32","author":"D. Bulavskij","year":"1996","unstructured":"Bulavskij, D., Zyubin, V., Karlson, N., Krivoruchko, V., and Mironov, V., An automated control system for a silicon single-crystal growth furnace, Optoelectron., Instrum. Data Process., 1996, vol. 32, no. 2, pp. 25\u201330.","journal-title":"Optoelectron., Instrum. Data Process."},{"key":"7403_CR9","doi-asserted-by":"publisher","first-page":"187","DOI":"10.3103\/S8756699016020126","volume":"52","author":"P.G. Kovadlo","year":"2016","unstructured":"Kovadlo, P.G., Lubkov, A., Bevzov, A., et al., Automation system for the large solar vacuum telescope, Optoelectron., Instrum. Data Process., 2016, vol. 52, pp. 187\u2013195.","journal-title":"Optoelectron., Instrum. Data Process."},{"key":"7403_CR10","series-title":"ch.\u00a018","volume-title":"Handbook of Model Checking","author":"A. Gupta","year":"2018","unstructured":"Gupta, A., Kahlon, V., Qadeer, S., and Touili, T., Handbook of Model Checking, Springer Int. Publ., 2018, ch.\u00a018, pp. 573\u2013577."},{"key":"7403_CR11","series-title":"ch. 1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"E.M. Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., and Veith, H., Handbook of Model Checking, Springer Int. Publ., 2018, ch. 1, pp. 1\u201313."},{"key":"7403_CR12","doi-asserted-by":"crossref","unstructured":"Dierks, H., PLC-automata: A new class of implementable real-time automata, in International AMAST Workshop on Aspects of Real-Time Systems and Concurrent and Distributed Software, Springer, 1997, vol. 1231, pp. 111\u2013125.","DOI":"10.1007\/3-540-63010-4_8"},{"key":"7403_CR13","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1007\/s10270-014-0448-7","volume":"4","author":"T. Ovatman","year":"2016","unstructured":"Ovatman, T., An overview of model checking practices on verification of PLC software, Software Syst. Model., 2016, vol. 4, no. 15, pp. 937\u2013960.","journal-title":"Software Syst. Model."},{"key":"7403_CR14","doi-asserted-by":"publisher","first-page":"510","DOI":"10.3103\/S0146411616070130","volume":"7","author":"E. Kuzmin","year":"2016","unstructured":"Kuzmin, E., Ryabukhin, D., and Sokolov, V.A., On the expressiveness of the approach to constructing PLC-programs by LTL-specification, Autom. Control Comput. Sci., 2016, vol. 7, no. 50, pp. 510\u2013519.","journal-title":"Autom. Control Comput. Sci."},{"key":"7403_CR15","doi-asserted-by":"crossref","unstructured":"Zhang, M., Towards automated safety vetting of PLC code in real-world plants, IEEE Symposium on Security and Privacy, IEEE, 2019, pp. 522\u2013538.","DOI":"10.1109\/SP.2019.00034"},{"key":"7403_CR16","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"A. Rajeev","year":"1994","unstructured":"Rajeev, A. and Henzinger, T., A really temporal logic, J. ACM, 1994, vol. 41, no. 1, pp. 181\u2013203.","journal-title":"J. ACM"},{"key":"7403_CR17","doi-asserted-by":"crossref","unstructured":"Xiong, J., A user-friendly verification approach for IEC 61131-3 PLC programs, Electronics, 2020, vol. 4, no. 9.","DOI":"10.3390\/electronics9040572"},{"key":"7403_CR18","doi-asserted-by":"crossref","unstructured":"Beckert, B., Regression verification for programmable logic controller software, International Conference on Formal Engineering Methods, Springer, 2015, vol. 9407.","DOI":"10.1007\/978-3-319-25423-4_15"},{"key":"7403_CR19","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1007\/s10664-012-9232-x","volume":"3","author":"O. Ljungkrantz","year":"2014","unstructured":"Ljungkrantz, O., An empirical study of control logic specifications for programmable logic controllers, Empirical Software Eng., 2014, vol. 3, no. 19, pp. 655\u2013677.","journal-title":"Empirical Software Eng."},{"key":"7403_CR20","doi-asserted-by":"crossref","unstructured":"Ljungkrantz, O., \u00c5kesson, K., Fabian, M., and Yuan, C., A formal specification language for PLC-based control logic, 8th IEEE International Conference on Industrial Informatics, IEEE, 2010, pp. 1067\u20131072.","DOI":"10.1109\/INDIN.2010.5549591"},{"key":"7403_CR21","series-title":"Monitoring temporal properties of continuous signals","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O. Maler","year":"2004","unstructured":"Maler, O. and Nickovic, D., Monitoring temporal properties of continuous signals, in Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Springer, 2004, pp. 152\u2013166."},{"key":"7403_CR22","first-page":"33","volume":"17","author":"N. Garanina","year":"2020","unstructured":"Garanina, N., Anureev, I., Zyubin, V., Rozov, A., Liakh, T., and Gorlatch, S., Reasoning about programmable logic controllers, Syst. Inf., 2020, vol. 17, pp. 33\u201342.","journal-title":"Syst. Inf."},{"key":"7403_CR23","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G., The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411621070038.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411621070038","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411621070038.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:02:05Z","timestamp":1773612125000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411621070038"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":23,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["7403"],"URL":"https:\/\/doi.org\/10.3103\/s0146411621070038","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"12 November 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 December 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 December 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2022","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"}}]}}