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;]

---

Reasoning about Strategies: on the Satisfiability Problem

Fabio Mogavero ; Aniello Murano ; Giuseppe Perelli ; Moshe Y. Vardi.

Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, subsuming all major previously studied modal logics&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;]

---