|Institutional Office Address
DMIF, Room NS3, Phone: +39 0432 558457
|Research Project Title
Model Checking for Interval Temporal Logics
|Research Project Description
Model checking (MC) consists in expressing some properties of a finite-state transition system in formulas of a temporal logic and then verifying them over a model of the system itself (usually a finite Kripke structure) through exhaustive enumeration of all the reachable states. This technique is fully automatic and every time the design violates a desired property, a counterexample is produced, which illustrates a behaviour that falsifies the property.
There are some properties we may want to check that are inherently ‘interval-based’ and thus can not be expressed by standard, point-based, temporal logics LTL, CTL and CTL*, e.g., ‘the average speed of a moving device must not exceed a given threshold’. Here interval temporal logics come into play, providing an alternative setting for reasoning about time. Such logics deal with intervals, instead of points, as their primitive entities: this choice gives them the ability to express temporal properties such as actions with duration, accomplishments, and temporal aggregations.
My research project deals with the MC problem for HS – the most prominent interval temporal logic – for which a little work has been done, if compared to MC for point-based logics. The idea is to evaluate HS formulas on Kripke structures, making it possible to check the correctness of the behaviour of systems with respect to meaningful interval properties.