LTL Model Checking with Neco

Authors

Łukasz Fronc, Alexandre Duret-Lutz

Where

Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13)

Place

Hanoi, Vietnam

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2013-06-15

Abstract

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.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  fronc.13.atva,
  author	= {{\L}ukasz Fronc and Alexandre Duret-Lutz},
  title		= {{LTL} Model Checking with {N}eco},
  booktitle	= {Proceedings of the 11th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'13)},
  year		= 2013,
  series	= {Lecture Notes in Computer Science},
  volume	= 8172,
  pages		= {451--454},
  address	= {Hanoi, Vietnam},
  month		= oct,
  publisher	= {Springer},
  abstract	= {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.},
  doi		= {10.1007/978-3-319-02444-8_33}
}