Current students

Temporal logics is the standard descriptive formalism adopted in literature for the formal specification of time-dependent systems.
Although computer systems are inherently discrete-time objects, their application to real-time control and monitoring often requires to deal with a continuous notion of time. For this reason, several descriptive models have been developed which support a continuous-time semantics, most notably Metric Temporal Logic (MTL). Unfortunately, in general, verification of continuous-time temporal logics is not as well supported as for discrete time.Moreover, the mainstream of theoretical studies on temporal logics has mostly been restricted to the propositional case. The reason is clear: most first-order temporal logics that are useful in computer science are not even decidable. Nevertheless, some decidability results for suitable fragments of first-order temporal logics have been obtained, thus opening the way for further studies [1]. The main issue with first-order temporal logics is that, even when decidability results are available for a certain fragment, there is often no actual implementation of a decision procedure for it. This drammatically limits the utility of such formalisms in verification. 
Our work is focused on defining decidable fragments of first order MTL, aiming at also providing effective decision procedures for them. The idea is to exploit and extend an existing complete and effective verification tool for propositional MITL (a syntactic fragment of MTL) [2].    

Essential bibliography 
[1]  I. Hodkinson, F. Wolter, M. Zakharyaschev, “Decidable fragments of first-order temporal logics”, Annals of Pure and Applied Logic 106 (2000) 85-134. 
[2] M.M. Bersani, M. Rossi, P. San Pietro, “An SMT-based approach to satisfiability checking of MITL”, Information and Computation 245 (2015) 72-97.