权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Verification of Weighted Timed Automata

加权时间自动机的验证

基本信息

批准号：
181095210
负责人：
Dr. Karin Quaas
金额：
--
依托单位：
Abteilung Algebraische und logische Grundlagen der Informatik
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
2010
资助国家：
德国
起止时间：
2009-12-31 至 2017-12-31
项目状态：
已结题

来源：
https://gepris.dfg.de/gepris/projekt/181095210?language=en
关键词：
Verification Weighted Timed Automata

项目摘要

Weighted timed automata extend classical finite automata with a finite set of real-valued clock variables that measure the time, and with a weight function that assigns an integer to the edges and the states of the automaton. The integer assigned to an edge determines the cost for taking this edge, and the integer assigned to a state determines the cost for staying in this state per time unit. Weighted timed automata are very useful to model the behaviour of real-time systems with continuous resources. Since their introduction in 2003 they have gained a lot of interest in the real-time community. However, many interesting verification problems for weighted timed automata are undecidable or have a bad computational complexity. For instance, model checking weighted timed automata with a weighted version of MTL is decidable only with non-primitive recursive complexity, and only if the automaton uses at most one clock variable and the weight rate assigned to a state is either one or zero. For all other variants of the model the problem is undecidable. In the project, we thus want to focus on timed automata with discrete edge weights in the integers, ie., we do not allow continuous weights resulting from rates assigned to the states. This is a very strong restriction compared to the original definition of weighted timed automata; however, the model is still capable to express interesting properties. This is also proved by the lively research on the related untimed model of one-counter systems. We also want to investigate useful combinations of timed automata and one-counter systems, with which one can express constraints on the weight values of the automaton. For these models, we want to examine the model checking problem and other problems useful in verification, like, e.g., the language inclusion problem. For specifying properties, we also want to consider well known extensions of Linear Temporal Logic, like, eg., MTL, Freeze LTL, and TPTL. Most of these logics yield undecidable satisfiability and model checking problems, and we thus want to focus on finding fragments that are both expressive and yield tractable decision problems. We hope to profit from recent results on decision problems for fragments of, eg., MTL, in both the research areas of real-time systems on the one side, and one-counter systems on the other side. With this project, we also hope to push forward the mutual enrichments of these two fields of theoretical computer science.

加权时间自动机扩展了经典的有限自动机与一组有限的实值时钟变量，测量时间，并与一个权重函数，分配一个整数的边缘和状态的自动机。分配给边的整数决定了获取该边的成本，而分配给状态的整数决定了每单位时间停留在该状态的成本。加权时间自动机是非常有用的建模实时系统的行为与连续资源。自2003年推出以来，它们在实时社区中引起了很大的兴趣。然而，许多有趣的验证问题的加权时间自动机是不可判定的或有一个坏的计算复杂度。例如，具有MTL的加权版本的模型检查加权时间自动机仅在非原始递归复杂度下是可判定的，并且仅当自动机最多使用一个时钟变量并且分配给状态的权重率为1或0时。对于模型的所有其他变体，该问题是不可判定的。因此，在这个项目中，我们希望专注于整数中具有离散边权重的时间自动机，即，我们不允许由分配给状态的速率产生连续权重。与加权时间自动机的原始定义相比，这是一个非常强的限制;然而，该模型仍然能够表达有趣的属性。对单计数器系统的相关不定时模型的研究也证明了这一点。我们还想研究有用的组合的时间自动机和一个计数器系统，其中一个可以表达的自动机的权重值的约束。对于这些模型，我们希望检查模型检查问题和其他在验证中有用的问题，例如，语言包容性问题。为了指定属性，我们还想考虑线性时态逻辑的众所周知的扩展，例如，MTL、Freeze LTL和TPTL。这些逻辑中的大多数产生不可判定的可满足性和模型检查问题，因此我们希望专注于寻找既有表达能力又能产生易处理的决策问题的片段。我们希望从最近的结果中获益，例如，MTL，一方面在实时系统的研究领域，另一方面在单计数器系统的研究领域。通过这个项目，我们也希望推动理论计算机科学这两个领域的相互丰富。