Rajeev Alur

NeurIPS Conference 2025 Conference Paper

CTSketch: Compositional Tensor Sketching for Scalable Neurosymbolic Learning

• Seewon Choi
• Alaia Solko-Breslin
• Rajeev Alur
• Eric Wong

Many computational tasks benefit from being formulated as the composition of neural networks followed by a discrete symbolic program. The goal of neurosymbolic learning is to train the neural networks using end-to-end input-output labels of the composite. We introduce CTSketch, a novel, scalable neurosymbolic learning algorithm. CTSketch uses two techniques to improve the scalability of neurosymbolic inference: decompose the symbolic program into sub-programs and summarize each sub-program with a sketched tensor. This strategy allows us to approximate the output distribution of the program with simple tensor operations over the input distributions and the sketches. We provide theoretical insight into the maximum approximation error. Furthermore, we evaluate CTSketch on benchmarks from the neurosymbolic learning literature, including some designed for evaluating scalability. Our results show that CTSketch pushes neurosymbolic learning to new scales that were previously unattainable, with neural predictors obtaining high accuracy on tasks with one thousand inputs, despite supervision only on the final output.

TMLR Journal 2025 Journal Article

Illustrated Landmark Graphs for Long-horizon Policy Learning

• Christopher Watson
• Arjun Krishna
• Rajeev Alur
• Dinesh Jayaraman

Applying learning-based approaches to long-horizon sequential decision-making tasks requires a human teacher to carefully craft reward functions or curate demonstrations to elicit desired behaviors. To simplify this, we first introduce an alternative form of task-specification, Illustrated Landmark Graph (ILG), that represents the task as a directed graph where each vertex corresponds to a region of the state space (a landmark), and each edge represents an easier to achieve sub-task. A landmark in the ILG is conveyed to the agent through a few illustrative examples grounded in the agent’s observation space. Second, we propose ILG-Learn, a human in the loop algorithm that interleaves planning over the ILG and sub-task policy learning. ILG-Learn adaptively plans through the ILG by relying on the human teacher’s feedback to estimate the success rates of learned policies. We conduct experiments on long-horizon block stacking and point maze navigation tasks, and find that our approach achieves considerably higher success rates (~ 50% improvement) compared to hierarchical reinforcement learning and imitation learning baselines. Additionally, we highlight how the flexibility of the ILG specification allows the agent to learn a sequence of sub-tasks that is better suited to its limited capabilities.

ICLR Conference 2025 Conference Paper

Logicbreaks: A Framework for Understanding Subversion of Rule-based Inference

• Anton Xue
• Avishree Khare
• Rajeev Alur
• Surbhi Goel
• Eric Wong 0001

We study how to subvert large language models (LLMs) from following prompt-specified rules. We first formalize rule-following as inference in propositional Horn logic, a mathematical system in which rules have the form "if $P$ and $Q$, then $R$" for some propositions $P$, $Q$, and $R$. Next, we prove that although small transformers can faithfully follow such rules, maliciously crafted prompts can still mislead both theoretical constructions and models learned from data. Furthermore, we demonstrate that popular attack algorithms on LLMs find adversarial prompts and induce attention patterns that align with our theory. Our novel logic-based framework provides a foundation for studying LLMs in rule-based settings, enabling a formal analysis of tasks like logical reasoning and jailbreak attacks.

NeurIPS Conference 2024 Conference Paper

Data-Efficient Learning with Neural Programs

• Alaia Solko-Breslin
• Seewon Choi
• Ziyang Li
• Neelay Velingker
• Rajeev Alur
• Mayur Naik
• Eric Wong

