TY - JOUR AB - We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology AU - Henzinger, Thomas A AU - Ho, Pei AU - Wong Toi, Howard ID - 4491 IS - 4 JF - IEEE Transactions on Automatic Control SN - 0018-9162 TI - Algorithmic analysis of nonlinear hybrid systems VL - 43 ER - TY - JOUR AB - We have developed general modeling software for a Cave Automatic Virtual Environment (CAVE); one of its applications is modeling 3D protein structures, generating both outside-in and inside-out views of geometric models. An advantage of the CAVE over other virtual environments is that multiple viewers can observe the same scene at the same time and place. Our software is scalable-from high-end virtual environments such as the CAVE, to mid-range immersive desktop systems, down to low-end graphics workstations. In the current configuration, a parallel Silicon Graphics Power Challenge supercomputer architecture performs the computationally intensive construction of surface patches remotely, and sends the results through the I-WAY (Information Wide Area Year) using VBNS (Very-high-Bandwidth Network Systems) to the graphics machines that drive the CAVE and our graphics visualization software, Valvis (Virtual ALpha shapes VISualizer). AU - Akkiraju, Nataraj AU - Edelsbrunner, Herbert AU - Fu, Ping AU - Qian, Jiang ID - 4024 IS - 4 JF - IEEE Computer Graphics and Applications SN - 0018-9162 TI - Viewing geometric protein structures from inside a CAVE VL - 16 ER - TY - CONF AB - We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise refinement) reasoning. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchronous message passing AU - Alur, Rajeev AU - Henzinger, Thomas A ID - 4588 SN - 0018-9162 T2 - Proceedings 11th Annual IEEE Symposium on Logic in Computer Science TI - Reactive modules ER - TY - JOUR AB - Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms AU - Alur, Rajeev AU - Henzinger, Thomas A AU - Ho, Pei ID - 4611 IS - 3 JF - IEEE Transactions on Software Engineering SN - 0018-9162 TI - Automatic symbolic verification of embedded systems VL - 22 ER - TY - CONF AB - Fairness is a mathematical abstraction: in a multiprogramming environment, fairness abstracts the details of admissible (“fair”) schedulers; in a distributed environment, fairness abstracts the speeds of independent processors. We argue that the standard definition of fairness often is unnecessarily weak and can be replaced by the stronger, yet still abstract, notion of finitary fairness. While standard weak fairness requires that no enabled transition is postponed forever, finitary weak fairness requires that for every run of a system there is an unknown bound k such that no enabled transition is postponed more than k consecutive times. In general, the finitary restriction fin(F) of any given fairness assumption F is the union of all w-regular safety properties that are contained in F. The adequacy of the proposed abstraction is demonstrated in two ways. Suppose that we prove a program property under the assumption of finitary fairness. In a multiprogramming environment, the program then satisfies the property for all fair finite-state schedulers. In a distributed environment, the program then satisfies the property for all choices of lower and upper bounds on the speeds (or timings) of processors AU - Alur, Rajeev AU - Henzinger, Thomas A ID - 4586 SN - 0018-9162 T2 - Proceedings 9th Annual IEEE Symposium on Logic in Computer Science TI - Finitary fairness ER - TY - CONF AB - 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. AU - Alur, Rajeev AU - Henzinger, Thomas A ID - 4596 SN - 0018-9162 T2 - 30th Annual Symposium on Foundations of Computer Science TI - A really temporal logic ER - TY - JOUR AB - A generalization of the convex hull of a finite set of points in the plane is introduced and analyzed. This generalization leads to a family of straight-line graphs, " \alpha -shapes," which seem to capture the intuitive notions of "fine shape" and "crude shape" of point sets. It is shown that a-shapes are subgraphs of the closest point or furthest point Delaunay triangulation. Relying on this result an optimal O(n \log n) algorithm that constructs \alpha -shapes is developed. AU - Edelsbrunner, Herbert AU - Kirkpatrick, David AU - Seidel, Raimund ID - 4128 IS - 4 JF - IEEE Transactions on Information Theory SN - 0018-9162 TI - On the shape of a set of points in the plane VL - 29 ER -