ACTAS : A System Design for Associative and Commutative Tree Automata Theory
ACTAS : A System Design for Associative and Commutative Tree Automata Theory
复制标题
ACTAS：关联和交换树自动机理论的系统设计
DOI：
10.1016/j.entcs.2004.07.017
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Toshinori Takai
中科院分区：
文献类型：
--
作者：
H. Ohsaki;Toshinori Takai
ACTAS是一个用于操作关联交换树自动机（简称AC树自动机）的集成系统，它具有AC树自动机的布尔运算、重写后代计算、空性和成员问题求解等多种功能。为了在合理的时间内处理高复杂性问题，还配备了过近似和欠近似算法。这样的功能使我们能够在无限状态模型中自动验证安全属性，这在例如网络安全的领域中是有帮助的，特别是对于允许等式属性的密码协议的安全问题。在模型构建过程中，为状态空间扩展分析提供了工具支持。计算的中间状态以数值数据表的形式显示，并生成折线图。此外，该系统的图形用户界面为我们提供了一个方便的使用环境。
ACTAS is an integrated system for manipulating associative and commutative tree automata (AC-tree automata for short), that has various functions such as for Boolean operations of AC-tree automata, computing rewrite descendants, and solving emptiness and membership problems. In order to deal with high-complexity problems in reasonable time, over- and under-approximation algorithms are also equipped. Such functionality enables us automated verification of safety property in infinite state models, that is helpful in the domain of, e.g. network security, in particular, for security problems of cryptographic protocols allowing an equational property. In runtime of model construction, a tool support for analysis of state space expansion is provided. The intermediate status of the computation is displayed in numerical data table, and also the line graphs are generated. Besides, a graphical user interface of the system provides us a user-friendly environment for handy use.