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

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

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

Example to run LTL verification using BMC:
../../hycomp -pre cpp -source sbmc.cmd fischer_star_hybrid_2.unsafe.hydi

NOTE:
The scripts run 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>)

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

