Benchmarks

Benchmarks

Effectiveness and robustness of VeriLHyS in proving LTL properties of hybrid systems is evaluated across several benchmarks.

  • Linear Overtake: A 4-dimensional linear hybrid system modeling overtaking behavior of a vehicle.

  • Multiple Choice: A scalable 2D benchmark with discrete jumps.

  • Navigation Benchmark: A 4D system (space and velocity variables) with linear dynamics and 25 locations.

  • Non-linear Circular: A 2D system with non-linear dynamics converging to the unit circle.

  • Multilayer Control (Linear and Nonlinear): A scalable 3D system with multiple locations converging (with linear or nonlinear dynamics) to different points in the space.

  • Bball: 2D linear systems representing a bouncing ball.

  • Circle: A 2D linear system with two locations representing circular motion.

  • Drivetrain: A 10D linear system modeling a vehicle’s drivetrain. Available in 2 different versions.

  • Rendezvous": A 4D nonlinear system modeling a spacecraft rendezvous maneuver. Available in 6 different versions.

Open Challenges

As the general problem of LTL verification for hybrid systems is undecidable, the VeriLHyS framework is not guaranteed to terminate successfully for all inputs and in many cases it may instead return "Unknown" or time out.

This applies to the first property encodded in the XML representation of the following benchmarks:

  • Bball

  • Circle

  • Drivetrain

  • Rendezvous

Inputs

The complete set of benchmarks is available here