A labelled transition system is a directed graph whose edges are labelled with letters from a finite alphabet. The vertices of the digraph are the states of the system, and, for an input letter, the system nondeterministically choses an outgoing edge labelled by this letter and moves to the next state according to it. If there are no such outgoing edges, the system “dies”, that is, moves to an unsafe state. We consider the setting where we know the structure of a labelled transition system and the sequence of input letters, but we don’t know the current state of the system and the nondeterministic choices it makes. We study sequences of letters that guarantee entering the unsafe state regardless of the current state of the system and the choices it makes. Such sequences are called mortal. I will discuss the following questions: what is the computational complexity of deciding if a mortal sequence exists? for a given number of states, what is the maximum length of a shortest mortal sequence? The latter question can be interpreted as follows: what is the lower bound on the time that we need to spend observing a system before we know that it has entered the unsafe state? I will describe two equivalent ways of talking about such systems: via nondeterministic finite automata and via sets of nonnegative matrices. I will also explain our recent results with Stefan Kiefer (University of Oxford) about a subclass of labelled transition systems where many similar properties can be efficiently decided.

Privacy concerns in smart contracts have led to systems that protect on-chain data but still rely on trusted off-chain parties. We propose a novel framework for doubly private execution that addresses both on-chain and off-chain privacy, allowing clients to submit requests confidentially to potentially untrusting servers that collaboratively process these requests without learning client identities or data. Our implementation, Jigsaw, extends the ZEXE architecture and Collaborative zkSNARKs to enable efficient proof generation by server groups. Jigsaw introduces a novel collaborative zkSNARK construction with low latency and reduced proving time, demonstrating 40-50x faster proof generation and orders-of-magnitude less bandwidth than naive approaches when tested on applications like decentralized exchanges, auctions, and voting.

Water theft claims between 30% and 50% of the global water supply, and despite policy efforts to tackle it, is still on the rise. The policy failure to tackle water theft has been attributed to the nonlinear adaptive responses by economic agents such as irrigators, which can affect and be affected by other socioeconomic (e.g., growing commodity prices) and ecological processes (e.g., water scarcity) via feedback loops with cascading impacts that are difficult to foresee. This has led to adaptation surprises with unexpected policy consequences, which have increased rather than reduced water theft, thus depleting water bodies and hampering sustainable development. WaterTheft is developing a novel approach to forecast adaptation surprises in complex human-water systems. To this end, it will 1) combine microeconomic mathematical programming models with behavioral economic methods to forecast the nonlinear adaptive responses of individual agents over time; 2) integrate the behavior of individual agents into agent-based models and macroeconomic models to forecast nonlinear spatial trends emerging from human interactions at the local to global level; 3) endogenize these socioeconomic processes into human-water system models to forecast nonlinear socio-hydrological phenomena; and 4) use ensemble experiments to quantify scenario and modeling uncertainties, and forecast nonlinearities that may emerge or be amplified due to issues of model parameterization/structure or scenario design. These innovations will allow to predict the emergence of nonlinearities and track their impact across coupled human-water systems, thus discovering adaptation surprises and their drivers. Methods will be empirically applied and tested in 3 living labs in Spain, Australia, and the US experiencing water theft.

Economic modeling This research develops and applies ensemble microeconomic models to simulate farmers’ behavior under uncertainty, with a focus on agricultural water use in the face of climate variability and policy change. By integrating high-resolution hydroclimatic inputs (e.g., future predictions of yields and water availability) into economic decision-making frameworks, we capture the dynamic feedback between natural systems and farm-level choices. Our modeling strategy embraces heterogeneity in farmer preferences, risk perceptions, and resource constraints. This microeconomic model ensemble is further coupled with a macroeconomic framework to evaluate, in a bidirectional manner, how shifts in local agricultural production influence global markets—and conversely, how global economic dynamics feedback into local farming decisions. A current limitation of the approach lies in its computational intensity, as it requires integrating hundreds of thousands of future scenarios into the microeconomic models, which must then converge with the hydrologic and macroeconomic models in a consistent and iterative solution process.

Hydrologic modeling This research focuses on advancing complex hydrological modeling by optimizing input structures to improve computational efficiency. The goal is to reduce model complexity by coupling data input models, enabling efficient routing while preserving the statistical integrity of primary data during model development. The Soil and Water Assessment Tool (SWAT) is a widely used hydrological model for simulating the impact of land management practices on water, sediment, and agricultural chemical yields. A key element in SWAT is the hydrological response unit (HRU), which represents a spatial area within a watershed that combines land use, soil type, and slope. The current approach involves refining these HRUs to enhance the performance of the semidistributed SWAT model by integrating both semidistributed and conceptual frameworks. This modification aims to reduce the computational time traditionally associated with SWAT, which is known for its high computational demands. Several alternatives have been tested in the Duero River basin to assess their potential for improving model efficiency. The effectiveness of these improvements will be tested in multiple regions, including a subbasin in California, the Duero River basin in Spain, and a subbasin of the Murray-Darling Basin in Australia, with the goal of advancing hydrological modeling efficiency across diverse geographic contexts.

The talk will be on microarchitecture research and why it plays an important role in our day-to-day computing world, keeping application developers, compiler writers, and OS designers in mind. A major part of the talk will be about microarchitects(my mentees) and their untold stories on some of the microarchitecture techniques that improve system performance (ISCA 2020, MICRO 2022), energy (MICRO 2022), scalability (MICRO 2023), and security (ISCA 2024, MICRO 2024).

The talk covers recent research, conducted by the speaker and his PhD students, aimed at addressing the challenges of high-throughput, low-latency stream processing across the cloud–edge continuum. As centralized data collection becomes increasingly impractical due to the sheer volume of data, transitioning to approaches that push computation closer to the edge emerges as both a promising and necessary alternative. However, the limited and often shared resources available on edge devices pose significant challenges to this shift. After a brief introduction to core stream processing concepts, the talk will cover:(i) how the fragmented landscape of frameworks and processing paradigms can be unified and bridged through a minimal set of stream processing abstractions, better supporting heterogeneous deployments across the cloud–edge spectrum; (ii) the role of stream provenance in enabling more efficient data analysis and selection at the edge; and (iii) the benefits of solutions that trade resource utilization for performance in stream processing, with a particular focus on memory compression in streaming aggregates.