The project originates from the combined efforts of researchers from different fields such as model checking, logics, process algebras, network science, constraints, hybrid systems. The goal is to extend and refine methods and software modules for modeling, analysis and synthesis of complex systems involving many, possibly partially known components which interact at different levels, involving also parameters and stochastic effects. Such interactions can produce dramatic effects and methods for the systematic analysis of the expected behaviors are necessary together with techniques for the synthesis of controllers/plans ensuring safety.
We are motivated by two observations: crucial aspects of such systems cannot be properly captured exploiting only one of the current existing approaches; recent advances in different formalisms make them mature for integration. We rely on a set of existing tools: temporal networks, process algebras, and automata as modeling languages; temporal logics, metric interval temporal logics, logic of knowledge, non-monotonic logics, logical frameworks, and behavioral equivalences as querying formalisms; constraint solvers and GPU implementations as efficient engines.
Instead of developing a general framework we focus on the analysis of two case studies: the European Train Control System (ETCS) and Breast Cancer Progression (BCP). On ETCS we will cooperate with FBK working on it since 2008. In BCP the models have to be inferred from existing descriptions and clinical data (see, e.g., cBioPortal data on detailed type Invasive Breast Carcinoma).
The novelty and effectiveness of our proposal is a consequence of the following peculiarities. The team members have complementary expertises and they have already cooperated on publications, tools, and projects. The efforts will be focused on the two selected case studies.