LTL-СПЕЦИФИКАЦИЯ ДЛЯ РАЗРАБОТКИ И ВЕРИФИКАЦИИ ПРОГРАММ ЛОГИЧЕСКОГО УПРАВЛЕНИЯ В СИСТЕМАХ С ОБРАТНОЙ СВЯЗЬЮ (2024)
Статья продолжает цикл публикаций по разработке и верификации управляющих программ на основе LTL-спецификаций специального вида. Ранее для описания строго детерминированного поведения программ была предложена декларативная LTL-спецификация, проработаны способы её верификации и трансляции: для верификации используется инструмент проверки модели nuXmv, трансляция осуществляется в императивный язык программирования ST для программируемых логических контроллеров. При верификации декларативной LTL-спецификации поведения программ может возникнуть необходимость в моделировании поведения её окружения. В общем случае требуется обеспечить возможность построения замкнутых систем «программа-окружение». В настоящей работе для описания поведения окружения программ логического управления предложена LTL-спецификация ограниченно недетерминированного поведения булевой переменной. Данная спецификация позволяет задавать поведение булевых сигналов обратной связи, а также условия справедливости для исключения нереалистичных сценариев поведения. В статье предлагается подход к разработке и верификации программ логического управления, в рамках которого модель поведения окружения программы описывается в виде ограничений на поведение её входных сигналов, что позволяет избежать отдельного детального представления процессов функционирования окружения. В результате полученная модель поведения замкнутой системы «программа-окружение» даёт ряд преимуществ: упрощение процесса моделирования, сокращение пространства состояний проверяемой модели, снижение времени верификации. При невозможности сведения поведения окружения к поведению имеющихся входных сигналов данный подход предполагает применение «мнимых» датчиков - дополнительных булевых переменных, использующихся как вспомогательное средство для описания поведения входных сигналов. Цель введения мнимых датчиков состоит в компенсации недостающих датчиков для отслеживания специфического поведения отдельных элементов окружения, которое необходимо учесть при задании реалистичного поведения входов программы логического управления. Предложенный подход к разработке и верификации программ с учётом поведения окружения (объекта управления) демонстрируется на примере промышленной установки для литья пластмасс.
Идентификаторы и классификаторы
- eLIBRARY ID
- 69174193
УПО работает циклически: считывает входные данные из окружения, выполняет вычисления, обновляет выходные данные для окружения. Таким образом, УПО КФС представляет собой реагирующую систему [8], так как постоянно взаимодействует со своим окружением. Совокупность всех входных и выходных сигналов УПО образует его интерфейс. Любой выходной сигнал УПО является сигналом прямой связи (feedforward) с ОУ. Входной сигнал УПО, который информирует о реакции ОУ на некоторое управляющее воздействие, является сигналом обратной связи (feedback). Система с прямой и обратной связями образует замкнутый контур (closed-loop), поэтому такие системы называются замкнутыми.
Список литературы
-
S. Oks and et al., “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook”, Information Systems Frontiers, pp. 1-42, 2022,. DOI: 10.1007/s10796-022-10252-x
-
K. Zhang, Y. Shi, S. Karnouskos, T. Sauter, H. Fang, and A. W. Colombo, “Advancements in Industrial Cyber-Physical Systems: An Overview and Perspectives”, IEEE Transactions on Industrial Informatics, vol. 19, no. 1, pp. 716-729, 2023,. DOI: 10.1109/TII.2022.3199481 EDN: QTNTCR
-
S. J. Oks, Industrial Cyber-Physical Systems: Advancing Industry 4.0 from Vision to Application, 1st ed. Springer, 2024.
-
C. Dey and S. K. Sen, Industrial Automation Technologies, 1st ed. CRC Press, 2020.
-
K. Thramboulidis, “A Cyber-Physical System-Based Approach for Industrial Automation Systems”, Computers in Industry, vol. 72, pp. 92-102, 2015,. DOI: 10.1016/j.compind.2015.04.006
-
“IEC 61131-1:2003 Programmable controllers - Part 1: General information”. [Online]. Available: https://webstore.iec.ch/publication/4550.
-
R. Langmann and L. F. Rojas-Peña, “A PLC as an Industry 4.0 Component”, in Remote Engineering and Virtual Instrumentation, 2016, pp. 10-15,. DOI: 10.1109/REV.2016.7444433
-
D. Harel and A. Pnueli, “On the Development of Reactive Systems”, in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477-498,. DOI: 10.1007/978-3-642-82453-1_17
-
A. Maurya and D. Kumar, “Reliability of safety-critical systems: A state-of-the-art review”, Quality and Reliability Engineering International, vol. 36, Aug. 2020,. DOI: 10.1002/qre.2715
-
D. J. Smith and K. G. L. Simpson, The Safety Critical Systems Handbook, 5th ed. Butterworth-Heinemann, 2020. -
V. Vyatkin, "Software Engineering in Industrial Automation: State-of-the-Art Review", IEEE Transactions on Industrial Informatics, vol. 9, no. 3, pp. 1234-1249, 2013,. DOI: 10.1109/TII.2013.2258165 EDN: RHOCMH -
S. Mitra, Verifying Cyber-Physical Systems: A Path to Safe Autonomy. MIT Press, 2021. -
V. D'Silva, D. Kroening, and G. Weissenbacher, "A Survey of Automated Techniques for Formal Software Verification", in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008, vol. 27, no. 7, pp. 1165-1178,. DOI: 10.1109/TCAD.2008.923410 -
R. Sinha, S. Patil, L. Gomes, and V. Vyatkin, "A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems", IEEE Transactions on Industrial Informatics, vol. 15, no. 7, pp. 3772-3783, 2019,. DOI: 10.1109/TII.2019.2908665 EDN: JOSVGL -
E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed., vol. 10. Springer, 2018. -
Y. G. Karpov, MODEL CHECKING. Verification of Parallel and Distributed Program Systems. BHV-Peterburg, 2010, p. 560. -
E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002, p. 416. -
A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends", in Current Trends in Concurrency, 1986, vol. 224, pp. 510-584,. DOI: 10.1007/BFb0027047 -
K. Schneider, J. Shabolt, and J. G. Taylor, Verification of reactive systems: formal methods and algorithms, 1st ed. Springer, 2004. -
Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, 1st ed. Springer, 2012. -
J. Galv ao, C. Oliveira, and et al., "Formal Verification: Focused on the Verification Using a Plant Model", in Innovation, Engineering and Entrepreneurship, 2019, pp. 124-131,. DOI: 10.1007/978-3-319-91334-6_18 -
G. Frey and L. Litz, "Formal Methods in PLC Programming", in IEEE International Conference On Systems, Man and Cybernetics, 2000, vol. 4, pp. 2431-2436,. DOI: 10.1109/ICSMC.2000.884356 -
J. M. Machado, B. Denis, and et al., "Logic Controllers Dependability Verification Using a Plant Model", IFAC Proceedings Volumes, vol. 39, no. 17, pp. 37-42, 2006,. DOI: 10.3182/20060926-3-PL-4904.00007 -
A. A. Shalyto, "Logic Control and ‘Reactive' Systems: Algorithmization and Programming", Automation and Remote Control, vol. 62, no. 1, pp. 1-29, 2001, :1002837232103. DOI: 10.1023/A EDN: DDYOKV -
E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, "Modeling a Consistent Behavior of PLC-Sensors", Modeling and Analysis of Information Systems, vol. 21, no. 4, pp. 75-90, 2014,. DOI: 10.18255/1818-1015-2014-4-75-90 EDN: SVJRWR -
E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, "Modeling a Consistent Behavior of PLC-Sensors", Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602-614, 2014,. DOI: 10.3103/S0146411614070256 EDN: WVVWCL -
M. V. Neyzov and E. V. Kuzmin, "LTL-specification for Development and Verification of Control Programs", Modeling and Analysis of Information Systems, vol. 30, no. 4, pp. 308-339, 2023,. DOI: 10.18255/1818-1015-2023-4-308-339 EDN: LDUGES -
M. V. Neyzov and E. V. Kuzmin, "Verification of Declarative LTL-specification of Control Programs Behavior", Modeling and Analysis of Information Systems, vol. 31, no. 2, pp. 120-141, 2024,. DOI: 10.18255/1818-1015-2024-2-120-141 EDN: THXCOX -
"nuXmv Home". [Online]. Available: https://nuxmv.fbk.eu/. -
M. Frappier, B. Fraikin, R. Chossart, R. Chane-Yack-Fa, and M. Ouenzar, "Comparison of Model Checking Tools for Information Systems", in Formal Methods and Software Engineering, 2010, vol. 6447, pp. 581-596,. DOI: 10.1007/978-3-642-16901-4_38 -
"Spot Home". [Online]. Available: https://spot.lre.epita.fr/. -
M. Xavier, S. Patil, V. Dubinin, and V. Vyatkin, "Formal Modelling, Analysis, and Synthesis of Modular Industrial Systems Inspired by Net Condition/Event Systems", in Applications and Theory of Petri Nets and Concurrency, 2023, pp. 16-33,. DOI: 10.1007/978-3-031-33620-1_2 -
S. Patil, S. Bhadra, and V. Vyatkin, "Closed-Loop Formal Verification Framework with Non-Determinism, Configurable by Meta-Modelling", in IEEE Industrial Electronics Society, 2011, pp. 3770-3775,. DOI: 10.1109/IECON.2011.6119923 -
S. Patil, V. Vyatkin, and M. Sorouri, "Formal Verification of Intelligent Mechatronic Systems with Decentralized Control Logic", in IEEE Emerging Technologies & Factory Automation, 2012, pp. 1-7,. DOI: 10.1109/ETFA.2012.6489678 -
S. Patil, V. Vyatkin, and C. Pang, "Counterexample-Guided Simulation Framework for Formal Verification of Flexible Automation Systems", in IEEE Industrial Informatics, 2015, pp. 1192-1197,. DOI: 10.1109/INDIN.2015.7281905 -
C. Gerber, S. Preuße, and H.-M. Hanisch, "A Complete Framework for Controller Verification in Manufacturing", in IEEE Emerging Technologies & Factory Automation, 2010, pp. 1-9,. DOI: 10.1109/ETFA.2010.5641220 -
S. Preuße, H.-C. Lapp, and H.-M. Hanisch, "Closed-Loop System Modeling, Validation, and Verification", in IEEE Emerging Technologies & Factory Automation, 2012, pp. 1-8,. DOI: 10.1109/ETFA.2012.6489679 -
J. Machado, B. Denis, and J.-J. Lesage, "A Generic Approach to Build Plant Models for DES Verification Purposes", in International Workshop on Discrete Event Systems, 2006, pp. 407-412,. DOI: 10.1109/WODES.2006.382508 -
J. Machado, E. Seabra, and et al., "Safe Controllers Design for Industrial Automation Systems", Computers & Industrial Engineering, vol. 60, no. 4, pp. 635-653, 2011,. DOI: 10.1016/j.cie.2010.12.020 EDN: OEMCNJ -
M. Perin and J.-M. Faure, "Building Meaningful Timed Models of Closed-Loop DES for Verification Purposes", Control Engineering Practice, vol. 21, no. 11, pp. 1620-1639, 2013,. DOI: 10.1016/j.conengprac.2012.05.002 -
V. Vyatkin, H.-M. Hanisch, C. Pang, and C.-H. Yang, "Closed-Loop Modeling in Future Automation System Engineering and Validation", IEEE Transactions on Systems, Man, and Cybernetics, Part C (Applications and Reviews), vol. 39, no. 1, pp. 17-28, 2009,. DOI: 10.1109/TSMCC.2008.2005785 -
A. Lobov, J. L. M. Lastra, and R. Tuokko, "Application of UML in Plant Modeling for Model-Based Verification: UML Translation to TNCES", in IEEE Industrial Informatics, 2005, pp. 495-501,. DOI: 10.1109/INDIN.2005.1560426 -
A. Lobov, J. L. M. Lastra, and R. Tuokko, "On Controller and Plant Modeling for Model-Based Formal Verification", in IEEE Emerging Technologies and Factory Automation, 2005, vol. 1, pp. 121-128,. DOI: 10.1109/ETFA.2005.1612510 -
S. Preu\sse, Technologies for Engineering Manufacturing Systems Control in Closed Loop, 10th ed. Logos Verlag Berlin GmbH, 2013. -
H.-M. Hanisch, "Closed-Loop Modeling and Related Problems of Embedded Control Systems in Engineering", in Abstract State Machines 2004. Advances in Theory and Practice, 2004, pp. 6-19,. DOI: 10.1007/978-3-540-24773-9_2 -
C. Pang and V. Vyatkin, "Systematic Closed-Loop Modelling in IEC 61499 Function Blocks: A Case Study", IFAC Proceedings Volumes, vol. 42, pp. 199-204, 2009,. DOI: 10.3182/20090603-3-RU-2001.0264 -
D. Drozdov, S. Patil, V. Dubinin, and V. Vyatkin, "Formal Verification of Cyber-Physical Automation Systems Modelled with Timed Block Diagrams", in IEEE Industrial Electronics, 2016, pp. 316-321,. DOI: 10.1109/ISIE.2016.7744910 EDN: YUWSZZ -
M. Xavier, S. Patil, and V. Vyatkin, "Cyber-Physical Automation Systems Modelling with IEC 61499 for their Formal Verification", in IEEE Industrial Informatics, 2021, pp. 1-6,. DOI: 10.1109/INDIN45523.2021.9557416 -
G. Lilli et al., "Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499", IEEE Open Journal of the Industrial Electronics Society, vol. 4, pp. 417-431, 2023,. DOI: 10.1109/OJIES.2023.3321084 EDN: TIPGEM -
N. O. Garanina, S. M. Staroletov, V. E. Zyubin, and I. S. Anureev, "Model Checking Programs in Process-Oriented IEC 61131-3 Structured Text", Modeling and Analysis of Information Systems, vol. 31, no. 1, pp. 32-53, 2024,. DOI: 10.18255/1818-1015-2024-1-32-53 EDN: WSZBTV -
N. Halbwachs, F. Lagnier, and C. Ratel, "Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE", IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 785-793, 1992,. DOI: 10.1109/32.159839 -
"IEC 61499-1:2012 Function blocks - Part 1: Architecture". [Online]. Available: https://webstore.iec.ch/publication/5506. -
V. E. Zyubin, A. S. Rozov, I. S. Anureev, N. O. Garanina, and V. Vyatkin, "poST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language", IEEE Access, vol. 10, pp. 35238-35250, 2022,. DOI: 10.1109/ACCESS.2022.3157601 EDN: JQKGUE -
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The Synchronous Data Flow Programming Language LUSTRE", Proceedings of the IEEE, vol. 79, no. 9, pp. 1305-1320, 1991,. DOI: 10.1109/5.97300 -
A. Champion, A. Gurfinkel, and et al., "CoCoSpec: A Mode-Aware Contract Language for Reactive Systems", in Software Engineering and Formal Methods, 2016, vol. 9763, pp. 347-366,. DOI: 10.1007/978-3-319-41591-8_24 -
A. Benveniste, P. Caspi, and et al., "The Synchronous Languages 12 Years Later", Proceedings of the IEEE, vol. 91, no. 1, pp. 64-83, 2003,. DOI: 10.1109/JPROC.2002.805826 -
A. Bouajjani, J. C. Fernandez, and N. Halbwachs, "On the Verification of Safety Properties", Rapport Technique SPECTRE L12, 1990. -
P. Raymond, "Synchronous Program Verification with Lustre/Lesar", in Modeling and Verification of Real-Time Systems, John Wiley & Sons, 2008, pp. 171-206. -
A. Champion, A. Mebsout, C. Sticksel, and C. Tinelli, "The Kind 2 Model Checker", in Computer Aided Verification, 2016, vol. 9780, pp. 510-517,. DOI: 10.1007/978-3-319-41540-6_29 -
N. Halbwachs, Synchronous Programming of Reactive Systems. Springer, 1993. -
M. Sirjani, E. A. Lee, and E. Khamespanah, "Verification of Cyberphysical Systems", Mathematics, vol. 8, no. 7, 2020,. DOI: 10.3390/math8071068 -
S. Lin et al., "Towards Building Verifiable CPS using Lingua Franca", ACM Transactions on Embedded Computing Systems, vol. 22, no. 5s, pp. 1-24, 2023,. DOI: 10.1145/3609134 -
P. Raymond, Y. Roux, and E. Jahier, "Lutin: A Language for Specifying and Executing Reactive Scenarios", EURASIP Journal on Embedded Systems, vol. 2008, pp. 1-11, 2008,. DOI: 10.1155/2008/753821 -
B. Finkbeiner, "Synthesis of Reactive Systems", Dependable Software Systems Engineering, vol. 45, pp. 72-98, 2016,. DOI: 10.3233/978-1-61499-627-9-72 -
N. Piterman, A. Pnueli, and Y. Sa'ar, "Synthesis of Reactive (1) Designs", in Verification, Model Checking, and Abstract Interpretation, 2006, vol. 3855, pp. 364-380,. DOI: 10.1007/11609773_24 -
M. Roth, L. Litz, and J.-J. Lesage, "Identification of Discrete Event Systems: Implementation Issues and Model Completeness", in Informatics in Control, Automation and Robotics, 2010, vol. 3, pp. 73-80. -
I. Buzhinsky and V. Vyatkin, "Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties", IEEE Transactions on Industrial Informatics, vol. 13, no. 4, pp. 1521-1530, 2017,. DOI: 10.1109/TII.2017.2670146 EDN: NBRWVZ -
P. Ovsiannikova, D. Chivilikhin, V. Ulyantsev, and A. Shalyto, "Closed-Loop Verification of a Compensating Group Drive Model Using Synthesized Formal Plant Model", in IEEE Emerging Technologies and Factory Automation, 2017, pp. 1-4,. DOI: 10.1109/ETFA.2017.8247714 -
I. Buzhinsky, A. Pakonen, and V. Vyatkin, "Scalable Methods of Discrete Plant Model Generation for Closed-Loop Model Checking", in IEEE Industrial Electronics Society, 2017, pp. 5483-5488,. DOI: 10.1109/IECON.2017.8216949 -
M. Xavier, J. Håkansson, S. Patil, and V. Vyatkin, "Plant Model Generator from Digital Twin for Purpose of Formal Verification", in IEEE Emerging Technologies and Factory Automation, 2021, pp. 1-4,. DOI: 10.1109/ETFA45728.2021.9613704 -
M. Xavier, V. Dubinin, S. Patil, and V. Vyatkin, "Plant Model Generation From Event Log Using ProM for Formal Verification of CPS", arXiv preprint arXiv:2211.03681, 2022,. DOI: 10.48550/arXiv.2211.03681 -
"nuXmv User Manual". [Online]. Available: https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf.
Выпуск
Другие статьи выпуска
В статье рассматриваются неориентированные кратные графы произвольной натуральной кратности k>1. Кратный граф содержит ребра трех типов: обычные, кратные и мультиребра. Ребра последних двух типов представляют собой объединение k связанных ребер, которые соединяют 2 или (k+1) вершину соответственно. Связанные ребра могут использоваться только согласованно. Если вершина инцидентна кратному ребру, то она может быть инцидентна другим кратным ребрам, а также она может быть общим концом k связанных ребер мультиребра. Если вершина является общим концом мультиребра, то она не может быть общим концом никакого другого мультиребра. Рассматривается задача об эйлеровом маршруте (цикле или цепи) в кратном графе, которая обобщает классическую задачу для обычного графа. Задача о кратном эйлеровом маршруте является NP-трудной. Обоснована полиномиальность двух подклассов задачи о кратном эйлеровом маршруте, разработаны полиномиальные алгоритмы. В первом подклассе задано ограничение на множества достижимости по обычным ребрам, которые представляют собой подмножества вершин, соединенных только обычными ребрами. Во втором подклассе задано ограничение на степень квазивершин в графе с квазивершинами. Структура этого обычного графа отражает структуру кратного графа, а каждая квазивершина определяется k индексами множеств достижимости по обычным ребрам, которые инцидентны какому-то мультиребру.
Приводятся оценки для минимальной нормы проектора при линейной интерполяции на компакте в Rn. Пусть Π1(Rn) - пространство многочленов от n переменных степени не выше 1, Ω - компакт в Rn, K=conv(E). Будем предполагать, что vol(K)>0. Пусть точки x(j)∈Ω, 1≤j≤n+1, являются вершинами n-мерного невырожденного симплекса. Интерполяционный проектор P:C(Ω)→Π1(Rn) с узлами x(j) определяется равенствами Pf(x(j))=f(x(j)). Под ∥P∥Ω будем понимать норму P как оператора из C(Ω) в C(Ω. Через θn(Ω) обозначим минимальную норму ∥P∥Ω из всех операторов P с узлами, принадлежащими Ω. Через simp(Ω) обозначим максимальный объём симплекса с вершинами в Ω. Устанавливаются неравенства χ−1n(vol(K)simp(Ω))≤θn(Ω)≤n+1. Здесь χn - стандартизованный многочлен Лежандра степени n. Нижняя оценка доказывается с применением полученной характеризации многочленов Лежандра через объёмы выпуклых многогранников. Именно, мы показываем, что при γ≥1 объём многогранника \left{x=(x_1,...,x_n)\in{\mathbb R}^n : \sum |x_j| +\left|1- \sum x_j\right|\le\gamma\right} равен χn(γ)/n!. В случае, когда Ω - n-мерный куб или n-мерный шар, нижняя оценка даёт возможность получить неравенства вида θn(Ω)⩾cn√. Формулируются некоторые открытые вопросы.Приводятся оценки для минимальной нормы проектора при линейной интерполяции на компакте в Rn. Пусть Π1(Rn) - пространство многочленов от n переменных степени не выше 1, Ω - компакт в Rn, K=conv(E). Будем предполагать, что vol(K)>0. Пусть точки x(j)∈Ω, 1≤j≤n+1, являются вершинами n-мерного невырожденного симплекса. Интерполяционный проектор P:C(Ω)→Π1(Rn) с узлами x(j) определяется равенствами Pf(x(j))=f(x(j)). Под ∥P∥Ω будем понимать норму P как оператора из C(Ω) в C(Ω. Через θn(Ω) обозначим минимальную норму ∥P∥Ω из всех операторов P с узлами, принадлежащими Ω. Через simp(Ω) обозначим максимальный объём симплекса с вершинами в Ω. Устанавливаются неравенства χ−1n(vol(K)simp(Ω))≤θn(Ω)≤n+1. Здесь χn - стандартизованный многочлен Лежандра степени n. Нижняя оценка доказывается с применением полученной характеризации многочленов Лежандра через объёмы выпуклых многогранников. Именно, мы показываем, что при γ≥1 объём многогранника \left{x=(x_1,...,x_n)\in{\mathbb R}^n : \sum |x_j| +\left|1- \sum x_j\right|\le\gamma\right} равен χn(γ)/n!. В случае, когда Ω - n-мерный куб или n-мерный шар, нижняя оценка даёт возможность получить неравенства вида θn(Ω)⩾cn√. Формулируются некоторые открытые вопросы.
В статье представлен метод семантического анализа данных посредством комплекснозначного матричного разложения. Метод основан на квантовой модели контекстно-чувствительных решений, согласно которой наблюдаемые вероятности порождаются кубитными состояниями, представляющими субъективный смысл контекстов для базисного решения. В простейшем трёхконтекстом случае один из кубитов раскладывается в суперпозицию оставшихся двух, математически представляющую смысловые отношения между контекстами. Для использования в задаче анализа данных эта модель представлена в матричной форме так, что строки и столбцы соответствуют контекстам и постановкам эксперимента. При этом наблюдаемые действительные данные порождаются матрицей комплекснозначных амплитуд, раскладываемой на произведение действительной матрицы базисных векторов и комплекснозначной матрицы коэффициентов суперпозиции. Это разложение выявляет устойчивые процессно-смысловые соотношения контекстов, не обнаруживаемые другими методами. В результате данные воспроизводятся более точно и с меньшим числом параметров, чем при использовании сингулярного и неотрицательного матричных разложений той же размерности. Модель успешно испытана в описательном и предсказательном режимах. Результат открывает возможности для разработки природоподобных вычислительных архитектур на новых логических принципах.
В работе сравнивается качество работы различных методов определения неявно упоминаемых аспектов социально-экономической жизни в публицистических предложениях на русском языке. Задача определения неявно упоминаемых аспектов является вспомогательной для задач аспектно-ориентированного анализа тональности. Эксперименты проводились на корпусе предложений, извлечённых из политической агитации. Лучшие результаты, с F1-мерой, достигающей 0.84, были получены с использованием эмбеддингов Navec и классификаторов, основанных на методе опорных векторов. Достаточно высокие результаты, с F1-мерой до 0.77, были получены при использовании модели «мешок слов» и наивного байесовского классификатора. Остальные методы показали более низкие результаты. Также в ходе экспериментов было выявлено, что качество определения различных аспектов может достаточно сильно отличаться. Лучше всего определяются аспекты, с которыми в речи связаны характерные слова-маркеры, например, «здравоохранение» и «проведение выборов» Хуже всего определяются упоминания достаточно общих аспектов, таких как «качество управления».
Издательство
- Издательство
- ЯрГУ им. П.Г. Демидова
- Регион
- Россия, Ярославль
- Почтовый адрес
- 150003, Ярославль, Советская, 14,
- Юр. адрес
- 150003, Ярославль, Советская, 14,
- ФИО
- Иванчин Артем Владимирович (Ректор)
- E-mail адрес
- rectorat@uniyar.ac.ru
- Контактный телефон
- +7 (485) 2797702