research
∙
05/15/2023
On Strategies in Synthesis Over Finite Traces
The innovations in reactive synthesis from Linear Temporal Logics over f...
share
research
∙
05/01/2023
Multi-Agent Systems with Quantitative Satisficing Goals
In the study of reactive systems, qualitative properties are usually eas...
research
∙
01/24/2023
Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints
Determining the satisfiability of Boolean constraint-satisfaction proble...
research
∙
09/26/2022
Quantum-Inspired Perfect Matching under Vertex-Color Constraints
We propose and study the graph-theoretical problem PM-VC: perfect matchi...
research
∙
05/20/2022
Synthesis from Satisficing and Temporal Goals
Reactive synthesis from high-level specifications that combine hard cons...
research
∙
05/19/2022
DPER: Dynamic Programming for Exist-Random Stochastic SAT
In Bayesian inference, the maximum a posteriori (MAP) problem combines t...
research
∙
05/17/2022
DPO: Dynamic-Programming Optimization on Hybrid Constraints
In Bayesian inference, the most probable explanation (MPE) problem reque...
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...
research
∙
05/02/2022
Verification and Realizability in Finite-Horizon Multiagent Systems
The problems of verification and realizability are two central themes in...
research
∙
08/26/2021
Automata Linear Dynamic Logic on Finite Traces
Temporal logics are widely used by the Formal Methods and AI communities...
research
∙
01/06/2021
On Satisficing in Quantitative Games
Several problems in planning and reactive synthesis can be reduced to th...
research
∙
01/03/2021
Nash Equilibria in Finite-Horizon Multiagent Concurrent Games
The problem of finding pure strategy Nash equilibria in multiagent concu...
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...
research
∙
12/06/2020
FPRAS Approximation of the Matrix Permanent in Practice
The matrix permanent belongs to the complexity class #P-Complete. It is ...
research
∙
09/23/2020
LTLf Synthesis on Probabilistic Systems
Many systems are naturally modeled as Markov Decision Processes (MDPs), ...
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...
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...
research
∙
08/12/2020
On Uniformly Sampling Traces of a Transition System (Extended Version)
A key problem in constrained random verification (CRV) concerns generati...
research
∙
06/28/2020
Parallel Weighted Model Counting with Tensor Networks
A promising new algebraic approach to weighted model counting makes use ...
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...
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...
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...
research
∙
10/30/2019
Solving Parity Games Using An Automata-Based Algorithm
Parity games are abstract infinite-round games that take an important ro...
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...
research
∙
08/08/2019
On Symbolic Approaches for Computing the Matrix Permanent
Counting the number of perfect matchings in bipartite graphs, or equival...
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...
research
∙
03/04/2019
Sequential Relational Decomposition
The concept of decomposition in computer science and engineering is cons...
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, ...
research
∙
12/17/2018
Comparator automata in quantitative verification
The notion of comparison between system runs is fundamental in formal ve...
research
∙
11/07/2018
SAT-based Explicit LTLf Satisfiability Checking
We present here a SAT-based framework for LTLf (Linear Temporal Logic on...
research
∙
08/24/2018
Functional Synthesis via Input-Output Separation
Boolean functional synthesis is the process of constructing a Boolean fu...
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...
research
∙
10/14/2017
On Hashing-Based Approaches to Approximate DNF-Counting
Propositional model counting is a fundamental problem in artificial inte...
research
∙
09/21/2017
A Symbolic Approach to Safety LTL Synthesis
Temporal synthesis is the automated design of a system that interacts wi...
research
∙
05/23/2017
Symbolic LTLf Synthesis
LTLf synthesis is the process of finding a strategy that satisfies a lin...
research
∙
11/24/2015
Approximate Probabilistic Inference via Word-Level Counting
Hashing-based model counting has emerged as a promising approach for lar...
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...
research
∙
01/16/2014
The Complexity of Integer Bound Propagation
Bound propagation is an important Artificial Intelligence technique used...
research
∙
08/20/2002