Bozena Wozna

Real Time CTL and Model Checking

The aim of the talk is to review existing real time temporal logics, give a short introduction to model checking methods, and show in details one of them, called Bounded Model Checking (BMC). BMC is based on SAT solvers, and it has been originally designed to verify LTL properties of untimed systems, and then has been extended to other logics and time systems. During the talk I will focus particularly on the BMC method for time systems, modelled by Timed Automata, that I have developed for my PhD.