5 results
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 […]
Published on December 18, 2014
Seth J. Fogarty ; Orna Kupferman ; Thomas Wilke ; Moshe Y. Vardi.
Complementation of B\"uchi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that […]
Published on March 27, 2013
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 […]
Published on June 30, 2014
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 […]
Published on July 29, 2022
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 […]
Published on March 3, 2022