Karp-Miller Trees for a Branching Extension of VASSReportar como inadecuado

Karp-Miller Trees for a Branching Extension of VASS - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LRR-TUM - Institut für Informatik 2 LSV - Laboratoire Spécification et Vérification Cachan 3 SECSI - Security of information systems LSV - Laboratoire Spécification et Vérification Cachan, ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643

Abstract : We study BVASS Branching VASS which extend VASS Vector Addition Systems with States by allowing addition transitions that merge two configurations. Runs in BVASS are tree-like structures instead of linear ones as for VASS. We show that the construction of Karp-Miller trees for VASS can be extended to BVASS. This entails that the coverability set for BVASS is computable. This allows us to obtain decidability results for certain classes of equational tree automata with an associative-commutative symbol. Recent independent work by de Groote et al. implies that decidability of reachability in BVASS is equivalent to decidability of provability in MELL multiplicative exponential linear logic, which is still an open problem. Hence our results are also a step towards answering this question in the affirmative.

Keywords : equational tree automata branching vector addition systems Karp-Miller trees coverability multiplicative exponential linear logic

Autor: Kumar Neeraj Verma - Jean Goubault-Larrecq -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados