und Theorie
diskreter Systeme

Informatik 7

Automata-theoretic verification with resource bounds

Martin Lang, Christof Löding

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, which 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.


  1. Martin Lang and Christof Löding. Modeling and Verification of Infinite Systems with Resources. Logical Methods in Computer Science 9(4), 2013. PDF BibTeX

    	author = {Martin Lang and Christof L{\"o}ding},
    	title = "Modeling and Verification of Infinite Systems with Resources",
    	journal = "Logical Methods in Computer Science",
    	volume = 9,
    	number = 4,
    	year = 2013,
    	ee = "http://dx.doi.org/10.2168/LMCS-9(4:22)2013, http://arxiv.org/pdf/1311.1043",
    	pdf = "/images/download/papers/lang/ll13.pdf",
    	abstract = "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."
  2. Martin Lang. Resource Reachability Games on Pushdown Graphs. In Anca Muscholl (ed.). Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science series, volume 8412, Springer Berlin Heidelberg, pages 195-209. URL, DOI BibTeX

    	la14 year = 2014,
    	isbn = "978-3-642-54829-1",
    	booktitle = "Foundations of Software Science and Computation Structures",
    	volume = 8412,
    	series = "Lecture Notes in Computer Science",
    	editor = "Muscholl, Anca",
    	doi = "10.1007/978-3-642-54830-7_13",
    	title = "Resource Reachability Games on Pushdown Graphs",
    	url = "http://dx.doi.org/10.1007/978-3-642-54830-7_13",
    	publisher = "Springer Berlin Heidelberg",
    	author = "Lang, Martin",
    	pages = "195-209",
    	abstract = "We consider two-player reachability games with additional resource counters on arenas that are induced by the configuration graphs of pushdown systems. For a play, we define the resource cost to be the highest occurring counter value. In this way, we quantify resources and memory that player 0 needs to win. We introduce the bounded winning problem: Is there a uniform bound k such that player 0 can win the game from a set of initial configurations with this bound k? We provide an effective, saturation-based method to solve this problem for regular sets of initial and goal configurations."
  3. Martin Lang, Christof Löding and Amaldev Manuel. Definability and Transformations for Cost Logics and Automatic Structures. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger and Zoltán Ésik (eds.). Mathematical Foundations of Computer Science 2014. Lecture Notes in Computer Science series, volume 8634, Springer Berlin Heidelberg, 2014, pages 390-401. URL, DOI BibTeX

    	year = 2014,
    	isbn = "978-3-662-44521-1",
    	booktitle = "Mathematical Foundations of Computer Science 2014",
    	volume = 8634,
    	series = "Lecture Notes in Computer Science",
    	editor = "Csuhaj-Varjú, Erzsébet and Dietzfelbinger, Martin and Ésik, Zoltán",
    	doi = "10.1007/978-3-662-44522-8_33",
    	title = "Definability and Transformations for Cost Logics and Automatic Structures",
    	url = "http://dx.doi.org/10.1007/978-3-662-44522-8_33",
    	publisher = "Springer Berlin Heidelberg",
    	author = "Lang, Martin and Löding, Christof and Manuel, Amaldev",
    	pages = "390-401",
    	abstract = "We provide new characterizations of the class of regular cost functions (Colcombet 2009) in terms of first-order logic. This extends a classical result stating that each regular language can be defined by a first-order formula over the infinite tree of finite words with a predicate testing words for equal length. Furthermore, we study interpretations for cost logics and use them to provide different characterizations of the class of resource automatic structures, a quantitative version of automatic structures. In particular, we identify a complete resource automatic structure for first-order interpretations."