Logics of repeating values on data trees and branching counter systems
We study connections between the satisfiability problem for logics on data trees and Branching Vector Addition Systems (BVAS). We consider a natural temporal logic of “repeating values” (LRV) featuring an operator which tests whether a data value in the current node is repeated in some descendant no...
| Publicado: |
2017
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10203LNCS_n_p196_Abriola http://hdl.handle.net/20.500.12110/paper_03029743_v10203LNCS_n_p196_Abriola |
| Aporte de: |
| id |
paper:paper_03029743_v10203LNCS_n_p196_Abriola |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_03029743_v10203LNCS_n_p196_Abriola2023-06-08T15:28:14Z Logics of repeating values on data trees and branching counter systems Computation theory Forestry Formal logic Merging Petri nets Vectors Branching structures Branching vector addition systems with state Control state Counter systems Coverability problem Satisfiability Satisfiability problems Vector addition systems Trees (mathematics) We study connections between the satisfiability problem for logics on data trees and Branching Vector Addition Systems (BVAS). We consider a natural temporal logic of “repeating values” (LRV) featuring an operator which tests whether a data value in the current node is repeated in some descendant node. On the one hand, we show that the satisfiability of a restricted version of LRV on ranked data trees can be reduced to the coverability problem for Branching Vector Addition Systems. This immediately gives elementary upper bounds for its satisfiability problem, showing that restricted LRV behaves much better than downward-XPath, which has a non-primitive-recursive satisfiability problem. On the other hand, satisfiability for LRV is shown to be reducible to the coverability for a novel branching model we introduce here, called Merging VASS (MVASS). MVASS is an extension of Branching Vector Addition Systems with States (BVASS) allowing richer merging operations of the vectors. We show that the control-state reachability for MVASS, as well as its bottom-up coverability, are in 3ExpTime. This work can be seen as a natural continuation of the work initiated by Demri, D’Souza and Gascon for the case of data words, this time considering branching structures and counter systems, although, as we show, in the case of data trees more powerful models are needed to encode satisfiability. © Springer-Verlag GmbH Germany 2017. 2017 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10203LNCS_n_p196_Abriola http://hdl.handle.net/20.500.12110/paper_03029743_v10203LNCS_n_p196_Abriola |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Computation theory Forestry Formal logic Merging Petri nets Vectors Branching structures Branching vector addition systems with state Control state Counter systems Coverability problem Satisfiability Satisfiability problems Vector addition systems Trees (mathematics) |
| spellingShingle |
Computation theory Forestry Formal logic Merging Petri nets Vectors Branching structures Branching vector addition systems with state Control state Counter systems Coverability problem Satisfiability Satisfiability problems Vector addition systems Trees (mathematics) Logics of repeating values on data trees and branching counter systems |
| topic_facet |
Computation theory Forestry Formal logic Merging Petri nets Vectors Branching structures Branching vector addition systems with state Control state Counter systems Coverability problem Satisfiability Satisfiability problems Vector addition systems Trees (mathematics) |
| description |
We study connections between the satisfiability problem for logics on data trees and Branching Vector Addition Systems (BVAS). We consider a natural temporal logic of “repeating values” (LRV) featuring an operator which tests whether a data value in the current node is repeated in some descendant node. On the one hand, we show that the satisfiability of a restricted version of LRV on ranked data trees can be reduced to the coverability problem for Branching Vector Addition Systems. This immediately gives elementary upper bounds for its satisfiability problem, showing that restricted LRV behaves much better than downward-XPath, which has a non-primitive-recursive satisfiability problem. On the other hand, satisfiability for LRV is shown to be reducible to the coverability for a novel branching model we introduce here, called Merging VASS (MVASS). MVASS is an extension of Branching Vector Addition Systems with States (BVASS) allowing richer merging operations of the vectors. We show that the control-state reachability for MVASS, as well as its bottom-up coverability, are in 3ExpTime. This work can be seen as a natural continuation of the work initiated by Demri, D’Souza and Gascon for the case of data words, this time considering branching structures and counter systems, although, as we show, in the case of data trees more powerful models are needed to encode satisfiability. © Springer-Verlag GmbH Germany 2017. |
| title |
Logics of repeating values on data trees and branching counter systems |
| title_short |
Logics of repeating values on data trees and branching counter systems |
| title_full |
Logics of repeating values on data trees and branching counter systems |
| title_fullStr |
Logics of repeating values on data trees and branching counter systems |
| title_full_unstemmed |
Logics of repeating values on data trees and branching counter systems |
| title_sort |
logics of repeating values on data trees and branching counter systems |
| publishDate |
2017 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10203LNCS_n_p196_Abriola http://hdl.handle.net/20.500.12110/paper_03029743_v10203LNCS_n_p196_Abriola |
| _version_ |
1768542839762845696 |