Lang, Martin and Löding, Christof - Modeling and Verification of Infinite Systems with Resources

lmcs:1162 - Logical Methods in Computer Science, December 17, 2013, Volume 9, Issue 4
Modeling and Verification of Infinite Systems with Resources

Authors: Lang, Martin and Löding, Christof

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.


Source : oai:arXiv.org:1311.1043
DOI : 10.2168/LMCS-9(4:22)2013
Volume: Volume 9, Issue 4
Published on: December 17, 2013
Submitted on: September 17, 2012
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 57 times.
This article's PDF has been downloaded 211 times.