11 found
Sort by:
  1. Orna Kupferman, Shmuel Safra & Moshe Y. Vardi (2006). Relating Word and Tree Automata. Annals of Pure and Applied Logic 138 (1):126-146.
    In the automata-theoretic approach to verification, we translate specifications to automata. Complexity considerations motivate the distinction between different types of automata. Already in the 60s, it was known that deterministic Büchi word automata are less expressive than nondeterministic Büchi word automata. The proof is easy and can be stated in a few lines. In the late 60s, Rabin proved that Büchi tree automata are less expressive than Rabin tree automata. This proof is much harder. In this work we relate the (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  2. Guoqiang Pan, Ulrike Sattler & Moshe Y. Vardi (2006). BDD-Based Decision Procedures for the Modal Logic K ★. Journal of Applied Non-Classical Logics 16 (1-2):169-207.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Moshe Y. Vardi & A. Voronkov (2003). Logic for Programming Artificial Intelligence and Reasoning 10th International Conference, Lpar 2003, Almaty, Kazakhstan, September 22-26, 2003 : Proceedings. [REVIEW]
    No categories
     
    My bibliography  
     
    Export citation  
  4. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi & Victor Vianu (2001). On the Unusual Effectiveness of Logic in Computer Science. Bulletin of Symbolic Logic 7 (2):213-236.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  5. Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Y. Vardi (1999). Common Knowledge Revisited. Annals of Pure and Applied Logic 96 (1-3):89-105.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  6. Orna Kupferman & Moshe Y. Vardi (1999). Church's Problem Revisited. Bulletin of Symbolic Logic 5 (2):245-263.
    In program synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, then at each moment it reads input signals and writes output signals, which depend on the input signals and the history of the computation so far. The specification considers all possible input sequences. Thus, if the specification is linear, it should hold in every computation generated by the interaction, and if the specification is branching, it should hold in (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  7. Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Y. Vardi (1997). Reasoning About Knowledge: A Response by the Authors. [REVIEW] Minds and Machines 7 (1):113-113.
  8. Erich Grädel, Phokion G. Kolaitis & Moshe Y. Vardi (1997). On the Decision Problem for Two-Variable First-Order Logic. Bulletin of Symbolic Logic 3 (1):53-69.
    We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  9. Moshe Y. Vardi (1997). Special Selection in Logic in Computer Science. Journal of Symbolic Logic 62 (2):608.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  10. Ronald Fagin, Joseph Y. Halpern & Moshe Y. Vardi (1992). What is an Inference Rule? Journal of Symbolic Logic 57 (3):1018-1045.
    What is an inference rule? This question does not have a unique answer. One usually finds two distinct standard answers in the literature; validity inference $(\sigma \vdash_\mathrm{v} \varphi$ if for every substitution $\tau$, the validity of $\tau \lbrack\sigma\rbrack$ entails the validity of $\tau\lbrack\varphi\rbrack)$, and truth inference $(\sigma \vdash_\mathrm{t} \varphi$ if for every substitution $\tau$, the truth of $\tau\lbrack\sigma\rbrack$ entails the truth of $\tau\lbrack\varphi\rbrack)$. In this paper we introduce a general semantic framework that allows us to investigate the notion of inference (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  11. Moshe Y. Vardi (1991). Verification of Concurrent Programs: The Automata-Theoretic Framework. Annals of Pure and Applied Logic 51 (1-2):79-98.
    Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 79–98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if a program PA, obtained by combining P and A, (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation