Verification of Weighted Timed Automata

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

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.