Moshe Y. Vardi

is this you? claim profile

George Distinguished Service Professor at Rice University. Consultant at Intel Corporation (1997-2000). Manager, Mathematics and Related Computer Science at IBM (1989 – 1993)

On Satisficing in Quantitative Games

Several problems in planning and reactive synthesis can be reduced to th...
01/06/2021 ∙ by Suguman Bansal, et al. ∙ 6 ∙ share

read it
Nash Equilibria in Finite-Horizon Multiagent Concurrent Games

The problem of finding pure strategy Nash equilibria in multiagent concu...
01/03/2021 ∙ by Senthil Rajasekaran, et al. ∙ 0 ∙ share

read it
On Continuous Local BDD-Based Search for Hybrid SAT Solving

We explore the potential of continuous local search (CLS) in SAT solving...
12/14/2020 ∙ by Anastasios Kyrillidis, et al. ∙ 2 ∙ share

read it
FPRAS Approximation of the Matrix Permanent in Practice

The matrix permanent belongs to the complexity class #P-Complete. It is ...
12/06/2020 ∙ by James E. Newman, et al. ∙ 0 ∙ share

read it
LTLf Synthesis on Probabilistic Systems

Many systems are naturally modeled as Markov Decision Processes (MDPs), ...
09/23/2020 ∙ by Andrew M. Wells, et al. ∙ 4 ∙ share

read it
LTLf Synthesis under Partial Observability: From Theory to Practice

LTL synthesis is the problem of synthesizing a reactive system from a fo...
09/23/2020 ∙ by Lucas M. Tabajara, et al. ∙ 0 ∙ share

read it
DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees

We propose a unifying dynamic-programming framework to compute exact lit...
08/20/2020 ∙ by Jeffrey M. Dudek, et al. ∙ 2 ∙ share

read it
On Uniformly Sampling Traces of a Transition System (Extended Version)

A key problem in constrained random verification (CRV) concerns generati...
08/12/2020 ∙ by Supratik Chakraborty, et al. ∙ 0 ∙ share

read it
Parallel Weighted Model Counting with Tensor Networks

A promising new algebraic approach to weighted model counting makes use ...
06/28/2020 ∙ by Jeffrey M. Dudek, et al. ∙ 0 ∙ share

read it
On the Power of Unambiguity in Büchi Complementation

In this work, we exploit the power of unambiguity for the complementatio...
05/18/2020 ∙ by Yong Li, et al. ∙ 0 ∙ share

read it
FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints

The Boolean SATisfiability problem (SAT) is of central importance in com...
12/02/2019 ∙ by Anastasios Kyrillidis, et al. ∙ 0 ∙ share

read it
Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications

LTLf synthesis is the automated construction of a reactive system from a...
11/19/2019 ∙ by Suguman Bansal, et al. ∙ 0 ∙ share

read it
Solving Parity Games Using An Automata-Based Algorithm

Parity games are abstract infinite-round games that take an important ro...
10/30/2019 ∙ by Antonio Di Stasio, et al. ∙ 0 ∙ share

read it
Efficient Contraction of Large Tensor Networks for Weighted Model Counting through Graph Decompositions

Constrained counting is a fundamental problem in artificial intelligence...
08/12/2019 ∙ by Jeffrey M. Dudek, et al. ∙ 3 ∙ share

read it
On Symbolic Approaches for Computing the Matrix Permanent

Counting the number of perfect matchings in bipartite graphs, or equival...
08/08/2019 ∙ by Supratik Chakraborty, et al. ∙ 0 ∙ share

read it
ADDMC: Exact Weighted Model Counting with Algebraic Decision Diagrams

We compute exact literal-weighted model counts of CNF formulas. Our algo...
07/11/2019 ∙ by Jeffrey M. Dudek, et al. ∙ 4 ∙ share

read it
Sequential Relational Decomposition

The concept of decomposition in computer science and engineering is cons...
03/04/2019 ∙ by Dror Fried, et al. ∙ 0 ∙ share

read it
First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation

Translating formulas of Linear Temporal Logic (LTL) over finite traces, ...
01/18/2019 ∙ by Shufang Zhu, et al. ∙ 0 ∙ share

read it
Comparator automata in quantitative verification

The notion of comparison between system runs is fundamental in formal ve...
12/17/2018 ∙ by Suguman Bansal, et al. ∙ 0 ∙ share

read it
SAT-based Explicit LTLf Satisfiability Checking

We present here a SAT-based framework for LTLf (Linear Temporal Logic on...
11/07/2018 ∙ by Jianwen Li, et al. ∙ 0 ∙ share

read it
Functional Synthesis via Input-Output Separation

Boolean functional synthesis is the process of constructing a Boolean fu...
08/24/2018 ∙ by Supratik Chakraborty, et al. ∙ 0 ∙ share

read it
The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas

Recent universal-hashing based approaches to sampling and counting cruci...
10/17/2017 ∙ by Jeffrey M. Dudek, et al. ∙ 0 ∙ share

read it
On Hashing-Based Approaches to Approximate DNF-Counting

Propositional model counting is a fundamental problem in artificial inte...
10/14/2017 ∙ by Kuldeep S. Meel, et al. ∙ 0 ∙ share

read it
A Symbolic Approach to Safety LTL Synthesis

Temporal synthesis is the automated design of a system that interacts wi...
09/21/2017 ∙ by Shufang Zhu, et al. ∙ 0 ∙ share

read it
Symbolic LTLf Synthesis

LTLf synthesis is the process of finding a strategy that satisfies a lin...
05/23/2017 ∙ by Shufang Zhu, et al. ∙ 0 ∙ share

read it
Approximate Probabilistic Inference via Word-Level Counting

Hashing-based model counting has emerged as a promising approach for lar...
11/24/2015 ∙ by Supratik Chakraborty, et al. ∙ 0 ∙ share

read it
Distribution-Aware Sampling and Weighted Model Counting for SAT

Given a CNF formula and a weight for each assignment of values to variab...
04/11/2014 ∙ by Supratik Chakraborty, et al. ∙ 0 ∙ share

read it
The Complexity of Integer Bound Propagation

Bound propagation is an important Artificial Intelligence technique used...
01/16/2014 ∙ by Lucas Bordeaux, et al. ∙ 0 ∙ share

read it
Complete Axiomatizations for Reasoning About Knowledge and Time

Sound and complete axiomatizations are provided for a number of differen...
08/20/2002 ∙ by Joseph Y. Halpern, et al. ∙ 0 ∙ share

read it

Moshe Y. Vardi

Featured Co-authors