ABSTRACT. This talk intends to take the listener along a path weaving a picture from threads of science, history and personal details. It is about connections, connections between theories, between people, between names and places. It is about the beauty and effectiveness of theories and of the individual random walks from which they emerge.

ABSTRACT. Moshe Vardi is a highly inspiring computer scientist, who has made groundbreaking contributions in the last four decades to logic and automata, as well as its diverse applications in computer science, including formal verification, databases, computational complexity, knowledge reasoning, to name a few. Moshe's research has personally inspired me to conduct research at the border of different areas in computer science, glued together by logic and automata. I would like to dedicate my recent work joint with Diego Figueira and Artur J\.{e}z, which is to appear in PODS'22, to Moshe. The work combines a number of different areas --- finite model theory, graph databases, automata theory, and SMT --- to all of which, Moshe has made significant contributions.

We initiate the study of data-path query languages (in particular, regular data path queries (RDPQ) and conjunctive RDPQ (CRDPQ)) in the classic setting of embedded finite model theory, wherein each graph is ``embedded'' into a background infinite structure (with a decidable FO theory or fragments thereof). Our goal is to address the current lack of support for typed attribute data (e.g.\ integer arithmetics) in existing data-path query languages, which are crucial in practice. We propose an extension of register automata by allowing powerful constraints over the theory and the database as guards, and having two types of registers: registers that can store values from the active domain, and read-only registers that can store arbitrary values. We prove NL data complexity for (C)RDPQ over various standard theories in SMT; namely, the Presburger arithmetic, the real-closed field, the existential theory of automatic structures and word equations with regular constraints. All these results strictly extend the known NL data complexity of RDPQ with only equality comparisons, and provides an answer to a recent open problem posed by Libkin et al. Among others, we introduce one crucial proof technique for obtaining NL data complexity for data path queries over embedded graph databases called ``Restricted Register Collapse (RRC)'', inspired by the notion of Restricted Quantifier Collapse (RQC) in embedded finite model theory.

ABSTRACT. Synthesis techniques for temporal logic specifications are typically based on exploiting symbolic techniques, as done in model checking. These symbolic techniques typically use backward fixpoint computation. Planning, which can be seen as a specific form of synthesis, is a witness of the success of forward search approaches. In this talk, we present a forward-search approach to full-fledged Linear Temporal Logic on finite traces (LTLf) synthesis. We show how to compute the Deterministic Finite Automaton (DFA) of an LTLf formula on-the-fly, while performing an adversarial forward search towards the final states, by considering the DFA as a sort of AND-OR graph. Our approach is characterized by branching on suitable propositional formulas, instead of individual evaluations, hence radically reducing the branching factor of the search space. Specifically, we take advantage of techniques developed for knowledge compilation, such as Sentential Decision Diagrams (SDDs), to implement the approach efficiently.

ABSTRACT. The main Web page of FLoC-2022 includes a rephrase of the opening sentence of the Aaron Bradley and Zohar Manna's book: "Logic is the calculus of computation". This phrase naturally leads to the question if there is a language with expressive syntax and semantics that can combine the strength of logic and calculus, and if there are reasoning mechanisms for solving practical problems formulated in that language ? It turns out that the answer is affirmative, and combinations of this kind have been already proposed. But I would like to argue they were not ambitious enough, and not motivated enough by practical problems outside of CS. There is a lot more that can be done. In particular, M.Vardi and his colleagues studied aspects of how to effectively integrate Task and Motion Planning (TAMP), a research direction that is explored by several research groups. This research direction is related to planning and control of hybrid systems. The latter are called hybrid because they include both discrete parameterized actions and continuous parameterized processes that can be initiated and terminated by the agent actions or by external events. It turns out, that there are interesting classes of hybrid systems, where the states have relation structure as in databases. I would like to argue that a recently developed Hybrid Temporal Situation Calculus provides a language for a combination of logic and calculus that can be useful for representation and reasoning about relational hybrid systems. This language develops the situation calculus of John McCarthy and Ray Reiter, in particular, sequential temporal situation calculus of Reiter, towards including ordinary differential equations to compute continuous change over time. Also, I would like to argue that constraint logic programming (CLP) leads naturally to reasoning algorithms that can find near-optimal solutions for the planning problem in relational hybrid systems. The computational problems of this kind are usually solved using the methods of the Mixed-Integer Non-Linear Programming (MINLP) by a large community. However, I formulate a hypothesis that logic and reasoning algorithms combined with calculus and strengthened by external NLP solvers can be better suited not only to the task of modelling relational hybrid systems, but also to the task of computing near-optimal plans more efficiently, and, moreover, for the larger scale system than are currently feasible with MINLP alone. I conclude with an invitation to explore more a new direction that can demonstrate "Not So Unusual Effectiveness of Logic" from the angle that was little explored before.