Many computational tasks can be naturally expressed as a composition of a DNN followed by a program written in a traditional programming language or an API call to an LLM. We call such composites "neural programs" and focus on the problem of learning the DNN parameters when the training data consist of end-to-end input-output labels for the composite. When the program is written in a differentiable logic programming language, techniques from neurosymbolic learning are applicable, but in general, the learning for neural programs requires estimating the gradients of black-box components. We present an algorithm for learning neural programs, called ISED, that only relies on input-output samples of black-box components. For evaluation, we introduce new benchmarks that involve calls to modern LLMs such as GPT-4 and also consider benchmarks from the neurosymbolic learning literature. Our evaluation shows that for the latter benchmarks, ISED has comparable performance to state-of-the-art neurosymbolic frameworks. For the former, we use adaptations of prior work on gradient approximations of black-box components as a baseline, and show that ISED achieves comparable accuracy but in a more data- and sample-efficient manner.

AAAI Conference 2024 Conference Paper

Relational Programming with Foundational Models

• Ziyang Li
• Jiani Huang
• Jason Liu
• Felix Zhu
• Eric Zhao
• William Dodds
• Neelay Velingker
• Rajeev Alur

Foundation models have vast potential to enable diverse AI applications. The powerful yet incomplete nature of these models has spurred a wide range of mechanisms to augment them with capabilities such as in-context learning, information retrieval, and code interpreting. We propose Vieira, a declarative framework that unifies these mechanisms in a general solution for programming with foundation models. Vieira follows a probabilistic relational paradigm and treats foundation models as stateless functions with relational inputs and outputs. It supports neuro-symbolic applications by enabling the seamless combination of such models with logic programs, as well as complex, multi-modal applications by streamlining the composition of diverse sub-models. We implement Vieira by extending the Scallop compiler with a foreign interface that supports foundation models as plugins. We implement plugins for 12 foundation models including GPT, CLIP, and SAM. We evaluate Vieira on 9 challenging tasks that span language, vision, and structured and vector databases. Our evaluation shows that programs in Vieira are concise, can incorporate modern foundation models, and have comparable or better accuracy than competitive baselines.

ICML Conference 2023 Conference Paper

Robust Subtask Learning for Compositional Generalization

• Kishor Jothimurugan
• Steve Hsu
• Osbert Bastani
• Rajeev Alur

Compositional reinforcement learning is a promising approach for training policies to perform complex long-horizon tasks. Typically, a high-level task is decomposed into a sequence of subtasks and a separate policy is trained to perform each subtask. In this paper, we focus on the problem of training subtask policies in a way that they can be used to perform any task; here, a task is given by a sequence of subtasks. We aim to maximize the worst-case performance over all tasks as opposed to the average-case performance. We formulate the problem as a two agent zero-sum game in which the adversary picks the sequence of subtasks. We propose two RL algorithms to solve this game: one is an adaptation of existing multi-agent RL algorithms to our setting and the other is an asynchronous version which enables parallel training of subtask policies. We evaluate our approach on two multi-task environments with continuous states and actions and demonstrate that our algorithms outperform state-of-the-art baselines.

NeurIPS Conference 2023 Conference Paper

Stability Guarantees for Feature Attributions with Multiplicative Smoothing

• Anton Xue
• Rajeev Alur
• Eric Wong

Explanation methods for machine learning models tend not to provide any formal guarantees and may not reflect the underlying decision-making process. In this work, we analyze stability as a property for reliable feature attribution methods. We prove that relaxed variants of stability are guaranteed if the model is sufficiently Lipschitz with respect to the masking of features. We develop a smoothing method called Multiplicative Smoothing (MuS) to achieve such a model. We show that MuS overcomes the theoretical limitations of standard smoothing techniques and can be integrated with any classifier and feature attribution method. We evaluate MuS on vision and language models with various feature attribution methods, such as LIME and SHAP, and demonstrate that MuS endows feature attributions with non-trivial stability guarantees.

PRL Workshop 2022 Workshop Paper

Compositional Reinforcement Learning from Logical Specifications

• Kishor Jothimurugan
• Suguman Bansal
• Osbert Bastani
• Rajeev Alur

