Search

• < Previous
• 1
• Next >

---

Unifying B\"uchi Complementation Constructions

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&nbsp;[&hellip;]

---

Multi-Objective Model Checking of Markov Decision Processes

Kousha Etessami ; Marta Kwiatkowska ; Moshe Y. Vardi ; Mihalis Yannakakis.

We study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, M, and given multiple linear-time (\omega -regular or LTL) properties \varphi\_i, and probabilities r\_i \epsilon [0,1], i=1,...,k, we ask whether there exists a&nbsp;[&hellip;]

---

The Complexity of Enriched Mu-Calculi

Piero A. Bonatti ; Carsten Lutz ; Aniello Murano ; Moshe Y. Vardi.

The fully enriched &mu;-calculus is the extension of the propositional &mu;-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched &mu;-calculus is known to be decidable and ExpTime-complete, it has recently been&nbsp;[&hellip;]

---