ABSTRACT. In this talk, I am going to present the results of SAT-based reasoning for LTL over finite and infinite traces, the crux of which is to utilize the SAT solver to compute the states of the automaton w.r.t. an LTL (or LTLf ) formula on the fly. The series of work is accomplished by working with Moshe since 2014 and partially working with Kristin as well. Up to now, we have several applications based on this framework, including LTL satisfiability checking [3, 4], LTLf satisfiability checking [1, 2], and LTLf synthesis [5]. I will show such applications in a high-level way and presents the state-of-the-art results we have obtained. Finally, I will also discuss the possible research directions that are worth exploring further, e.g., on-the-fly LTL model checking, LTL synthesis and etc.

ABSTRACT. In formal system design, model checking is a well-established method to automatically check for global correctness of systems. In such a framework, in order to verify whether a system is correct with respect to a desired property, we describe its structure with a mathematical model, specify the property with a temporal logic formula, and check formally that the model satisfies the specification. This method has been first conceived for closed systems whose behavior is completely determined by their internal states and transitions.

In late 90s, interest has arisen in analyzing the behavior of individual components (or sets of components) in systems with multiple entities. The interest began in the field of reactive systems, which are systems that interact continually with their environments and whose behaviour depends on this interaction. Successively, researchers have looked for logics to reason about, and verify strategic behavior of agents in multi-agent systems.

The aim of this contribution is to report on the main developments made in the last 20 years in formal verification of reactive and multi-agent systems. In particular, we will report on CTL* module checking, ATL* model checking, and Strategy Logic.

ABSTRACT. The codication of legal artefacts in formal logic has a long tradition, dating back, among others, to seminal works be G. W. Leibniz. More recent works include the use of epistemic and deontic logics in the formalization of laws and contracts. While many of the existing approaches focus on issues of expressiveness, adequateness and non-automated reasoning with respect to the considered logics, our interest lies in a Computer Science and System Analysis perspective. In particular, we aim at developing tools that build on mechanized logics and perform automated consistency analysis for legal contract documents. Inconsistencies in legal contracts can be static, which means that they include contradictory textual information, or they can be dynamic, leading to (a potential) non-executability of the contract during its dynamic execution. We will present a method and tool called Con- tractCheck [1], which performs static and dynamic logical consistency analyses of Share Purchase Agreements (SPAs) based on the SMT solver Z3. We focus on its application to SPAs in the acquisition of corporations, since these are typically shielded from many of the implicit legal background facts implied by legal dogmatics. Starting from the denition of an ontology for SPAs, we provide structured text blocks in ContractCheck from which the contract can be composed. ContractCheck encodes the relevant legal facts from each of the blocks of an SPA in a logic encompassing decidable fragments of rst-order logic (linear real arithmetic, uninterpreted functions). The logical model, together with the applicable logical consistency constraints, are handed over to the SMT solver, and the analysis results are then depicted by ContractCheck. Using an illustrative example we will exemplify the capabilities of ContractCheck. In addition to the computation of inconsistencies, the model construction capabilities of the SMT solver synthesize dynamic contract executions consistent with the contractual constraints. The MaxSMT capabilities even permit to compute preferable orders of claim executions. We view our work as an illustration of how far mechanized logic can take us in understanding and improving even the non-technical facets of the world that we live in. [1] Alan Khoja, Martin Kolbl, Stefan Leue, and Rudiger Wilhelmi. Automated consistency analysisfor legal contracts. In Proc. of the SPIN Symposium on Model Checking Software, SPIN 2022, LNCS. Springer Verlag, 2022. To appear.

