Research
Research
My research interests lie in various aspects of logic in Computer Science and their application to areas of formal methods and verification, and automated reasoning. My group deploys tools from logic, theory and algorithms, and artificial intelligence, to find solutions and construct tools that meet our research challenges. I describe below two of our current projects, feel free to contact me to discuss or to collaborate.
Boolean functional synthesis is the process of constructing a Boolean skolem function from a Boolean specification (often given as a CNF formula) that relates input and output variables. Such a function indicates a concrete output assignment for any given input assignment, that all in all satisfies the initial specification. Despite significant recent developments in synthesis algorithms, Boolean functional synthesis remains a challenging problem. A much more generalized problem is that of reactive synthesis, where the specification is given in a form of a temporal logic (typically Linear Temporal Logic - LTL) and the solution comes in a form of a strategy, often described as a finite states transducer.
Since propositional formulas are a special case of LTL formulas, it is only natural to try and elevate some of the insights and success gained on Boolean functioncal synthesis, towards insights in reactive synthesis, and apply these to construct more efficient reactive synthesis tools. One concept is that of a syntacitic separation of a formula to inputs and outputs fragment. In the Boolean case, every formula is equivalent to a set of constraints, where each constraint is separated to an input fragment that contains only input variables, and an output fragment that contains only output variables. This separateion is then deployed in a Boolean functional synthesis tool. Together with my students, I explore the concept of LTL formulas that are also separated to inputs and outputs fragments. Such formulas, while being a special case of LTL, describe various relations between temporal behaviors of two systems, such as adaptation of a behavior from one system to another. We explore this special case of LTL and try to see whether we can elevate the techniques from Boolean functional synthesis to the temporal one. More on this can be found here: FMCAD2018 ,CAV2021, JAIR2023 .
Another concept fairly prevalant in Boolean formulas, is that of dependent variables, for which in every potential solution, the assignment for such variables is completely determined, once the assigmnent for the other variables is decided. Various Boolean functional synthesis techniques make use of dependent variables, and try to find and reason on these mostly in a pre-process step, before the heavier synthesis techniques come into play. In our work, we reason on the concept of dependent variables in LTL formulas, starting with properly deifning the concept of dependency in LTL, then searching for techniques to detect and utilize such dependent variables, towards an all in all a construction of a better synthesis tool. For details see here: TACAS2024.
Model Counting (MC) is the problem of counting the number of satisfying assignments for a given Boolean formula. This problem is related to problems such as system testing, probabilistic inferences, and networks. It is also known to be #P-hard, which means that an efficient solution is unlikely to be found. In my group, we are studying problems that are related problems to exact and approximated model counting.
One of the projects that we are exploring is the role of the formula's solution space in efficient model counting. It is known that certain solution space structures allow fast model checking even by means of binary search. We are interested to see whether a given formula can be transformed to another formula with the same number of solution, and with a solution space that allows fast solution. Such a transformation should also be as a efficient as possible, in order to yield an effective model counting tool. More details can be found here: FSTTCS2019.
Another problem that we are exploting is of Weighted Model Counting (WMC), in which every assignment has a weight (typically a product of the weighted "true" assignment of the literals) and the objective is to find the summed weights of the assignments that satisfy the formula. The approach that we are currently exploring is to use specific formulas, called chain formulas, to transform weights to specific additional Boolean clauses with additional variables, and thus effectively reduce WMC to MC. This method has already proven itself for exact and approximated WMC, but it seems that much more can be done with chain formulas wrt compact representations of weights, specifically in probabilistic inference models. See here for details: IJCAI2015, NeurIPS2020 .