@inproceedings{4434,
abstract = {The algorithmic approach to the analysis of timed and hybrid systems is fundamentally limited by undecidability, of universality in the timed case (where all continuous variables are clocks), and of emptiness in the rectangular case (which includes drifting clocks). Traditional proofs of undecidability encode a single Turing computation by a single timed trajectory. These proofs have nurtured the hope that the introduction of “fuzziness” into timed and hybrid models (in the sense that a system cannot distinguish between trajectories that are sufficiently similar) may lead to decidability. We show that this is not the case, by sharpening both fundamental undecidability results. Besides the obvious blow our results deal to the algorithmic method, they also prove that the standard model of timed and hybrid systems, while not “robust” in its definition of trajectory acceptance (which is affected by tiny perturbations in the timing of events), is quite robust in its mathematical properties: the undecidability barriers are not affected by reasonable perturbations of the model.},
author = {Thomas Henzinger and Raskin, Jean-François},
pages = {145 -- 159},
publisher = {Springer},
title = {{Robust undecidability of timed and hybrid systems}},
doi = {10.1007/3-540-46430-1_15},
volume = {1790},
year = {2000},
}
@inproceedings{4435,
abstract = {An important case of hybrid systems are the rectangular automata. First, rectangular dynamics can naturally and arbitrarily closely approximate more general, nonlinear dynamics. Second, rectangular automata are the most general type of hybrid systems for which model checking -in particular, Ltl model checking- is decidable. However, on one hand, the original proofs of decidability did not suggest practical algorithms and, on the other hand, practical symbolic model-checking procedures -such as those implemented in HyTech- were not known to terminate on rectangular automata. We remedy this unsatisfactory situation: we present a symbolic method for Ltl model checking which can be performed by HyTech and is guaranteed to terminate on all rectangular automata. We do so by proving that our method for symbolic Ltl model checking terminates on an infinite-state transition system if the trace-equivalence relation of the system has finite index, which is the case for all rectangular automata.},
author = {Thomas Henzinger and Majumdar, Ritankar S},
pages = {142 -- 156},
publisher = {Springer},
title = {{Symbolic model checking for rectangular hybrid systems}},
doi = {10.1007/3-540-46419-0_11},
volume = {1785},
year = {2000},
}
@inproceedings{4439,
abstract = {We define five increasingly comprehensive classes of infinite-state systems, called STS1–5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.
STS1 These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by (1) iterating the predecessor and boolean operations starting from a finite set of observable state sets, and (2) terminating when no new state sets are generated. This enables model checking of the μ-calculus.
STS2 These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive boolean operations. This enables model checking of the existential and universal fragments of the μ-calculus.
STS3 These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive boolean operations (intersection is restricted to intersection with observables). This enables model checking of linear temporal logic.
STS4 These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the μ-calculus.
STS5 These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered. This enables model checking of reachability properties.},
author = {Thomas Henzinger and Majumdar, Ritankar S},
pages = {13 -- 34},
publisher = {Springer},
title = {{A classification of symbolic transition systems}},
doi = {10.1007/3-540-46541-3_2},
volume = {1770},
year = {2000},
}
@inproceedings{4481,
abstract = {Since hybrid embedded systems are pervasive and often safety-critical, guarantees about their correct performance are desirable. The hybrid systems model checker HyTech provides such guarantees and has successfully verified some systems. However, HyTech severely restricts the continuous dynamics of the system being analyzed and, therefore, often forces the use of prohibitively expensive discrete and polyhedral abstractions. We have designed a new algorithm, which is capable of directly verifying hybrid systems with general continuous dynamics, such as linear and nonlinear differential equations. The new algorithm conservatively overapproximates the reachable states of a hybrid automaton by using interval numerical methods. Interval numerical methods return sets of points that enclose the true result of numerical computation and, thus, avoid distortions due to the accumulation of round-off errors. We have implemented the new algorithm in a successor tool to HyTech called HyperTech. We consider three examples: a thermostat with delay, a two-tank water system, and an air-traffic collision avoidance protocol. HyperTech enables the direct, fully automatic analysis of these systems, which is also more accurate than the use of polyhedral abstractions.},
author = {Thomas Henzinger and Horowitz, Benjamin and Majumdar, Ritankar S and Wong-Toi, Howard},
pages = {130 -- 144},
publisher = {Springer},
title = {{Beyond HyTech: Hybrid systems analysis using interval numerical methods}},
doi = {10.1007/3-540-46430-1_14},
volume = {1790},
year = {2000},
}
@inproceedings{4482,
abstract = {We apply the theory of abstract interpretation to the verification of game properties for reactive systems. Unlike properties expressed in standard temporal logics, game properties can distinguish adversarial from collaborative relationships between the processes of a concurrent program, or the components of a parallel system. We consider two-player concurrent games –say, component vs. environment– and specify properties of such games –say, the component has a winning strategy to obtain a resource, no matter how the environment behaves– in the alternating-time μ-calculus (Aμ ). A sound abstraction of such a game must at the same time restrict the behaviors of the component and increase the behaviors of the environment: if a less powerful component can win against a more powerful environment, then surely the original component can win against the original environment.
We formalize the concrete semantics of a concurrent game in terms of controllable and uncontrollable predecessor predicates, which suffice for model checking all Aμ properties by applying boolean operations and iteration. We then define the abstract semantics of a concurrent game in terms of abstractions for the controllable and uncontrollable predecessor predicates. This allows us to give general characterizations for the soundness and completeness of abstract games with respect to Aμ properties. We also present a simple programming language for multi-process programs, and show how approximations of the maximal abstraction (w.r.t. Aμ properties) can be obtained from the program text. We apply the theory to two practical verification examples, a communication protocol developed at the Berkeley Wireless Research Center, and a protocol converter. In the wireless protocol, both the use of a game property for specification and the use of abstraction for automatic verification were instrumental to uncover a subtle bug.},
author = {Thomas Henzinger and Majumdar, Ritankar S and Mang, Freddy Y and Raskin, Jean-François},
pages = {220 -- 239},
publisher = {Springer},
title = {{Abstract interpretation of game properties}},
doi = {10.1007/978-3-540-45099-3_12},
volume = {1824},
year = {2000},
}
@inproceedings{4483,
abstract = {Model-checking algorithms can be used to verify, formally and automatically, if a low-level description of a design conforms with a high-level description. However, for designs with very large state spaces, prior to the application of an algorithm, the refinement-checking task needs to be decomposed into subtasks of manageable complexity. It is natural to decompose the task following the component structure of the design. However, an individual component often does not satisfy its requirements unless the component is put into the right context, which constrains the inputs to the component. Thus, in order to verify each component individually, we need to make assumptions about its inputs, which are provided by the other components of the design. This reasoning is circular: component A is verified under the assumption that context B behaves correctly, and symmetrically, B is verified assuming the correctness of A. The assume-guarantee paradigm provides a systematic theory and methodology for ensuring the soundness of the circular style of postulating and discharging assumptions in component-based reasoning.We give a tutorial introduction to the assume-guarantee paradigm for decomposing refinement-checking tasks. To illustrate the method, we step in detail through the formal verification of a processor pipeline against an instruction set architecture. In this example, the verification of a three-stage pipeline is broken up into three subtasks, one for each stage of the pipeline.},
author = {Thomas Henzinger and Qadeer,Shaz and Rajamani, Sriram K},
pages = {245 -- 252},
publisher = {IEEE},
title = {{Decomposing refinement proofs using assume-guarantee reasoning}},
doi = {10.1109/ICCAD.2000.896481},
year = {2000},
}
@inproceedings{4512,
abstract = {Masaccio is a formal model for hybrid dynamical systems which are built from atomic discrete components (difference equations) and atomic continuous components (differential equations) by parallel and serial composition, arbitrarily nested. Each system component consists of an interface, which determines the possible ways of using the component, and a set of executions, which define the possible behaviors of the component in real time.
Version 1.0 (May 2000).
},
author = {Thomas Henzinger},
pages = {549 -- 563},
publisher = {Springer},
title = {{Masaccio: A formal model for embedded components}},
doi = {10.1007/3-540-44929-9_38},
volume = {1872},
year = {2000},
}
@inbook{4513,
author = {Thomas Henzinger},
booktitle = {Verification of Digital and Hybrid Systems},
editor = {Inan, M. Kemal and Kurshan, Robert P.},
pages = {265 -- 292},
publisher = {Springer},
title = {{The theory of hybrid automata}},
volume = {170},
year = {2000},
}
@article{4598,
abstract = {A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analyzed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas.},
author = {Alur, Rajeev and Thomas Henzinger and Lafferriere, Gerardo and Pappas, George J.},
journal = {Proceedings of the IEEE},
number = {7},
pages = {971 -- 984},
publisher = {IEEE},
title = {{Discrete abstractions of hybrid systems}},
doi = {10.1109/5.871304 },
volume = {88},
year = {2000},
}
@inproceedings{4627,
abstract = {We consider two-player games, which are played on a finite state space for an infinite number of rounds. The games are concurrent, that is, in each round, the two players choose their moves independently and simultaneously; the current state and the two moves determine a successor state. We consider omega-regular winning conditions on the resulting infinite state sequence. To model the independent choice of moves, both players are allowed to use randomization for selecting their moves. This gives rise to the following qualitative modes of winning, which can be studied without numerical considerations concerning probabilities: sure-win (player 1 can ensure winning with certainty), almost-sure-win (player 1 can ensure winning with probability 1), limit-win (player 1 can ensure winning with probability arbitrarily close to 1), bounded-win (player 1 can ensure winning with probability bounded away from 0), positive-win (player 1 can ensure winning with positive probability), and exist-win (player 1 can ensure that at least one possible outcome of the game satisfies the winning condition).We provide algorithms for computing the sets of winning states for each of these winning modes. In particular, we solve concurrent Rabin-chain games in n0 (m) time, where n is the size of the game structure and m is the number of pairs in the Rabin-chain condition. While this complexity is in line with traditional turn-based games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games are. This is because concurrent games violate two of the most fundamental properties of turn-based games. First, concurrent games are not determined, but rather exhibit a more general duality property, which involves multiple modes of winning. Second, winning strategies for concurrent games may require infinite memory.},
author = {de Alfaro, Luca and Thomas Henzinger},
pages = {141 -- 154},
publisher = {IEEE},
title = {{Concurrent omega-regular games}},
doi = {10.1109/LICS.2000.855763},
year = {2000},
}
@inproceedings{4637,
abstract = {In the synchronous composition of processes, one process may prevent another process from proceeding unless compositions without a well-defined product behavior are ruled out. They can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping processes with types, which make the dependencies between input and output signals transparent. We classify various typing mechanisms and study their effects on the control problem.
A static type enforces fixed, acyclic dependencies between input and output ports. For example, synchronous hardware without combinational loops can be typed statically. A dynamic type may vary the dependencies from state to state, while maintaining acyclicity, as in level-sensitive latches. Then, two dynamically typed processes can be syntactically compatible, if all pairs of possible dependencies are compatible, or semantically compatible, if in each state the combined dependencies remain acyclic. For a given plant process and control objective, there may be a controller of a static type, or only a controller of a syntactically compatible dynamic type, or only a controller of a semantically compatible dynamic type. We show this to be a strict hierarchy of possibilities, and we present algorithms and determine the complexity of the corresponding control problems.
Furthermore, we consider versions of the control problem in which the type of the controller (static or dynamic) is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions},
author = {de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {458 -- 473},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{The control of synchronous systems}},
doi = {10.1007/3-540-44618-4_33},
volume = {1877},
year = {2000},
}
@inproceedings{4638,
abstract = {Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) rather than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented, which can be long before it actually occurs; for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated.
The key observation is that “unpreventability” is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on different degrees of information available about the environment, we define and implement several notions of “unpreventability,” including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples, a distributed database protocol and a wireless communication protocol.},
author = {de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {186 -- 201},
publisher = {Springer},
title = {{Detecting errors before reaching them}},
doi = {10.1007/10722167_17},
volume = {1855},
year = {2000},
}
@inproceedings{2710,
author = {László Erdös},
pages = {111 -- 119},
publisher = {American Mathematical Society},
title = {{The kernel of Dirac operators on S3 and R3}},
volume = {16},
year = {2000},
}
@article{2731,
abstract = {We study the time evolution of a quantum particle in a Gaussian random environment. We show that in the weak coupling limit the Wigner distribution of the wave function converges to a solution of a linear Boltzmann equation globally in time. The Boltzmann collision kernel is given by the Born approximation of the quantum differential scattering cross section.},
author = {László Erdös and Yau, Horng-Tzer},
journal = {Communications on Pure and Applied Mathematics},
number = {6},
pages = {667 -- 735},
publisher = {Wiley-Blackwell},
title = {{Linear Boltzmann equation as the weak coupling limit of a random Schrödinger equation}},
doi = {10.1002/(SICI)1097-0312(200006)53:6<667::AID-CPA1>3.0.CO;2-5},
volume = {53},
year = {2000},
}
@article{2732,
abstract = {We consider a quantum particle moving in a harmonic exterior potential and linearly coupled to a heat bath of quantum oscillators. Caldeira and Leggett derived the Fokker Planck equation with friction for the Wigner distribution of the particle in the large-temperature limit: however, their (nonrigorous) derivation was not free of criticism, especially since the limiting equation is not of Lindblad form. In this paper we recover the correct form of their result in a rigorous way. We also point out that the source of the diffusion is physically restrictive under this scaling. We investigate the model at a fixed temperature and in the large-time limit, where the origin of the diffusion is a cumulative effect of many resonant collisions. We obtain a heat equation with a friction term for the radial process in phase space and we prove the Einstein relation in this case.},
author = {Castella, François and László Erdös and Frommlet, Florian and Markowich, Peter A},
journal = {Journal of Statistical Physics},
number = {3-4},
pages = {543 -- 601},
publisher = {Springer},
title = {{Fokker-Planck equations as scaling limits of reversible quantum systems}},
doi = {10.1023/A:1018667323830},
volume = {100},
year = {2000},
}
@article{2733,
abstract = {The Li-Yau semiclassical lower bound for the sum of the first N eigenvalues of the Dirichlet–Laplacian is extended to Dirichlet–Laplacians with constant magnetic fields. Our method involves a new diamagnetic inequality for constant magnetic fields.},
author = {László Erdös and Loss, Michael and Vougalter, Vitali},
journal = {Annales de l'Institut Fourier},
number = {3},
pages = {891 -- 907},
publisher = {Association des Annales de l'Institut Fourier},
title = {{Diamagnetic behavior of sums Dirichlet eigenvalues}},
doi = {10.5802/aif.1777},
volume = {50},
year = {2000},
}
@article{3149,
abstract = {The prohormone convertases (PCs) are an evolutionarily ancient group of proteases required for the maturation of neuropeptide and peptide hormone precursors. In Drosophila melanogaster, the homolog of prohormone convertase 2, dPC2 (amontillado), is required for normal hatching behavior, and immunoblotting data indicate that flies express 80- and 75-kDa forms of this protein. Because mouse PC2 (mPC2) requires 7B2, a helper protein for productive maturation, we searched the fly data base for the 7B2 signature motif PPNPCP and identified an expressed sequence tag clone encoding the entire open reading frame for this protein. dPC2 and d7B2 cDNAs were subcloned into expression vectors for transfection into HEK-293 cells; mPC2 and rat 7B2 were used as controls. Although active mPC2 was detected in medium in the presence of either d7B2 or r7B2, dPC2 showed no proteolytic activity upon coexpression of either d7B2 or r7B2. Labeling experiments showed that dPC2 was synthesized but not secreted from HEK-293 cells. However, when dPC2 and either d7B2 or r7B2 were coexpressed in Drosophila S2 cells, abundant immunoreactive dPC2 was secreted into the medium, coincident with the appearance of PC2 activity. Expression and secretion of dPC2 enzyme activity thus appears to require insect cell-specific posttranslational processing events. The significant differences in the cell biology of the insect and mammalian enzymes, with 7B2 absolutely required for secretion of dPC2 and zymogen conversion occurring intracellularly in the case of dPC2 but not mPC2, support the idea that the Drosophila enzyme has specific requirements for maturation and secretion that can be met only in insect cells.},
author = {Hwang, Jae R and Daria Siekhaus and Fuller, Robert S and Taghert, Paul H and Lindberg, Iris},
journal = {Journal of Biological Chemistry},
number = {23},
pages = {17886 -- 17893},
publisher = {American Society for Biochemistry and Molecular Biology},
title = {{Interaction of Drosophila melanogaster prohormone convertase 2 and 7B2: Insect cell specific processing and secretion}},
doi = {10.1074/jbc.M000032200 },
volume = {275},
year = {2000},
}
@inproceedings{1736,
abstract = {A coding scheme called diode is compared with duobinary signalling and with normal binary transmission. It is shown that the diode coding suppresses the FWM products of a three channel DWDM system and this reduction against that achieved with duobinary coding is presented. The results presented show how the average level of the FWM products relative to the average levels of the three optical carriers vary over the channel spacing range. The suppression observed is about / dB more than that achieved with duobinary modulation and is greater for narrow channel spacing.},
author = {Georgios Katsaros and Lane, Phil M and Murphy, Michelle M},
pages = {27 -- 28},
publisher = {IEEE},
title = {{Comparison of the impact of FWM on binary, duobinary and dicode modulation in DWDM systems}},
doi = {10.1109/LEOS.2000.890656},
volume = {1},
year = {2000},
}
@article{1957,
abstract = {NADH:ubiquinone oxidoreductase (complex I) is the first and largest enzyme of the mitochondrial respiratory chain. The low-resolution structure of the complex is known from electron microscopy studies. The general shape of the complex is in the form of an L, with one arm in the membrane and the other peripheral. We have purified complex I from beef heart mitochondria and reconstituted the enzyme into lipid bilayers. Under different conditions, several two-dimensional crystal forms were obtained. Crystals belonging to space groups p2221 and c12 (unit cell 488 Å x 79 Å) were obtained at 22°C and contained only the membrane fragment of complex I similar to hydrophobic subcomplex Iβ but lacking the ND5 subunit. A crystal form with larger unit cell (534 Å x 81 Å, space group c12) produced at 4°C contained both the peripheral and membrane arms of the enzyme, except that ND5 was missing. Projection maps from frozen hydrated samples were calculated for all crystal forms. By comparing two different c12 crystal forms, extra electron density in the projection map of large crystal form was assigned to the peripheral arm of the enzyme. One of the features of the map is a deep, channel-like, cleft next to peripheral arm. Comparison with available structures of the intact enzyme indicates that large hydrophobic subunit ND5 is situated at the distal end of the membrane domain. Possible locations of sub-unit ND4 and of other subunits in the membrane domain are proposed. Implications of our findings for the mechanism of proton pumping by complex I are discussed. (C) 2000 Academic Press.},
author = {Leonid Sazanov and Walker, John E},
journal = {Journal of Molecular Biology},
number = {2},
pages = {455 -- 464},
publisher = {Elsevier},
title = {{Cryo-electron crystallography of two sub-complexes of bovine complex I reveals the relationship between the membrane and peripheral arms}},
doi = {10.1006/jmbi.2000.4079},
volume = {302},
year = {2000},
}
@article{1958,
abstract = {
Complex I (NADH:ubiquinone oxidoreductase) purified from bovine heart mitochondria was treated with the detergent N,N-dimethyldodecylamine N-oxide (LDAO). The enzyme dissociated into two known subcomplexes, Iα and Iβ, containing mostly hydrophilic and hydrophobic subunits, and a previously undetected fragment referred to as Iγ. Subcomplex Iγ contains the hydrophobic subunits ND1, ND2, ND3, and ND4L which are encoded in the mitochondrial genome, and the nuclear-encoded subunit KFYL. During size- exclusion chromatography in the presence of LDAO, subcomplex Iα lost several subunits and formed another characterized subcomplex known as Iλ. Similarly, subcomplex Iβ dissociated into two smaller subcomplexes, one of which contains the hydrophobic subunits ND4 and ND5; subcomplex Iγ released a fragment containing ND1 and ND2. These results suggest that in the intact complex subunits ND1 and ND2 are likely to be in a different region of the membrane domain than subunits ND4 and ND5. The compositions of the various subcomplexes and fragments of complex I provide an organization of the subunits of the enzyme in the framework of the known low resolution structure of the enzyme.},
author = {Leonid Sazanov and Peak-Chew, Sew Y and Fearnley, Ian M and Walker, John E},
journal = {Biochemistry},
number = {24},
pages = {7229 -- 7235},
publisher = {ACS},
title = {{Resolution of the membrane domain of bovine complex I into subcomplexes: implications for the structural organization of the enzyme}},
doi = {10.1021/bi000335t},
volume = {39},
year = {2000},
}