In November 2024 Communications Vardi's Insights column, "What Is Theoretical Computer Science?", Moshe Vardi raised an interesting point of whether theoretical CS is CS or math. The question is: What is math? Most people outside math consider math as a science of studying abstract structures--just like biology is studying living creatures. However, most mathematicians we know define mathematics not by its subject, but by its level of rigor--mathematics (in contrast, for example, to physics) is making conclusions at the highest level of rigor, that is, proving theorems. Some of these theorems are abstract, some are related to applications. When a researcher proves a theorem about Schroedinger equations, and the result is of interest to physics, of course this is physics, but this is also mathematics--since it is a theorem.

We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf backup specification is satisfied in case of unreliability of certain input variables. We formally define the problem and characterize its worst-case complexity as 2EXPTIME-complete, like standard LTLf synthesis. Then we devise three different solution techniques: one based on direct automata manipulation, which is 2EXPTIME, one disregarding unreliable input variables by adopting a belief construction, which is 3EXPTIME, and one leveraging second-order quantified LTLf (QLTLf), which is 2EXPTIME and allows for a direct encoding into monadic second-order logic, which in turn is worst-case nonelementary. We prove their correctness and evaluate them against each other empirically. Interestingly, theoretical worst-case bounds do not translate into observed performance; the MSO technique performs best, followed by belief construction and direct automata manipulation. As a byproduct of our study, we provide a general synthesis procedure for arbitrary QLTLf specifications.

Consider an agent acting to achieve its temporal goal, but with a "trembling hand". In this case, the agent may mistakenly instruct, with a certain (typically small) probability, actions that are not intended due to faults or imprecision in its action selection mechanism, thereby leading to possible goal failure. We study the trembling-hand problem in the context of reasoning about actions and planning for temporally extended goals expressed in Linear Temporal Logic on finite traces (LTLf), where we want to synthesize a strategy (aka plan) that maximizes the probability of satisfying the LTLf goal in spite of the trembling hand. We consider both deterministic and nondeterministic (adversarial) domains. We propose solution techniques for both cases by relying respectively on Markov Decision Processes and on Markov Decision Processes with Set-valued Transitions with LTLf objectives, where the set-valued probabilistic transitions capture both the nondeterminism from the environment and the possible action instruction errors from the agent. We formally show the correctness of our solution techniques and demonstrate their effectiveness experimentally through a proof-of-concept implementation.

Devising a strategy to make a system mimic behaviors from another system is a problem that naturally arises in many areas of Computer Science. In this work, we interpret this problem in the context of intelligent agents, from the perspective of ltlf , a formalism commonly used in AI for expressing finite-trace properties. Our model consists of two separated dynamic domains, DA and DB, and an LTLf specification that formalizes the notion of mimicking by mapping properties on behaviors (traces) of DA into properties on behaviors of DB. The goal is to synthesize a strategy that step-by-step maps every behavior of DA into a behavior of DB so that the specification is met. We consider several forms of mapping specifications, ranging from simple ones to full LTLf , and for each, we study synthesis algorithms and computational properties.

In his January 2023 Communications Viewpoint, "The End of Programming," Matt Welsh wrote "nobody actually understands how large AI models work." However, already no one person understands existing large computer systems. Indeed, no team of people understands them. Staff turnover and other practicalities of real life mean not even the team that wrote them originally (should it still exist) nor the team currently responsible for maintaining them, fully understands large software systems, which can now exceed a billion lines of code. And yet such systems are in worldwide daily use and deliver economic benefits.

Moshe Vardi's horizons are big when it comes to computer science. Celebrated for his contributions to formal methods and computational complexity, he is also well known for his role with ACM, and, in particular, with this publication. Vardi took over as Editor-in-Chief of Communications of the ACM in 2008. Though he stepped down to become a Senior Editor in 2017, he continues to publish regularly on topics from corporate ethics to post-graduate education. Here, he talks about socioeconomics, social media, and the impact of computing on society.

Artificial intelligence (AI) and machine learning have made modern life infinitely easier, quicker and more connected. But the limits of "smart machines" also are on display every day--self-driving cars that crash and catch fire, facial recognition and law enforcement software that are biased against minorities and those with darker skin, and algorithms that eliminate swaths of the population from home loan and credit card qualification. It's clear artificial intelligence needs reasonable boundaries, mathematician and computer scientist Moshe Vardi told those gathered for a virtual symposium, "AI & Society," Sept. 21 and 22. The problem will be reaching agreement on the methods of regulation and implementing them over time, said Vardi, who heads Rice University's Initiative on Technology, Culture and Society. The answer is, right now, that society has given up.

Artificial Intelligence (AI) has opened myriad possibilities to make life better--faster, more efficient, cheaper. At the same time, using data and machines to speed things up has also increased the chances of lost human connections, missed steps in deliberation, and over-simplification of life's messiness. The Utah Informatics Initiative (UI2) and Tanner Humanities Center are hosting a virtual symposium Sept. 21 and 22 to explore the facets of AI's role in society. The University of Utah is uniquely situated as the host for these discussions, said Mike Kirby, UI2 director. The U has a notable cohort of researchers studying informatics, data science and machine learning, while working alongside interdisciplinary partners in the humanities and arts.

Linear temporal logic (LTL) is a modal logic where formulas are built over temporal operators relating events happening in different time instants. According to the standard semantics, LTL formulas are interpreted on traces spanning over an infinite timeline. However, applications related to the specification and verification of business processes have recently pointed out the need for defining and reasoning about a variant of LTL, which we name LTLp, whose semantics is defined over process traces, that is, over finite traces such that, at each time instant, precisely one propositional variable (standing for the execution of some given activity) evaluates true. The paper investigates the theoretical underpinnings of LTLp and of a related logic formalism, named LTLf, which had already attracted attention in the literature and where formulas have the same syntax as in LTLp and are evaluated over finite traces, but without any constraint on the number of variables simultaneously evaluating true. The two formalisms are comparatively analyzed, by pointing out similarities and differences. In addition, a thorough complexity analysis has been conducted for reasoning problems about LTLp and LTLf, by considering arbitrary formulas as well as classes of formulas defined in terms of restrictions on the temporal operators that are allowed. Finally, based on the theoretical findings of the paper, a practical reasoner specifically tailored for LTLp and LTLf has been developed by leveraging state-of-the-art SAT solvers. The behavior of the reasoner has been experimentally compared with other systems available in the literature.

His concern is warranted and will require us to strike a balance between protecting the democratic and egalitarian values that made the Internet great to begin with while ensuring those values are used for good. The fundamental issue, then, in creating a 21st-century Internet becomes what changes are warranted and who will be responsible for defining and administering them. On the technology dimension, computer scientists and engineers must develop smarter systems for detecting, addressing, and preventing malicious content on the Web. Cerf's argument on behalf of user training is helpful but will not ultimately solve the problem of an untrustworthy, ungovernable, potentially malicious network. I myself recently fell for a phishing attack, which only proves that today's attacks can fool even savvy, experienced users.