Bounded reachability in resource pushdown systems

In the talk, we present a model for recursive programs with resource
consumption. It combines the well-known theory of pushdown systems,
which are capable of modeling recursive programs, and the recent theory
of regular cost functions, which can represent resource consumption. For
these kind of systems, we investigate an extension of the traditional
reachability question between two sets of configurations - bounded
reachability. It asks whether there is a finite bound k such that no
more than k resources are needed to achieve reachability. We introduce a
quantitative variant of first-order logic as a framework to solve
bounded reachability and specify constraints for resource consuming
systems. Moreover, we show that this logic is decidable for an extension
of the well-known class of automatic structures.