Games for Quantitative Analysis of Real Time Systems

实时系统定量分析游戏

基本信息

批准号：
EP/E022030/1
负责人：
Marcin Jurdzinski
金额：
$ 15.09万
依托单位：
University of Warwick
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2007
资助国家：
英国
起止时间：
2007 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FE022030%2F1
关键词：
Games Quantitative Analysis Real Time

项目摘要

Algorithmic formal methods are a collection of mathematical models andalgorithmic techniques for computer aided systems engineering. Bysystems engineering we mean modelling, design, quality control,performance evaluation, optimal control, etc., of modern complex computational systems. Examples of such systems include hardware and(embedded) software, but also industrial processes, e-commerceservices, biochemical regulatory networks. Temporal logic modelchecking is one of the recent success stories of theoretical computerscience. Amir Pnueli won the Turing Award in 1996 for introducingtemporal logic into computer science, and the 2000 Goedel Prize andthe 1998 and 2005 ACM Kanellakis Theory and Practice Awards were givento researchers in the community for the development of symbolic andautomata theoretic model checking.Formal methods valuably complement traditional approaches to qualitycontrol in systems engineering such as simulation and testing.The industrial acceptance of model checking techniques is due to theirextra benefits. One of them is the automation of formal analysisachieved by focus on developing efficient algorithms. Another benefitis informative feedback provided to the designer when faults are detected.The applicability of formal methods in systems engineering depends onautomation of analysis methods as well as on having appropriatemathematical models of the analyzed systems and their desiredproperties. The classical model checking methods apply to verificationof non-terminating and discrete time reactive systems modeled usingfinite automata. Modern complex embedded systems are built out of manyheterogenous components that interact with a (possibly adversarial)physical environment. In order to faithfully model such systems thefollowing extensions to the basic automata models andanalysis tasks are considered. Models can be: deterministic orstochastic; and discrete time or real time. The analysis can be:qualitative (deciding yes/no properties) or quantitative (optimizationof performance measures); and performed through verification(non-adversarial) or synthesis (adversarial).The mathematical roots of the automata theoretic model checkingtechniques can be traced to the powerful decidability results forlogics and finite automata on infinite words and trees. The study of(stochastic) real time models with adversarial interaction andquantitative performance measures calls for concepts developed within(stochastic) game theory and control theory. As traditional modelchecking is about qualitative verification (given a system and aqualitative property, determine whether the system satisfies theproperty or not), the analysis of the richer models we argue for isabout (stochastic) quantitative real time synthesis (given aquantitative objective, synthesize a real time strategy/controller forthe system that optimizes the objective). The algorithmic techniquesfor qualitative and quantitative synthesis, for quantitative real timeverification, and for qualitative real time verification andsynthesis, have attracted a lot of attention, but algorithmic resultsfor quantitative real time synthesis are very recent and incomplete.Timed automata are real time models which enjoy efficient algorithmicmethods for qualitative and quantitative verification while beingexpressive enough to be useful in modelling and analysis of real timesystems. A number of tools for analysis of timed automata have beenimplemented and applied in industrial scale case studies.Our proposed research is to pursue the exploration of efficientalgorithmic methods for (stochastic) quantitative real time synthesiswith models based on timed automata. More specifically, we plan towork on computational complexity and algorithms for solving 2-playergames with quantitative objectives played on timed automata and othersubclasses of hybrid systems.

算法形式方法是用于计算机辅助系统工程的数学模型和数学模型的集合。 BIDSYSTEMS工程是指现代复杂计算系统的建模，设计，质量控制，性能评估，最佳控制等。此类系统的示例包括硬件和（嵌入式）软件，以及工业流程，电子服务，生化调节网络。时间逻辑模型检查是理论计算机科学的最新成功故事之一。 Amir Pnueli于1996年获得了Turing Award，该奖项因在计算机科学中引入时空的逻辑而获得了Turing Award，2000年Goedel奖和1998年和2005年ACM Kanellakis理论和实践奖是社区中的Givento研究人员，以开发符号和辅助方法的象征性和互补方法，以实现象征性和互补方法。模型检查技术是由于其优势。其中之一是通过专注于开发有效算法的正式分析的自动化。当检测到故障时，另一种受益人的信息提供了向设计人员提供的反馈。系统工程中形式方法的适用性取决于分析方法的侵蚀，以及具有分析系统及其所需的份量的适当模型。经典模型检查方法适用于使用Finite Automata建模的非末端和离散时间反应性系统的验证。现代复杂的嵌入式系统是由与（可能是对抗性的）物理环境相互作用的多型组件构建的。为了忠实地对这样的系统进行建模，考虑到基本自动机模型和分析任务的标题扩展。模型可以是：确定性的orstochastic;和离散的时间或实时。分析可以是：定性（确定是/否属性）或定量（绩效指标的优化）；并通过验证（非对抗性）或合成（对抗性）进行。自动机理论模型检查技术的数学根可以追溯到无效的单词和树上的功能强大的可决定性结果。对（随机）实时模型具有对抗性相互作用和质量绩效措施的研究要求在（随机）游戏理论和控制理论中开发的概念。由于传统的模型检查是关于定性验证的（给定系统和含水性属性，确定该系统是否满足PROPERTY），因此对我们为ISABOUT（随机）定量实时合成的更丰富模型的分析（给定的含水目标（给定的含水目标），合成了目标的实时策略/对目标的实时策略/对目标的构成）。 The algorithmic techniquesfor qualitative and quantitative synthesis, for quantitative real timeverification, and for qualitative real time verification andsynthesis, have attracted a lot of attention, but algorithmic resultsfor quantitative real time synthesis are very recent and incomplete.Timed automata are real time models which enjoy efficient algorithmicmethods for qualitative and quantitative verification while beingexpressive enough可用于建模和分析现实时段系统。许多用于分析定时自动机的工具已在工业规模的案例研究中进行了体现和应用。我们所提出的研究是为基于定时自动机的（随机）定量实时综合模型探索（随机）定量实时综合模型的有效方法。更具体地说，我们计划在计算复杂性和算法上搜索以定时的自动机和其他混合系统的其他UBCLASSES来解决2播放目标的算法。