СЕМИНАР „АЛГЕБРА И ЛОГИКА”

Следващото заседание на семинара ще се проведе на 25 март 2016 г. (петък) от 11:00 часа в зала 578 на ИМИ – БАН.

Доклад на тема:

Влагане на (още) модели за паралелизъм в интервалната темпорална логика с поточкова проекция

ще изнесе доц. Димитър Гелев, ИМИ - БАН.

Поканват се всички желаещи.

Резюме. Операторът за поточкова проекция Π е исторически първият (1983) оператор за проекция в интервалната темпорална логика за дискретно време на Мошковски ITL. По-късно (1985) Мошковски въвежда в ITL и оператор за стъпкова проекция, който прилага за изразяването на паралелна композиция. През 2015 г. съвместно с Мошковски показахме, че стъпковата проекция е изразима чрез Π. Независимо от това, на основата на Π построихме прост и интуитивен модел за квази-паралелизъм. Π улеснява и влагането в ITL на други силно застъпени в литературата темпорални интервални логики със специализирани оператори за проекция и паралелна композиция, запазвайки компактния вид на ключови елементи от семантиката им. Така разрешимостта на валидността и, следователно, на задачи за верификация формулирани в ITL с Π или в тези други логики, се свежда до известната разрешимост на валидността в ITL. Всички казани дотук модели предвиждат споделени променливи. В този доклад разширявам модела за квази-паралелизъм в ITL с Π. Показвам как в разширението се изразява синхронна комуникация (handshaking, предаване на съобщения по канали с капацитет 0), застъпена в алгебрата от процеси CSP и езици за програмиране като Occam и Ада.

.