Predictability Verification with Parallel LTL-X Model Checking Based on Petri Net Unfoldings

  1. Lookup NU author(s)
  2. Agnes Madalinski
  3. Dr Victor Khomenko
Author(s)Madalinski A, Khomenko V
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Source Publication DateSeptember 2011
Report Number1276
Full text is available for this publication:
We show that the predictability problem for a Petri net can be reduced to LTL-X model checking. The advantage of this is that existing efficient methods and tools can be employed, in particular parallel model checking based on Petri net unfoldings. The experimental results show that this approach is efficient, and a good level of parallelisation can be achieved.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
ActionsLink to this publication