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.

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.

Ryan Calo's "law and Technology" Viewpoint "Is the Law Ready for Driverless Cars?" (May 2018) explored the implications, as Calo said, of " ... genuinely unforeseeable categories of harm" in potential liability cases where death or injury is caused by a driverless car. He argued that common law would take care of most other legal issues involving artificial intelligence in driverless cars, apart from such "foreseeability." Calo also said the courts have worked out problems like AI before and seemed confident that AI foreseeability will eventually be accommodated. One can agree with this overall judgment but question the time horizon. AI may be quite different from anything the courts have seen or judged before for many reasons, as the technology is indeed designed to someday make its own decisions.