Verification based on merged processes
Victor Khomenko
- 11:30 23rd May 2012 ( week 5, Trinity Term 2012 )147
Model checking based on Petri net unfoldings is an approach widely applied to cope with the state space explosion problem caused by concurrency. In this talk I will describe a recent condensed representation of a Petri net's behaviour called merged processes, which copes well not only with concurrency, but also with other sources of state space explosion, like sequences of choices and non-safeness. Moreover, this representation is sufficiently similar to the traditional unfoldings, so that a large body of results developed for the latter can be re-used. Experiments indicate that this representation of a Petri net's behaviour alleviates the state space explosion problem to a significant degree and is suitable for model checking.
Speaker bio
Victor Khomenko obtained his PhD in Computing Science in 2003 from Newcastle University. He was a Program Committee Chair for the International Conference on Application of Concurrency to System Design (ACSD'10). He also organised the Workshop on UnFOlding and partial order techniques (UFO'07) and Workshop on BALSA Re-Synthesis (RESYN'09). In January 2005 Victor became a Lecturer in the School of Computing Science, Newcastle University, and in September 2005 he obtained a Royal Academy of Engineering / EPSRC Post-doctoral Research Fellowship and worked on the Design and Verification of Asynchronous Circuits (DAVAC) project. After the end of this award, in September 2010, he switched back to Lectureship. Victor's research interests include model checking of Petri nets, Petri net unfolding techniques, verification and synthesis of self-timed (asynchronous) circuits.Share this:
