View article

T hispaperconsiders nite-autom ata based algorithm sforhandling lineararithm eticw ith both real and integer variables. P revious w ork has show n that this theory can be dealt w ith by using nite autom ata on in nite w ords, but this involves som e di cult and delicate to im plem ent algorithm s. T he contribution ofthis paper is to show, using topologicalargum ents, that only a restricted class ofautom ata on in nite w ords are necessary for handling realand integer linear arithm etic. T his allow s the use ofsubstantially sim pler algorithm s, w hich have been successfully im plem ented.