Formal model for verification of personalized educational trajectories based on ALLOY

• Дата: 2026
• Автори: Poltoratskyi, M.Yu., Volianiuk, A.S.
• Формат: Стаття
• Мова: Українська
• Опубліковано: PROBLEMS IN PROGRAMMING 2026
• Теми: personalized learning; educational trajectory; verification; educational engineering; adaptability; skills; career goal; algorithm; model; course; UDC 004.942:37.018.43
• Онлайн доступ: https://pp.isofts.kiev.ua/index.php/ojs1/article/view/1029
• Назва журналу: Problems in programming

The article addresses the problem of verification of personalized educational trajectories in modern educa tional engineering under the conditions of digitalization of the educational process. The necessity of verifying the correctness of learning pathways formed with regard to individual educational needs, prior experience, level of training, and professional goals of learners is substantiated. It is emphasized that the effectiveness of personalized learning is determined not only by the quality of individual trajectory design but also by the possibility of its formal verification in terms of consistency, completeness, and attainability of results. A formal model implemented using the Alloy specification language is proposed, which enables verification of the correspondence between acquired skills and the requirements of a career goal. Within the model, key entities are defined, including the learner, educational subjects, acquired and required skills, as well as pro fessional aspirations, and the relationships between them are formalized. A system of invariants and con straints is introduced to ensure the correctness of educational trajectories, including the presence of a defined career goal, the meaningfulness of educational components, and the alignment of learning outcomes with professional requirements. The model provides dynamic verification of the attainability of educational results through the analysis of changes in the set of acquired skills at different stages of learning. This makes it possible to identify potential errors in trajectory construction, evaluate the effectiveness of course recommen dation algorithms, and confirm the attainability of defined goals. The obtained results demonstrate that the application of a formal approach contributes to increasing the validity of personalized learning, the soundness of educational decisions, and the efficiency of adaptive educational systems. Prospects for further research are related to extending the system of constraints, taking into account data uncertainty, and improving mech anisms for adapting educational trajectories.Prombles in programming 2026; 2: 87-96