
On Satisficing in Quantitative Games
Several problems in planning and reactive synthesis can be reduced to th...
read it

Nash Equilibria in FiniteHorizon Multiagent Concurrent Games
The problem of finding pure strategy Nash equilibria in multiagent concu...
read it

On Continuous Local BDDBased Search for Hybrid SAT Solving
We explore the potential of continuous local search (CLS) in SAT solving...
read it

FPRAS Approximation of the Matrix Permanent in Practice
The matrix permanent belongs to the complexity class #PComplete. It is ...
read it

LTLf Synthesis on Probabilistic Systems
Many systems are naturally modeled as Markov Decision Processes (MDPs), ...
read it

LTLf Synthesis under Partial Observability: From Theory to Practice
LTL synthesis is the problem of synthesizing a reactive system from a fo...
read it

DPMC: Weighted Model Counting by Dynamic Programming on ProjectJoin Trees
We propose a unifying dynamicprogramming framework to compute exact lit...
read it

On Uniformly Sampling Traces of a Transition System (Extended Version)
A key problem in constrained random verification (CRV) concerns generati...
read it

Parallel Weighted Model Counting with Tensor Networks
A promising new algebraic approach to weighted model counting makes use ...
read it

On the Power of Unambiguity in Büchi Complementation
In this work, we exploit the power of unambiguity for the complementatio...
read it

FourierSAT: A Fourier ExpansionBased Algebraic Framework for Solving Hybrid Boolean Constraints
The Boolean SATisfiability problem (SAT) is of central importance in com...
read it

Hybrid Compositional Reasoning for Reactive Synthesis from FiniteHorizon Specifications
LTLf synthesis is the automated construction of a reactive system from a...
read it

Solving Parity Games Using An AutomataBased Algorithm
Parity games are abstract infiniteround games that take an important ro...
read it

Efficient Contraction of Large Tensor Networks for Weighted Model Counting through Graph Decompositions
Constrained counting is a fundamental problem in artificial intelligence...
read it

On Symbolic Approaches for Computing the Matrix Permanent
Counting the number of perfect matchings in bipartite graphs, or equival...
read it

ADDMC: Exact Weighted Model Counting with Algebraic Decision Diagrams
We compute exact literalweighted model counts of CNF formulas. Our algo...
read it

Sequential Relational Decomposition
The concept of decomposition in computer science and engineering is cons...
read it

FirstOrder vs. SecondOrder Encodings for LTLftoAutomata Translation
Translating formulas of Linear Temporal Logic (LTL) over finite traces, ...
read it

Comparator automata in quantitative verification
The notion of comparison between system runs is fundamental in formal ve...
read it

SATbased Explicit LTLf Satisfiability Checking
We present here a SATbased framework for LTLf (Linear Temporal Logic on...
read it

Functional Synthesis via InputOutput Separation
Boolean functional synthesis is the process of constructing a Boolean fu...
read it

The Hard Problems Are Almost Everywhere For Random CNFXOR Formulas
Recent universalhashing based approaches to sampling and counting cruci...
read it

On HashingBased Approaches to Approximate DNFCounting
Propositional model counting is a fundamental problem in artificial inte...
read it

A Symbolic Approach to Safety LTL Synthesis
Temporal synthesis is the automated design of a system that interacts wi...
read it

Symbolic LTLf Synthesis
LTLf synthesis is the process of finding a strategy that satisfies a lin...
read it

Approximate Probabilistic Inference via WordLevel Counting
Hashingbased model counting has emerged as a promising approach for lar...
read it

DistributionAware Sampling and Weighted Model Counting for SAT
Given a CNF formula and a weight for each assignment of values to variab...
read it

The Complexity of Integer Bound Propagation
Bound propagation is an important Artificial Intelligence technique used...
read it

Complete Axiomatizations for Reasoning About Knowledge and Time
Sound and complete axiomatizations are provided for a number of differen...
read it
Moshe Y. Vardi
is this you? claim profile
George Distinguished Service Professor at Rice University. Consultant at Intel Corporation (19972000). Manager, Mathematics and Related Computer Science at IBM (1989 – 1993)