Seminar on 'Verification of Multi-Agent System Models via Nested Petri Net Unfoldings'
Vera Ermakova, HSE master's student presented the report 'Verification of Multi-Agent System Models via Nested Petri Net Unfoldings' at PAIS seminar.
Model checking is one of the most common ways of verification. In the case when the system consists of concurrent interacting agents we obtain the explosive growth of the number of states in particular due to the use of interleaving semantics. To overcome this problem an unfolding approach is applied to models of highly-concurrent systems. The purpose of the research is to study the application of unfoldings into nested Petri nets – a Petri nets extension for modeling multi-agent systems behavior.