Quantitative Model Checking and Synthesis

定量模型检验与综合

• 批准号: 2751001
• 金额: --
• 依托单位: University of Southampton
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2751001
• 关键词: Quantitative; Model; Checking; Synthesis

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.

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