We study the problem of learning control policies for complex tasks given by logical specifications. Recent approaches automatically generate a reward function from a given specification and use a suitable reinforcement learning algorithm to learn a policy that maximizes the expected reward. These approaches, however, scale poorly to complex tasks that require high-level planning. In this work, we develop a compositional learning approach, called D I RL, that interleaves highlevel planning and reinforcement learning. First, D I RL encodes the specification as an abstract graph; intuitively, vertices and edges of the graph correspond to regions of the state space and simpler sub-tasks, respectively. Our approach then incorporates reinforcement learning to learn neural network policies for each edge (sub-task) within a Dijkstra-style planning algorithm to compute a high-level plan in the graph. An evaluation of the proposed approach on a set of challenging control benchmarks with continuous state and action spaces demonstrates that it outperforms state-of-the-art baselines.

NeurIPS Conference 2021 Conference Paper

Compositional Reinforcement Learning from Logical Specifications

• Kishor Jothimurugan
• Suguman Bansal
• Osbert Bastani
• Rajeev Alur

We study the problem of learning control policies for complex tasks given by logical specifications. Recent approaches automatically generate a reward function from a given specification and use a suitable reinforcement learning algorithm to learn a policy that maximizes the expected reward. These approaches, however, scale poorly to complex tasks that require high-level planning. In this work, we develop a compositional learning approach, called DIRL, that interleaves high-level planning and reinforcement learning. First, DIRL encodes the specification as an abstract graph; intuitively, vertices and edges of the graph correspond to regions of the state space and simpler sub-tasks, respectively. Our approach then incorporates reinforcement learning to learn neural network policies for each edge (sub-task) within a Dijkstra-style planning algorithm to compute a high-level plan in the graph. An evaluation of the proposed approach on a set of challenging control benchmarks with continuous state and action spaces demonstrates that it outperforms state-of-the-art baselines.

Highlights Conference 2021 Conference Abstract

Synchronization Schemas for Modeling Data Streams

• Rajeev Alur

We present a type-theoretic framework for data stream processing for real-time decision making, where the desired computation involves a mix of sequential computation, such as smoothing and detection of peaks and surges, and naturally parallel computation, such as relational operations, key-based partitioning, and map-reduce. To unify sequential (ordered) and relational (unordered) data models, we define synchronization schemas as types and series-parallel streams (SPS) as objects of these types. A synchronization schema imposes a hierarchical structure over relational types that succinctly captures ordering and synchronization requirements among different kinds of data items. Series-parallel streams naturally model objects such as relations, sequences, sequences of relations, sets of streams indexed by key values, time-based and event-based windows, and more complex structures obtained by nesting of these. We introduce series-parallel stream transformers (SPST) as a domain-specific language for modular specification of deterministic transformations over such streams. SPSTs provably specify only monotonic transformations allowing streamability, have a modular structure that can be exploited for correct parallel implementation, and are composable allowing specification of complex queries as a pipeline of transformations. We conclude by discussing research directions for both theory of automata, logics, and transducers for distributed stream processing.

TCS Journal 2020 Journal Article

Streamable regular transductions

• Rajeev Alur
• Dana Fisman
• Konstantinos Mamouras
• Mukund Raghothaman
• Caleb Stanford

Motivated by real-time monitoring and data processing applications, we develop a formal theory of quantitative queries for streaming data that can be evaluated efficiently. We consider the model of unambiguous Cost Register Automata (CRAs), which are machines that combine finite-state control (for identifying regular patterns) with a finite set of data registers (for computing numerical aggregates). The definition of CRAs is parameterized by the collection of numerical operations that can be applied to the registers. These machines give rise to the class of streamable regular transductions ( SR ), and to the class of streamable linear regular transductions ( SLR ) when the register updates are copyless, i. e. every register appears at most once in the right-hand-side expressions of the updates. We give a logical characterization of the class SR (resp. , SLR ) using MSO-definable transformations from strings to DAGs (resp. , trees) without backward edges. Additionally, we establish that the two classes SR and SLR are closed under operations that are relevant for designing query languages. Finally, we study the relationship with weighted automata (WA), and show that CRAs over a suitably chosen set of operations correspond to WA, thus establishing that WA are a special case of CRAs.

NeurIPS Conference 2019 Conference Paper

