| Summary: | We consider formal verification of recursive programs with resource
consumption. We introduce prefix replacement systems with non-negative integer
counters which can be incremented and reset to zero as a formal model for such
programs. In these systems, we investigate bounds on the resource consumption
for reachability questions. Motivated by this question, we introduce relational
structures with resources and a quantitative first-order logic over these
structures. We define resource automatic structures as a subclass of these
structures and provide an effective method to compute the semantics of the
logic on this subclass. Subsequently, we use this framework to solve the
bounded reachability problem for resource prefix replacement systems. We
achieve this result by extending the well-known saturation method to annotated
prefix replacement systems. Finally, we provide a connection to the study of
the logic cost-WMSO.
|
|---|