Since Sept 2022 this repository has been merged into https://github.com/lip6/libITS
This repository is now archived.
ITS tools and SPOT combine to provide symbolic model-checking of LTL.
This command line tool takes as input a model in ITS-tools syntax (e.g. a GAL model, a Petri net, an ETF, ...) and an LTL/PSL property (or even an automaton in HOAF format) and checks whether all traces of the system are part of the language of the formula (for HOAF, the automaton is expected to represent the negation of the property language).
Tool main page is at : https://ddd.lip6.fr
Download page for its-ltl prebuilt binaries : https://lip6.github.io/ITS-LTL/
This tool is available under GPL license v3 or better.
(c) Sorbonne Université, CNRS