The equivalence problem for program schemata with nonintersecting loops

Publisher Website
Google Scholar
Abstract
In his thesis Paterson proved that equivalence is decidable for program schemata such that every instruction falls on at most one loop and only monadic function signs appear. Here we remove the restriction on function signs. The problem reduces to that of showing that the numerical exponents which satisfy certain "word equations" over a semigroup of acyclic directed graphs may be characterized by sentences of Presburger arithmetic; these exponents correspond to loop coefficients of the program schemata. The central construction is a finite automaton whose memory is a window of bounded size on an acyclic directed graph corresponding to a solution to such a "word equation".

This publication has 0 references indexed in Scilit: