Verification of 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.