Formal model for verification of personalized educational trajectories based on ALLOY

M.Yu. Poltoratskyi, A.S. Volianiuk

Abstract


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


Keywords


personalized learning; educational trajectory; verification; educational engineering; adaptability; skills; career goal; algorithm; model; course

References


H. Peng, J. Spector, Personalized adaptive learning: an emerging pedagogical approach enabled by a smart learning environment, in: Smart Learning Environments, 2019.

L. Tetzlaff, F. Schmiedek, G. Brod, Developing personalized education:a dynamic framework, in: Educational Psychology Review, 33 (2020) 863–882.

A. Shemshack, J. Spector, A comprehensive analysis of personalized learning components, in: Journal of Computers in Education, 8 (2021) 485–503.

S. Alekseeva, Didactic algorithm for designing an individual educational trajectory, in: Origins of Pedagogical Mastery, 32 (2023) 5-9.

M. Lavrenova, N. Lalak, T. Molnar, L. Fenchak, Development trajectory of primary education students: from theory to practice, in: Visnyk of Lviv University. Pedagogical Series, 35 (2021) 130–138.

A. Spivakovsky, L. Petukhova, O. Anisimova, A. Horlova, V. Kotkova, A. Volianiuk, ICT as a key instrument for a balanced system of pedagogical education, in: ICTERI, 2020.

Z. Papamitsiou, Development and research of algorithms for the formation of individual educational trajectories of students in the digital educational platform, 2019.

T. Kovaliuk, N. Kobets, V. Dvornyk, Information technology for constructing individual educational trajectories based on latent-semantic analysis of motivational letters and professional achievements of students, 2020, pp. 115–128.

W3C Semantic Web Wiki, 2001.

RDF 1.1 Primer [Electronic resource], W3C, 2014.

Notation3 (N3): A readable RDF syntax.

T. Berners-Lee, N3Logic: A logical framework for the World Wide Web, W3C, 2008.

M. Poltoratskyi, O. Konnova, Use of semantic web technologies for validation of educational models, in: Information Technologies and Learning Tools, 106(2) (2025) 94–106.

Shapes Constraint Language (SHACL) W3C Recommendation, 2017.

SPARQL 1.1 Query Language. W3C Recommendation, 2013.

Alloy: A language and analyzer for software modeling.

Alloy Analyzer – User Guide.

M. Poltoratskyi, One approach to creating a personalized educational environment, in: Measuring and Computing Devices in Technological Processes, 1 (2026) 77–86.

Alloy Documentation. Analyzer.


Refbacks

  • There are currently no refbacks.