@article{4491, abstract = {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}, author = {Henzinger, Thomas A and Ho, Pei and Wong Toi, Howard}, issn = {0018-9162}, journal = {IEEE Transactions on Automatic Control}, number = {4}, pages = {540 -- 554}, publisher = {IEEE}, title = {{Algorithmic analysis of nonlinear hybrid systems}}, doi = {10.1109/9.664156 }, volume = {43}, year = {1998}, } @article{4024, abstract = {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).}, author = {Akkiraju, Nataraj and Edelsbrunner, Herbert and Fu, Ping and Qian, Jiang}, issn = {0018-9162}, journal = {IEEE Computer Graphics and Applications}, number = {4}, pages = {58 -- 61}, publisher = {IEEE}, title = {{Viewing geometric protein structures from inside a CAVE}}, doi = {10.1109/38.511855}, volume = {16}, year = {1996}, } @inproceedings{4588, abstract = {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}, author = {Alur, Rajeev and Henzinger, Thomas A}, booktitle = {Proceedings 11th Annual IEEE Symposium on Logic in Computer Science}, issn = {0018-9162}, location = {New Brunswick, NJ, USA}, pages = {207 -- 218}, publisher = {IEEE}, title = {{Reactive modules}}, doi = {10.1109/LICS.1996.561320}, year = {1996}, } @article{4611, abstract = {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}, author = {Alur, Rajeev and Henzinger, Thomas A and Ho, Pei}, issn = {0018-9162}, journal = {IEEE Transactions on Software Engineering}, number = {3}, pages = {181 -- 201}, publisher = {IEEE}, title = {{Automatic symbolic verification of embedded systems}}, doi = {10.1109/32.489079}, volume = {22}, year = {1996}, } @inproceedings{4586, abstract = {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}, author = {Alur, Rajeev and Henzinger, Thomas A}, booktitle = {Proceedings 9th Annual IEEE Symposium on Logic in Computer Science}, issn = {0018-9162}, location = {Paris, France}, pages = {52 -- 61}, publisher = {IEEE}, title = {{Finitary fairness}}, doi = {10.1109/LICS.1994.316087 }, year = {1994}, } @inproceedings{4596, abstract = {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.}, author = {Alur, Rajeev and Henzinger, Thomas A}, booktitle = {30th Annual Symposium on Foundations of Computer Science}, isbn = {0-8186-1982-1}, issn = {1558-0814}, location = {Research Triangle Park, NC, USA}, pages = {164 -- 169}, publisher = {IEEE}, title = {{A really temporal logic}}, doi = {10.1109/SFCS.1989.63473}, year = {1989}, } @article{4128, abstract = {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.}, author = {Edelsbrunner, Herbert and Kirkpatrick, David and Seidel, Raimund}, issn = {1558-0814}, journal = {IEEE Transactions on Information Theory}, number = {4}, pages = {551 -- 559}, publisher = {IEEE}, title = {{On the shape of a set of points in the plane}}, doi = {10.1109/TIT.1983.1056714 }, volume = {29}, year = {1983}, }