Search

• < Previous
• 1
• Next >

---

Reasoning about Data Repetitions with Counter Systems

Stephane Demri ; Diego Figueira ; M Praveen.

We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability&nbsp;[&hellip;]

---

On Functions Weakly Computable by Pushdown Petri Nets and Related Systems

J. Leroux ; M. Praveen ; Ph. Schnoebelen ; G. Sutre.

We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growing functions $F_\alpha$ for $\alpha<\omega^\omega$, hence they are computationally more powerful than standard vector&nbsp;[&hellip;]

---

Playing with Repetitions in Data Words Using Energy Games

Diego Figueira ; Anirban Majumdar ; M. Praveen.

We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables ranging over an infinite data domain, thus generating&nbsp;[&hellip;]

---

Verification of Flat FIFO Systems

Alain Finkel ; M. Praveen.

The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by&nbsp;[&hellip;]

---