![](/images/ico/ico_close.png)
![](/images/ico/ico5.png)
Author: Abdulla Parosh Aziz Iyer S. Purushothaman Nylén Aletta
Publisher: Springer Publishing Company
ISSN: 0925-9856
Source: Formal Methods in System Design, Vol.24, Iss.1, 2004-01, pp. : 25-43
Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.
Abstract
Net unfoldings have attracted great attention as a powerful technique for combating state space explosion in model checking, and have been applied to verification of finite state systems including 1-safe (finite) Petri nets and synchronous products of finite transition systems. Given that net unfoldings represent the state space in a distributed, implicit manner the verification algorithm is necessarily a two step process: generation of the unfolding and reasoning about it. In his seminal work McMillan (K.L. McMillan,
Related content
![](/images/ico/ico_close.png)
![](/images/ico/ico5.png)
Small Vertex Cover makes Petri Net Coverability and Boundedness Easier
By Praveen M.
Algorithmica, Vol. 65, Iss. 4, 2013-04 ,pp. :
![](/images/ico/ico_close.png)
![](/images/ico/ico5.png)
On the composition of time Petri nets
Discrete Event Dynamic Systems, Vol. 21, Iss. 3, 2011-09 ,pp. :
![](/images/ico/ico_close.png)
![](/images/ico/ico5.png)
Theoretical Computer Science, Vol. 153, Iss. 1, 1996-01 ,pp. :
![](/images/ico/ico_close.png)
![](/images/ico/ico5.png)
Natural Computing, Vol. 10, Iss. 2, 2011-06 ,pp. :