Liveness Verification in TRSs Using Tree Automata and Termination Analysis
Mousa Mousazadeh ; Behrouz Tork Ladani ; Hans Zantema
Computing and Informatics, Tome 28 (2012) no. 1, / Harvested from Computing and Informatics
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).
Publié le : 2012-01-26
Classification:  Term rewriting systems; liveness properties; finite tree automata; termination
@article{cai91,
     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 = {28},
     number = {1},
     year = {2012},
     language = {en},
     url = {http://dml.mathdoc.fr/item/cai91}
}
Mousa Mousazadeh; Behrouz Tork Ladani; Hans Zantema. Liveness Verification in TRSs Using Tree Automata and Termination Analysis. Computing and Informatics, Tome 28 (2012) no. 1, . http://gdmltest.u-ga.fr/item/cai91/