Navegar

Colección

Datos Estadísticas

Artículo

Abriola, S.; Figueira, D.; Figueira, S.; Esparza J.; Murawski A.S. "Logics of repeating values on data trees and branching counter systems" (2017) 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017. 10203 LNCS:196-212
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

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.

Registro:

Documento: Artículo
Título:Logics of repeating values on data trees and branching counter systems
Autor:Abriola, S.; Figueira, D.; Figueira, S.; Esparza J.; Murawski A.S.
Filiación:University of Buenos Aires, Buenos Aires, Argentina
ICC-CONICET, Buenos Aires, Argentina
CNRS, LaBRI, Talence, France
Palabras clave: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)
Año:2017
Volumen:10203 LNCS
Página de inicio:196
Página de fin:212
DOI: http://dx.doi.org/10.1007/978-3-662-54458-7_12
Título revista:20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10203LNCS_n_p196_Abriola

Referencias:

  • Baelde, D., Lunel, S., Schmitz, S., A sequent calculus for a modal logic on finite data trees (2016) 25Th EACSL Annual Conference on Computer Science Logic, pp. 1-32. , CSL 29, 1 September 2016, Marseille, France
  • Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., Two-variable logic on data trees and XML reasoning (2009) JACM, 56 (3), p. 13
  • Bojańczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L., Two-variable logic on data words ACM Trans. Comput. Log, 12 (4), p. 2010
  • Bollig, B., Cyriac, A., Gastin, P., Narayan Kumar, K., Model checking languages of data words (2012) Fossacs 2012. LNCS, 7213, pp. 391-405. , Birkedal, L. (ed.), Springer, Heidelberg
  • Demri, S., D’Souza, D., Gascon, R., A decidable temporal logic of repeating values (2007) LFCS 2007. LNCS, 4514, pp. 180-194. , Artemov, S.N., Nerode, A. (eds.), Springer, Heidelberg
  • Demri, S., D’Souza, D., Gascon, R., Temporal logics of repeating values (2012) J. Log. Comput., 22 (5), pp. 1059-1096
  • Demri, S., Figueira, D., Praveen, M., Reasoning about data repetitions with counter systems (2013) LICS, pp. 33-42. , IEEE Press
  • Demri, S., Jurdziński, M., Lachish, O., Lazić, R., The covering and boundedness problems for branching vector addition systems (2013) J. Comput. Syst. Sci., 79 (1), pp. 23-38
  • Demri, S., Lazić, R., LTL with the freeze quantifier and register automata (2009) ACM Trans. Comput. Log., 10 (3)
  • Emerson, E.A., Halpern, J.Y., “Sometimes” and “not never” revisited: On branching versus linear time temporal logic (1986) JACM, 33 (1), pp. 151-178
  • Figueira, D., (2010) Forward-Xpath and Extended Register Automata on Data-Trees, , ICDT. ACM
  • Figueira, D., Alternating register automata on finite data words and trees (2012) Log. Methods Comput. Sci., 8 (1)
  • Figueira, D., Decidability of downward XPath (2012) ACM Trans. Comput. Log., 13 (4)
  • Figueira, D., (2013) On Xpath with Transitive Axes and Data Tests, pp. 249-260. , PODS
  • Figueira, D., Figueira, S., Areces, C., Basic model theory of XPath on data trees (2014) ICDT, pp. 50-60
  • Figueira, D., Libkin, L., Pattern logics and auxiliary relations (2014) CSL-LICS, pp. 1-40
  • Figueira, D., Segoufin, L., Future-looking logics on data words and trees (2009) MFCS 2009. LNCS, 5734, pp. 331-343. , Královič, R., Niwiński, D. (eds.), Springer, Heidelberg
  • Figueira, D., Segoufin, L., (2011) Bottom-up automata on data trees and vertical XPath, 9, pp. 93-104. , STACS, of LIPIcs
  • Jacquemard, F., Segoufin, L., Dimino, J., FO2(< +1, ∼) on data trees, data tree automata and branching vector addition systems (2016) Log. Methods Comput. Sci, 12 (2)
  • Jurdziński, M., Lazić, R., Alternating automata on data trees and XPath satisfiability (2011) ACM Trans. Comput. Log., 12 (3), p. 19
  • Kara, A., Schwentick, T., Zeume, T., (2010) Temporal Logics on Words with Multiple Data Values, , FST & TCS
  • Kupferman, O., Vardi, M., Memoryful branching-time logic (2006) LICS, pp. 265-274. , IEEE Press
  • Lazić, R., Sylvain, S., Nonelementary complexities for branching VASS, MELL, and extensions (2015) ACM Trans. Comput. Log., 16 (3), p. 20
  • Lisitsa, A., Potapov, I., Temporal logic with predicate λ-abstraction (2005) TIME, pp. 147-155
  • Neven, F., Schwentick, T., Vianu, V., Finite state machines for strings over infinite alphabets (2004) ACM Trans. Comput. Log., 5 (3), pp. 403-435
  • Pnueli, A., The temporal logic of programs (1977) FOCS, pp. 46-57
  • Rackoff, C., The covering and boundedness problems for vector addition systems (1978) Theoret. Comput. Sci., 6 (2), pp. 223-231
  • Segoufin, L., Automata and logics for words and trees over an infinite alphabet (2006) CSL 2006. LNCS, 4207, pp. 41-57. , Ésik, Z. (ed.), Springer, Heidelberg
  • Verma, K.N., Goubault-Larrecq, J., Karp-Miller trees for a branching extension of VASS (2005) Discrete Math. Theor. Comput. Sci., 7 (1), pp. 217-230A4 -

Citas:

---------- APA ----------
Abriola, S., Figueira, D., Figueira, S., Esparza J. & Murawski A.S. (2017) . Logics of repeating values on data trees and branching counter systems. 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017, 10203 LNCS, 196-212.
http://dx.doi.org/10.1007/978-3-662-54458-7_12
---------- CHICAGO ----------
Abriola, S., Figueira, D., Figueira, S., Esparza J., Murawski A.S. "Logics of repeating values on data trees and branching counter systems" . 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017 10203 LNCS (2017) : 196-212.
http://dx.doi.org/10.1007/978-3-662-54458-7_12
---------- MLA ----------
Abriola, S., Figueira, D., Figueira, S., Esparza J., Murawski A.S. "Logics of repeating values on data trees and branching counter systems" . 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017, vol. 10203 LNCS, 2017, pp. 196-212.
http://dx.doi.org/10.1007/978-3-662-54458-7_12
---------- VANCOUVER ----------
Abriola, S., Figueira, D., Figueira, S., Esparza J., Murawski A.S. Logics of repeating values on data trees and branching counter systems. Lect. Notes Comput. Sci. 2017;10203 LNCS:196-212.
http://dx.doi.org/10.1007/978-3-662-54458-7_12