Sciweavers

STACS
1999
Springer
13 years 9 months ago
The Weakness of Self-Complementation
Model checking is a method for the verification of systems with respect to their specifications. Symbolic model-checking, which enables the verification of large systems, procee...
Orna Kupferman, Moshe Y. Vardi
ADL
2000
Springer
225views Digital Library» more  ADL 2000»
13 years 9 months ago
Using Regular Tree Automata as XML Schemas
We address the problem of tight XML schemas and propose regular tree automata to model XML data. We show that the tree automata model is more powerful that the XML DTDs and is clo...
Boris Chidlovskii
CSL
2001
Springer
13 years 9 months ago
Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories
Abstract. A new tree automata framework, called equational tree automata, is presented. In the newly introduced setting, congruence closures of recognizable tree languages are reco...
Hitoshi Ohsaki
CAV
2004
Springer
152views Hardware» more  CAV 2004»
13 years 10 months ago
Abstract Regular Model Checking
Regular Tree Model Checking Ahmed Bouajjani, Peter Habermehl 1 LIAFA, University Paris 7, Case 7014, 2, place Jussieu, F-75251 Paris Cedex 05, France Adam Rogalewicz, Tom´aˇs Voj...
Ahmed Bouajjani, Peter Habermehl, Tomás Voj...
FROCOS
2007
Springer
13 years 11 months ago
Languages Modulo Normalization
Abstract. We propose a new class of tree automata, called tree automata with normalization (TAN). This framework extends equational tree automata, and improved the results of them:...
Hitoshi Ohsaki, Hiroyuki Seki
FOSSACS
2007
Springer
13 years 11 months ago
Tree Automata with Memory, Visibility and Structural Constraints
Tree automata with one memory have been introduced in
Hubert Comon-Lundh, Florent Jacquemard, Nicolas Pe...
CSR
2007
Springer
13 years 11 months ago
Marrying Words and Trees
Traditionally, data that has both linear and hierarchical structure, such as annotated linguistic data, is modeled using ordered trees and queried using tree automata. In this pap...
Rajeev Alur
LICS
2007
IEEE
13 years 11 months ago
A Contraction Method to Decide MSO Theories of Deterministic Trees
In this paper we generalize the contraction method, originally proposed by Elgot and Rabin and later extended by Carton and Thomas, from labeled linear orderings to colored determ...
Angelo Montanari, Gabriele Puppis
IRI
2008
IEEE
13 years 11 months ago
Modeling and synthesis of service composition using tree automata
— We revisit the problem of synthesis of service composition in the context of service oriented architecture from a tree automata perspective. Comparing to existing finite state...
Ken Q. Pu, Ying Zhu
RP
2009
Springer
124views Control Systems» more  RP 2009»
13 years 11 months ago
Forward Analysis of Dynamic Network of Pushdown Systems Is Easier without Order
Dynamic networks of Pushdown Systems (PDN in short) have been introduced to perform static analysis of concurrent programs that may spawn threads dynamically. In this model the se...
Denis Lugiez