ABSTRACT. We survey our results on a formalism to model and reason about systems with reconfigurable communication interfaces. Processes in our formalism are independent state machines communicating by exchanging messages on broadcast and multicast channels. Messages can include additional data values allowing for further design flexibility. Broadcasts can be customized to target only recipients satisfying certain conditions on their states. Processes can connect to and disconnect from multicast channels and messages can go through only once a condition on the state of all recipients (those listening to the channel) is satisfied. Dependence on the local state of senders and receivers implies that interaction interfaces are reconfigured through execution. Reconfiguration occurs both at message level and channel level.

We show that such systems can be represented and reasoned about symbolically by including existential quantification in the definition of the transition relation. The quantification allows to apply conditions imposed by senders in a way that depends on the local state of recipients. While this symbolic representation supports a global semantics and efficient analysis, it is not compositional. We match the symbolic representation with a compositional semantics through Channeled Transition Systems. When coming to consider the partial order semantics of such reconfigurable systems, we identify that additional information about interleaving needs to be included in the partial order.

On the reasoning side, we consider an extension of LTL that allows to reason about the contents of messages and the intentions of senders when setting conditions on receivers. We support modelling and analysis through model checking of a simple programming language tailored for the production of such processes.

ABSTRACT. I will talk about Strategy Logic: a powerful language for strategic reasoning that Moshe Vardi introduced a decade ago and quickly became widely applied in Formal Methods and AI. I will do it with a special focus on its expressiveness in Multi-Agent Systems and Game Theory, as well as for solving Rational Synthesis problems.

ABSTRACT. Mechanism Design aims to design a game so that a desirable outcome is reached regardless of agents’ self-interests. In this paper, we show how this problem can be rephrased as a synthesis problem, where mechanisms are automatically synthesized from a partial or complete specification in a high-level logical language. We show that Quantitative StrategyLogic is a perfect candidate for specifying mechanisms as it can express complex strategic and quantitative properties. We solve automated mechanism design in two cases: when the number of actions is bounded, and when agents play in turn.

ABSTRACT. Logical, or formal, specifications have proved extremely useful for automated synthesis of plans, strategies, and other objects such as norms of behaviour in software systems. In addition to purely software systems, synthesis of plans conforming to logical specification has been shown to work for cyber-physical systems, in particular, for manufacturing systems. Among many synthesis problems Moshe Vardi worked on is synthesis for manufacturing. The problem in manufacturing synthesis is as follows: given a production recipe, that is, a description of which operations need to be performed in order to have different versions of a product to be manufactured, and a description of a manufacturing facility, synthesise a controller specific to this manufacturing facility, where each operation is assigned to a specific set of manufacturing robots [3]. In [2, 1], synthesis for manufacturing has been investigated, where both the production recipes and manufacturing facilities are modelled as transducers (Mealy machines). It was shown that this version of the synthesis for manufacturing problem is decidable in 2EXPTime when the set of manufacturing resources is fixed, and is undecidable if the problem requires to find how many copies of each manufacturing resource are needed to manufacture the product. In this talk, I would like to outline possible extensions of the problem while keeping it decidable, for example using first order specifications of the production recipes as in [4] and specifying additional constraints on how the production facilities should be used.

ABSTRACT. We give a logical epistemic characterization of iterated admissibility (i.e., iterated deletion of weakly dominated strategies), based on the intuition that a strategy is admissible if it is one used by an agent who is rational, knows that other agents satisfy the appropriate rationality requirements, and that is "all the agent knows'', in that she considers possible all strategies compatible with these assumptions.

ABSTRACT. In automata-theoretic verification, fair simulation is a sufficient condition for trace inclusion. The two notions coincide if the specification automaton is history-deterministic (also called "good-for-games"). History-determinism is nondeterminism that can be resolved by remembering the past, without need for guessing the future. History-determinism is a natural automaton- and game-theoretic concept that can replace determinism for many verification and synthesis questions.

ABSTRACT. This is a talk proposal for the VardiFest where I want to recount my one and half years of learning directly from Moshe and having worked with him on a paper. This talk will be more of ruminations on that wonderful experience (1995-1996) and a homage to the wonderous computer scientist that I get inspired by even today.

