ABSTRACT. The research of Moshe Vardi has influenced many researchers in the field of robotics. During this talk I will give a birds' eye view of how logic and synthesis are used in robotics where a central question is how to produce robot motion from high-level specifications. The specifications declare what the robot must do, rather than how the task is to be done. I will focus on describing how Moshe Vardi's work has led to efficient task and motion planning solutions and synthesis methodologies for human-robot collaboration. 

ABSTRACT. The Safety Fragment of LTL

ABSTRACT. A significant challenge to widespread adoption of reinforcement learning (RL) is the faithful translation of designer’s intent to the scalar reward signal required by RL algorithms. Logic-based specifications help in two ways: by precisely capturing the intended objective, and by allowing its automatic translation to a reward function. Omega-regular objectives, such as those expressed in LTL and by omega-automata, have recently been proposed to specify learning objectives in RL. In this talk, we will discuss the impact of Vardi's contributions to automata-theoretic reinforcement learning.

ABSTRACT. Fifteen years have passed since the introduction of the original turn-based variant of Strategy Logic, and twelve since its full-fledged concurrent extension. Several interesting results have been obtained and, for sure, many more are still to come. The ones that I consider more meaningful concern, in particular, the enlightening connections with other subfields of theoretical computer science, most notably algorithmic game theory and finite model theory, which have enriched and broadened the scientific literature. In this talk, I will overview some of these results, starting with anecdotes on the original work done in 2008, while I was a visiting Ph.D. student at Rice University under Moshe’s supervision, and terminating with a few open questions.

ABSTRACT. The paper discusses a collaboration with Moshe Vardi that started with a work presenting an algorithm that takes one regular expression E and n regular expressions S as input, and returns an automaton which is shown to be the maximal rewriting of E with respect to S.

ABSTRACT. The paper itself is an extended abstract.

ABSTRACT. I propose to present our recent results [LICS'19,LICS'21] on capturing various bisimilarity notions— covering not only the conventional relational notion but also its quantitative extensions such as probabilistic bisimulation and bisimulation metric—in the language of category theory. The theory combines abstract category theory and concrete games—so-called codensity games which are played in categories—which I believe will be of interest of Moshe and the audience.

ABSTRACT. In order to improve the effectiveness of law enforcement agencies, we address the problem of capturing absconding using graph theory, formal methods and game theory. We define a set of problems and we outline an approach to solve them.

ABSTRACT. We point out the surprising connections which have recently been observed between the famous Kochen-Specker theorem in the foundations of quantum mechanics, and algorithmic questions relating to constraint satisfaction and the celebrated Feder-Vardi Dichotomy Conjecture (recently proved by Bulatov and Zhuk), and to the Weisfeiler-Leman approximations to structure isomorphism.

ABSTRACT. In his 1982 landmark paper “The Complexity of Relational Query Languages” [7], Moshe Vardi defined and studied the concept of data complexity of relational query languages, which is the complexity of evaluating a fixed query in the language as a function of the size of the database. Vardi also defines the notion of expression complexity (fixed database, query as input), now often called “program complexit”, and the combined complexity (where both, the database and the query constitute the input). Data complexity has become the standard method for assessing the complexity of query languages. Vardi [7] analysed various query languages and showed that fixed-point queries are complete for PTIME in data complexity by a proof from which the same result for Datalog follows. He noticed that ”the expression complexity of the investigated languages is usually one exponential higher than the data complexity” [7]. Vardi also notes that over ordered structures fixed-point queries (and implicitly Datalog queries) capture PTIME, which was shown independently by Immerman [6], and more explicitly for the second-order Horn fragment corresponding to Datalog by Gr ̈adel [5]. The first part of the talk will give a short overview of these results.

