Author name cluster

R. Alur

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

TCS Journal 1995 Journal Article

The algorithmic analysis of hybrid systems

R. Alur
C. Courcoubetis
N. Halbwachs
T.A. Henzinger
P.-H. Ho
X. Nicollin
A. Olivero
J. Sifakis

We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge.

Details DOI

I&C Journal 1995 Journal Article

Timing Verification by Successive Approximation

R. Alur
A. Itai
R.P. Kurshan
M. Yannakakis

We present an algorithm for verifying that a model M with timing constraints satisfies a given temporal property T. The model M is given as a parallel composition of ω-automata Pi, where each automaton Pi is constrained by bounds on delays. The property T is given as an ω-automaton as well, and the verification problem is posed as a language inclusion question L (M) ⊆ L (T). In constructing the composition M of the constrained automata Pi, one needs to rule out the behaviors that are inconsistent with the delay bounds, and this step is (provably) computationally expensive. We propose an iterative solution which involves generating successive approximations Mj to M, with containment L (M) ⊆ L (Mj ) and monotone convergence L (Mj ) → L (M) within a bounded number of steps. As the succession progresses, the approximations Mj become more complex. At any step of the iteration one may get a proof or a counter-example to the original language inclusion question. The described algorithm is implemented into the verifier Cospan. We illustrate the benefits of our strategy through some examples.

Details DOI

I&C Journal 1993 Journal Article

Model-Checking in Dense Real-Time

R. Alur
C. Courcoubetis
D. Dill

Model-checking is a method of verifying concurrent systems in which a state-transition graph model of the system behavior is compared with a temporal logic formula. This paper extends model-checking for the branching-time logic CTL to the analysis of real-time systems, whose correctness depends on the magnitudes of the timing delays. For specifications, we extend the syntax of CTL to allow quantitative temporal operators such as ∃♢ <5, meaning "possibly within 5 time units. " The formulas of the resulting logic, Timed CTL (TCTL), are interpreted over continuous computation trees, trees in which paths are maps from the set of nonnegative reals to system states. To model finite-state systems we introduce timed graphs-state-transition graphs annotated with timing constraints. As our main result, we develop an algorithm for model-checking, for determining the truth of a TCTL-formula with respect to a timed graph. We argue that choosing a dense domain instead of a discrete domain to model time does not significantly blow up the complexity of the model-checking problem. On the negative side, we show that the denseness of the underlying time domain makes the validity problem for TCTL Π 1 1-hard. The question of deciding whether there exists a timed graph satisfying a TCTL-formula is also undecidable.

Details DOI

I&C Journal 1993 Journal Article

Real-Time Logics: Complexity and Expressiveness

R. Alur
T.A. Henzinger

The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal logic. To study temporal logics that are suitable for reasoning about real-time systems, we combine this classical theory of infinite state sequences with a theory of discrete time, via a monotonic function that maps every state to its time. The resulting theory of timed state sequences is shown to be decidable, albeit nonelementary, and its expressive power is characterized by ω-regular sets. Several more expressive variants are proved to be highly undecidable. This framework allows us to classify a wide variety of real-time logics according to their complexity and expressiveness. Indeed, it follows that most formalisms proposed in the literature cannot be decided. We are, however, able to identify two elementary real-time temporal logics as expressively complete fragments of the theory of timed state sequences, and we present tableau-based decision procedures for checking validity. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems.

Details DOI