@inproceedings{4457, abstract = {We present a compositional approach to the implementation of hard real-time software running on a distributed platform. We explain how several code suppliers, coordinated by a system integrator, can independently generate different parts of the distributed software. The task structure, interaction, and timing is specified as a Giotto program. Each supplier is given a part of the Giotto program and a timing interface, from which the supplier generates task and scheduling code. The integrator then checks, individually for each supplier, in pseudo-polynomial time, if the supplied code meets its timing specification. If all checks succeed, then the supplied software parts are guaranteed to work together and implement the original Giotto program. The feasibility of the approach is demonstrated by a prototype implementation.}, author = {Thomas Henzinger and Kirsch, Christoph M and Matic, Slobodan}, pages = {21 -- 30}, publisher = {ACM}, title = {{Composable code generation for distributed Giotto}}, doi = {10.1145/1065910.1065914}, year = {2005}, } @inproceedings{4536, abstract = {We show how to automatically construct and refine rectangular abstractions of systems of linear differential equations. From a hybrid automaton whose dynamics are given by a system of linear differential equations, our method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton. We prove an optimality criterion for successive refinements. We also show that this method can take into account a safety property to be verified, refining only relevant parts of the state space. The practicability of the method is illustrated on a benchmark case study. }, author = {Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François}, pages = {144 -- 161}, publisher = {Springer}, title = {{Automatic rectangular refinement of affine hybrid systems}}, doi = {DOI: 10.1007/11603009_13}, volume = {3829}, year = {2005}, } @inproceedings{4541, abstract = {Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete. We study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives. }, author = {Krishnendu Chatterjee and Thomas Henzinger}, pages = {1 -- 18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Semiperfect-information games}}, doi = {10.1007/11590156_1}, volume = {3821}, year = {2005}, } @inproceedings{4553, abstract = {The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We show that for Rabin winning conditions, both problems are in NP. As these problems were known to be NP-hard, it follows that they are NP-complete for Rabin conditions, and dually, coNP-complete for Streett conditions. The proof proceeds by showing that pure memoryless strategies suffice for qualitatively and quantitatively winning stochastic graph games with Rabin conditions. This insight is of interest in its own right, as it implies that controllers for Rabin objectives have simple implementations. We also prove that for every ω-regular condition, optimal winning strategies are no more complex than almost-sure winning strategies.}, author = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger}, pages = {878 -- 890}, publisher = {Springer}, title = {{The complexity of stochastic Rabin and Streett games}}, doi = {10.1007/11523468_71}, volume = {3580}, year = {2005}, } @inproceedings{4554, abstract = {Games played on graphs may have qualitative objectives, such as the satisfaction of an ω-regular property, or quantitative objectives, such as the optimization of a real-valued reward. When games are used to model reactive systems with both fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding objective combines both a qualitative and a quantitative component. In a general case of interest, the qualitative component is a parity condition and the quantitative component is a mean-payoff reward. We study and solve such mean-payoff parity games. We also prove some interesting facts about mean-payoff parity games which distinguish them both from mean-payoff and from parity games. In particular, we show that optimal strategies exist in mean-payoff parity games, but they may require infinite memory.}, author = {Krishnendu Chatterjee and Thomas Henzinger and Jurdziński, Marcin}, pages = {178 -- 187}, publisher = {IEEE}, title = {{Mean-payoff parity games}}, doi = {10.1109/LICS.2005.26}, year = {2005}, } @inproceedings{4557, abstract = {Planning in adversarial and uncertain environments can be modeled as the problem of devising strategies in stochastic perfect information games. These games are generalizations of Markov decision processes (MDPs): there are two (adversarial) players, and a source of randomness. The main practical obstacle to computing winning strategies in such games is the size of the state space. In practice therefore, one typically works with abstractions of the model. The diffculty is to come up with an abstraction that is neither too coarse to remove all winning strategies (plans), nor too fine to be intractable. In verification, the paradigm of counterexample-guided abstraction refinement has been successful to construct useful but parsimonious abstractions automatically. We extend this paradigm to probabilistic models (namely, perfect information games and, as a special case, MDPs). This allows us to apply the counterexample-guided abstraction paradigm to the AI planning problem. As special cases, we get planning algorithms for MDPs and deterministic systems that automatically construct system abstractions.}, author = {Krishnendu Chatterjee and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S}, pages = {104 -- 111}, publisher = {AUAI Press}, title = {{Counterexample-guided planning}}, year = {2005}, } @inproceedings{4560, abstract = {We define and study a quantitative generalization of the traditional boolean framework of model-based specification and verification. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a system with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values. Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quantitative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specified by quantitative-bound automata, which are finite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an integer f(K). Along with the linear-time, automaton-based view of quantitative verification, we present a corresponding branching-time view based on a quantitative-bound μ-calculus, and we study the relationship, expressive power, and complexity of both views. }, author = {Chakrabarti, Arindam and Krishnendu Chatterjee and Thomas Henzinger and Kupferman, Orna and Majumdar, Ritankar S}, pages = {50 -- 64}, publisher = {Springer}, title = {{Verifying quantitative properties using bound functions}}, doi = {10.1007/11560548_7}, volume = {3725}, year = {2005}, } @inproceedings{4576, abstract = {We present a language for specifying web service interfaces. A web service interface puts three kinds of constraints on the users of the service. First, the interface specifies the methods that can be called by a client, together with types of input and output parameters; these are called signature constraints. Second, the interface may specify propositional constraints on method calls and output values that may oc- cur in a web service conversation; these are called consis- tency constraints. Third, the interface may specify temporal constraints on the ordering of method calls; these are called protocol constraints. The interfaces can be used to check, first, if two or more web services are compatible, and second, if a web service A can be safely substituted for a web ser- vice B. The algorithm for compatibility checking verifies that two or more interfaces fulfill each others’ constraints. The algorithm for substitutivity checking verifies that service A demands fewer and fulfills more constraints than service B.}, author = {Beyer, Dirk and Chakrabarti, Arindam and Thomas Henzinger}, pages = {148 -- 159}, publisher = {ACM}, title = {{Web service interfaces}}, doi = {10.1145/1060745.1060770}, year = {2005}, } @inproceedings{4579, abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how BLAST can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use Ccured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that BLAST can remove many of the run-time checks added by Ccured and provide useful information to the programmer about many of the remaining checks.}, author = {Beyer, Dirk and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S}, pages = {2 -- 18}, publisher = {Springer}, title = {{Checking memory safety with BLAST}}, doi = {10.1007/978-3-540-31984-9_2}, volume = {3442}, year = {2005}, } @inproceedings{4624, abstract = {Surveying results from [5] and [6], we motivate and introduce the theory behind formalizing rich interfaces for software and hardware components. Rich interfaces specify the protocol aspects of component interaction. Their formalization, called interface automata, permits a compiler to check the compatibility of component interaction protocols. Interface automata support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, while still maintaining compatibility.}, author = {de Alfaro, Luca and Thomas Henzinger}, pages = {83 -- 104}, publisher = {Springer}, title = {{Interface-based design}}, doi = {10.1007/1-4020-3532-2_3}, volume = {195}, year = {2005}, } @article{4625, abstract = {Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators ⋄ and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path. We interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics.}, author = {de Alfaro, Luca and Faella, Marco and Thomas Henzinger and Majumdar, Ritankar S and Stoelinga, Mariëlle}, journal = {Theoretical Computer Science}, number = {1}, pages = {139 -- 170}, publisher = {Elsevier}, title = {{Model checking discounted temporal properties}}, doi = {10.1016/j.tcs.2005.07.033}, volume = {345}, year = {2005}, } @article{12203, abstract = {Geranylgeranyl diphosphate synthase (GGPPS, EC: 2.5.1.29) catalyzes the biosynthesis of geranylgeranyl diphosphate (GGPP), which is a key precursor for ginkgolide biosynthesis. Here we reported for the first time the cloning of a new full-length cDNA encoding GGPPS from the living fossil plant Ginkgo biloba. The full-length cDNA encoding G. biloba GGPPS (designated as GbGGPPS) was 1657bp long and contained a 1176bp open reading frame encoding a 391 amino acid protein. Comparative analysis showed that GbGGPPS possessed a 79 amino acid transit peptide at its N-terminal, which directed GbGGPPS to target to the plastids. Bioinformatic analysis revealed that GbGGPPS was a member of polyprenyltransferases with two highly conserved aspartate-rich motifs like other plant GGPPSs. Phylogenetic tree analysis indicated that plant GGPPSs could be classified into two groups, angiosperm and gymnosperm GGPPSs, while GbGGPPS had closer relationship with gymnosperm plant GGPPSs.}, author = {Liao, Zhihua and Chen, Min and Gong, Yifu and Guo, Liang and Tan, Qiumin and Feng, Xiaoqi and Sun, Xiaofen and Tan, Feng and Tang, Kexuan}, issn = {1042-5179}, journal = {DNA Sequence}, keywords = {Endocrinology, Genetics, Molecular Biology, Biochemistry}, number = {2}, pages = {153--158}, publisher = {Informa UK Limited}, title = {{A new geranylgeranyl Diphosphate synthase gene from Ginkgo biloba, which intermediates the biosynthesis of the key precursor for ginkgolides}}, doi = {10.1080/10425170410001667348}, volume = {15}, year = {2004}, } @article{12658, abstract = {[1] During the ablation period 2001 a glaciometeorological experiment was carried out on Haut Glacier d'Arolla, Switzerland. Five meteorological stations were installed on the glacier, and one permanent automatic weather station in the glacier foreland. The altitudes of the stations ranged between 2500 and 3000 m a.s.l., and they were in operation from end of May to beginning of September 2001. The spatial arrangement of the stations and temporal duration of the measurements generated a unique data set enabling the analysis of the spatial and temporal variability of the meteorological variables across an alpine glacier. All measurements were taken at a nominal height of 2 m, and hourly averages were derived for the analysis. The wind regime was dominated by the glacier wind (mean value 2.8 m s−1) but due to erosion by the synoptic gradient wind, occasionally the wind would blow up the valley. A slight decrease in mean 2 m air temperatures with altitude was found, however the 2 m air temperature gradient varied greatly and frequently changed its sign. Mean relative humidity was 71% and exhibited limited spatial variation. Mean incoming shortwave radiation and albedo both generally increased with elevation. The different components of shortwave radiation are quantified with a parameterization scheme. Resulting spatial variations are mainly due to horizon obstruction and reflections from surrounding slopes, i.e., topography. The effect of clouds accounts for a loss of 30% of the extraterrestrial flux. Albedos derived from a Landsat TM image of 30 July show remarkably constant values, in the range 0.49 to 0.50, across snow covered parts of the glacier, while albedo is highly spatially variable below the zone of continuous snow cover. These results are verified with ground measurements and compared with parameterized albedo. Mean longwave radiative fluxes decreased with elevation due to lower air temperatures and the effect of upper hemisphere slopes. It is shown through parameterization that this effect would even be more pronounced without the effect of clouds. Results are discussed with respect to a similar study which has been carried out on Pasterze Glacier (Austria). The presented algorithms for interpolating, parameterizing and simulating variables and parameters in alpine regions are integrated in the software package AMUNDSEN which is freely available to be adapted and further developed by the community.}, author = {Strasser, Ulrich and Corripio, Javier and Pellicciotti, Francesca and Burlando, Paolo and Brock, Ben and Funk, Martin}, issn = {0148-0227}, journal = {Journal of Geophysical Research: Atmospheres}, keywords = {Paleontology, Space and Planetary Science, Earth and Planetary Sciences (miscellaneous), Atmospheric Science, Earth-Surface Processes, Geochemistry and Petrology, Soil Science, Water Science and Technology, Ecology, Aquatic Science, Forestry, Oceanography, Geophysics}, number = {D3}, publisher = {American Geophysical Union}, title = {{Spatial and temporal variability of meteorological variables at Haut Glacier d'Arolla (Switzerland) during the ablation season 2001: Measurements and simulations}}, doi = {10.1029/2003jd003973}, volume = {109}, year = {2004}, } @article{8517, abstract = {We consider the evolution of a connected set on the plane carried by a space periodic incompressible stochastic flow. While for almost every realization of the stochastic flow at time t most of the particles are at a distance of order equation image away from the origin, there is a measure zero set of points that escape to infinity at the linear rate. We study the set of points visited by the original set by time t and show that such a set, when scaled down by the factor of t, has a limiting nonrandom shape.}, author = {Dolgopyat, Dmitry and Kaloshin, Vadim and Koralov, Leonid}, issn = {0010-3640}, journal = {Communications on Pure and Applied Mathematics}, keywords = {Applied Mathematics, General Mathematics}, number = {9}, pages = {1127--1158}, publisher = {Wiley}, title = {{A limit shape theorem for periodic stochastic dispersion}}, doi = {10.1002/cpa.20032}, volume = {57}, year = {2004}, } @article{8518, author = {Koralov, Leonid and Kaloshin, Vadim and Dolgopyat, Dmitry}, issn = {0091-1798}, journal = {The Annals of Probability}, number = {1A}, pages = {1--27}, publisher = {Institute of Mathematical Statistics}, title = {{Sample path properties of the stochastic flows}}, doi = {10.1214/aop/1078415827}, volume = {32}, year = {2004}, } @article{864, abstract = {We present a method for prediction of functional sites in a set of aligned protein sequences. The method selects sites which are both well conserved and clustered together in space, as inferred from the 3D structures of proteins included in the alignment. We tested the method using 86 alignments from the NCBI CDD database, where the sites of experimentally determined ligand and/or macromolecular interactions are annotated. In agreement with earlier investigations, we found that functional site predictions are most successful when overall background sequence conservation is low, such that sites under evolutionary constraint become apparent. In addition, we found that averaging of conservation values across spatially clustered sites improves predictions under certain conditions: that is, when overall conservation is relatively high and when the site in question involves a large macromolecular binding interface. Under these conditions it is better to look for clusters of conserved sites than to look for particular conserved sites.}, author = {Panchenko, Anna R and Fyodor Kondrashov and Bryant, Stephen H}, journal = {Protein Science}, number = {4}, pages = {884 -- 892}, publisher = {Wiley-Blackwell}, title = {{Prediction of functional sites by analysis of sequence and structure conservation}}, doi = {10.1110/ps.03465504}, volume = {13}, year = {2004}, } @article{870, abstract = {Only a fraction of eukaryotic genes affect the phenotype drastically. We compared 18 parameters in 1273 human morbid genes, known to cause diseases, and in the remaining 16 580 unambiguous human genes. Morbid genes evolve more slowly, have wider phylogenetic distributions, are more similar to essential genes of Drosophila melanogaster, code for longer proteins containing more alanine and glycine and less histidine, lysine and methionine, possess larger numbers of longer introns with more accurate splicing signals and have higher and broader expressions. These differences make it possible to classify as non-morbid 34% of human genes with unknown morbidity, when only 5% of known morbid genes are incorrectly classified as non-morbid. This classification can help to identify disease-causing genes among multiple candidates.}, author = {Fyodor Kondrashov and Ogurtsov, Aleksey Yu and Kondrashov, Alexey S}, journal = {Nucleic Acids Research}, number = {5}, pages = {1731 -- 1737}, publisher = {Oxford University Press}, title = {{Bioinformatical assay of human gene morbidity}}, doi = {10.1093/nar/gkh330}, volume = {32}, year = {2004}, } @article{875, abstract = {The dominance of wild-type alleles and the concomitant recessivity of deleterious mutant alleles might have evolved by natural selection or could be a by-product of the molecular and physiological mechanisms of gene action. We compared the properties of human haplosufficient genes, whose wild-type alleles are dominant over loss-of-function alleles, with haploinsufficient (recessive wild-type) genes, which produce an abnormal phenotype when heterozygous for a loss-of-function allele. The fraction of haplosufficient genes is the highest among the genes that encode enzymes, which is best compatible with the physiological theory. Haploinsufficient genes, on average, have more paralogs than haplosufficient genes, supporting the idea that gene dosage could be important for the initial fixation of duplications. Thus, haplo(in)sufficiency of a gene and its propensity for duplication might have a common evolutionary basis.}, author = {Fyodor Kondrashov and Koonin, Eugene V}, journal = {Trends in Genetics}, number = {7}, pages = {287 -- 291}, publisher = {Elsevier}, title = {{A common framework for understanding the origin of genetic dominance and evolutionary fates of gene duplications}}, doi = {10.1016/j.tig.2004.05.001}, volume = {20}, year = {2004}, } @article{889, abstract = {The function of protein and RNA molecules depends on complex epistatic interactions between sites. Therefore, the deleterious effect of a mutation can be suppressed by a compensatory second-site substitution. In relating a list of 86 pathogenic mutations in human IRNAs encoded by mitochondrial genes to the sequences of their mammalian orthologs, we noted that 52 pathogenic mutations were present in normal tRNAs of one or several nonhuman mammals. We found at least five mechanisms of compensation for 32 pathogenic mutations that destroyed a Watson-Crick pair in one of the four tRNA stems: restoration of the affected Watson-Crick interaction (25 cases), strengthening of another pair (4 cases), creation of a new pair (8 cases), changes of multiple interactions in the affected stem (11 cases) and changes involving the interaction between the loop and stem structures (3 cases). A pathogenic mutation and its compensating substitution are fixed in a lineage in rapid succession, and often a compensatory interaction evolves convergently in different clades. At least 10%, and perhaps as many as 50%, of all nucleotide substitutions in evolving mammalian (RNAs participate in such interactions, indicating that the evolution of tRNAs proceeds along highly epistatic fitness ridges.}, author = {Kern, Andrew D and Fyodor Kondrashov}, journal = {Nature Genetics}, number = {11}, pages = {1207 -- 1212}, publisher = {Nature Publishing Group}, title = {{Mechanisms and convergence of compensatory evolution in mammalian mitochondrial tRNAs}}, doi = {10.1038/ng1451}, volume = {36}, year = {2004}, } @article{898, abstract = {New alleles become fixed owing to random drift of nearly neutral mutations or to positive selection of substantially advantageous mutations. After decades of debate, the fraction of fixations driven by selection remains uncertain. Within 9,390 genes, we analysed 28,196 codons at which rat and mouse differ from each other at two nucleotide sites and 1,982 codons with three differences. At codons where rat-mouse divergence involved two non-synonymous substitutions, both of them occurred in the same lineage, either rat or mouse, in 64% of cases; however, independent substitutions would occur in the same lineage with a probability of only 50%. All three non-synonymous substitutions occurred in the same lineage for 46% of codons, instead of the 25% expected. Furthermore, comparison of 12 pairs of prokaryotic genomes also shows clumping of multiple non-synonymous substitutions in the same lineage. This pattern cannot be explained by correlated mutation or episodes of relaxed negative selection, but instead indicates that positive selection acts at many sites of rapid, successive amino acid replacement.}, author = {Bazykin, Georgii A and Fyodor Kondrashov and Ogurtsov, Aleksey Yu and Sunyaev, Shamil R and Kondrashov, Alexey S}, journal = {Nature}, number = {6991}, pages = {558 -- 562}, publisher = {Nature Publishing Group}, title = {{Positive selection at sites of multiple amino acid replacements since rat-mouse divergence}}, doi = {10.1038/nature02601}, volume = {429}, year = {2004}, }