Back to: FsmReg
AbbrName Ceta
FullName Ceta: A Library for Equational Tree Automata
ItemDesc 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.



Type FsmCompiler









LatestVersion Alpha 4
Topic revision: r1 - 2008-10-23 - AnssiYliJyra
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2019 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback