5 results
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 […]
Published on March 17, 2017
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 […]
Published on November 12, 2008
Piero A. Bonatti ; Carsten Lutz ; Aniello Murano ; Moshe Y. Vardi.
The fully enriched μ-calculus is the extension of the propositional μ-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched μ-calculus is known to be decidable and ExpTime-complete, it has recently been […]
Published on September 22, 2008
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 […]
Published on February 27, 2012
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