In the second part, I briefly address the complexity and expressive power of ontological reasoning formalisms such as ontology-based data access via description logics [3] or via variants of Datalog [4,1,2]. I will essentially illustrate two points. First, rather than a typical single-exponential jump from data to expression (or combined) complexity for classical logical query languages addressed by Vardi, we now typically have a double-exponential jump. Second, to better understand the expressive power of ontological reasoning formalisms where, in addition to a database (or ABox) and a query, there is an ontology (or TBox or Datalog± program), it is convenient to consider a refined concept of expressive power studied in [1,2], which is defined by the set of Boolean queries that can be expressed when keeping ontologies fixed.

References

[1] Marcelo Arenas, Georg Gottlob, and Andreas Pieris. Expressive languages for querying the semantic web. ACM Trans. Database Syst., 43(3):13:1–13:45, 2018. [2] Gerald Berger, Georg Gottlob, Andreas Pieris, and Emanuel Sallinger. The space-efficient core of vadalog. ACM Trans. Database Syst., 47(1), apr 2022. [3] Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, Antonella Poggi, Mariano Rodriguez-Muro, Riccardo Rosati, Marco Ruzzi, and Domenico Fabio Savo. The mastro system for ontology-based data access. Semantic Web, 2(1):43–53, 2011. [4] Georg Gottlob, Thomas Lukasiewicz, and Andreas Pieris. Datalog+/-: Questions and answers. In 14th Intl. Conf. on the Principles of Knowledge Representation and Reasoning (KR’14), 2014. [5] Erich Gr ̈adel. Capturing complexity classes by fragments of second-order logic. Theoretical Com- puter Science, 101(1):35–57, 1992. [6] Neil Immerman. Relational queries computable in polynomial time (extended abstract). In Pro- ceedings of STOC’82, May 5-7, 1982, San Francisco, California, USA. [7] Moshe Y. Vardi. The complexity of relational query languages. In Proc. of STOC’82, 1982.

ABSTRACT. In this talk we present some of the many examples where Prof. Moshe Vardi’s research has enabled progress in solving some of the most challenging technical problems present in aviation. We touch upon a subset of use-cases from knowledge acquisition, advanced reasoning, planning, environment health and safety, and energy efficiency.

ABSTRACT. The determinization of a nondeterministic B\"uchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman's approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC \emph{independently} from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in a prototype tool named ourDC and empirically evaluate ourDC with the state-of-the-art tools on a large set of benchmarks from the literature. The experimental results show that our prototype ourDC outperforms Spot and Owl regarding the number of states and transitions.

ABSTRACT. We have been studying LTL misconceptions with multiple populations to determine *in what ways* LTL is tricky and to decide *what we can do* to address the issues. We propose an interactive remote talk that aims to demonstrate the LTL misconceptions and expert blind spots that we have found.

ABSTRACT. I will discuss ways to simplify inexpressibility proofs. In particular, I will discuss an approach by Fagin, Stockmeyer and Vardi that greatly simplifies my earlier proof (from my Ph.D. thesis) that monadic NP is not closed under complement, where monadic NP consists of properties defined by existential second-order sentences, where the existential second-order quantifiers range only over subsets of the domain.

ABSTRACT. The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science, such as program analysis and automated verification. Unfortunately, its decidability has been open for nearly a century! In this talk, I will present a brief survey of what is known on the Skolem Problem and related questions, including recent and ongoing developments.

ABSTRACT. I will explain how old papers by Moshe Vardi and Ray Reiter on query answering over incomplete databases led to new recently discovered schemes of efficient approximation of certain answers, and present a previously unknown and exceptionally simple formulation of such schemes for first-order queries over relational databases.

ABSTRACT. I describe my work in connection with several papers by Moshe Vardi.

ABSTRACT. In this talk I will recall a fruitful collaboration between Serge Abiteboul and myself with Moshe, that resulted in the 1997 JACM article with the above title. Under Moshe's impetus, the article completed in a very elegant way previous results, providing a comprehensive and compelling picture, and remains one of my favorite papers.

