LTL model checking with neco. We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Fronc, Łukasz; Duret-Lutz, Alexandre: LTL model checking with Neco (2013)