Шкільняк Степан СтепановичЄрьоменко Іван2023-03-102024-05-152023-03-102022Єрьоменко І. Темпоральні логіки та їх застосування : кваліфікаційна робота ... бакалавра : 122 Комп’ютерні науки / Іван Єрьоменко. - Київ, 2022. - 58 с.https://ir.library.knu.ua/handle/123456789/2745Проаналізована актуальність даної теми та проблеми які вона вирішує, виконано огляд систем темпоральної логіки, описано мови та реляційну семантику таких логік, розглянуто лінійну пропозиційну темпоральну логіку, наведено приклад її застосування для вирішення проблеми взаємного виключення алгоритмом Петерсона. Описано потужний метод верифікації програмних систем Model cheking та верифікатор SPIN, які використовують апарат лінійної темпоральної логіки. Наведено змістовний приклад застосування апарату темпоральної логіки на практиці – верифікація програми автоматної реалізації математичної гри Нім із використанням SPIN.uaБакалаврська робота