A temporal view on Model Checking Hybrid Logics

We tackle the problem of Hybrid Logics Model Checking and its current limitations on what it concerns the available instrumentation support. In this direction, we present an extended version of an available Hybrid Logics model checking tool, which supports the use of both specific Hybrid Logics and also temporal operators for verifying system properties. By adding support for temporal operators, the extended version will make easier the model verification problem by taking the advantages of both worlds in one place.