Розглянуто розширену модель стану паралельної програми в мовах Interleaving Parallel Compositional Languages (IPCL). Середовище виконання IPCL - паралельне з почерговим переключенням зі спільною пам'яттю. Багатопотоковість та суперкомп'ютери є прикладами цієї моделі. Модифікація моделі IPCL з динамічним станом взята за основу в цій роботі. Тут вона розширена новими функціями. Задано семантику атомарних операцій test_and_set, swap та atomic у розширеній транзиційній моделі для IPCL. Семантична модель включає стани всіх паралельно виконуваних програм, глобальне дане та локальні дані кожної з них. Кількість екземплярів може змінюватись в ході виконання програми. Локальні та глобальні дані подаються номінативними структурами. Введення атомарних операцій є важливим розширенням мови, оскільки надає змогу моделювати роботу з критичними ресурсами та організовувати взаємне виключення та синхронізацію. Атомарні операції в цілому широко застосовуються у операційних системах. Таке розширення мов IPCL важливе для ширшого охоплення реальних програм і моделювання їх поведінки. Також розширюється область практичного застосування методу.

Досліджено середовище паралельного виконання з переключенням і взаємодією через спільну пам'ять. В роботі введено модель паралелізму з динамічним станом транзиційної системи для породження екземплярів паралельних підпрограм та приєднання їх після завершення виконання. У введеній моделі динамічного стану визначено семантику функцій start та join. Судження проведено в межах методу доведення властивостей програм (у тому числі - коректності) у Interleaving Parallel Compositional Languages (IPCL). Мови класу IPCL є адекватною моделлю суперкомп'ютерів з архітектурою спільної пам'яті (UMA та NUMA, апаратних архітектур симетричної багатопроцесорної обробки, операційних систем, систем управління базами даних, централізованих сховищ даних, серверної частини програмного забезпечення клієнт-серверних комплексів тощо). Це розширення є важливим, адже надає змогу моделювати роботу multithreading програм. Залишається важливим питання щодо еквівалентності (або взаємовиразності) двох моделей - з фіксованою параметричною кількістю паралельних програм та з породженням нових екземплярів програм і, відповідно, динамічним станом, семантику якого введено у даній роботі.