Verification of Data in Space and Time
Mieke Massink, National Research Council of Italy (CNR)
Verification of data in space and time
Date: Jeudi 30 janvier 2020 à 11h00
Lieu: CUI / Battelle bât. A, Salle de réunion 432-433 (3ème étage)
Research data can take very many forms, but in many cases there are interesting relations between elements of data. Such relations could be of various nature, for example causal relations, temporal relations, spatial relations or any combination thereof, to mention a few. Reasoning about time and space and their combination has a long history. Only more recently, reasoning about spatial aspects of systems, that is, the properties of entities that relate to their position, distance, connectivity and reachability in space, have received increasing attention in computer science. We present recent results in spatial and spatio-temporal logic, that have their origin in Modal logic and early work dating back to McKinsey and Tarksi, and their evolution into efficient spatial and spatio-temporal model checking methods. We illustrate these methods by their application to various domains ranging from smart public transportation to medical imaging. In the latter domain, data-analysis techniques, such as machine learning, provide a popular new area of research too, opening the way for an interesting discussion on how various methods could be used profitable in a complementary way.
Mieke Massink received her master’s degree in computer science from the University of Nijmegen, The Netherlands in 1988; she received her Laurea in Computer Science from the University of Pisa in 1995 and her PhD degree in computer science from the University of Nijmegen in 1996. In 1992 she received the “Dr. I.B.M. Frye Stipend” of the University of Nijmegen for the most promising female PhD researcher. She is currently a researcher in the Formal Methods and Tools lab at CNR-ISTI (Institute of Information Science and Technology “A. Faedo”), a computer science research institute of the National Research Council of Italy (CNR). Her research interests include the development and application of formal languages for specification and verification of concurrent, safety critical and software intensive systems, including collective adaptive systems which may exhibit emergent behaviour, and human interaction related aspects of such systems. In particular her interest is in semantic models and scalable verification techniques for process algebras and automata, and their extension with aspects of mobility, time, space e/o probability, with a focus on temporal and modal logics for the specification and verification of related properties through logic-based model checking.