Search

• < Previous
• 1
• Next >

---

Model Checking Vector Addition Systems with one zero-test

Rémi Bonnet ; Alain FInkel ; Jérôme Leroux ; Marc Zeitoun.

We design a variation of the Karp-Miller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zero-test. This algorithm yields decision procedures for several problems for these&nbsp;[&hellip;]

---

The Covering Problem

Thomas Place ; Marc Zeitoun.

An important endeavor in computer science is to understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, "understanding" is not a mathematical notion. This investigation requires therefore a concrete objective to capture this understanding. In the&nbsp;[&hellip;]

---

Separating Regular Languages with First-Order Logic

Thomas Place ; Marc Zeitoun.

Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in&nbsp;[&hellip;]

---

Separation for dot-depth two

Thomas Place ; Marc Zeitoun.

The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free languages of finite words. By a theorem of McNaughton and Papert, these are also the first-order definable languages. The dot-depth rose to prominence following the work of Thomas, who proved an exact correspondence with the&nbsp;[&hellip;]

---