Modeling and Verification of Infinite Systems with Resources
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 consumpt...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2013-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1162/pdf |
| _version_ | 1797268684229574656 |
|---|---|
| author | Martin Lang Christof Löding |
| author_facet | Martin Lang Christof Löding |
| author_sort | Martin Lang |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:23Z |
| format | Article |
| id | doaj.art-355a73b5e1a54086af371f2c3755ade9 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:23Z |
| publishDate | 2013-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-355a73b5e1a54086af371f2c3755ade92024-03-08T09:30:37ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742013-12-01Volume 9, Issue 410.2168/LMCS-9(4:22)20131162Modeling and Verification of Infinite Systems with ResourcesMartin LangChristof LödingWe 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.https://lmcs.episciences.org/1162/pdfcomputer science - logic in computer science |
| spellingShingle | Martin Lang Christof Löding Modeling and Verification of Infinite Systems with Resources Logical Methods in Computer Science computer science - logic in computer science |
| title | Modeling and Verification of Infinite Systems with Resources |
| title_full | Modeling and Verification of Infinite Systems with Resources |
| title_fullStr | Modeling and Verification of Infinite Systems with Resources |
| title_full_unstemmed | Modeling and Verification of Infinite Systems with Resources |
| title_short | Modeling and Verification of Infinite Systems with Resources |
| title_sort | modeling and verification of infinite systems with resources |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/1162/pdf |
| work_keys_str_mv | AT martinlang modelingandverificationofinfinitesystemswithresources AT christofloding modelingandverificationofinfinitesystemswithresources |