Prelegent(ci)

Jerome Leroux

Afiliacja

University of Bordeaux

Termin

17 października 2018 14:15

Pokój

p. 5050

Tytuł w języku angielskim

CHANGE!) Reachability for Two-Counter Machines with One Test and One Rese

Seminarium

Seminarium „Teoria automatów”

---

We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.

Joint work with Alain Finkel and Grégoire Sutre.

---