A Composable Specification Language for Reinforcement Learning Tasks

• Kishor Jothimurugan
• Rajeev Alur
• Osbert Bastani

Reinforcement learning is a promising approach for learning control policies for robot tasks. However, specifying complex tasks (e. g. , with multiple objectives and safety constraints) can be challenging, since the user must design a reward function that encodes the entire task. Furthermore, the user often needs to manually shape the reward to ensure convergence of the learning algorithm. We propose a language for specifying complex control tasks, along with an algorithm that compiles specifications in our language into a reward function and automatically performs reward shaping. We implement our approach in a tool called SPECTRL, and show that it outperforms several state-of-the-art baselines.

I&C Journal 2018 Journal Article

Compositional and symbolic synthesis of reactive controllers for multi-agent systems

• Rajeev Alur
• Salar Moarref
• Ufuk Topcu

We consider the controller synthesis problem for multi-agent systems that consist of a set of controlled and uncontrolled agents. Controlled agents may need to cooperate with each other and react to actions of uncontrolled agents in order to fulfill their objectives. Moreover, agents may be imperfect, i. e. , only partially observe their environment. We propose a framework for controller synthesis based on compositional reactive synthesis. We implement the algorithms symbolically and apply them to a robot motion planning case study where multiple robots are placed on a grid-world with static obstacles and other dynamic, uncontrolled and potentially adversarial robots. We consider different objectives such as collision avoidance, keeping a formation and bounded reachability. We show that by taking advantage of the structure of the system, compositional synthesis algorithm can significantly outperform centralized alternative, both from time and memory perspective, and can solve problems where the centralized algorithm is infeasible.

CSL Conference 2016 Conference Paper

Hedging Bets in Markov Decision Processes

• Rajeev Alur
• Marco Faella
• Sampath Kannan
• Nimit Singhania

The classical model of Markov decision processes with costs or rewards, while widely used to formalize optimal decision making, cannot capture scenarios where there are multiple objectives for the agent during the system evolution, but only one of these objectives gets actualized upon termination. We introduce the model of Markov decision processes with alternative objectives (MDPAO) for formalizing optimization in such scenarios. To compute the strategy to optimize the expected cost/reward upon termination, we need to figure out how to balance the values of the alternative objectives. This requires analysis of the underlying infinite-state process that tracks the accumulated values of all the objectives. While the decidability of the problem of computing the exact optimal strategy for the general model remains open, we present the following results. First, for a Markov chain with alternative objectives, the optimal expected cost/reward can be computed in polynomial-time. Second, for a single-state process with two actions and multiple objectives we show how to compute the optimal decision strategy. Third, for a process with only two alternative objectives, we present a reduction to the minimum expected accumulated reward problem for one-counter MDPs, and this leads to decidability for this case under some technical restrictions. Finally, we show that optimal cost/reward can be approximated up to a constant additive factor for the general problem.

IJCAI Conference 2013 Conference Paper

Automated Grading of DFA Constructions

• Rajeev Alur
• Loris D'Antoni
• Sumit Gulwani
• Dileep Kini
• Mahesh Viswanathan

One challenge in making online education more effective is to develop automatic grading software that can provide meaningful feedback. This paper provides a solution to automatic grading of the standard computation-theory problem that asks a student to construct a deterministic finite automaton (DFA) from the given description of its language. We focus on how to assign partial grades for incorrect answers. Each student’s answer is compared to the correct DFA using a hybrid of three techniques devised to capture different classes of errors. First, in an attempt to catch syntactic mistakes, we compute the edit distance between the two DFA descriptions. Second, we consider the entropy of the symmetric difference of the languages of the two DFAs, and compute a score that estimates the fraction of the number of strings on which the student answer is wrong. Our third technique is aimed at capturing mistakes in reading of the problem description. For this purpose, we consider a description language MOSEL, which adds syntactic sugar to the classical Monadic Second Order Logic, and allows defining regular languages in a concise and natural way. We provide algorithms, along with optimizations, for transforming MOSEL descriptions into DFAs and vice-versa. These allow us to compute the syntactic edit distance of the incorrect answer from the correct one in terms of their logical representations. We report an experimental study that evaluates hundreds of answers submitted by (real) students by comparing grades/feedback computed by our tool with human graders. Our conclusion is that the tool is able to assign partial grades in a meaningful way, and should be preferred over the human graders for both scalability and consistency.

