Liveness Verification in TRSs Using Tree Automata and Termination Analysis

Authors

  • Mousa Mousazadeh
  • Behrouz Tork Ladani
  • Hans Zantema

Keywords:

Term rewriting systems, liveness properties, finite tree automata, termination

Abstract

This paper considers verification of the liveness property Live(R, I, G) for a term rewrite system (TRS) R, where I (Initial states) and G (Good states) are two sets of ground terms represented by finite tree automata. Considering I and G, we transform R to a new TRS R' such that termination of R' proves the property Live(R, I, G).

Downloads

Download data is not yet available.

Author Biographies

Mousa Mousazadeh

Department of Computer Engineering
University of Isfahan
Hezar Jerib Av., Isfahan, Iran

Behrouz Tork Ladani

Department of Computer Engineering
University of Isfahan
Hezar Jerib Av., Isfahan, Iran

Hans Zantema

Department of Computer Science
TU Eindhoven
P. O. Box 513, 5600 MB Eindhoven, The Netherlands
&
Institute for Computing and Information Sciences
Radboud University
Nijmegen, P. O. Box 9010, 6500 GL Nijmegen, The Netherlands

Downloads

Published

2012-01-26

How to Cite

Mousazadeh, M., Ladani, B. T., & Zantema, H. (2012). Liveness Verification in TRSs Using Tree Automata and Termination Analysis. COMPUTING AND INFORMATICS, 29(3), 407–426. Retrieved from https://www.cai.sk/ojs/index.php/cai/article/view/91

Issue

Vol. 29 No. 3 (2010): Computing and Informatics

Section

Articles