The results establish a general connection between fixpoint logic and complexity. On one side, we have fixpoint logic, parameterized by the choices of 1st-order operators (inflationary or noninflationary) and iteration constructs (deterministic, nondeterministic, or alternating). On the other side, we have the complexity classes between P and EXPTIME. The parameterized fixpoint logics express the complexity classes P, NP, PSPACE, and EXPTIME, but only over ordered structures.

The order requirement highlights an inherent mismatch between complexity and logic -- while computational devices work on encodings of problems, logic is applied directly to the underlying mathematical structures. To overcome this mismatch, we used a theory of relational complexity based on the relational machine, a computational device that operates directly on structures. Relational complexity bridges the gap between standard complexity and fixpoint logic. On one hand, questions about containments among standard complexity classes can be translated to questions about containments among relational complexity classes. On the other hand, the expressive power of fixpoint logic can be precisely characterized in terms of relational complexity classes. This tight, three-way relationship among fixpoint logics, relational complexity and standard complexity yields in a uniform way logical analogs to all containments among the complexity classes P, NP, PSPACE, and EXPTIME. The logical formulation shows that some of the most tantalizing questions in complexity theory boil down to a single question: the relative power of inflationary vs. noninflationary 1st-order operators.

ABSTRACT. Although I have worked closely with Moshe on counting problems, it will be a tall order to count all the things I've learnt from him -- through his articles, lectures, one-on-one conversations and gems of advice over the years. So I'd rather not try to count but briefly talk of a few (among many) occasions at different stages of my career, when I kept running into Moshe's profound contributions and insights. Starting from my grad school days, Moshe's result with Pierre Wolper on automata theoretic LTL model checking was among my first few introductions to formal verification. Much later, while working with my Ph.D. student on logic and some aspects of finite model theory, we kept running into beautiful results due to Moshe and his collaborators. More recently, while working with Moshe on PAC counting, I recall some very interesting discussions on how 2-, 3- or even 2.5-universal hashing might just be the sweet spot to help achieve a balance between scalability and strong formal guarantees. Almost a decade later, we know how spot-on his prediction was.

ABSTRACT. In this short talk, we will give a retrospective of the collaboration Moshe had with Intel over the past 25 years! This long-lasting collaboration was key in bringing formal verification to industry. It is an excellent example of Vardi’s unique contribution and ability to bridge theory and practice.

ABSTRACT. This summer, we gather to celebrate Moshe Vardi's many pioneering contributions to the theory and practice of computer science, and his leadership qualities and activities. My toast will focus on some less-known ingenious traits he exhibited starting very early in his career. In particular, I will discuss how Moshe acted in the role of a grand translator who applied advanced archery strategies in database research, and will comment on his role as a member of the Gang-of-Four.

ABSTRACT. Proofs of unsatisfiability facilitate the validation of SAT solver results. Practically all top-tier solvers support proof logging and these proofs can efficiently be checked using formally-verified tools. However, the size of these proofs is typically large and sometimes gigantic, thereby making them impossible to understand. On the other hand, one can extract useful information out of proofs, such as unsatisfiable cores or interpolants.

We present some results on extracting some understanding from proofs of unsatisfiability. This work started after a question by Moshe Vardi about the effect of using a large interval for the Pythagorean Triples problem on the size of the proof. Increasing the size of the interval turned out to reduce the size of the proof substantially. It might even be possible to produce a humanly-understandable proof for this problem if the interval is large enough.

We also show some other results in this direction. For example, short proofs of unsatisfiability have been crucial to constructing small unit-distance graphs with chromatic number 5. These graphs are important building blocks to solving the Hadwiger-Nelson problem. Also, compact proofs of mutilated chessboard problems provided an alternative short, humanly-understandable argument of unsatisfiability.

ABSTRACT. In 2008, Moshe Y. Vardi received the ACM SIGMOD Edgar F. Codd Innovations Award for "fundamental contributions to the foundations of relational databases". In his acceptance speech, Moshe referred to database theory as his "first love". The purpose of this talk is to give a bird's eye view of Moshe's contributions to database theory and of his enduring legacy by highlighting some of Moshe's most influential papers in this area.

