Hybrid Spatio-Temporal Logic for Automotive Applications: Modeling and Model-Checking

This artifact implements in Python the three model-checking algorithms for Hybrid Spatiotemporal Logic for Automotive Safety introduced in the paper "Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking": a baseline algorithm, an optimized variant, and a motion-based algorithm. By default, the artifact is configured to reproduce the test cases and benchmarks from the paper, but the user can also define and analyze new scenarios by following the provided documentation of the specification language.