@article{2121, abstract = {Let H be a separable real Hubert space and let double struck F sign = (ℱt)t∈[0,T] be the augmented filtration generated by an H-cylindrical Brownian motion (WH(t))t∈[0,T] on a probability space (Ω, ℱ ℙ). We prove that if E is a UMD Banach space, 1 ≤ p < ∞, and F ∈ double struck D sign1,p(Ω E) is ℱT-measurable, then F = double struck E sign(F) + ∫0T Pdouble struck F sign(DF) dW H, where D is the Malliavin derivative of F and P double struck F sign is the projection onto the F-adapted elements in a suitable Banach space of Lp-stochastically integrable ℒ(H, E)-valued processes.}, author = {van Neerven, Jan M and Jan Maas}, journal = {Electronic Communications in Probability}, pages = {151 -- 164}, publisher = {Institute of Mathematical Statistics}, title = {{A Clark-Ocone formula in UMD Banach spaces}}, volume = {13}, year = {2008}, } @article{2146, abstract = {We present an analytic model of thermal state-to-state rotationally inelastic collisions of polar molecules in electric fields. The model is based on the Fraunhofer scattering of matter waves and requires Legendre moments characterizing the “shape” of the target in the body-fixed frame as its input. The electric field orients the target in the space-fixed frame and thereby effects a striking alteration of the dynamical observables: both the phase and amplitude of the oscillations in the partial differential cross sections undergo characteristic field-dependent changes that transgress into the partial integral cross sections. As the cross sections can be evaluated for a field applied parallel or perpendicular to the relative velocity, the model also offers predictions about steric asymmetry. We exemplify the field-dependent quantum collision dynamics with the behavior of the Ne–OCS(Σ1) and Ar–NO(Π2) systems. A comparison with the close-coupling calculations available for the latter system [Chem. Phys. Lett.313, 491 (1999)] demonstrates the model’s ability to qualitatively explain the field dependence of all the scattering features observed.}, author = {Mikhail Lemeshko and Friedrich, Břetislav}, journal = {Journal of Chemical Physics}, number = {2}, publisher = {American Institute of Physics}, title = {{An analytic model of rotationally inelastic collisions of polar molecules in electric fields}}, doi = {10.1063/1.2948392}, volume = {129}, year = {2008}, } @misc{2147, abstract = {We present the physics of the quantum Zeno effect, whose gist is often expressed by invoking the adage "a watched pot never boils". We review aspects of the theoretical and experimental work done on the effect since its inception in 1977, and mention some applications. We dedicate the article - with our very best wishes - to Rudolf Zahradnik at the occasion of his great jubilee. Perhaps Rudolf's lasting youthfulness and freshness are due to that he himself had been frequently observed throughout his life: until the political turn-around in 1989 by those who wished, by their surveillance, to prevent Rudolf from spoiling the youth by his personal culture and his passion for science and things beautiful and useful in general. This attempt had failed. Out of gratitude, the youth has infected Rudolf with its youthfulness. Chronically. Since 1989, Rudolf has been closely watched by the public at large. For the same traits of his as before, but with the opposite goal and for the benefit of all generations. We relish keeping him in sight...}, author = {Mikhail Lemeshko and Friedrich, Břetislav}, booktitle = {Chemicke Listy}, number = {10}, pages = {880 -- 883}, publisher = {Czech Society of Chemical Engineering}, title = {{Kvantový Zenonův jev aneb co nesejde z očí, nezestárne}}, volume = {102}, year = {2008}, } @article{2148, abstract = {Despite the growing geological evidence that fluid boiling and vapour-liquid separation affect the distribution of metals in magmatic-hydrothermal systems significantly, there are few experimental data on the chemical status and partitioning of metals in the vapour and liquid phases. Here we report on an in situ measurement, using X-ray absorption fine structure (XAFS) spectroscopy, of antimony speciation and partitioning in the system Sb2O3-H2O-NaCl-HCl at 400°C and pressures 270–300 bar corresponding to the vapour-liquid equilibrium. Experiments were performed using a spectroscopic cell which allows simultaneous determination of the total concentration and atomic environment of the absorbing element (Sb) in each phase. Results show that quantitative vapour-brine separation of a supercritical aqueous salt fluid can be achieved by a controlled decompression and monitoring the X-ray absorbance of the fluid phase. Antimony concentrations in equilibrium with Sb2O3 (cubic, senarmontite) in the coexisting vapour and liquid phases and corresponding SbIII vapour-liquid partitioning coefficients are in agreement with recent data obtained using batch-reactor solubility techniques. The XAFS spectra analysis shows that hydroxy-chloride complexes, probably Sb(OH)2Cl0, are dominant both in the vapour and liquid phase in a salt-water system at acidic conditions. This first in situ XAFS study of element fractionation between coexisting volatile and dense phases opens new possibilities for systematic investigations of vapour-brine and fluid-melt immiscibility phenomena, avoiding many experimental artifacts common in less direct techniques.}, author = {Pokrovski, Gleb S and Roux, Jacques L and Hazemann, Jean L and Borisova, Anastassia Y and Gonchar, Anastasia A and Mikhail Lemeshko}, journal = {Mineralogical Magazine}, number = {2}, pages = {667 -- 681}, publisher = {Mineralogical Society}, title = {{In situ X-ray absorption spectroscopy measurement of vapour-brine fractionation of antimony at hydrothermal conditions}}, doi = {10.1180/minmag.2008.072.2.667 }, volume = {72}, year = {2008}, } @article{21512, abstract = {The possibility to fill cavities of finite geometry could be described using an analytical model of the hot-embossing process of viscoelastic polymers. This model is based on the volume conservation during the forming process which allows to predict data concerning the geometrical evolution of the material on one hand, and on the other hand the filling time of cavities in the mould. A particular attention was drawn on the necessary time to fill the cavities depending on their shape or a scale factor for a given cavity shape.}, author = {Sahli, M. and Roques-Carmes, Charles and Khan Malek, C. and Gelin, J. C.}, issn = {1432-1858}, journal = {Microsystem Technologies}, pages = {1545--1551}, publisher = {Springer Nature}, title = {{Modelling of the filling of micro-cavities of finite geometry by amorphous polymers using hot-embossing}}, doi = {10.1007/s00542-008-0565-8}, volume = {14}, year = {2008}, } @article{13422, abstract = {Make like a leaf: The synthesis and characterization of a family of “flowerlike” Au/Fe3O4 nanoparticles is described, whereby Fe3O4 “leaves” adhere to a gold core (see image). The size and numbers of iron oxide domains can be adjusted flexibly by changing the proportion of the starting materials and the reaction time.}, author = {Wei, Yanhu and Klajn, Rafal and Pinchuk, Anatoliy O. and Grzybowski, Bartosz A.}, issn = {1613-6829}, journal = {Small}, keywords = {Biomaterials, Biotechnology, General Materials Science, General Chemistry}, number = {10}, pages = {1635--1639}, publisher = {Wiley}, title = {{Synthesis, shape control, and optical properties of hybrid Au/Fe3O4 “nanoflowers”}}, doi = {10.1002/smll.200800511}, volume = {4}, year = {2008}, } @article{13423, abstract = {Supraspheres (SS) composed of hundreds to thousands of metal nanoparticles (NPs) and crosslinked by dithiol linkers are assembled into larger structures, which are subsequently converted into nanoporous metals (NMs). Conversion is achieved by heating which removes organic molecules stabilizing the NPs and allows for NP fusion. Heating of SS solutions leads to NMs of overall macroscopic dimensions; localized radiation using collimated electron beam is used to prepare metallized surface micropatterns. Depending on the composition of supraspherical precursors, nanoporous materials composed of up to three metals can be obtained. Strategies for controlling pore size and nanoscale surface roughness of these materials are discussed.}, author = {Klajn, Rafal and Gray, Timothy P. and Wesson, Paul J. and Myers, Benjamin D. and Dravid, Vinayak P. and Smoukov, Stoyan K. and Grzybowski, Bartosz A.}, issn = {1616-3028}, journal = {Advanced Functional Materials}, keywords = {Electrochemistry, Condensed Matter Physics, Biomaterials, Electronic, Optical and Magnetic Materials}, number = {18}, pages = {2763--2769}, publisher = {Wiley}, title = {{Bulk synthesis and surface patterning of nanoporous metals and alloys from supraspherical nanoparticle aggregates}}, doi = {10.1002/adfm.200800293}, volume = {18}, year = {2008}, } @article{1460, abstract = {We calculate the E-polynomials of certain twisted GL(n,ℂ)-character varieties Mn of Riemann surfaces by counting points over finite fields using the character table of the finite group of Lie-type GL(n, q) and a theorem proved in the appendix by N. Katz. We deduce from this calculation several geometric results, for example, the value of the topological Euler characteristic of the associated PGL(n,ℂ)-character variety. The calculation also leads to several conjectures about the cohomology of Mn: an explicit conjecture for its mixed Hodge polynomial; a conjectured curious hard Lefschetz theorem and a conjecture relating the pure part to absolutely indecomposable representations of a certain quiver. We prove these conjectures for n=2.}, author = {Tamas Hausel and Rodríguez Villegas, Fernando}, journal = {Inventiones Mathematicae}, number = {3}, pages = {555 -- 624}, publisher = {Springer}, title = {{Mixed Hodge polynomials of character varieties: With an appendix by Nicholas M. Katz}}, doi = {10.1007/s00222-008-0142-x}, volume = {174}, year = {2008}, } @article{1717, abstract = {Two key processes are in the basis of morphogenesis: the spatial allocation of cell types in fields of naïve cells and the regulation of growth. Both are controlled by morphogens, which activate target genes in the growing tissue in a concentration-dependent manner. Thus the morphogen model is an intrinsically quantitative concept. However, quantitative studies were performed only in recent years on two morphogens: Bicoid and Decapentaplegic. This review covers quantitative aspects of the formation and precision of the Decapentaplegic morphogen gradient. The morphogen gradient concept is transitioning from a soft definition to a precise idea of what the gradient could really do.}, author = {Anna Kicheva and González-Gaitán, Marcos A}, journal = {Current Opinion in Cell Biology}, number = {2}, pages = {137 -- 143}, publisher = {Elsevier}, title = {{The Decapentaplegic morphogen gradient a precise definition}}, doi = {10.1016/j.ceb.2008.01.008}, volume = {20}, year = {2008}, } @article{1719, abstract = {We study the mechanics of tissue growth via cell division and cell death (apoptosis). The rearrangements of cells can on large scales and times be captured by a continuum theory which describes the tissue as an effective viscous material with active stresses generated by cell division. We study the effects of anisotropies of cell division on cell rearrangements and show that average cellular trajectories exhibit anisotropic scaling behaviors. If cell division and apoptosis balance, there is no net growth, but for anisotropic cell division the tissue undergoes spontaneous shear deformations. Our description is relevant for the study of developing tissues such as the imaginal disks of the fruit fly Drosophila melanogaster, which grow anisotropically.}, author = {Bittig, Thomas and Wartlick, Ortrud and Anna Kicheva and González-Gaitárr, Marcos and Julicher, Frank}, journal = {New Journal of Physics}, publisher = {IOP Publishing Ltd.}, title = {{Dynamics of anisotropic tissue growth}}, doi = {10.1088/1367-2630/10/6/063001}, volume = {10}, year = {2008}, } @article{1967, abstract = {Complex I of respiratory chains transfers electrons from NADH to ubiquinone, coupled to the translocation of protons across the membrane. Two alternative coupling mechanisms are being discussed, redox-driven or conformation-driven. Using "zero-length" cross-linking reagent and isolated hydrophilic domains of complex I from Escherichia coli and Thermus thermophilus, we show that the pattern of cross-links between subunits changes significantly in the presence of NADH. Similar observations were made previously with intact purified E. coli and bovine complex I. This indicates that, upon reduction with NADH, similar conformational changes are likely to occur in the intact enzyme and in the isolated hydrophilic domain (which can be used for crystallographic studies). Within intact E. coli complex I, the cross-link between the hydrophobic subunits NuoA and NuoJ was abolished in the presence of NADH, indicating that conformational changes extend into the membrane domain, possibly as part of a coupling mechanism. Unexpectedly, in the absence of any chemical cross-linker, incubation of complex I with NADH resulted in covalent cross-links between subunits Nqo4 (NuoCD) and Nqo6 (NuoB), as well as between Nqo6 and Nqo9. Their formation depends on the presence of oxygen and so is likely a result of oxidative damage via reactive oxygen species (ROS) induced cross-linking. In addition, ROS- and metal ion-dependent proteolysis of these subunits (as well as Nqo3) is observed. Fe-S cluster N2 is coordinated between subunits Nqo4 and Nqo6 and could be involved in these processes. Our observations suggest that oxidative damage to complex I in vivo may include not only side-chain modifications but also protein cross-linking and degradation.}, author = {Berrisford, John M and Thompson, Christopher J and Leonid Sazanov}, journal = {Biochemistry}, number = {39}, pages = {10262 -- 10270}, publisher = {ACS}, title = {{Chemical and NADH-induced, ROS-dependent, cross-linking between sublimits of complex I from Escherichia coli and Thermus thermophilus}}, doi = {10.1021/bi801160u}, volume = {47}, year = {2008}, } @article{1968, abstract = { Complex I (NADH:ubiquinone oxidoreductase) is the largest protein complex of bacterial and mitochondrial respiratory chains. The first three-dimensional structure of bacterial complex I in vitrified ice was determined by electron cryo-microscopy and single particle analysis. The structure of the Escherichia coli enzyme incubated with either NAD+ (as a reference) or NADH was calculated to 35 and 39 Å resolution, respectively. The X-ray structure of the peripheral arm of Thermus thermophilus complex I was docked into the reference EM structure. The model obtained indicates that Fe-S cluster N2 is close to the membrane domain interface, allowing for effective electron transfer to membrane-embedded quinone. At the current resolution, the structures in the presence of NAD+ or NADH are similar. Additionally, side-view class averages were calculated for the negatively stained bovine enzyme. The structures of bovine complex I in the presence of either NAD+ or NADH also appeared to be similar. These observations indicate that conformational changes upon reduction with NADH, suggested to occur by a range of studies, are smaller than had been thought previously. The model of the entire bacterial complex I could be built from the crystal structures of subcomplexes using the EM envelope described here.}, author = {Morgan, David J and Leonid Sazanov}, journal = {Biochimica et Biophysica Acta - Bioenergetics}, number = {7-8}, pages = {711 -- 718}, publisher = {Elsevier}, title = {{Three-dimensional structure of respiratory complex I from Escherichia coli in ice in the presence of nucleotides}}, doi = {10.1016/j.bbabio.2008.03.023}, volume = {1777}, year = {2008}, } @inproceedings{4366, abstract = {Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential.}, author = {Podelski, Andreas and Rybalchenko, Andrey and Wies, Thomas}, booktitle = {Proceedings of the 30th international conference of computer aided verifacation}, isbn = {9783540705437}, location = {Princeton, NJ, United Stated}, pages = {314 -- 327}, publisher = {Springer Nature}, title = {{Heap Assumptions on Demand}}, doi = {10.1007/978-3-540-70545-1_31}, volume = {5123}, year = {2008}, } @inbook{4371, abstract = {We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real-time logic MITL.}, author = {Maler, Oded and Nickovic, Dejan and Pnueli, Amir}, booktitle = {Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday}, isbn = {9783540781264}, pages = {475 -- 505}, publisher = {Springer}, title = {{Checking Temporal Properties of Discrete, Timed and Continuous Behaviors}}, doi = {10.1007/978-3-540-78127-1_26}, year = {2008}, } @inproceedings{4384, abstract = {Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom. Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.}, author = {Guerraoui, Rachid and Thomas Henzinger and Jobstmann, Barbara and Vasu Singh}, pages = {372 -- 382}, publisher = {ACM}, title = {{Model checking transactional memories}}, doi = {10.1145/1375581.1375626}, year = {2008}, } @inproceedings{4386, abstract = {We introduce the notion of permissiveness in transactional memories (TM). Intuitively, a TM is permissive if it never aborts a transaction when it need not. More specifically, a TM is permissive with respect to a safety property p if the TM accepts every history that satisfies p. Permissiveness, like safety and liveness, can be used as a metric to compare TMs. We illustrate that it is impractical to achieve permissiveness deterministically, and then show how randomization can be used to achieve permissiveness efficiently. We introduce Adaptive Validation STM (AVSTM), which is probabilistically permissive with respect to opacity; that is, every opaque history is accepted by AVSTM with positive probability. Moreover, AVSTM guarantees lock freedom. Owing to its permissiveness, AVSTM outperforms other STMs by up to 40% in read dominated workloads in high contention scenarios. But, in low contention scenarios, the book-keeping done by AVSTM to achieve permissiveness makes AVSTM, on average, 20-30% worse than existing STMs.}, author = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh}, pages = {305 -- 319}, publisher = {Springer}, title = {{Permissiveness in transactional memories}}, doi = {10.1007/978-3-540-87779-0_21}, volume = {5218}, year = {2008}, } @inproceedings{4387, abstract = {Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first deterministic specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a complete verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is nondeterministic and establishes correctness for all possible contention management schemes.}, author = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh}, pages = {21 -- 35}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Completeness and nondeterminism in model checking transactional memories}}, doi = {10.1007/978-3-540-85361-9_6}, volume = {5201}, year = {2008}, } @inproceedings{4397, author = {Beyer, Dirk and Damien Zufferey and Majumdar, Ritankar S}, pages = {304 -- 308}, publisher = {Springer}, title = {{CSIsat: Interpolation for LA+EUF}}, year = {2008}, } @inproceedings{4400, abstract = {This paper summarizes a security analysis of the DRE and optical scan voting systems manufactured by Election Systems and Software (ES&S), as used in Ohio (and many other jurisdictions inside and outside the US). We found numerous exploitable vulnerabilities in nearly every component of the ES&S system. These vulnerabilities enable attacks that could alter or forge precinct results, install corrupt firmware, and erase audit records. Our analysis focused on architectural issues in which the interactions between various software and hardware modules leads to systemic vulnerabilities that do not appear to be easily countered with election procedures or software updates. Despite a highly compressed schedule (ten weeks) during which we audited hundreds of thousands of lines of source code (much of which runs on custom hardware), we discovered numerous security flaws in the ES&S system that had escaped the notice of the certification authorities. We discuss our approach to the audit, which was part of Project EVEREST, commissioned by Ohio Secretary of State Jennifer Brunner.}, author = {Aviv, Adam and Cerny, Pavol and Clark, Sandy and Cronin, Eric and Shah, Gaurav and Sherr, Micah and Blaze, Matt}, booktitle = {17th USENIX Security Symposium}, location = {San Jose, CA, United States}, title = {{Security evaluation of ES&S voting machines and election management system}}, year = {2008}, } @phdthesis{4409, abstract = {Models of timed systems must incorporate not only the sequence of system events, but the timings of these events as well to capture the real-time aspects of physical systems. Timed automata are models of real-time systems in which states consist of discrete locations and values for real-time clocks. The presence of real-time clocks leads to an uncountable state space. This thesis studies verification problems on timed automata in a game theoretic framework. For untimed systems, two systems are close if every sequence of events of one system is also observable in the second system. For timed systems, the difference in timings of the two corresponding sequences is also of importance. We propose the notion of bisimulation distance which quantifies timing differences; if the bisimulation distance between two systems is epsilon, then (a) every sequence of events of one system has a corresponding matching sequence in the other, and (b) the timings of matching events in between the two corresponding traces do not differ by more than epsilon. We show that we can compute the bisimulation distance between two timed automata to within any desired degree of accuracy. We also show that the timed verification logic TCTL is robust with respect to our notion of quantitative bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula. Timed games are used for distinguishing between the actions of several agents, typically a controller and an environment. The controller must achieve its objective against all possible choices of the environment. The modeling of the passage of time leads to the presence of zeno executions, and corresponding unrealizable strategies of the controller which may achieve objectives by blocking time. We disallow such unreasonable strategies by restricting all agents to use only receptive strategies --strategies which while not being required to ensure time divergence by any agent, are such that no agent is responsible for blocking time. Time divergence is guaranteed when all players use receptive strategies. We show that timed automaton games with receptive strategies can be solved by a reduction to finite state turn based game graphs. We define the logic timed alternating-time temporal logic for verification of timed automaton games and show that the logic can be model checked in EXPTIME. We also show that the minimum time required by an agent to reach a desired location, and the maximum time an agent can stay safe within a set of locations, against all possible actions of its adversaries are both computable. We next study the memory requirements of winning strategies for timed automaton games. We prove that finite memory strategies suffice for safety objectives, and that winning strategies for reachability objectives may require infinite memory in general. We introduce randomized strategies in which an agent can propose a probabilistic distribution of moves and show that finite memory randomized strategies suffice for all omega-regular objectives. We also show that while randomization helps in simplifying winning strategies, and thus allows the construction of simpler controllers, it does not help a player in winning at more states, and thus does not allow the construction of more powerful controllers. Finally we study robust winning strategies in timed games. In a physical system, a controller may propose an action together with a time delay, but the action cannot be assumed to be executed at the exact proposed time delay. We present robust strategies which incorporate such jitters and show that the set of states from which an agent can win robustly is computable.}, author = {Prabhu, Vinayak}, pages = {1 -- 137}, publisher = {University of California, Berkeley}, title = {{Games for the verification of timed systems}}, year = {2008}, }