Семинар лаборатории ИССА: "A new rule for LTL tableaux". Докладчик: Марк Рейнольдс
Марк Рейнольдс - профессор, руководитель школы компьютерных наук и программной инженерии Унивеситета Западной Австралии, соавтор фундаментальной двухтомной монографии "Темпоральная логика: математические основания и вычислительные аспекты", ведущий специалист в данной области.
Тема: "A new rule for LTL tableaux"
Докладчик: Mark Reynolds, профессор, руководитель школы компьютерных наук и программной инженерии Унивеситета Западной Австралии
Дата: 28 сентября, 16:40
Место: Москва, Кочновский проезд, дом 3, ауд. 322
Аннотация:
Propositional linear time temporal logic (LTL) is the standard temporal logic for computing applications and many reasoning techniques and tools have been developed for it. Tableaux for deciding satisfiability have existed since the 1980s. However, the tableaux for this logic do not look like traditional tree-shaped tableau systems and their processing is often quite complicated.
In this talk, we introduce a novel style of tableau rule which supports a new simple traditional-style tree-shaped tableau for LTL. We prove that it is sound and complete. As well as being simple to understand, to introduce to students and to use, it is also simple to implement and is competitive against state of the art systems. It is particularly suitable for parallel implementations.
Приглашаются все желающие. По всем вопросам и для заказа пропуска необходимо написать Ларисе Ивановне Антроповой по электронной почте: lantropova@hse.ru