ABSTRACT. Differential privacy is a mathematical framework for developing statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of differential privacy, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a general accepted definition; accuracy claims of differential privacy algorithms vary from algorithm to algorithm and are not instantiations of a general definition. In a recent paper~\cite{bcksv21}. we identify program discontinuity as a common cause for \emph{ad hoc} definitions and introduce an alternative notion of accuracy parametrized by, what we call, {distance to disagreement} --- the {distance to disagreement} of an input $x$ w.r.t.\, a deterministic computation $f$ and a distance $d$ is the minimal distance $d(x,y)$ over all $y$ such that $f(y)\neq f(x)$. The talk will discuss what this definition entails and identify circumstance under which verifying claims of accuracy is decidable.

ABSTRACT. In this talk I will share the technical stepping stones that were the path from my research world to Moshe’s. My background is in hardware verification and this led to my interest in developing practical SAT solvers that could handle hardware verification problems at scale. This led to the two key contributions of the Chaff SAT solver form my group – the two-literal watching algorithm for unit propagation and the VSIDS (Variable State Independent Decaying Sum) decision heuristic. These techniques built on the earlier success of what is now known as CDCL (Conflict Driven Clause Learning). Collectively these techniques dramatically improved the capabilities to SAT solvers enabling them to tackle problems at scale in not just hardware verification, but system verification and even beyond instances from verification. The practical success of these and subsequent solvers seemed to fly in the face of the theoretical complexity of SAT. This piqued Moshe’s interest and led to his taking a major leadership role in trying to develop the theoretical foundations for what makes these solvers effective for the practical instances of interest –the relationship between the search algorithm and the search space characteristics of the practical instances. He was the driver of a series of workshops titled “Theory and Practice of Satisfiability Solving” held at BIRS Banff (2014), Dagstuhl (2015) and BIRS Oxaca (2018). These workshops were remarkable in their bringing together theoreticians and practitioners interested in SAT in an immersive setting to learn from each other and build bridges between theory and practice for this simultaneously simple and complex problem. Moshe was also instrumental in shepherding articles on the practical successes of SAT and SMT solvers in CACM – making sure this reached out to the broad CS community. My chance to collaborate directly with Moshe came through when Kuldeep Meel visited me at Princeton while he was Moshe’s student. We started working on the problem of finding the minimum/minimal set of independent variables for a given CNF SAT formula. This could significantly simplify the cost of the uniform sampling and model counting algorithms that Kuldeep and Moshe were working on. The collaboration expanded to include Alex Ivrii and led to a nice algorithm for this problem – making my Moshe number 1!

ABSTRACT. Many of us got involved in computing because programming was fun.  The advantages of computing seemed intuitive to us.  We truly believed that computing yields tremendous societal benefits; for example, the life-saving potential of driverless cars is enormous!  Recently, however, computer scientists realized that computing is not a game--it isreal--and it brings with it not only societal benefits, but alsosignificant societal costs, such as labor polarization, disinformation, and smart-phone addiction.

A common reaction to this crisis is to label it as an "ethics crisis".But corporations are driven by profits, not ethics, and machines are just machines.  Only people can be expected to act ethically. In this talk, the speaker will discuss how computer scientists should behave ethically.

(The talk will be also broadcast live. For a webinar link to this talk, please register here: https://bit.ly/VardiFest )

Short Bio: Moshe Y. Vardi, the founding chair of FLoC, is a University Professor and the George Distinguished Service Professor in Computational Engineering at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, the Southeastern Universities Research Association's Distinguished Scientist Award, the ACM SIGLOG Church Award, the Knuth Prize, the ACM Allen Newell Award, and IEEE Norbert Wiener Award for Social and Professional Responsibility.  He holds seven honorary doctorates.