Abstract

This paper considers verification of the liveness property textsfLive(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 textsfLive(R, I, G).

Keywords

Cite this article

@article{cai-1915,
  author  = {Mousa Mousazadeh and Behrouz Tork Ladani and Hans Zantema},
  title   = {Liveness Verification in TRSs Using Tree Automata and Termination Analysis},
  journal = {Computing and Informatics},
  volume  = {29},
  number  = {3},
  pages   = {407--426},
  year    = {2010},
  issn    = {1335-9150},
  url     = {https://cai.type.sk/content/2010/3/liveness-verification-in-trss-using-tree-automata-and-termination-analysis/}
}
Download .bib