Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
5 results

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;]
Published on September 22, 2008
Volume 4, Issue 3

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;]
Published on November 12, 2008
Volume 4, Issue 4

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;]
Published on December 18, 2014
Volume 10, Issue 4

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;]
Published on March 27, 2013
Volume 9, Issue 1

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;]
Published on June 30, 2014
Volume 10, Issue 2
  • < Previous
  • 1
  • Next >