@article{4474, abstract = {The simulation preorder for labeled transition systems is defined locally, and operationally, as a game that relates states with their immediate successor states. Simulation enjoys many appealing properties. First, simulation has a denotational characterization: system S simulates system I iff every computation tree embedded in the unrolling of I can be embedded also in the unrolling of S. Second, simulation has a logical characterization: S simulates I iff every universal branching-time formula satisfied by S is satisfied also by I. It follows that simulation is a suitable notion of implementation, and it is the coarsest abstraction of a system that preserves universal branching-time properties. Third, based on its local definition, simulation between finite-state systems can be checked in polynomial time. Finally, simulation implies trace containment, which cannot be defined locally and requires polynomial space for verification. Hence simulation is widely used both in manual and in automatic verification. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We propose a new view of fair simulation by extending the local definition of simulation to account for fairness: system View the MathML sourcefairly simulates system View the MathML source iff in the simulation game, there is a strategy that matches with each fair computation of View the MathML source a fair computation of View the MathML source. Our definition enjoys a denotational characterization and has a logical characterization: View the MathML source fairly simulates View the MathML source iff every fair computation tree (whose infinite paths are fair) embedded in the unrolling of View the MathML source can be embedded also in the unrolling of View the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by View the MathML source is satisfied also by View the MathML source (∀AFMC is the universal fragment of the alternation-free μ-calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace containment and is therefore useful as an efficiently computable local criterion for proving linear-time abstraction hierarchies of fair systems.}, author = {Henzinger, Thomas A and Kupferman, Orna and Rajamani, Sriram}, issn = {0890-5401}, journal = {Information and Computation}, number = {1}, pages = {64 -- 81}, publisher = {Elsevier}, title = {{Fair simulation}}, doi = {10.1006/inco.2001.3085}, volume = {173}, year = {2002}, } @inproceedings{4476, abstract = {One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.}, author = {Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Ritankar and Sutre, Grégoire}, booktitle = {Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, isbn = {9781581134506}, location = {Portland, OR, USA}, pages = {58 -- 70}, publisher = {ACM}, title = {{Lazy abstraction}}, doi = {10.1145/503272.503279}, year = {2002}, } @inproceedings{4562, abstract = {We present interface models that describe both the input assumptions of a component, and its output behavior. By enabling us to check that the input assumptions of a component are met in a design, interface models provide a compatibility check for component-based design. When refining a design into an implementation, interface models require that the output behavior of a component satisfies the design specification only when the input assumptions of the specification are satisfied, yielding greater flexibility in the choice of implementations. Technically, our interface models are games between two players, Input and Output; the duality of the players accounts for the dual roles of inputs and outputs in composition and refinement. We present two interface models in detail, one for a simple synchronous form of interaction between components typical in hardware, and the other for more complex synchronous interactions on bidirectional connections. As an example, we specify the interface of a bidirectional bus, with the input assumption that at any time at most one component has write access to the bus. For these interface models, we present algorithms for compatibility and refinement checking, and we describe efficient symbolic implementations.}, author = {Chakrabarti, Arindam and De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 14th International Conference on Computer Aided Verification}, isbn = {9783540439974}, location = {Copenhagen, Denmark}, pages = {414 -- 427}, publisher = {Springer}, title = {{Synchronous and bidirectional component interfaces}}, doi = {10.1007/3-540-45657-0_34}, volume = {2404}, year = {2002}, } @inproceedings{4563, abstract = {We present a formal methodology and tool for uncovering errors in the interaction of software modules. Our methodology consists of a suite of languages for defining software interfaces, and algorithms for checking interface compatibility. We focus on interfaces that explain the method-call dependencies between software modules. Such an interface makes assumptions about the environment in the form of call and availability constraints. A call constraint restricts the accessibility of local methods to certain external methods. An availability constraint restricts the accessibility of local methods to certain states of the module. For example, the interface for a file server with local methods open and read may assert that a file cannot be read without having been opened. Checking interface compatibility requires the solution of games, and in the presence of availability constraints, of pushdown games. Based on this methodology, we have implemented a tool that has uncovered incompatibilities in TinyOS, a small operating system for sensor nodes in adhoc networks.}, author = {Chakrabarti, Arindam and De Alfaro, Luca and Henzinger, Thomas A and Jurdziński, Marcin and Mang, Freddy}, booktitle = {Proceedings of the 14th International Conference on Computer Aided Verification}, isbn = { 9783540439974}, location = {Copenhagen, Denmark}, pages = {428 -- 441}, publisher = {Springer}, title = {{Interface compatibility checking for software modules}}, doi = {10.1007/3-540-45657-0_35}, volume = {2404}, year = {2002}, } @inproceedings{4565, abstract = {In the literature, we find several formulations of the control problem for timed and hybrid systems. We argue that formulations where a controller can cause an action at any point in dense (rational or real) time are problematic, by presenting an example where the controller must act faster and faster, yet causes no Zeno effects (say, the control actions are at times 0, 1/2, 1, 1 1/4, 2, 2 1/8, 3, 3 1/16 ,...). Such a controller is, of course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well- understood if the time unit, or “sampling rate” of the controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We prove that this problem is undecidable even in the special case of timed automata.}, author = {Cassez, Franck and Henzinger, Thomas A and Raskin, Jean}, booktitle = {Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control}, isbn = {9783540433217}, location = {Stanford, CA, USA}, pages = {134 -- 148}, publisher = {Springer}, title = {{A comparison of control problems for timed and hybrid systems}}, doi = {10.1007/3-540-45873-5_13}, volume = {2289}, year = {2002}, } @article{4595, abstract = {Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures. Every state transition of a concurrent game structure results from a choice of moves, one for each player. The players represent individual components and the environment of an open system. Concurrent game structures can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. Over structures without fairness constraints, the model-checking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic model-checking algorithm for CTL extends with few modifications to ATL. Over structures with weak-fairness constraints, ATL model checking requires the solution of 1-pair Rabin games, and can be done in polynomial time. Over structures with strong-fairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. In the case of ATL*, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time.}, author = {Alur, Rajeev and Henzinger, Thomas A and Kupferman, Orna}, issn = {0004-5411}, journal = {Journal of the ACM}, number = {5}, pages = {672 -- 713}, publisher = {ACM}, title = {{Alternating-time temporal logic}}, doi = {10.1145/585265.585270}, volume = {49}, year = {2002}, } @article{11755, abstract = {Hyperlink analysis algorithms significantly improve the relevance of the search results on the Web, so much so that all major Web search engines claim to use some type of hyperlink analysis. However, the search engines do not disclose details about the type of hyperlink analysis they perform, mostly to avoid manipulation of search results by Web-positioning companies. The article discusses how hyperlink analysis can be applied to ranking algorithms, and surveys other ways Web search engines can use this analysis.}, author = {Henzinger, Monika H}, issn = {1941-0131}, journal = {IEEE Internet Computing}, number = {1}, pages = {45--50}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Hyperlink analysis for the Web}}, doi = {10.1109/4236.895141}, volume = {5}, year = {2001}, } @article{11892, abstract = {We present the first fully dynamic algorithm for maintaining a minimum spanning forest in time 𝑜(𝑛√) per operation. To be precise, the algorithm uses O(n1/3 log n) amortized time per update operation. The algorithm is fairly simple and deterministic. An immediate consequence is the first fully dynamic deterministic algorithm for maintaining connectivity and bipartiteness in amortized time O(n1/3 log n) per update, with O(1) worst case time per query.}, author = {Henzinger, Monika H and King, Valerie}, issn = {1095-7111}, journal = {SIAM Journal on Computing}, number = {2}, pages = {364--374}, publisher = {Society for Industrial & Applied Mathematics}, title = {{Maintaining minimum spanning forests in dynamic graphs}}, doi = {10.1137/s0097539797327209}, volume = {31}, year = {2001}, } @inproceedings{11914, abstract = {Previous studies of the Web graph structure have focused on the graph structure at the level of individual pages. In actuality the Web is a hierarchically nested graph, with domains, hosts and Web sites introducing intermediate levels of affiliation and administrative control. To better understand the growth of the Web we need to understand its macro-structure, in terms of the linkage between Web sites. We approximate this by studying the graph of the linkage between hosts on the Web. This was done based on snapshots of the Web taken by Google in Oct 1999, Aug 2000 and Jun 2001. The connectivity between hosts is represented by a directed graph, with hosts as nodes and weighted edges representing the count of hyperlinks between pages on the corresponding hosts. We demonstrate how such a "hostgraph" can be used to study connectivity properties of hosts and domains over time, and discuss a modified "copy model" to explain observed link weight distributions as a function of subgraph size. We discuss changes in the Web over time in the size and connectivity of Web sites and country domains. We also describe a data mining application of the hostgraph: a related host finding algorithm which achieves a precision of 0.65 at rank 3.}, author = {Bharat, K. and Chang, Bay-Wei and Henzinger, Monika H and Ruhl, M.}, booktitle = {1st IEEE International Conference on Data Mining}, isbn = {0-7695-1119-8}, issn = {15504786}, location = {San Jose, CA, United States}, pages = {51--58}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Who links to whom: Mining linkage between Web sites}}, doi = {10.1109/ICDM.2001.989500}, year = {2001}, } @inbook{2709, author = {Erdös, László}, booktitle = {13th International Congress of Mathematical Physics}, isbn = {9781571460851}, pages = {273 -- 281}, publisher = { International Press of Boston}, title = {{Long time dynamics of an electron in a weakly coupled phonon field}}, year = {2001}, } @article{2734, abstract = {In this paper we describe an intrinsically geometric way of producing magnetic fields on S3 and R3 for which the corresponding Dirac operators have a non-trivial kernel. In many cases we are able to compute the dimension of the kernel. In particular we can give examples where the kernel has any given dimension. This generalizes the examples of Loss and Yau [1].}, author = {Erdös, László and Solovej, Jan}, issn = {0129-055X}, journal = {Reviews in Mathematical Physics}, number = {10}, pages = {1247 -- 1280}, publisher = {World Scientific Publishing}, title = {{The kernel of Dirac operators on S3 and R3}}, doi = {10.1142/S0129055X01000983}, volume = {13}, year = {2001}, } @article{2735, abstract = {We establish the exact low-energy asymptotics of the integrated density of states (Lifschitz tail) in a homogeneous magnetic field and Poissonian impurities with a repulsive single-site potential of Gaussian decay. It has been known that the Gaussian potential tail discriminates between the so-called “classical” and “quantum” regimes, and precise asymptotics are known in these cases. For the borderline case, the coexistence of the classical and quantum regimes was conjectured. Here we settle this last remaining open case to complete the full picture of the magnetic Lifschitz tails.}, author = {Erdös, László}, issn = {0044-3719}, journal = {Probability Theory and Related Fields}, number = {2}, pages = {219 -- 236}, publisher = {Springer}, title = {{Lifschitz tail in a magnetic field: Coexistence of classical and quantum behavior in the borderline case}}, doi = {10.1007/PL00008803}, volume = {121}, year = {2001}, } @article{2736, abstract = {We consider the time evolution of N bosonic particles interacting via a mean field Coulomb potential. Suppose the initial state is a product wavefunction. We show that at any finite time the correlation functions factorize in the limit N → ∞. Furthermore, the limiting one particle density matrix satisfies the nonlinear Hartree equation. The key ingredients are the uniqueness of the BBGKY hierarchy for the correlation functions and a new apriori estimate for the many-body Schrödinger equations.}, author = {Erdös, László and Yau, Horng}, issn = {1095-0761}, journal = {Advances in Theoretical and Mathematical Physics}, number = {6}, pages = {1169 -- 1205}, publisher = {International Press}, title = {{Derivation of the nonlinear Schrödinger equation from a many body Coulomb system}}, doi = {10.48550/arXiv.math-ph/0111042}, volume = {5}, year = {2001}, } @article{2981, abstract = {Plants contain a novel unique subfamily of Rho GTPases, vital components of cellular signalling networks. Here we report a general role for some members of this family in polarized plant growth processes. We show that Arabidopsis AtRop4 and AtRop6 encode functional GTPases with similar intrinsic GTP hydrolysis rates. We localized AtRop proteins in root meristem cells to the cross-wall and cell plate membranes. Polar localization of AtRops in trichoblasts specifies the growth sites for emerging root hairs. These sites were visible before budding and elongation of the Arabidopsis root hair when AtRops accumulated at their tips. Expression of constitutively active AtRop4 and AtRop6 mutant proteins in root hairs of transgenic Arabidopsis plants abolished polarized growth and delocalized the tip-focused Ca2+ gradient. Polar localization of AtRops was inhibited by brefeldin A, but not by other drugs such as latrunculin B, cytochalasin D or caffeine. Our results demonstrate a general function of AtRop GTPases in tip growth and in polar diffuse growth.}, author = {Molendijk, Arthur and Bischoff, Friedrich and Rajendrakumar, Chadalavada and Friml, Jirí and Braun, Markus and Gilroy, Simon and Palme, Klaus}, issn = {0261-4189}, journal = {EMBO Journal}, number = {11}, pages = {2779 -- 2788}, publisher = {Wiley-Blackwell}, title = {{Arabidopsis thaliana Rop GTPases are localized to tips of root hairs and control polar growth}}, doi = {10.1093/emboj/20.11.2779}, volume = {20}, year = {2001}, } @article{2982, abstract = {Polar auxin transport is crucial for the regulation of auxin action and required for some light-regulated responses during plant development. We have found that two mutants of Arabidopsis - doc1, which displays altered expression of light-regulated genes, and tir3, known for its reduced auxin transport - have similar defects and define mutations in a single gene that we have renamed BIG. BIG is very similar to the Drosophila gene Calossin/Pushover, a member of a gene family also present in Caenorhabditis elegans and human genomes. The protein encoded by BIG is extraordinary in size, 560 kD, and contains several putative Zn-finger domains. Expression-profiling experiments indicate that altered expression of multiple light-regulated genes in doc1 mutants can be suppressed by elevated levels of auxin caused by overexpression of an auxin biosynthetic gene, suggesting that normal auxin distribution is required to maintain low-level expression of these genes in the dark. Double mutants of tir3 with the auxin mutants pin1, pid, and axr1 display severe defects in auxin-dependent growth of the inflorescence. Chemical inhibitors of auxin transport change the intracellular localization of the auxin efflux carrier PIN1 in doc1/tir3 mutants, supporting the idea that BIG is required for normal auxin efflux.}, author = {Gil, Pedro and Dewey, Elizabeth and Friml, Jirí and Zhao, Yunde and Snowden, Kimberley and Putterill, Jo and Palme, Klaus and Estelle, Mark and Chory, Joanne}, issn = {0890-9369}, journal = {Genes and Development}, number = {15}, pages = {1985 -- 1997}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{BIG: A calossin-like protein required for polar auxin transport in Arabidopsis}}, doi = {10.1101/gad.905201}, volume = {15}, year = {2001}, } @article{2983, abstract = {Polar transport of the phytohormone auxin mediates various processes in plant growth and development, such as apical dominance, tropisms, vascular patterning and axis formation. This view is based largely on the effects of polar auxin transport inhibitors. These compounds disrupt auxin efflux from the cell but their mode of action is unknown. It is thought that polar auxin flux is caused by the asymmetric distribution of efflux carriers acting at the plasma membrane. The polar localization of efflux carrier candidate PIN1 supports this model. Here we show that the seemingly static localization of PIN1 results from rapid actin-dependent cycling between the plasma membrane and endosomal compartments. Auxin transport inhibitors block PIN1 cycling and inhibit trafficking of membrane proteins that are unrelated to auxin transport. Our data suggest that PIN1 cycling is of central importance for auxin transport and that auxin transport inhibitors affect efflux by generally interfering with membrane-trafficking processes. In support of our conclusion, the vesicle-trafficking inhibitor brefeldin A mimics physiological effects of auxin transport inhibitors.}, author = {Geldner, Niko and Friml, Jirí and Stierhof, York and Jürgens, Gerd and Palme, Klaus}, issn = {0028-0836}, journal = {Nature}, number = {6854}, pages = {425 -- 428}, publisher = {Nature Publishing Group}, title = {{Auxin transport inhibitors block PIN1 cycling and vesicle trafficking}}, doi = {10.1038/35096571}, volume = {413}, year = {2001}, } @article{2984, abstract = {Auxins represent an important class of plant hormone that regulate plant development. Plants use specialized carrier proteins to transport the auxin indole-3-acetic acid (IAA) to target tissues. To date, efflux carrier-mediated polar auxin transport has been assumed to represent the sole mode of long distance IAA movement. Localization of the auxin permease AUX1 in the Arabidopsis root apex has revealed a novel phloem-based IAA transport pathway. AUX1, asymmetrically localized to the plasma membrane of root protophloem cells, is proposed to promote the acropetal, post-phloem movement of auxin to the root apex. MS analysis shows that IAA accumulation in aux1 mutant root apices is impaired, consistent with an AUX1 phloem unloading function. AUX1 localization to columella and lateral root cap tissues of the Arabidopsis root apex reveals that the auxin permease regulates a second IAA transport pathway. Expression studies using an auxin-regulated reporter suggest that AUX1 is necessary for root gravitropism by facilitating basipetal auxin transport to distal elongation zone tissues.}, author = {Swarup, Ranjan and Friml, Jirí and Marchant, Alan and Ljung, Karin and Sandberg, Göran and Palme, Klaus and Bennett, Malcolm}, issn = {Genes and Development}, journal = {Genes and Development}, number = {20}, pages = {2648 -- 2653}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{Localization of the auxin permease AUX1 suggests two functionally distinct hormone transport pathways operate in the Arabidopsis root apex}}, doi = {10.1101/gad.210501}, volume = {15}, year = {2001}, } @article{2985, abstract = {The elimination voltammetry with linear scan (EVLS) was used to study adenine and cytosine reduction signals at the mercury electrode. In comparison with the linear scan voltammetry (which provides only one unresolved peak), two elimination functions provide good resolution of individual peaks and significant increase of sensitivity. The first elimination function eliminates the kinetic current (Ik) and conserves the diffusion current (Id). The second elimination function eliminates kinetic and charging currents (Ik and Ic) simultaneously and conserves the diffusion current (Id). Both functions give two well-resolved peaks of adenine and cytosine in a wide concentration range, while the linear sweep voltammetry gives badly resolved peaks due to hydrogen evolution. The best resolution of peaks is observed in acetate buffer at pH 3.8 and the detection limit for both substances is 500 nM. The concentration dependence of EVLS peak heights for one substance at the constant concentration of the other substance is linear. The peak potentials differ in these elimination functions. The difference in EVLS peak potentials gives the possibility to evaluate αna. Elimination voltammetry with linear scan contributes to the resolution of cathodic signals of purine and pyrimidine bases at very negative potentials near supporting electrolyte discharge. Copyright © 2001 Elsevier Science B.V.}, author = {Trnková, Libuše and Friml, Jirí and Dračka, Oldřich}, isbn = {1567-5394}, journal = {Bioelectrochemistry}, number = {2}, pages = {131 -- 136}, publisher = {Elsevier}, title = {{Elimination voltammetry of adenine and cytosine mixtures}}, doi = {10.1016/S1567-5394(01)00119-0}, volume = {54}, year = {2001}, } @inproceedings{3169, abstract = {Several new algorithms for visual correspondence based on graph cuts [7, 14, 17] have recently been developed. While these methods give very strong results in practice, they do not handle occlusions properly. Specifically, they treat the two input images asymmetrically, and they do not ensure that a pixel corresponds to at most one pixel in the other image. In this paper, we present a new method which properly addresses occlusions, while preserving the advantages of graph cut algorithms. We give experimental results for stereo as well as motion, which demonstrate that our method performs well both at detecting occlusions and computing disparities.}, author = {Kolmogorov, Vladimir and Zabih, Ramin}, booktitle = {Proceedings of the 8th IEEE International Conference on Computer Vision}, isbn = {0769511430}, location = {Vancouver, Canada}, pages = {508 -- 515}, publisher = {IEEE}, title = {{Computing visual correspondence with occlusions using graph cuts}}, doi = {10.1109/ICCV.2001.937668}, volume = {2}, year = {2001}, } @article{1452, abstract = {In this Note we present pairs of hyperkähler orbifolds which satisfy two different versions of mirror symmetry. On the one hand, we show that their Hodge numbers (or more precisely, stringy E-polynomials) are equal. On the other hand, we show that they satisfy the prescription of Strominger, Yau, and Zaslow (which in the present case goes back to Bershadsky, Johansen, Sadov and Vafa): that a Calabi-Yau and its mirror should fiber over the same real manifold, with special Lagrangian fibers which are tori dual to each other. Our examples arise as moduli spaces of local systems on a curve with structure group SL(n); the mirror is the corresponding space with structure group PGL(n). The special Lagrangian tori come from an algebraically completely integrable Hamiltonian system: the Hitchin system.}, author = {Hausel, Tamas and Thaddeus, Michael}, issn = {0764-4442}, journal = {Comptes Rendus de l'Academie des Sciences - Series I: Mathematics}, number = {4}, pages = {313 -- 318}, publisher = {Elsevier}, title = {{Examples of mirror partners arising from integrable systems}}, doi = {10.1016/S0764-4442(01)02057-2}, volume = {333}, year = {2001}, }