Automata-theoretic verification with resource bounds



Automata-theoretic techniques are successfully used in verification by model checking. Besides verification of finite systems, many techniques can be lifted to classes of infinite systems, e.g., pushdown systems, wich are used for modelling recursion, and ground term rewriting systems, which extend pushdown systems by a restricted kind of parallelism. The core of many verification problems consists of reachbility problems, i.e., the question whether certain states of the system are reachable in finitely many computation steps from other states of the system. In this project we consider systems that additionally model the consumption of resources. The reachability questions are then formulated under the condition of a bound for the resource consumption. This bound is not given a priori but the question is on the existence of such a bound. The goal of the project is to develop algorithms for this new class of verification problems for systems with resource consumption. We use the theory of finite resource automata (often called distance of cost automata in the literature) that has been developed recently and provides suitable tools for tackling these algorithmically difficult problems.



[Lan11] M. Lang. Resource-bounded Reachability on Pushdown Systems. Master thesis, RWTH Aachen, 2011.