ACTAS
General information
About ACTAS and CETA
ACTAS is an integrated system for manipulating monotone associative and commutative tree automata
(monotone AC tree automata). The system has various functions such as for computing Boolean closures
of AC tree automata (partly supported by CETA);
incrementally computing rewrite descendants of AC tree automata provided that rewrite system is given;
and, solving emptiness and membership problems for monotone AC tree automata.
In order to deal with high-complexity problems in reasonable time, several
computations can be over- and under-approximated. This functionality enables us
to automate verification of safety property in infinite state models.
In practice, this might be useful in dealing with, for instance, security problems of
cryptographic protocols with equational properties.
In runtime of model construction, a tool support for analyzing state space expansion
is provided. The intermediate status of the computation is displayed as in numerical
data table and in line graphs. Besides, a graphical user interface
of the system provides a user-friendly environment for convenient use. (See the above figure)
The ACTAS tool is developed by
Hitoshi Ohsaki and
Toshinori Takai at AIST.
The project was partly supported by
PRESTO "Information and Systems" program of JST (2002.11–2006.4).
The optional software library CETA,
based on Ginsburg's algorithm for semi-linear sets, is developed by
Joe Hendrix at UIUC. This library is also
used in the
Maude Sufficient Completeness checker.
For experimental challenge, a translator from a protocol description language
(PROUVÉ) to ACTAS has been designed under collaboration with
Ralf Treinen.
See the project report 11 for details.
Download
Latest version: (beta-version for Linux is distributed individually by request)
Document, icon and logo
- User guide (in Japanese)
- ACTAS icon
- ACTAS logo (1, 2)
Copyright notice
The ACTAS tool including user guide, icon and logo is distributed by and copyrighted to Hitoshi Ohsaki, AIST. The CETA library is available under the GPL license.