RTA open problem #101

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #101

Originator: Hitoshi Ohsaki [OT02]
Date: July 2002

Summary: Are universality and inclusion of AC-recognizable languages decidable?

An AC-tree automaton as defined by [Ohs01] is given by a signature Σ, a set of AC-axioms (that is, associativity and commutativity) for some function symbols of Σ, and a set of rewrite rules R of the form

f(q₁,…,q_n)	→	q	(1)
f(q₁,…,q_n)	→	f(p₁,…,p_n)	(2)
q	→	p	(3)

where the q’s and p’s are state symbols. Such an automaton accepts a term t iff it rewrites t modulo the given AC-axioms to some final state. L(A) denotes the language recognized by an AC-tree automaton A; a language L is called AC-recognizable iff L=L(A) for some AC-tree automaton A.

Are the following questions decidable?

Universality: Given an AC-tree automaton A, is L(A) equal to the set of all ground terms over the given signature Σ?
Inclusion: Given AC-tree automata A and B, is L(A) a subset of L(B)?

It has been shown [OT02] that emptiness of AC-recognizable languages is decidable. Furthermore, as a consequence of the results of [ZL03], universality and inclusion are decidable if transition rules of the form f(q₁,…,q_n) → f(p₁,…,p_n) are not allowed (this is the sub-class of so-called regular AC tree-automata). However, both questions are still open in the general case.

Remark

The inclusion problem of AC-tree automata is undecidable [OTTR05]. Decidability of universality is still an open question.

References

[Ohs01]: Hitoshi Ohsaki. Beyond regularity: Equational tree automata for associative and commutative theories. In Laurent Fribourg, editor, 15th International Workshop on Computer Science Logic, volume 2142 of Lecture Notes in Computer Science, pages 539–553, Paris, France, September 2001. Springer-Verlag.
[OT02]: Hitoshi Ohsaki and Toshinori Takai. Decidability and closure properties of equational tree languages. In Sophie Tison, editor, Rewriting Techniques and Applications, volume 2378 of Lecture Notes in Computer Science, pages 114–128, Copenhagen, Denmark, July 2002. Springer-Verlag.
[OTTR05]: Hitoshi Ohsaki, Jean-Marc Talbot, Sophie Tison, and Yves Roos. Monotone AC-tree automata. In Geoff Sutcliffe and Andrei Voronkov, editors, 12th International Conference on Logic Programming and Automated Reasoning, volume 3835 of Lecture Notes in Artificial Intelligence, pages 337–351, Montego Bay, Jamaica, December 2005. Springer-Verlag.
[ZL03]: Silvano Dal Zilio and Denis Lugiez. XML schema, tree logic and sheaves automata. In Robert Nieuwenhuis, editor, 14th International Conference on Rewriting Techniques, volume 2706 of Lecture Notes in Computer Science, pages 246–263, Valencia, Spain, June 2003. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]