Highlights Conference 2013 Conference Abstract

Automated grading of DFA constructions

• Rajeev Alur
• Loris D'Antoni
• Sumit Gulwani
• Dileep Kini
• Mahesh Viswanathan

One challenge in making online education more effective is to develop automatic grading software that can provide meaningful feedback. This paper provides a solution to automatic grading of the standard computation-theory problem that asks a student to construct a deterministic finite automaton from the given description of its language. We focus on how to assign partial grades for incorrect answers. We experimentally show that the tool is able to assign partial grades in a meaningful way, and should be preferred over the human graders for both scalability and consistency. 13: 00 14: 00 Lunch

Highlights Conference 2013 Conference Abstract

Decision problems for additive regular functions

• Rajeev Alur
• Mukund Raghothaman

We introduce cost register automata (CRA) -- this is a deterministic model to associate costs with strings that is parametrized by operations of interest (such as addition, scaling, and minimum), and a notion of regularity that provides a yardstick to measure expressiveness. Our notion of regularity relies on the notion of string-to-tree transducers, and allows associating costs with events that are conditioned on regular properties of future events. CRAs compute regular functions using multiple write-only registers whose values can be combined using the allowed set of operations. We then discuss various analysis problems associated with CRAs and regular functions, including the decidability of equivalance and containment, register and state minimization, and Angluin-style learning of cost functions.

Highlights Conference 2013 Conference Abstract

Streaming tree transducers

• Loris D'Antoni
• Rajeev Alur

We introduce streaming tree transducers as an analyzable, executable, and expressive model for transforming unranked ordered trees. Given a linear encoding of the input tree, the transducer makes a single left-to-right pass through the input, and computes the output using a finite-state control, a visibly pushdown stack, and a finite set of variables storing output chunks that can be combined using concatenation and insertion. We prove the model to be equivalent to monadic second-order logic transductions. We show complexity bounds of ExpTime for type-checking and NExpTime for equivalence.

CSL Conference 2009 Conference Paper

Algorithmic Analysis of Array-Accessing Programs

• Rajeev Alur
• Pavol Cerný
• Scott Weinstein

Abstract For programs whose data variables range over boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this paper, we consider algorithmic verification of programs that use boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over a potentially unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) Pspace -complete for programs in which the array-accessing for -loops are not nested, (2) decidable for a restricted class of programs with doubly-nested loops. The second result establishes connections to automata and logics defining languages over data words.

TCS Journal 2006 Journal Article

Counterexample-guided predicate abstraction of hybrid systems

• Rajeev Alur
• Thao Dang
• Franjo Ivančić

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counterexamples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counterexamples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach.

TCS Journal 2006 Journal Article

Modular strategies for recursive game graphs

• Rajeev Alur
• Salvatore La Torre
• P. Madhusudan

Many problems in formal verification and program analysis can be formalized as computing winning strategies for two-player games on graphs. In this paper, we focus on solving games in recursive game graphs which can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global) pushdown games is known to be EXPTIME-complete, we show reachability in modular games to be NP-complete. We present a fixed-point computation algorithm for solving modular games such that in the worst case the number of iterations is exponential in the total number of returned values from the modules. If the strategy within a module does not depend on the global history, but can remember the history of the past invocations of this module, that is, if memory is local but persistent, we show that reachability becomes undecidable.

TCS Journal 2005 Journal Article

Realizability and verification of MSC graphs

• Rajeev Alur
• Kousha Etessami
• Mihalis Yannakakis

