Ceta: A Library for Equational Tree Automata


Ceta is a library for reasoning about combinations of equational tree languages. It supports emptiness testing of tree languages definable by a boolean combination of regular tree automaton over an equational theory containing operators that are associative and/or commutative with identity symbols. Ceta is based on propositional tree automata, and offers algorithms and datastructures for representing tree automata, combining tree automata using boolean operations, and testing emptiness. ACTAS screenshot

Ceta is currently being used in the Maude Sufficient Completeness checker, and ACTAS a reachability analysis tool. Using Ceta, ACTAS has been able to verify the security of the Diffie-Hellman key-exchange protoco" and Shamir's three-path protocol without approximation techniques.

Ceta is being developed at the University of Illinois at Urbana-Champaign in the United States as part of a joint project with National Institute of Advanced Industrial Science and Technology in Japan. The primary software developer is Joe Hendrix with significant support from Josè Meseguer of UIUC and Hitoshi Ohsaki of AIST.

The project is currently in active development, and a number of key planned features have not yet been implemented. An alpha version is now available which supports combining equational tree automata and testing emptiness of automaton that are associative, commutative, and free. We do not yet support support rules with constraints, but that is planned for a future release. Ceta is available under the GPL license.


Feb. 4, 2007
Released Alpha 4. This release should significantly improve the performance of the emptiness test with AC symbols, and adds support for membership.


The source code for Ceta is now available as a gzipped tar file. Building Ceta requires the followig be installed:

The following files are available for download:

Name Format Date
ceta-alpha4.tar.gz Source gzipped tar 2007-02-05
ceta-alpha3a.tar.gz Source gzipped tar 2006-03-06
ceta-alpha2.tar.gz Source gzipped tar 2005-11-17
ceta-alpha1.tar.gz Source gzipped tar 2005-09-12

Due to the alpha nature of Ceta and the current world of C++ ABI compatibilities, we do not offer a precompiled version of Ceta at this time.


Ceta's documentation is automatically generated using Doxygen. A copy of the documentation is included in the source, but may also be browsed online.

Announcement Mailing list

In order to be informed of new releases, users are strongly encouraged to subscribe to the ceta-announce mailing list. This is an announce only list used to notify subscribed about news related to Ceta's development. The traffic will be at most a few messages per month. Subscribe or unsubscribe at the ceta-announce homepage.


If you are interested in doing development on the library, please contact Joe Hendrix to discuss ideas for improving Ceta and how to add your code to the main repository.