In earlier work it has been shown that finite state CTL model checking of reactive systems can be achieved by a relatively simple interpreter written in tabled logic programming. This approach is flexible in the sense that various specification formalisms can be easily targeted (e.g., Petri nets, CSP, ...). Moreover, infinite state CTL model checking can be performed by analysing this interpreter using a combination of partial deduction and abstract interpretation. It has also been shown that this approach is powerful enough to decide coverability properties of various kinds of Petri nets. In this ongoing work, we are empirically evaluating these approaches on various case studies of finite, parameterised and infinite systems. For finite state systems, we show how our approach and tool compares to standard tools for finite state model checking For parameterised or infinite state model checking, we are comparing our results with, e.g., XMC, Hytech.
展开▼