Scenario-based specifications such as message sequence charts (MSC) offer an intuitive and visual way to describe design requirements. MSC-graphs allow convenient expression of multiple scenarios, and can be viewed as an early model of the system that can be subjected to a variety of analyses. Problems such as LTL model checking are undecidable for MSC-graphs in general, but are known to be decidable for the class of bounded MSC-graphs. Our first set of results concerns checking realizability of bounded MSC-graphs. An MSC-graph is realizable if there is a distributed implementation that generates precisely the behaviors in the graph. There are two notions of realizability, weak and safe, depending on whether or not we require the implementation to be deadlock-free. It is known that for a finite set of MSCs, weak realizability is coNP-complete while safe realizability has a polynomial-time solution. We establish that for bounded MSC-graphs, weak realizability is, surprisingly, undecidable, while safe realizability is in EXPSPACE. Our second set of results concerns verification of MSC-graphs. While checking properties of a graph G, besides verifying all the scenarios in the set L ( G ) of MSCs specified by G, it is desirable to verify all the scenarios in the set L w ( G ) —the closure of G, that contains the implied scenarios that any distributed implementation of G must include. For checking whether a given MSC M is a possible behavior, checking M ∈ L ( G ) is NP-complete, but checking M ∈ L w ( G ) has a quadratic solution. For temporal logic specifications, considering the closure makes the verification problem harder: while checking LTL properties of L ( G ) is PSPACE-complete for bounded graphs G, checking even simple “local” properties of L w ( G ) is undecidable.

TCS Journal 2004 Journal Article

Optimal paths in weighted timed automata

• Rajeev Alur
• Salvatore La Torre
• George J. Pappas

We consider the optimal-reachability problem for a timed automaton with respect to a linear cost function which results in a weighted timed automaton. Our solution to this optimization problem consists of reducing it to computing (parametric) shortest paths in a finite weighted directed graph. We call this graph a parametric sub-region graph. It refines the region graph, a standard tool for the analysis of timed automata, by adding the information which is relevant to solving the optimal-reachability problem. We present an algorithm to solve the optimal-reachability problem for weighted timed automata that takes time exponential in O(n(|δ(A)|+|w max |)), where n is the number of clocks, |δ(A)| is the size of the clock constraints and |w max| is the size of the largest weight. We show that this algorithm can be improved, if we restrict to weighted timed automata with a single clock. In case we consider a single starting state for the optimal-reachability problem, our approach yields an algorithm that takes exponential time only in the length of clock constraints.

STOC Conference 2004 Conference Paper

Visibly pushdown languages

• Rajeev Alur
• P. Madhusudan

We propose the class of visibly pushdown languages as embeddings of context-free languages that is rich enough to model program analysis questions and yet is tractable and robust like the class of regular languages. In our definition, the input symbol determines when the pushdown automaton can push or pop, and thus the stack depth at every position. We show that the resulting class Vpl of languages is closed under union, intersection, complementation, renaming, concatenation, and Kleene-*, and problems such as inclusion that are undecidable for context-free languages are Exptime-complete for visibly pushdown automata. Our framework explains, unifies, and generalizes many of the decision procedures in the program analysis literature, and allows algorithmic verification of recursive programs with respect to many context-free properties including access control properties via stack inspection and correctness of procedures with respect to pre and post conditions. We demonstrate that the class Vpl is robust by giving two alternative characterizations: a logical characterization using the monadic second order (MSO) theory over words augmented with a binary matching predicate, and a correspondence to regular tree languages. We also consider visibly pushdown languages of infinite words and show that the closure properties, MSO-characterization and the characterization in terms of regular trees carry over. The main difference with respect to the case of finite words turns out to be determinizability: nondeterministic Büchi visibly pushdown automata are strictly more expressive than deterministic Muller visibly pushdown automata.

I&C Journal 2000 Journal Article

Model-Checking of Correctness Conditions for Concurrent Objects

• Rajeev Alur
• Ken McMillan
• Doron Peled

The notions of serializability, linearizability, and sequential consistency are used in the specification of concurrent systems. We show that the model checking problem for each of these properties can be cast in terms of the containment of one regular language in another regular language shuffled using a semicommutative alphabet. The three model checking problems are shown to be, respectively, in P space, in E xpspace, and undecidable.