ABSTRACT. I was introduced to the elegance of automata-theoretic constructions through Prof. Vardi's seminal work on automata over infinite words and infinite trees and their role in decision procedures for temporal logics. In this talk, I will describe ongoing work on developing a theory of regular languages over series-parallel graphs motivated by distributed data stream applications. These graphs, besides sequential composition, allow both ordered ranked parallelism and unordered unranked parallelism. The latter feature means that in the corresponding automata, the transition function needs to account for an arbitrary number of predecessors by counting each type of state only up to a specified constant, thus leading to a notion of counting complexity that is distinct from the classical notion of state complexity. The resulting theory turns out to be robust: we show that both deterministic and non-deterministic automata have the same expressive power, which can be equivalently characterized by Monadic Second-Order logic as well as the graded mu-calculus, and questions such as membership, emptiness, and equivalence are all decidable.

ABSTRACT. Quantitative reasoning is synonymous with numerical methods. The techniques that come to mind to solve problems involving quantitative properties are numerical methods --- linear programming, optimization, and similar other methods. In this talk, I will introduce a novel framework, called comparators, for quantitative reasoning which is purely based in automata methods as opposed to numerical methods, and discuss their pros and cons.

ABSTRACT. In synthesis, environment specifications are constraints on the environments that rule out certain environment behaviors. To solve synthesis of LTLf goals under environment assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. Recently, it has been shown that when the environment specifications are in form of fairness or stability, or GR(1) formulas, we can avoid such a detour to LTL and keep the simplicity of LTLf synthesis. Furthermore, even when the environment specifications are specified in full LTL we can partially avoid this detour.

In this talk, I give a review on how to effetely tackle the synthesis problem for reachability and safety environment task under reachability and safety environment specifications by using synthesis techniques based on finite-state automata, thus exploiting the intrinsic simplicity of LTLf.

ABSTRACT. Boolean synthesis is the process of synthesizing a multiple-output Boolean function from a declarative specification describing a relation between its inputs and outputs. Motivated by applications in diverse areas such as digital-circuit design, QBF certification and reactive synthesis, a number of different approaches have been developed to tackle this problem. This talk intends to give a brief overview of the ongoing development of Boolean-synthesis algorithms based on decision diagrams. This approach to Boolean synthesis is intrinsically connected to its application as a component of reactive synthesis, since decision diagrams are common in a number of successful reactive-synthesis algorithms. We will contrast the original algorithm based on Binary Decision Diagrams (BDDs) with a newly-introduced version making use of a symbolic CNF representation using Zero-Suppressed Decision Diagrams (ZDDs), and show how this alternative representation can mitigate some of the scalability limitations of BDDs. In the course of the talk we will touch on some of the algorithmic insights that went into the design of such techniques.

ABSTRACT. Given a Markov decision process (MDP) $M$ and a formula $\Phi$, the strategy synthesis problem asks if there exists a strategy $\sigma$ s.t. the resulting Markov chain $M[\sigma]$ satisfies $\Phi$. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.

ABSTRACT. Moshe's has made key contributions in the areas of logic and formal methods, and more recently, he has been one of the main voices discussing publicly the social impact of modern computer technology and AI. I propose to talk about two themes that are related to these. The first is about recent work that highlights the role of formal languages and logic in representation learning. The second is about my experience teaching an optional, upper division course that I developed, called ``Social and technological change'' related to Moshe's concerns.

ABSTRACT. The proposed theory of survival of the fitted [1] explains the evolution of species in the biosphere based on sustainability of multi-scale interaction networks: interaction patterns are what sustains the network and its constituents. Winning in struggles, and having reproductive advantages as associated with Darwinian and Neo-Darwinian survival of the fittest and Natural Selection is secondary. We define a species as the collective of organisms that share a set of fundamental, core, sustaining interactions, which we term the species interaction code. Here (see also [2]), we show that interaction codes are formed, and subsequently evolve, in response to genetic, environmental and other changes, in a process that in some ways relates to the well-studied concepts of autoencoding or dimensionality reduction in machine learning. In a unique autoencoding process, which we term natural autoencoding, every biological process or interaction in the entire biosphere takes part in multiple functions: encoding existing organisms and interactions; decoding such codes into networks of sustained ecosystems, and reacting to innovation and change by adjusting species interaction codes. DNA is only one element in this mechanism. One result of this process is that species interaction codes both map and construct the species environment.

