Research Topics

Partially due to the recent breakthrough in deep learning, artificial intelligence is penetrating into safety-critical systems and these systems are becoming more and more intelligent. Notable examples of safety-critical intelligent systems are autonomous vehicles, e.g. self-driving cars and unmanned aircraft. It is of paramount importance to guarantee the trustworthiness of these systems, since errors in these systems may entail catastrophic consequences, e.g. deaths of human beings. Our group has been contributing to developing theories, techniques, and tools for guaranteeing the trustworthiness of intelligent systems. In the sequel, we state the main research directions of our group:

• Formal methods for Artificial Intelligence: We investigate robustness verification of various neural networks, such as DNNs, RNNs and GNNs. We apply techniques such as abstract interpretation, counterexample guided refinement. We apply model learning techniques in this context to learn approximating models, which also provide tools for neural model explanations. We have implemented a platform PRODeep, for analyzing various robustness properties of DNNs. It incorporates constraint-based, abstraction-based, and optimization-based robustness verification algorithms. It has a modular architecture, enabling easy comparison of different algorithms.
• Probabilistic Model Checking: We work on algorithms for verifying properties of probabilistic systems, and applying them in applications such as networked systems, differential privacy protocols. We have implemented our algorithms in our tool ePMC. It supports Markov chains and Markov decision Processes (MDPs), and properties specified in PCTL, PLTL and their combination PCTL*. ePMC is highly modular, which allows everyone to extend and improve the functionalities of the model checker. For instance, we have extended it to dpCTL, a tool for checking differential privacy CTL properties on Markov chains and Markov decision processes, and Petl, a tool for model checking probabilistic epistemic logic for probabilistic multiagent systems, and QMC, a model checker for quantum Markov chains.

Publications and Tools

We have published a wide body of literature, see our page publications for details. Moreover, our group have developed multiple tools and applied them to several case studies. The main tools are:

• ISS: Iscas Self-driving System strives to deliver a highly modularized autonomous driving platform. By decoupling modules and establishing standardized information flow, this solution enables swift and cost-effective migration to diverse simulation platforms and physical vehicles. Moreover, ISS has developed interfaces for algorithm evaluation and verification of each module, reducing the learning curve for researchers and catering to a wide range of research needs.
• ROLL: a library of learning algorithms for ω-regular languages. It consists of some learning algorithms for FDFAs and for Büchi automata.
• PRODeep: a platform for robustness verification of deep neural networks.
• ePMC: the successor of IscasMC, a tool for verifying properties over probabilistic systems.
• SVMRanker: a tool for synthesizing multiphase/nested ranking functions of loop programs based on SVM.

The source code of most of the tools can be found here.

The research has been supported by several ongoing and completed projects.