TCS Journal 1999 Journal Article

Event-clock automata: a determinizable class of timed automata

• Rajeev Alur
• Limor Fix
• Thomas A. Henzinger

We introduce event-recording automata. An event-recording automaton is a timed automaton that contains, for every event a, a clock that records the time of the last occurrence of a. The class of event-recording automata is, on one hand, expressive enough to model (finite) timed transition systems and, on the other hand, determinizable and closed under all boolean operations. As a result, the language-inclusion problem is decidable for event-recording automata. We present a translation from timed transition systems to event-recording automata, which leads to an algorithm for checking if two timed transition systems have the same set of timed behaviors. We also consider event-predicting automata, which contain clocks that predict the time of the next occurrence of an event. The class of event-clock automata, which contain both event-recording and event-predicting clocks, is a suitable specification language for real-time properties. We provide an algorithm for checking if a timed automaton meets a specification that is given as an event-clock automaton.

FOCS Conference 1997 Conference Paper

Alternating-time Temporal Logic

• Rajeev Alur
• Thomas A. Henzinger
• Orna Kupferman

Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas.

I&C Journal 1996 Journal Article

Contention-Free Complexity of Shared Memory Algorithms

• Rajeev Alur
• Gadi Taubenfeld

Worst-case time complexity is a measure of the maximum time needed to solve a problem over all runs. Contention-free time complexity indicates the maximum time needed when a process executes by itself, without competition from other processes. Since contention is rare in well-designed systems, it is important to design algorithms which perform well in the absence of contention. We study the contention-free time complexity of shared memory algorithms using two measures: step complexity, which counts the number of accesses to shared registers; and register complexity, which measures the number of different registers accessed. Depending on the system architecture, one of the two measures more accurately reflects the elapsed time. We provide lower and upper bounds for the contention-free step and register complexity of solving the mutual exclusion problem as a function of the number of processes and the size of the largest register that can be accessed in one atomic step. We also present bounds on the worst-case and contention-free step and register complexities of solving the naming problem. These bounds illustrate that the proposed complexity measures are useful in differentiating among the computational powers of different primitives

STOC Conference 1995 Conference Paper

Distinguishing tests for nondeterministic and probabilistic machines

• Rajeev Alur
• Costas Courcoubetis
• Mihalis Yannakakis

TCS Journal 1994 Journal Article

A theory of timed automata

• Rajeev Alur
• David L. Dill

We propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words–infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Büchi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable (Π1 1-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.

STOC Conference 1994 Conference Paper

Time-adaptive algorithms for synchronization

• Rajeev Alur
• Hagit Attiya
• Gadi Taubenfeld

STOC Conference 1993 Conference Paper

Parametric real-time reasoning

• Rajeev Alur
• Thomas A. Henzinger
• Moshe Y. Vardi

FOCS Conference 1992 Conference Paper

Back to the Future: Towards a Theory of Timed Regular Languages

• Rajeev Alur
• Thomas A. Henzinger

The authors introduce two-way timed automata-timed automata that can move back and forth while reading a timed word. Two-wayness in its unrestricted form leads, like nondeterminism, to the undecidability of language inclusion. However, if they restrict the number of times an input symbol may be revisited, then two-wayness is both harmless and desirable. The authors show that the resulting class of bounded two-way deterministic timed automata is closed under all boolean operations, has decidable (PSPACE-complete) emptiness and inclusion problems, and subsumes all decidable real-time logics we know. They obtain a strict hierarchy of real-time properties: deterministic timed automata can accept more languages as the bound on the number of times an input symbol may be revisited is increased. This hierarchy is also enforced by the number of alternations between past and future operators in temporal logic. The combination of the results leads to a decision procedure for a real-time logic with past operators. >

FOCS Conference 1989 Conference Paper

A Really Temporal Logic

• Rajeev Alur
• Thomas A. Henzinger

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable. >