Modeling and verification of infinite systems with resources

DOI10.2168/LMCS-9(4:22)2013MaRDI QIDQ2871475zbMATH OpenFDO

Authors Martin Lang, Christof Löding

Publication date 8 January 2014

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1311.1043

zbMATH Keywords

pushdown systemsquantitative automata and logicsreachability with annotations

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• scientific article; zbMATH DE number 2080052
• Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
• Complexity of model checking recursion schemes for fragments of the modal mu-calculus
• Computer Science Logic
• scientific article; zbMATH DE number 1670791

Cited in

(2)

• Programming with Infinitesimals: A While-Language for Hybrid System Modeling
• Decidable models of integer-manipulating programs with recursive parallelism

Describes a project that uses

Uses Software

• jMoped

This page was built for publication: Modeling and verification of infinite systems with resources

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2871475)