The current folder contains examples to run LTL verification of hybrid systems.

README: this file.
kzeno.cmd: script file to run LTL verification

Example to run LTL verification:
../../hycomp -pre cpp -source kzeno.cmd counter_03.hydi

NOTE:
- The script runs LTL verification on ALL the properties contained
in the hydi model (you can specify the property to verify in the
hycomp_check_ltl command with -n <prop_number>)
- The scripts alternates one step of kzeno and one step of BMC.
If you want to run only kzeno, add the options -

References:
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta: Verifying LTL Properties of Hybrid Systems with K-Liveness. CAV 2014: 424-440

