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

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

Model Checking of Mobile Systems Using Net Unfoldings

ще изнесе Prof. Maciej Koutny (University of Newcastle upon Tyne, U. K.).

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

Резюме. Mobility is a central feature of many distributed systems, and is often modelled using process algebras; in particular, the pi-calculus. A well-established method of verifying the correctness of such models has been model-checking which is completely automatic, and so particularly attractive in industrial context. However, mobile systems are highly concurrent causing state space explosion when applying model-checking techniques. To cope with this problem, techniques based on partial order semantics of concurrency can be used. The talk discusses how model-checking based unfoldings of Petri nets could be used to verify pi-calculus terms. The talk describes a prototype tool based on theoretical translation and an existing efficient Petri net unfolder and verifier. It also presents experimental results in support of specific design choices.