Moshe Y. Vardi

research

∙ 05/20/2022

Synthesis from Satisficing and Temporal Goals

Reactive synthesis from high-level specifications that combine hard cons...

Suguman Bansal, et al. ∙

research

∙ 05/19/2022

DPER: Dynamic Programming for Exist-Random Stochastic SAT

In Bayesian inference, the maximum a posteriori (MAP) problem combines t...

Vu H. N. Phan, et al. ∙

research

∙ 05/17/2022

DPO: Dynamic-Programming Optimization on Hybrid Constraints

In Bayesian inference, the most probable explanation (MPE) problem reque...

Vu H. N. Phan, et al. ∙

research

∙ 05/08/2022

DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving

Boolean MaxSAT, as well as generalized formulations such as Min-MaxSAT a...

Anastasios Kyrillidis, et al. ∙

research

∙ 05/02/2022

Verification and Realizability in Finite-Horizon Multiagent Systems

The problems of verification and realizability are two central themes in...

Senthil Rajasekaran, et al. ∙

research

∙ 08/26/2021

Automata Linear Dynamic Logic on Finite Traces

Temporal logics are widely used by the Formal Methods and AI communities...

Kevin W. Smith, et al. ∙

research

∙ 01/06/2021

On Satisficing in Quantitative Games

Several problems in planning and reactive synthesis can be reduced to th...

Suguman Bansal, et al. ∙

research

∙ 01/03/2021

Nash Equilibria in Finite-Horizon Multiagent Concurrent Games

The problem of finding pure strategy Nash equilibria in multiagent concu...

Senthil Rajasekaran, et al. ∙

research

∙ 12/14/2020

On Continuous Local BDD-Based Search for Hybrid SAT Solving

We explore the potential of continuous local search (CLS) in SAT solving...

Anastasios Kyrillidis, et al. ∙

research

∙ 12/06/2020

FPRAS Approximation of the Matrix Permanent in Practice

The matrix permanent belongs to the complexity class #P-Complete. It is ...

James E. Newman, et al. ∙

research

∙ 09/23/2020

LTLf Synthesis on Probabilistic Systems

Many systems are naturally modeled as Markov Decision Processes (MDPs), ...

Andrew M. Wells, et al. ∙

research

∙ 09/23/2020

LTLf Synthesis under Partial Observability: From Theory to Practice

LTL synthesis is the problem of synthesizing a reactive system from a fo...

Lucas M. Tabajara, et al. ∙

research

∙ 08/20/2020

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

We propose a unifying dynamic-programming framework to compute exact lit...

Jeffrey M. Dudek, et al. ∙

research

∙ 08/12/2020

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

A key problem in constrained random verification (CRV) concerns generati...

Supratik Chakraborty, et al. ∙

research

∙ 06/28/2020

Parallel Weighted Model Counting with Tensor Networks

A promising new algebraic approach to weighted model counting makes use ...

Jeffrey M. Dudek, et al. ∙

research

∙ 05/18/2020

On the Power of Unambiguity in Büchi Complementation

In this work, we exploit the power of unambiguity for the complementatio...

Yong Li, et al. ∙

research

∙ 12/02/2019

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

The Boolean SATisfiability problem (SAT) is of central importance in com...

Anastasios Kyrillidis, et al. ∙

research

∙ 11/19/2019

Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications

LTLf synthesis is the automated construction of a reactive system from a...

Suguman Bansal, et al. ∙

research

∙ 10/30/2019

Solving Parity Games Using An Automata-Based Algorithm

Parity games are abstract infinite-round games that take an important ro...

Antonio Di Stasio, et al. ∙

research

∙ 08/12/2019

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

Constrained counting is a fundamental problem in artificial intelligence...

Jeffrey M. Dudek, et al. ∙

research

∙ 08/08/2019

On Symbolic Approaches for Computing the Matrix Permanent

Counting the number of perfect matchings in bipartite graphs, or equival...

Supratik Chakraborty, et al. ∙

research

∙ 07/11/2019

ADDMC: Exact Weighted Model Counting with Algebraic Decision Diagrams

We compute exact literal-weighted model counts of CNF formulas. Our algo...

Jeffrey M. Dudek, et al. ∙

research

∙ 03/04/2019

Sequential Relational Decomposition

The concept of decomposition in computer science and engineering is cons...

Dror Fried, et al. ∙

research

∙ 01/18/2019

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

Translating formulas of Linear Temporal Logic (LTL) over finite traces, ...

Shufang Zhu, et al. ∙

research

∙ 12/17/2018

Comparator automata in quantitative verification

The notion of comparison between system runs is fundamental in formal ve...

Suguman Bansal, et al. ∙

research

∙ 11/07/2018

SAT-based Explicit LTLf Satisfiability Checking

We present here a SAT-based framework for LTLf (Linear Temporal Logic on...

Jianwen Li, et al. ∙

research

∙ 08/24/2018

Functional Synthesis via Input-Output Separation

Boolean functional synthesis is the process of constructing a Boolean fu...

Supratik Chakraborty, et al. ∙

research

∙ 10/17/2017

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

Recent universal-hashing based approaches to sampling and counting cruci...

Jeffrey M. Dudek, et al. ∙

research

∙ 10/14/2017

On Hashing-Based Approaches to Approximate DNF-Counting

Propositional model counting is a fundamental problem in artificial inte...

Kuldeep S. Meel, et al. ∙

research

∙ 09/21/2017

A Symbolic Approach to Safety LTL Synthesis

Temporal synthesis is the automated design of a system that interacts wi...

Shufang Zhu, et al. ∙

research

∙ 05/23/2017

Symbolic LTLf Synthesis

LTLf synthesis is the process of finding a strategy that satisfies a lin...

Shufang Zhu, et al. ∙

research

∙ 11/24/2015

Approximate Probabilistic Inference via Word-Level Counting

Hashing-based model counting has emerged as a promising approach for lar...

Supratik Chakraborty, et al. ∙

research

∙ 04/11/2014

Distribution-Aware Sampling and Weighted Model Counting for SAT

Given a CNF formula and a weight for each assignment of values to variab...

Supratik Chakraborty, et al. ∙

research

∙ 01/16/2014

The Complexity of Integer Bound Propagation

Bound propagation is an important Artificial Intelligence technique used...

Lucas Bordeaux, et al. ∙

research

∙ 08/20/2002

Complete Axiomatizations for Reasoning About Knowledge and Time

Sound and complete axiomatizations are provided for a number of differen...

Joseph Y. Halpern, et al. ∙

Moshe Y. Vardi

Featured Co-authors