Quantitative Model Checking and Synthesis

这个博士项目将通过研究共代数定量逻辑及其相关的验证技术，作为为期3年的leverhulme资助的研究项目COVER （COalgebraic Foundations for Quantitative VERification）的一部分进行补充。该博士生将与COVER研究团队（两名学者和两名PDRAs）一起工作，扩展现有的定量逻辑，并开发相关的模型检查和合成算法，这些算法在定量模型类型中是参数化的。这项工作将最终将模型检查和综合技术的适用性扩展到具有一系列正确性和最优性保证的复杂系统。作为博士学位的一部分开发的技术将在自主系统领域的案例研究中进行评估。

This PhD project will complement work carried out as part of the 3-year Leverhulme-funded research project COVER (COalgebraic Foundations for Quantitative VERification), by studying coalgebraic quantitative logics and their associated verification techniques. The PhD student will work alongside the COVER research team (two academics and two PDRAs) to extend existing quantitative logics and develop associated model checking and synthesis algorithms which are parametric in the type of quantitative model. This work will ultimately extend the applicability of model checking and synthesis techniques to complex systems with a range of correctness and optimality guarantees. The techniques developed as part of the PhD will be evaluated on case studies from the autonomous systems domain.