The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Este artigo apresenta uma estratégia juntamente com ferramentas de suporte para a tradução de máquinas de estados de teorias equacionais para teorias de reescrita, visando gerar automaticamente especificações de teorias de reescrita. Esforços duplicados podem ser economizados na especificação de máquinas de estado tanto em teorias equacionais quanto em teorias de reescrita, quando incorporamos os recursos de prova de teoremas do CafeOBJ com os recursos de verificação de modelos de Maude. Os resultados experimentais mostram que as eficiências das especificações geradas pela estratégia proposta são significativamente melhoradas, em comparação com aquelas geradas por três outras estratégias de tradução existentes.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copiar
Min ZHANG, Kazuhiro OGATA, Masaki NAKAMURA, "Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support" in IEICE TRANSACTIONS on Information,
vol. E94-D, no. 5, pp. 976-988, May 2011, doi: 10.1587/transinf.E94.D.976.
Abstract: This paper presents a strategy together with tool support for the translation of state machines from equational theories into rewrite theories, aiming at automatically generating rewrite theory specifications. Duplicate effort can be saved on specifying state machines both in equational theories and rewrite theories, when we incorporate the theorem proving facilities of CafeOBJ with the model checking facilities of Maude. Experimental results show that efficiencies of the generated specifications by the proposed strategy are significantly improved, compared with those that are generated by three other existing translation strategies.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E94.D.976/_p
Copiar
@ARTICLE{e94-d_5_976,
author={Min ZHANG, Kazuhiro OGATA, Masaki NAKAMURA, },
journal={IEICE TRANSACTIONS on Information},
title={Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support},
year={2011},
volume={E94-D},
number={5},
pages={976-988},
abstract={This paper presents a strategy together with tool support for the translation of state machines from equational theories into rewrite theories, aiming at automatically generating rewrite theory specifications. Duplicate effort can be saved on specifying state machines both in equational theories and rewrite theories, when we incorporate the theorem proving facilities of CafeOBJ with the model checking facilities of Maude. Experimental results show that efficiencies of the generated specifications by the proposed strategy are significantly improved, compared with those that are generated by three other existing translation strategies.},
keywords={},
doi={10.1587/transinf.E94.D.976},
ISSN={1745-1361},
month={May},}
Copiar
TY - JOUR
TI - Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support
T2 - IEICE TRANSACTIONS on Information
SP - 976
EP - 988
AU - Min ZHANG
AU - Kazuhiro OGATA
AU - Masaki NAKAMURA
PY - 2011
DO - 10.1587/transinf.E94.D.976
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E94-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2011
AB - This paper presents a strategy together with tool support for the translation of state machines from equational theories into rewrite theories, aiming at automatically generating rewrite theory specifications. Duplicate effort can be saved on specifying state machines both in equational theories and rewrite theories, when we incorporate the theorem proving facilities of CafeOBJ with the model checking facilities of Maude. Experimental results show that efficiencies of the generated specifications by the proposed strategy are significantly improved, compared with those that are generated by three other existing translation strategies.
ER -