Search

• < Previous
• 1
• Next >

---

B\"uchi Complementation and Size-Change Termination

Seth Fogarty ; Moshe Y. Vardi.

We compare tools for complementing nondeterministic B\"uchi automata with a recent termination-analysis algorithm. Complementation of B\"uchi automata is a key step in program verification. Early constructions using a Ramsey-based argument have been supplanted by rank-based constructions with&nbsp;[&hellip;]

---

Synthesis from Probabilistic Components

Sumit Nain ; Yoad Lustig ; Moshe Y Vardi.

Synthesis is the automatic construction of a system from its specification. In classical synthesis algorithms, it is always assumed that the system is "constructed from scratch" rather than composed from reusable components. This, of course, rarely happens in real life, where almost every&nbsp;[&hellip;]

---

State of B\"uchi Complementation

Ming-Hsien Tsai ; Seth Fogarty ; Moshe Y. Vardi ; Yih-Kuen Tsay.

Complementation of B\"uchi automata has been studied for over five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. Regarding the performance of these&nbsp;[&hellip;]

---

Sequential Relational Decomposition

Dror Fried ; Axel Legay ; Joël Ouaknine ; Moshe Y. Vardi.

The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in&nbsp;[&hellip;]

---

Comparator automata in quantitative verification

Suguman Bansal ; Swarat Chaudhuri ; Moshe Y. Vardi.

The notion of comparison between system runs is fundamental in formal verification. This concept is implicitly present in the verification of qualitative systems, and is more pronounced in the verification of quantitative systems. In this work, we identify a novel mode of comparison in quantitative&nbsp;[&hellip;]

---