Natural autoencoding differs from typical artificial autoencoding; natural autoencoding is: 1. Sustainment-guided: Typical artificial autoencoders iteratively optimize a loss function: each input is encoded, its representation is then decoded, and the differences between inputs and corresponding reconstructed outputs are computed. In natural autoencoding, evolving species interaction codes stabilize around de-facto sustained interaction patterns. This is retrospective; there is no sustainability assessment of a present state. What works works. 2. Multi-species and multi-scale: Natural autoencoding concurrently generates many species interaction codes, at multiple scales/levels, including biochemical, cellular, and organism. 3. Recursive and Reflective: The biosphere drives its own evolution: the input to the "natural autoencoder" is the entire biosphere, incorporating all available outputs of previous steps, and the autoencoder itself.

Our team is now designing computer-based autoencoders to model natural autoencoding.

Principles associated with Natural Selection and survival of the fittest have significantly affected human political, social, economical, and educational norms. Survival-of-the-fitted by natural autoencoding explains why a habitable environment requires diverse networked interactions. This perspective can help drive much needed changes in human behavior, both environmental and social, including the kind of social responsibility advocated by Moshe Vardi [3].

Acknowledgement: We thank D. Harel, S. Szekely and G. Frankel for valuable contributions.

ABSTRACT. in the 1990s, during my PhD studies at Imperial College, London. One of his particular papers, on why modal logic is robustly decidable clearly called my attention, as he neatly explained not only the paper's main topic but also handed the reader the understanding of model checking and validity \cite{Vardi96}. This paper inspired our work on Connectionist Modal Logics years later \cite{DAVILAGARCEZ200734} and our approach to Neurosymbolic AI in general \cite{3rdwave}. Several years later, we invited him to be a keynote at the Brazilian National Conference on Computer Science. Since then, we have become friends and met several times. Our recent collaboration aims at better understanding and explaining machine learning \cite{Tavares2020}, showing that neural learning and logic can lead to richer neurosymbolic AI models, and at integrating machine learning and reasoning toward more robust AI \cite{Lamb2020,PratesALLV19}. In this talk, I will highlight Vardi's contribution to this endeavour and the inspiration that I have drawn from his exquisite yet humongous contribution to computer science, logic, and artificial intelligence.

ABSTRACT. We intend to present our line of work based on epistemic logic, lasting since some years, where we cope with group dynamics in multi-agent settings. We have proposed and extended over time the epistemic logic \textit{L-DINF}, that allows one to formalize such dynamics, with special attention to explainability, modularity, and to the ability of modelling cognitive aspects related to agents' operation within the application at hand.

ABSTRACT. Logic and graph theory form the basis of a fascinating interplay between combinatorial structures and their algorithmic properties. Some of the most important examples of this are relations between logic, hypergraphs and constraint satisfaction problems, graph width parameters, and connections with monadic second-order logic.

The interaction between logic and graphs have had an important impact on applications in computer science, from database query optimization to temporal reasoning and verification, as well as identifying tractable cases of their relevant constraint satisfaction problems.

In this brief talk, we will explore a number of themes in which logic and algorithmic graph theory have influenced each other.

ABSTRACT. I will discuss the highlights of two papers written with the late Ashok Chandra between 1979 and 1982. The subject is computability and complexity on finite unordered structures (e.g., graphs). Despite the original papers being couched in the framework of relational databases, the ideas and results constitute a rather elegant generalization of Turing computability and classical complexity theory. They have also triggered a large amount of research in finite model theory and descriptive complexity, including seminal work of Moshe Vardi.

Among other things, I will describe a tantalizing problem we posed in the second paper, which is still unsolved after over 40 years, concerning a fundamental issue around PTIME.

ABSTRACT. Nondeterminism allows us to guess the future. The talk surveys the interesting phenomenon of how remembering the past can help us make successful guesses (especially if we are automata, but not only).