Algebra and Logic Seminar

The next meeting of the seminar will be held on October 23, 2015 (Friday), at 11:00, in Room 578 of the Institute of Mathematics and Informatics.

A talk on

Model Checking of Mobile Systems Using Net Unfoldings

will be delivered by Prof. Maciej Koutny (University of Newcastle upon Tyne, U. K.).

Everybody is invited.

Abstract. 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.