[{"title":"A reusable and platform-independent framework for distributed control systems","day":"06","type":"conference","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","month":"08","publication":"Proceedings of the 20th Digital Avionics Systems Conference","abstract":[{"text":"This paper presents a concept for integrating the embedded programming methodology Giotto and the object-oriented AOCS Framework to create an environment for the rapid development of distributed software for safety-critical embedded control systems with hard real-time requirements of the kind typically found in aerospace applications.","lang":"eng"}],"scopus_import":"1","doi":"10.1109/DASC.2001.964169","conference":{"start_date":"2001-10-14","name":"DASC: Digital Avionics Systems Conference","location":"Daytona Beach, FL, USA","end_date":"2001-10-18"},"citation":{"ista":"Brown T, Pasetti A, Pree W, Henzinger TA, Kirsch C. 2001. A reusable and platform-independent framework for distributed control systems. Proceedings of the 20th Digital Avionics Systems Conference. DASC: Digital Avionics Systems Conference, 1–11.","ama":"Brown T, Pasetti A, Pree W, Henzinger TA, Kirsch C. A reusable and platform-independent framework for distributed control systems. In: Proceedings of the 20th Digital Avionics Systems Conference. IEEE; 2001:1-11. doi:10.1109/DASC.2001.964169","chicago":"Brown, Timothy, Alessandro Pasetti, Wolfgang Pree, Thomas A Henzinger, and Christoph Kirsch. “A Reusable and Platform-Independent Framework for Distributed Control Systems.” In Proceedings of the 20th Digital Avionics Systems Conference, 1–11. IEEE, 2001. https://doi.org/10.1109/DASC.2001.964169.","mla":"Brown, Timothy, et al. “A Reusable and Platform-Independent Framework for Distributed Control Systems.” Proceedings of the 20th Digital Avionics Systems Conference, IEEE, 2001, pp. 1–11, doi:10.1109/DASC.2001.964169.","apa":"Brown, T., Pasetti, A., Pree, W., Henzinger, T. A., & Kirsch, C. (2001). A reusable and platform-independent framework for distributed control systems. In Proceedings of the 20th Digital Avionics Systems Conference (pp. 1–11). Daytona Beach, FL, USA: IEEE. https://doi.org/10.1109/DASC.2001.964169","short":"T. Brown, A. Pasetti, W. Pree, T.A. Henzinger, C. Kirsch, in:, Proceedings of the 20th Digital Avionics Systems Conference, IEEE, 2001, pp. 1–11.","ieee":"T. Brown, A. Pasetti, W. Pree, T. A. Henzinger, and C. Kirsch, “A reusable and platform-independent framework for distributed control systems,” in Proceedings of the 20th Digital Avionics Systems Conference, Daytona Beach, FL, USA, 2001, pp. 1–11."},"acknowledgement":"This research was supported in part by DARPA under grants F336 15-C-98-36 14, F33615-00-(2-1693, and F33615-00-C-1703, and by MARC0 under grant 98-DT-660. ","publist_id":"143","oa_version":"None","extern":"1","status":"public","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:30Z","_id":"4564","article_processing_charge":"No","page":"1 - 11","quality_controlled":"1","publisher":"IEEE","author":[{"full_name":"Brown, Timothy","first_name":"Timothy","last_name":"Brown"},{"full_name":"Pasetti, Alessandro","last_name":"Pasetti","first_name":"Alessandro"},{"full_name":"Pree, Wolfgang","first_name":"Wolfgang","last_name":"Pree"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph"}],"date_published":"2001-08-06T00:00:00Z","publication_status":"published","publication_identifier":{"isbn":["0780370341"]},"year":"2001","date_updated":"2023-05-09T12:23:16Z"},{"language":[{"iso":"eng"}],"article_processing_charge":"No","publist_id":"108","status":"public","extern":"1","oa_version":"None","date_published":"2001-03-01T00:00:00Z","publication_identifier":{"issn":["0925-9856"]},"year":"2001","publication_status":"published","page":"97 - 116","publisher":"Springer","quality_controlled":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"journal_article","title":"Partial-order reduction in symbolic state-space exploration","doi":"10.1023/A:1008767206905","publication":"Formal Methods in System Design","abstract":[{"text":"State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.","lang":"eng"}],"_id":"4599","date_created":"2018-12-11T12:09:41Z","issue":"2","volume":18,"acknowledgement":"Gerard Holzmann provided us with information on SPIN. Ken McMillan and Doron Peled contributed through discussions. The VIS group at UC Berkeley and Rajeev Ranjan in particular helped with the experiments.","date_updated":"2023-05-08T12:22:38Z","article_type":"original","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"last_name":"Brayton","first_name":"Robert","full_name":"Brayton, Robert"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"},{"first_name":"Sriram","last_name":"Rajamani","full_name":"Rajamani, Sriram"}],"month":"03","day":"01","intvolume":" 18","scopus_import":"1","citation":{"ieee":"R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order reduction in symbolic state-space exploration,” Formal Methods in System Design, vol. 18, no. 2. Springer, pp. 97–116, 2001.","apa":"Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., & Rajamani, S. (2001). Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design. Springer. https://doi.org/10.1023/A:1008767206905","short":"R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, Formal Methods in System Design 18 (2001) 97–116.","mla":"Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.” Formal Methods in System Design, vol. 18, no. 2, Springer, 2001, pp. 97–116, doi:10.1023/A:1008767206905.","ista":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 2001. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design. 18(2), 97–116.","ama":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design. 2001;18(2):97-116. doi:10.1023/A:1008767206905","chicago":"Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” Formal Methods in System Design. Springer, 2001. https://doi.org/10.1023/A:1008767206905."}},{"citation":{"short":"R. Alur, L. De Alfaro, R. Grosu, T.A. Henzinger, M. Kang, C. Kirsch, R. Majumdar, F. Mang, B. Wang, in:, Proceedings of the 23rd International Conference on Software Engineering, IEEE, 2001, pp. 835–836.","apa":"Alur, R., De Alfaro, L., Grosu, R., Henzinger, T. A., Kang, M., Kirsch, C., … Wang, B. (2001). jMocha: A model-checking tool that exploits design structure. In Proceedings of the 23rd International Conference on Software Engineering (pp. 835–836). IEEE. https://doi.org/10.1109/ICSE.2001.919196","mla":"Alur, Rajeev, et al. “JMocha: A Model-Checking Tool That Exploits Design Structure.” Proceedings of the 23rd International Conference on Software Engineering, IEEE, 2001, pp. 835–36, doi:10.1109/ICSE.2001.919196.","ista":"Alur R, De Alfaro L, Grosu R, Henzinger TA, Kang M, Kirsch C, Majumdar R, Mang F, Wang B. 2001. jMocha: A model-checking tool that exploits design structure. Proceedings of the 23rd International Conference on Software Engineering. ICSE: Software Engineering, 835–836.","chicago":"Alur, Rajeev, Luca De Alfaro, Radu Grosu, Thomas A Henzinger, Myong Kang, Christoph Kirsch, Ritankar Majumdar, Freddy Mang, and Bow Wang. “JMocha: A Model-Checking Tool That Exploits Design Structure.” In Proceedings of the 23rd International Conference on Software Engineering, 835–36. IEEE, 2001. https://doi.org/10.1109/ICSE.2001.919196.","ama":"Alur R, De Alfaro L, Grosu R, et al. jMocha: A model-checking tool that exploits design structure. In: Proceedings of the 23rd International Conference on Software Engineering. IEEE; 2001:835-836. doi:10.1109/ICSE.2001.919196","ieee":"R. Alur et al., “jMocha: A model-checking tool that exploits design structure,” in Proceedings of the 23rd International Conference on Software Engineering, 2001, pp. 835–836."},"doi":"10.1109/ICSE.2001.919196","conference":{"name":"ICSE: Software Engineering"},"abstract":[{"text":"Model checking is a practical tool for automated debugging of embedded software. In model checking, a high-level description of a system is compared against a logical correctness requirement to discover inconsistencies. Since model checking is based on exhaustive state-space exploration and the size of the state space of a design grows exponentially with the size of the description, scalability remains a challenge. We have thus developed techniques for exploiting modular design structure during model checking, and the model checker jMocha (Java MOdel-CHecking Algorithm) is based on this theme. Instead of manipulating unstructured state-transition graphs, it supports the hierarchical modeling framework of reactive modules. jMocha is a growing interactive software environment for specification, simulation and verification, and is intended as a vehicle for the development of new verification algorithms and approaches. It is written in Java and uses native C-code BDD libraries from VIS. jMocha offers: (1) a GUI that looks familiar to Windows/Java users; (2) a simulator that displays traces in a message sequence chart fashion; (3) requirements verification both by symbolic and enumerative model checking; (4) implementation verification by checking trace containment; (5) a proof manager that aids compositional and assume-guarantee reasoning; and (6) SLANG (Scripting LANGuage) for the rapid and structured development of new verification algorithms. jMocha is available publicly at ; it is a successor and extension of the original Mocha tool that was entirely written in C.","lang":"eng"}],"publication":"Proceedings of the 23rd International Conference on Software Engineering","month":"08","type":"conference","day":"07","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"jMocha: A model-checking tool that exploits design structure","date_updated":"2023-05-08T14:06:55Z","year":"2001","publication_identifier":{"isbn":["0769510507"]},"publication_status":"published","date_published":"2001-08-07T00:00:00Z","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"full_name":"De Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Kang, Myong","last_name":"Kang","first_name":"Myong"},{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"},{"first_name":"Freddy","last_name":"Mang","full_name":"Mang, Freddy"},{"last_name":"Wang","first_name":"Bow","full_name":"Wang, Bow"}],"publisher":"IEEE","quality_controlled":"1","page":"835 - 836","article_processing_charge":"No","_id":"4600","date_created":"2018-12-11T12:09:41Z","language":[{"iso":"eng"}],"extern":"1","status":"public","oa_version":"None","publist_id":"109","acknowledgement":"We thank Himyanshu Anand, Ben Horowitz, Franjo Ivancic, Michael McDougall, Marius Minea, Oliver Moeller. Shaz Qadeer, Sriram Rajamani, and Jean-Francois Raskin for their assistance in the development of JMOCHA. The MOCHA project is funded in part by the DARPA grant NAG2-1214, the NSF CAREER awards CCR95-01708 and CCR97-34115, the NSF grant CCR99-70925, the NSF ITR grant CCR0085949, the MARC0 grant 98-DT-660, and the SRC contracts 99-TJ-683.003 and 99-TJ-688. "},{"date_published":"2001-06-01T00:00:00Z","date_updated":"2023-05-08T12:01:02Z","publication_status":"published","year":"2001","publication_identifier":{"isbn":["9781581133905"]},"page":"109 - 120","publisher":"ACM","author":[{"full_name":"De Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"quality_controlled":"1","_id":"4622","date_created":"2018-12-11T12:09:48Z","language":[{"iso":"eng"}],"article_processing_charge":"No","publist_id":"83","acknowledgement":"We thank Edward A. Lee, Xiaojun Liu, Freddy Mang, and Yuhong Xiong for fruitful discussions. This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA MoBIES grant F33615-00-C-1703, the MARCO GSRC grant 98-DT-660, the NSF Theory grant CCR-9988172, and the NSF ITR grant CCR-0085949.","extern":"1","status":"public","oa_version":"None","conference":{"end_date":"2001-09-14","location":"Vienna, Austria","name":"FSE: Foundations of Software Engineering","start_date":"2001-09-10"},"doi":"10.1145/503209.503226","scopus_import":"1","citation":{"ieee":"L. De Alfaro and T. A. Henzinger, “Interface automata,” in Proceedings of the 8th European software engineering conference, Vienna, Austria, 2001, pp. 109–120.","apa":"De Alfaro, L., & Henzinger, T. A. (2001). Interface automata. In Proceedings of the 8th European software engineering conference (pp. 109–120). Vienna, Austria: ACM. https://doi.org/10.1145/503209.503226","short":"L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 8th European Software Engineering Conference, ACM, 2001, pp. 109–120.","mla":"De Alfaro, Luca, and Thomas A. Henzinger. “Interface Automata.” Proceedings of the 8th European Software Engineering Conference, ACM, 2001, pp. 109–20, doi:10.1145/503209.503226.","ama":"De Alfaro L, Henzinger TA. Interface automata. In: Proceedings of the 8th European Software Engineering Conference. ACM; 2001:109-120. doi:10.1145/503209.503226","ista":"De Alfaro L, Henzinger TA. 2001. Interface automata. Proceedings of the 8th European software engineering conference. FSE: Foundations of Software Engineering, 109–120.","chicago":"De Alfaro, Luca, and Thomas A Henzinger. “Interface Automata.” In Proceedings of the 8th European Software Engineering Conference, 109–20. ACM, 2001. https://doi.org/10.1145/503209.503226."},"publication":"Proceedings of the 8th European software engineering conference","abstract":[{"text":"Conventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input assumptions about the order in which the methods of a component are called, and output guarantees about the order in which the component calls external methods. The formalism supports automatic compatability checks between interface models, and thus constitutes a type system for component interaction. Unlike traditional uses of automata, our formalism is based on an optimistic approach to composition, and on an alternating approach to design refinement. According to the optimistic approach, two components are compatible if there is some environment that can make them work together. According to the alternating approach, one interface refines another if it has weaker input assumptions, and stronger output guarantees. We show that these notions have game-theoretic foundations that lead to efficient algorithms for checking compatibility and refinement.","lang":"eng"}],"month":"06","type":"conference","day":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Interface automata"},{"conference":{"end_date":"2001-10-10","start_date":"2001-10-08","name":"EMSOFT: Embedded Software ","location":"Tahoe City, CA, USA"},"scopus_import":"1","citation":{"ieee":"L. De Alfaro and T. A. Henzinger, “Interface theories for component-based design,” in Proceedings of the 1st International Workshop on Embedded Software, Tahoe City, CA, USA, 2001, vol. 2211, pp. 148–165.","ama":"De Alfaro L, Henzinger TA. Interface theories for component-based design. In: Proceedings of the 1st International Workshop on Embedded Software. Vol 2211. ACM; 2001:148-165. doi:10.1007/3-540-45449-7_11","chicago":"De Alfaro, Luca, and Thomas A Henzinger. “Interface Theories for Component-Based Design.” In Proceedings of the 1st International Workshop on Embedded Software, 2211:148–65. ACM, 2001. https://doi.org/10.1007/3-540-45449-7_11.","ista":"De Alfaro L, Henzinger TA. 2001. Interface theories for component-based design. Proceedings of the 1st International Workshop on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2211, 148–165.","apa":"De Alfaro, L., & Henzinger, T. A. (2001). Interface theories for component-based design. In Proceedings of the 1st International Workshop on Embedded Software (Vol. 2211, pp. 148–165). Tahoe City, CA, USA: ACM. https://doi.org/10.1007/3-540-45449-7_11","mla":"De Alfaro, Luca, and Thomas A. Henzinger. “Interface Theories for Component-Based Design.” Proceedings of the 1st International Workshop on Embedded Software, vol. 2211, ACM, 2001, pp. 148–65, doi:10.1007/3-540-45449-7_11.","short":"L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 1st International Workshop on Embedded Software, ACM, 2001, pp. 148–165."},"day":"26","intvolume":" 2211","month":"09","author":[{"full_name":"De Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"date_updated":"2023-05-08T12:11:20Z","volume":2211,"acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA ITO grant F33615-00-C-1693, the MARCO grant 98-DT-660, and the NSF ITR grant CCR-0085949.","_id":"4623","date_created":"2018-12-11T12:09:48Z","publication":"Proceedings of the 1st International Workshop on Embedded Software","abstract":[{"lang":"eng","text":"We classify component-based models of computation into component models and interface models. A component model specifies for each component howthe component behaves in an arbitrary environment; an interface model specifies for each component what the component expects from the environment. Component models support compositional abstraction, and therefore component-based verification. Interface models support compositional refinement, and therefore componentbased design. Many aspects of interface models, such as compatibility and refinement checking between interfaces, are properly viewed in a gametheoretic setting, where the input and output values of an interface are chosen by different players."}],"doi":"10.1007/3-540-45449-7_11","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"conference","title":"Interface theories for component-based design","page":"148 - 165","publisher":"ACM","quality_controlled":"1","date_published":"2001-09-26T00:00:00Z","publication_identifier":{"isbn":["9783540426738"]},"publication_status":"published","year":"2001","publist_id":"84","extern":"1","status":"public","oa_version":"None","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"article_processing_charge":"No"},{"scopus_import":"1","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2001-08-20","location":"Aalborg, Denmark","end_date":"2001-08-25"},"citation":{"ieee":"L. De Alfaro, T. A. Henzinger, and R. Jhala, “Compositional methods for probabilistic systems,” in Proceedings of the 12th International Conference on on Concurrency Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 351–365.","apa":"De Alfaro, L., Henzinger, T. A., & Jhala, R. (2001). Compositional methods for probabilistic systems. In Proceedings of the 12th International Conference on on Concurrency Theory (Vol. 2154, pp. 351–365). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_24","mla":"De Alfaro, Luca, et al. “Compositional Methods for Probabilistic Systems.” Proceedings of the 12th International Conference on on Concurrency Theory, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–65, doi:10.1007/3-540-44685-0_24.","short":"L. De Alfaro, T.A. Henzinger, R. Jhala, in:, Proceedings of the 12th International Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–365.","ista":"De Alfaro L, Henzinger TA, Jhala R. 2001. Compositional methods for probabilistic systems. Proceedings of the 12th International Conference on on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2154, 351–365.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ranjit Jhala. “Compositional Methods for Probabilistic Systems.” In Proceedings of the 12th International Conference on on Concurrency Theory, 2154:351–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. https://doi.org/10.1007/3-540-44685-0_24.","ama":"De Alfaro L, Henzinger TA, Jhala R. Compositional methods for probabilistic systems. In: Proceedings of the 12th International Conference on on Concurrency Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:351-365. doi:10.1007/3-540-44685-0_24"},"month":"08","intvolume":" 2154","day":"13","date_updated":"2023-05-08T10:24:59Z","author":[{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"}],"date_created":"2018-12-11T12:09:51Z","_id":"4632","volume":2154,"acknowledgement":"This research was supported in part by the SRC contract 99-TJ-683.003, the AFOSR MURI grant F49620-00-1-0327, the MARCO GSRC grant 98-DT-660, the NSF Theory grant CCR-9988172, and the DARPA SEC grant F33615-C-98-3614.","doi":"10.1007/3-540-44685-0_24","publication":"Proceedings of the 12th International Conference on on Concurrency Theory","abstract":[{"text":"We present a compositional trace-based model for probabilistic systems. The behavior of a system with probabilistic choice is a stochastic process, namely, a probability distribution on traces, or “bundle.” Consequently, the semantics of a system with both nondeterministic and probabilistic choice is a set of bundles. The bundles of a composite system can be obtained by combining the bundles of the components in a simple mathematical way. Refinement between systems is bundle containment. We achieve assume-guarantee compositionality for bundle semantics by introducing two scoping mechanisms. The first mechanism, which is standard in compositional modeling, distinguishes inputs from outputs and hidden state. The second mechanism, which arises in probabilistic systems, partitions the state into probabilistically independent regions.","lang":"eng"}],"title":"Compositional methods for probabilistic systems","type":"conference","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_published":"2001-08-13T00:00:00Z","publication_status":"published","publication_identifier":{"isbn":["9783540424970"]},"year":"2001","page":"351 - 365","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"article_processing_charge":"No","publist_id":"75","oa_version":"None","extern":"1","status":"public"},{"date_updated":"2023-05-08T09:57:31Z","author":[{"full_name":"De Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"}],"date_created":"2018-12-11T12:09:52Z","_id":"4633","volume":2154,"acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF Theory grant CCR-9988172, and the NSF ITR grant CCR-0085949.","citation":{"ieee":"L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Symbolic algorithms for infinite-state games,” in Proceedings of the 12th International Conference on on Concurrency Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 536–550.","apa":"De Alfaro, L., Henzinger, T. A., & Majumdar, R. (2001). Symbolic algorithms for infinite-state games. In Proceedings of the 12th International Conference on on Concurrency Theory (Vol. 2154, pp. 536–550). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_36","mla":"De Alfaro, Luca, et al. “Symbolic Algorithms for Infinite-State Games.” Proceedings of the 12th International Conference on on Concurrency Theory, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–50, doi:10.1007/3-540-44685-0_36.","short":"L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 12th International Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–550.","ista":"De Alfaro L, Henzinger TA, Majumdar R. 2001. Symbolic algorithms for infinite-state games. Proceedings of the 12th International Conference on on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2154, 536–550.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Symbolic Algorithms for Infinite-State Games.” In Proceedings of the 12th International Conference on on Concurrency Theory, 2154:536–50. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. https://doi.org/10.1007/3-540-44685-0_36.","ama":"De Alfaro L, Henzinger TA, Majumdar R. Symbolic algorithms for infinite-state games. In: Proceedings of the 12th International Conference on on Concurrency Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:536-550. doi:10.1007/3-540-44685-0_36"},"scopus_import":"1","conference":{"end_date":"2001-08-25","location":"Aalborg, Denmark","name":"CONCUR: Concurrency Theory","start_date":"2001-08-20"},"month":"08","intvolume":" 2154","day":"13","year":"2001","publication_status":"published","publication_identifier":{"isbn":["9783540424970"]},"date_published":"2001-08-13T00:00:00Z","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","page":"536 - 550","article_processing_charge":"No","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"oa_version":"None","status":"public","extern":"1","publist_id":"73","doi":"10.1007/3-540-44685-0_36","abstract":[{"text":"A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories:\r\n1 \tClass 1 consists of infinite-state structures for which all safety and reachability games can be solved.\r\n2 \tClass 2 consists of infinite-state structures for which all ω-regular games can be solved.\r\n3 \tClass 3 consists of infinite-state structures for which all nested positive boolean combinations of ω-regular games can be solved.\r\n4 \tClass 4 consists of infinite-state structures for which all nested boolean combinations of ω-regular games can be solved.\r\nWe give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies (“controller synthesis”) for infinitestate games with arbitrary ω-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems.","lang":"eng"}],"publication":"Proceedings of the 12th International Conference on on Concurrency Theory","title":"Symbolic algorithms for infinite-state games","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"conference"},{"title":"The control of synchronous systems, Part II","type":"conference","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","doi":"10.1007/3-540-44685-0_38","abstract":[{"lang":"eng","text":"A controller is an environment for a system that achieves a particular control objective by providing inputs to the system without constraining the choices of the system. For synchronous systems, where system and controller make simultaneous and interdependent choices, the notion that a controller must not constrain the choices of the system can be formalized by type systems for composability. In a previous paper, we solved the control problem for static and dynamic types: a static type is a dependency relation between inputs and outputs, and composition is well-typed if it does not introduce cyclic dependencies; a dynamic type is a set of static types, one for each state. Static and dynamic types, however, cannot capture many important digital circuits, such as gated clocks, bidirectional buses, and random-access memory. We therefore introduce more general type systems, so-called dependent and bidirectional types, for modeling these situations, and we solve the corresponding control problems.\r\nIn a system with a dependent type, the dependencies between inputs and outputs are determined gradually through a game of the system against the controller. In a system with a bidirectional type, also the distinction between inputs and outputs is resolved dynamically by such a game. The game proceeds in several rounds. In each round the system and the controller choose to update some variables dependent on variables that have already been updated. The solution of the control problem for dependent and bidirectional types is based on algorithms for solving these games."}],"publication":"Proceedings of the 12th International Conference on on Concurrency Theory","article_processing_charge":"No","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"oa_version":"None","status":"public","extern":"1","publist_id":"74","year":"2001","publication_identifier":{"isbn":["9783540424970"]},"publication_status":"published","date_published":"2001-08-13T00:00:00Z","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","page":"566 - 581","month":"08","intvolume":" 2154","day":"13","citation":{"chicago":"De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous Systems, Part II.” In Proceedings of the 12th International Conference on on Concurrency Theory, 2154:566–81. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. https://doi.org/10.1007/3-540-44685-0_38.","ista":"De Alfaro L, Henzinger TA, Mang F. 2001. The control of synchronous systems, Part II. Proceedings of the 12th International Conference on on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2154, 566–581.","ama":"De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems, Part II. In: Proceedings of the 12th International Conference on on Concurrency Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:566-581. doi:10.1007/3-540-44685-0_38","mla":"De Alfaro, Luca, et al. “The Control of Synchronous Systems, Part II.” Proceedings of the 12th International Conference on on Concurrency Theory, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–81, doi:10.1007/3-540-44685-0_38.","apa":"De Alfaro, L., Henzinger, T. A., & Mang, F. (2001). The control of synchronous systems, Part II. In Proceedings of the 12th International Conference on on Concurrency Theory (Vol. 2154, pp. 566–581). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_38","short":"L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–581.","ieee":"L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems, Part II,” in Proceedings of the 12th International Conference on on Concurrency Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 566–581."},"scopus_import":"1","conference":{"location":"Aalborg, Denmark","start_date":"2001-08-20","name":"CONCUR: Concurrency Theory","end_date":"2001-08-25"},"date_created":"2018-12-11T12:09:52Z","_id":"4634","volume":2154,"acknowledgement":"This research was supported in part by the SRC contract 99-TJ-683.003, the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the AFOSR MURI grant F49620-00-1-0327, and the NSF Theory grant CCR-9988172.","date_updated":"2023-05-08T10:20:19Z","author":[{"full_name":"De Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Mang","first_name":"Freddy","full_name":"Mang, Freddy"}]},{"publist_id":"71","oa_version":"None","status":"public","extern":"1","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:52Z","_id":"4635","article_processing_charge":"No","page":"86 - 87","quality_controlled":"1","publisher":"ACM","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Mang, Freddy","last_name":"Mang","first_name":"Freddy"}],"date_published":"2001-05-01T00:00:00Z","publication_identifier":{"isbn":["9781581133486"]},"publication_status":"published","year":"2001","date_updated":"2023-05-08T09:39:02Z","main_file_link":[{"url":"https://ir.webis.de/anthology/2001.wwwconf_conference-2001p.57/"}],"title":"MCWEB: A model-checking tool for web-site debugging","day":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"conference","month":"05","publication":"Proceedings of the 10th international conference on World Wide Web","abstract":[{"text":"We show how model checking techniques can be applied to the analysis of connectivity and cost-of-traversal properties of Web sites.","lang":"eng"}],"conference":{"end_date":"2000-05-05","start_date":"2001-05-01","name":"WWW: World Wide Web Conference","location":"Hong Kong, Hong Kong"},"citation":{"ieee":"L. De Alfaro, T. A. Henzinger, and F. Mang, “MCWEB: A model-checking tool for web-site debugging,” in Proceedings of the 10th international conference on World Wide Web, Hong Kong, Hong Kong, 2001, pp. 86–87.","apa":"De Alfaro, L., Henzinger, T. A., & Mang, F. (2001). MCWEB: A model-checking tool for web-site debugging. In Proceedings of the 10th international conference on World Wide Web (pp. 86–87). Hong Kong, Hong Kong: ACM.","mla":"De Alfaro, Luca, et al. “MCWEB: A Model-Checking Tool for Web-Site Debugging.” Proceedings of the 10th International Conference on World Wide Web, ACM, 2001, pp. 86–87.","short":"L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 10th International Conference on World Wide Web, ACM, 2001, pp. 86–87.","ama":"De Alfaro L, Henzinger TA, Mang F. MCWEB: A model-checking tool for web-site debugging. In: Proceedings of the 10th International Conference on World Wide Web. ACM; 2001:86-87.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “MCWEB: A Model-Checking Tool for Web-Site Debugging.” In Proceedings of the 10th International Conference on World Wide Web, 86–87. ACM, 2001.","ista":"De Alfaro L, Henzinger TA, Mang F. 2001. MCWEB: A model-checking tool for web-site debugging. Proceedings of the 10th international conference on World Wide Web. WWW: World Wide Web Conference, 86–87."}},{"date_published":"2001-08-07T00:00:00Z","date_updated":"2023-05-08T09:48:06Z","year":"2001","publication_identifier":{"isbn":["076951281X"]},"publication_status":"published","page":"279 - 290","publisher":"IEEE","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"}],"quality_controlled":"1","_id":"4636","date_created":"2018-12-11T12:09:52Z","language":[{"iso":"eng"}],"article_processing_charge":"No","publist_id":"72","extern":"1","status":"public","oa_version":"None","conference":{"end_date":"2001-06-19","location":"Boston, MA, USA","name":"LICS: Logic in Computer Science","start_date":"2001-06-16"},"doi":"10.1109/LICS.2001.932504","citation":{"ieee":"L. De Alfaro, T. A. Henzinger, and R. Majumdar, “From verification to control: dynamic programs for omega-regular objectives,” in Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, Boston, MA, USA, 2001, pp. 279–290.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “From Verification to Control: Dynamic Programs for Omega-Regular Objectives.” In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 279–90. IEEE, 2001. https://doi.org/10.1109/LICS.2001.932504.","ama":"De Alfaro L, Henzinger TA, Majumdar R. From verification to control: dynamic programs for omega-regular objectives. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. IEEE; 2001:279-290. doi:10.1109/LICS.2001.932504","ista":"De Alfaro L, Henzinger TA, Majumdar R. 2001. From verification to control: dynamic programs for omega-regular objectives. Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 279–290.","apa":"De Alfaro, L., Henzinger, T. A., & Majumdar, R. (2001). From verification to control: dynamic programs for omega-regular objectives. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (pp. 279–290). Boston, MA, USA: IEEE. https://doi.org/10.1109/LICS.2001.932504","mla":"De Alfaro, Luca, et al. “From Verification to Control: Dynamic Programs for Omega-Regular Objectives.” Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2001, pp. 279–90, doi:10.1109/LICS.2001.932504.","short":"L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2001, pp. 279–290."},"publication":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science","abstract":[{"text":"Abstract. Dynamic programs, or fixpoint iteration schemes, are useful for solving many problems on state spaces, including model checking on Kripke structures (“verification”), computing shortest paths on weighted graphs (“optimization”), computing the value of games played on game graphs (“control”). For Kripke structures, a rich fixpoint theory is available in the form of the µ-calculus. Yet few connections have been made between different interpretations of fixpoint algorithms. We study the question of when a particular fixpoint iteration scheme ϕ for verifying an ω-regular property Ψ on a Kripke structure can be used also for solving a two-player game on a game graph with winning objective Ψ. We provide a sufficient and necessary criterion for the answer to be affirmative in the form of an extremal-model theorem for games: under a game interpretation, the dynamic program ϕ solves the game with objective Ψ if and only if both (1) under an existential interpretation on Kripke structures, ϕ is equivalent to ∃Ψ, and (2) under a universal interpretation on Kripke structures, ϕ is equivalent to ∀Ψ. In other words, ϕ is correct on all two-player game graphs iff it is correct on all extremal game graphs, where one or the other player has no choice of moves. The theorem generalizes to quantitative interpretations, where it connects two-player games with costs to weighted graphs. While the standard translations from ω-regular properties to the µ-calculus violate (1) or (2), we give a translation that satisfies both conditions. Our construction, therefore, yields fixpoint iteration schemes that can be uniformly applied on Kripke structures, weighted graphs, game graphs, and game graphs with costs, in order to meet or optimize a given ω-regular objective.","lang":"eng"}],"month":"08","day":"07","type":"conference","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"From verification to control: dynamic programs for omega-regular objectives"},{"intvolume":" 333","day":"15","arxiv":1,"month":"08","external_id":{"arxiv":["math/0106140"]},"citation":{"ista":"Hausel T, Thaddeus M. 2001. Examples of mirror partners arising from integrable systems. Comptes Rendus de l’Academie des Sciences - Series I: Mathematics. 333(4), 313–318.","ama":"Hausel T, Thaddeus M. Examples of mirror partners arising from integrable systems. Comptes Rendus de l’Academie des Sciences - Series I: Mathematics. 2001;333(4):313-318. doi:10.1016/S0764-4442(01)02057-2","chicago":"Hausel, Tamás, and Michael Thaddeus. “Examples of Mirror Partners Arising from Integrable Systems.” Comptes Rendus de l’Academie Des Sciences - Series I: Mathematics. Elsevier, 2001. https://doi.org/10.1016/S0764-4442(01)02057-2.","apa":"Hausel, T., & Thaddeus, M. (2001). Examples of mirror partners arising from integrable systems. Comptes Rendus de l’Academie Des Sciences - Series I: Mathematics. Elsevier. https://doi.org/10.1016/S0764-4442(01)02057-2","mla":"Hausel, Tamás, and Michael Thaddeus. “Examples of Mirror Partners Arising from Integrable Systems.” Comptes Rendus de l’Academie Des Sciences - Series I: Mathematics, vol. 333, no. 4, Elsevier, 2001, pp. 313–18, doi:10.1016/S0764-4442(01)02057-2.","short":"T. Hausel, M. Thaddeus, Comptes Rendus de l’Academie Des Sciences - Series I: Mathematics 333 (2001) 313–318.","ieee":"T. Hausel and M. Thaddeus, “Examples of mirror partners arising from integrable systems,” Comptes Rendus de l’Academie des Sciences - Series I: Mathematics, vol. 333, no. 4. Elsevier, pp. 313–318, 2001."},"scopus_import":"1","acknowledgement":"The authors are grateful for Nigel Hitchin for suggesting the similarity between [4] and [12] in 1996 and for Pierre Deligne for numerous useful comments","volume":333,"issue":"4","date_created":"2018-12-11T11:52:06Z","_id":"1452","author":[{"full_name":"Hausel, Tamas","last_name":"Hausel","id":"4A0666D8-F248-11E8-B48F-1D18A9856A87","first_name":"Tamas"},{"full_name":"Thaddeus, Michael","last_name":"Thaddeus","first_name":"Michael"}],"article_type":"original","date_updated":"2023-05-31T09:57:48Z","title":"Examples of mirror partners arising from integrable systems","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"journal_article","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/math/0106140"}],"abstract":[{"text":"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.","lang":"eng"}],"publication":"Comptes Rendus de l'Academie des Sciences - Series I: Mathematics","doi":"10.1016/S0764-4442(01)02057-2","oa_version":"Preprint","extern":"1","status":"public","oa":1,"publist_id":"5742","article_processing_charge":"No","language":[{"iso":"eng"}],"quality_controlled":"1","publisher":"Elsevier","page":"313 - 318","year":"2001","publication_status":"published","publication_identifier":{"issn":["0764-4442"]},"date_published":"2001-08-15T00:00:00Z"},{"issue":"1-2","acknowledgement":"We would like to acknowledge the financial support provided by the Miller Institute of Basic Research in Science, the Japan Society for the Promotion of Science, grant No. P99736 and the partial support by OTKA grant No. T032478.","volume":514,"_id":"1453","date_created":"2018-12-11T11:52:07Z","article_type":"original","author":[{"full_name":"Etesi, Gábor","first_name":"Gábor","last_name":"Etesi"},{"full_name":"Hausel, Tamas","id":"4A0666D8-F248-11E8-B48F-1D18A9856A87","last_name":"Hausel","first_name":"Tamas"}],"date_updated":"2023-05-31T11:51:37Z","day":"09","intvolume":" 514","arxiv":1,"month":"08","external_id":{"arxiv":["hep-th/0105118"]},"citation":{"ama":"Etesi G, Hausel T. Geometric construction of new Yang-Mills instantons over Taub-NUT space. Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics. 2001;514(1-2):189-199. doi:10.1016/S0370-2693(01)00821-8","chicago":"Etesi, Gábor, and Tamás Hausel. “Geometric Construction of New Yang-Mills Instantons over Taub-NUT Space.” Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics. Elsevier, 2001. https://doi.org/10.1016/S0370-2693(01)00821-8.","ista":"Etesi G, Hausel T. 2001. Geometric construction of new Yang-Mills instantons over Taub-NUT space. Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics. 514(1–2), 189–199.","apa":"Etesi, G., & Hausel, T. (2001). Geometric construction of new Yang-Mills instantons over Taub-NUT space. Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics. Elsevier. https://doi.org/10.1016/S0370-2693(01)00821-8","mla":"Etesi, Gábor, and Tamás Hausel. “Geometric Construction of New Yang-Mills Instantons over Taub-NUT Space.” Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics, vol. 514, no. 1–2, Elsevier, 2001, pp. 189–99, doi:10.1016/S0370-2693(01)00821-8.","short":"G. Etesi, T. Hausel, Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics 514 (2001) 189–199.","ieee":"G. Etesi and T. Hausel, “Geometric construction of new Yang-Mills instantons over Taub-NUT space,” Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics, vol. 514, no. 1–2. Elsevier, pp. 189–199, 2001."},"scopus_import":"1","status":"public","extern":"1","oa_version":"Preprint","publist_id":"5743","oa":1,"article_processing_charge":"No","language":[{"iso":"eng"}],"publisher":"Elsevier","quality_controlled":"1","page":"189 - 199","publication_identifier":{"issn":["0370-2693"]},"publication_status":"published","year":"2001","date_published":"2001-08-09T00:00:00Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"journal_article","title":"Geometric construction of new Yang-Mills instantons over Taub-NUT space","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/hep-th/0105118"}],"abstract":[{"lang":"eng","text":"In this Letter we exhibit a one-parameter family of new Taub-NUT instantons parameterized by a half-line. The endpoint of the half-line will be the reducible Yang-Mills instanton corresponding to the Eguchi-Hanson-Gibbons L2 harmonic 2-form, while at an inner point we recover the Pope-Yuille instanton constructed as a projection of the Levi-Civitá connection onto the positive su(2)+ ⊂ so(4) subalgebra. Our method imitates the Jackiw-Nohl-Rebbi construction originally designed for flat R4. That is we find a one-parameter family of harmonic functions on the Taub-NUT space with a point singularity, rescale the metric and project the obtained Levi-Civitá connection onto the other negative su(2)- ⊂ so(4) part. Our solutions will possess the full U(2) symmetry, and thus provide more solutions to the recently proposed U(2) symmetric ansatz of Kim and Yoon."}],"publication":"Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics","doi":"10.1016/S0370-2693(01)00821-8"},{"doi":"10.1016/S0393-0440(00)00040-1","publication":"Journal of Geometry and Physics","abstract":[{"text":"We address the problem of finding Abelian instantons of finite energy on the Euclidean Schwarzschild manifold. This amounts to construct self-dual L2 harmonic 2-forms on the space. Gibbons found a non-topological L2 harmonic form in the Taub-NUT metric, leading to Abelian instantons with continuous energy. We imitate his construction in the case of the Euclidean Schwarzschild manifold and find a non-topological self-dual L2 harmonic 2-form on it. We show how this gives rise to Abelian instantons and identify them with SU(2)-instantons of Pontryagin number 2n2 found by Charap and Duff in 1977. Using results of Dodziuk and Hitchin we also calculate the full L2 harmonic space for the Euclidean Schwarzschild manifold.","lang":"eng"}],"main_file_link":[{"url":"http://arxiv.org/abs/hep-th/0003239","open_access":"1"}],"type":"journal_article","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Geometric interpretation of Schwarzschild instantons","date_published":"2001-01-01T00:00:00Z","publication_identifier":{"issn":["0393-0440"]},"publication_status":"published","year":"2001","page":"126 - 136","publisher":"Elsevier","quality_controlled":"1","language":[{"iso":"eng"}],"article_processing_charge":"No","publist_id":"5744","oa":1,"extern":"1","status":"public","oa_version":"Preprint","scopus_import":"1","citation":{"ieee":"G. Etesi and T. Hausel, “Geometric interpretation of Schwarzschild instantons,” Journal of Geometry and Physics, vol. 37, no. 1–2. Elsevier, pp. 126–136, 2001.","apa":"Etesi, G., & Hausel, T. (2001). Geometric interpretation of Schwarzschild instantons. Journal of Geometry and Physics. Elsevier. https://doi.org/10.1016/S0393-0440(00)00040-1","short":"G. Etesi, T. Hausel, Journal of Geometry and Physics 37 (2001) 126–136.","mla":"Etesi, Gábor, and Tamás Hausel. “Geometric Interpretation of Schwarzschild Instantons.” Journal of Geometry and Physics, vol. 37, no. 1–2, Elsevier, 2001, pp. 126–36, doi:10.1016/S0393-0440(00)00040-1.","ama":"Etesi G, Hausel T. Geometric interpretation of Schwarzschild instantons. Journal of Geometry and Physics. 2001;37(1-2):126-136. doi:10.1016/S0393-0440(00)00040-1","ista":"Etesi G, Hausel T. 2001. Geometric interpretation of Schwarzschild instantons. Journal of Geometry and Physics. 37(1–2), 126–136.","chicago":"Etesi, Gábor, and Tamás Hausel. “Geometric Interpretation of Schwarzschild Instantons.” Journal of Geometry and Physics. Elsevier, 2001. https://doi.org/10.1016/S0393-0440(00)00040-1."},"external_id":{"arxiv":["hep-th/0003239"]},"month":"01","arxiv":1,"day":"01","intvolume":" 37","date_updated":"2023-05-31T12:08:45Z","author":[{"full_name":"Etesi, Gábor","first_name":"Gábor","last_name":"Etesi"},{"full_name":"Hausel, Tamas","first_name":"Tamas","id":"4A0666D8-F248-11E8-B48F-1D18A9856A87","last_name":"Hausel"}],"article_type":"original","_id":"1454","date_created":"2018-12-11T11:52:07Z","issue":"1-2","volume":37,"acknowledgement":"The work in this paper was done when Tamás Hausel visited the Yukawa Institute of Kyoto University in February 2000. We are grateful for Prof. G.W. Gibbons for insightful discussions and Prof. H. Kodama and the Yukawa Institute for the invitation and hospitality."},{"pmid":1,"department":[{"_id":"DaZi"}],"month":"06","intvolume":" 292","day":"15","citation":{"ieee":"A. M. Lindroth et al., “Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation,” Science, vol. 292, no. 5524. American Association for the Advancement of Science, pp. 2077–2080, 2001.","ista":"Lindroth AM, Cao X, Jackson JP, Zilberman D, McCallum CM, Henikoff S, Jacobsen SE. 2001. Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation. Science. 292(5524), 2077–2080.","chicago":"Lindroth, A. M., Xiaofeng Cao, James P. Jackson, Daniel Zilberman, Claire M. McCallum, Steven Henikoff, and Steven E. Jacobsen. “Requirement of CHROMOMETHYLASE3 for Maintenance of CpXpG Methylation.” Science. American Association for the Advancement of Science, 2001. https://doi.org/10.1126/science.1059745.","ama":"Lindroth AM, Cao X, Jackson JP, et al. Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation. Science. 2001;292(5524):2077-2080. doi:10.1126/science.1059745","apa":"Lindroth, A. M., Cao, X., Jackson, J. P., Zilberman, D., McCallum, C. M., Henikoff, S., & Jacobsen, S. E. (2001). Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation. Science. American Association for the Advancement of Science. https://doi.org/10.1126/science.1059745","short":"A.M. Lindroth, X. Cao, J.P. Jackson, D. Zilberman, C.M. McCallum, S. Henikoff, S.E. Jacobsen, Science 292 (2001) 2077–2080.","mla":"Lindroth, A. M., et al. “Requirement of CHROMOMETHYLASE3 for Maintenance of CpXpG Methylation.” Science, vol. 292, no. 5524, American Association for the Advancement of Science, 2001, pp. 2077–80, doi:10.1126/science.1059745."},"scopus_import":"1","external_id":{"pmid":["11349138"]},"date_created":"2021-06-02T13:35:16Z","_id":"9444","volume":292,"issue":"5524","date_updated":"2021-12-14T08:40:32Z","author":[{"first_name":"A. M.","last_name":"Lindroth","full_name":"Lindroth, A. M."},{"first_name":"Xiaofeng","last_name":"Cao","full_name":"Cao, Xiaofeng"},{"last_name":"Jackson","first_name":"James P.","full_name":"Jackson, James P."},{"full_name":"Zilberman, Daniel","orcid":"0000-0002-0123-8649","first_name":"Daniel","id":"6973db13-dd5f-11ea-814e-b3e5455e9ed1","last_name":"Zilberman"},{"last_name":"McCallum","first_name":"Claire M.","full_name":"McCallum, Claire M."},{"full_name":"Henikoff, Steven","first_name":"Steven","last_name":"Henikoff"},{"first_name":"Steven E.","last_name":"Jacobsen","full_name":"Jacobsen, Steven E."}],"article_type":"original","keyword":["Multidisciplinary"],"title":"Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation","type":"journal_article","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","doi":"10.1126/science.1059745","abstract":[{"lang":"eng","text":"Epigenetic silenced alleles of the Arabidopsis SUPERMANlocus (the clark kent alleles) are associated with dense hypermethylation at noncanonical cytosines (CpXpG and asymmetric sites, where X = A, T, C, or G). A genetic screen for suppressors of a hypermethylated clark kent mutant identified nine loss-of-function alleles of CHROMOMETHYLASE3(CMT3), a novel cytosine methyltransferase homolog. These cmt3 mutants display a wild-type morphology but exhibit decreased CpXpG methylation of the SUP gene and of other sequences throughout the genome. They also show reactivated expression of endogenous retrotransposon sequences. These results show that a non-CpG DNA methyltransferase is responsible for maintaining epigenetic gene silencing."}],"publication":"Science","article_processing_charge":"No","language":[{"iso":"eng"}],"oa_version":"None","extern":"1","status":"public","publication_identifier":{"issn":["0036-8075"],"eissn":["1095-9203"]},"publication_status":"published","year":"2001","date_published":"2001-06-15T00:00:00Z","quality_controlled":"1","publisher":"American Association for the Advancement of Science","page":"2077-2080"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","day":"01","intvolume":" 31","title":"Maintaining minimum spanning forests in dynamic graphs","month":"03","abstract":[{"text":"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.","lang":"eng"}],"publication":"SIAM Journal on Computing","citation":{"ieee":"M. H. Henzinger and V. King, “Maintaining minimum spanning forests in dynamic graphs,” SIAM Journal on Computing, vol. 31, no. 2. Society for Industrial & Applied Mathematics, pp. 364–374, 2001.","ama":"Henzinger MH, King V. Maintaining minimum spanning forests in dynamic graphs. SIAM Journal on Computing. 2001;31(2):364-374. doi:10.1137/s0097539797327209","ista":"Henzinger MH, King V. 2001. Maintaining minimum spanning forests in dynamic graphs. SIAM Journal on Computing. 31(2), 364–374.","chicago":"Henzinger, Monika H, and Valerie King. “Maintaining Minimum Spanning Forests in Dynamic Graphs.” SIAM Journal on Computing. Society for Industrial & Applied Mathematics, 2001. https://doi.org/10.1137/s0097539797327209.","short":"M.H. Henzinger, V. King, SIAM Journal on Computing 31 (2001) 364–374.","apa":"Henzinger, M. H., & King, V. (2001). Maintaining minimum spanning forests in dynamic graphs. SIAM Journal on Computing. Society for Industrial & Applied Mathematics. https://doi.org/10.1137/s0097539797327209","mla":"Henzinger, Monika H., and Valerie King. “Maintaining Minimum Spanning Forests in Dynamic Graphs.” SIAM Journal on Computing, vol. 31, no. 2, Society for Industrial & Applied Mathematics, 2001, pp. 364–74, doi:10.1137/s0097539797327209."},"doi":"10.1137/s0097539797327209","scopus_import":"1","status":"public","extern":"1","oa_version":"None","issue":"2","volume":31,"article_processing_charge":"No","_id":"11892","language":[{"iso":"eng"}],"date_created":"2022-08-17T08:43:43Z","publisher":"Society for Industrial & Applied Mathematics","author":[{"first_name":"Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"},{"full_name":"King, Valerie","first_name":"Valerie","last_name":"King"}],"article_type":"original","quality_controlled":"1","page":"364-374","date_updated":"2023-02-17T14:24:55Z","publication_identifier":{"eissn":["1095-7111"],"issn":["0097-5397"]},"year":"2001","publication_status":"published","date_published":"2001-03-01T00:00:00Z"},{"page":"51-58","quality_controlled":"1","author":[{"full_name":"Bharat, K.","last_name":"Bharat","first_name":"K."},{"full_name":"Chang, Bay-Wei","first_name":"Bay-Wei","last_name":"Chang"},{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"},{"full_name":"Ruhl, M.","first_name":"M.","last_name":"Ruhl"}],"publisher":"Institute of Electrical and Electronics Engineers","date_published":"2001-12-01T00:00:00Z","publication_status":"published","publication_identifier":{"isbn":["0-7695-1119-8"],"issn":["15504786"]},"year":"2001","date_updated":"2023-02-17T09:59:47Z","oa_version":"None","extern":"1","status":"public","language":[{"iso":"eng"}],"date_created":"2022-08-18T07:12:46Z","_id":"11914","article_processing_charge":"No","publication":"1st IEEE International Conference on Data Mining","abstract":[{"lang":"eng","text":"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."}],"scopus_import":"1","conference":{"end_date":"2001-12-02","start_date":"2001-11-29","name":"ICMD: International Conference on Data Mining","location":"San Jose, CA, United States"},"doi":"10.1109/ICDM.2001.989500","citation":{"ieee":"K. Bharat, B.-W. Chang, M. H. Henzinger, and M. Ruhl, “Who links to whom: Mining linkage between Web sites,” in 1st IEEE International Conference on Data Mining, San Jose, CA, United States, 2001, pp. 51–58.","ista":"Bharat K, Chang B-W, Henzinger MH, Ruhl M. 2001. Who links to whom: Mining linkage between Web sites. 1st IEEE International Conference on Data Mining. ICMD: International Conference on Data Mining, 51–58.","ama":"Bharat K, Chang B-W, Henzinger MH, Ruhl M. Who links to whom: Mining linkage between Web sites. In: 1st IEEE International Conference on Data Mining. Institute of Electrical and Electronics Engineers; 2001:51-58. doi:10.1109/ICDM.2001.989500","chicago":"Bharat, K., Bay-Wei Chang, Monika H Henzinger, and M. Ruhl. “Who Links to Whom: Mining Linkage between Web Sites.” In 1st IEEE International Conference on Data Mining, 51–58. Institute of Electrical and Electronics Engineers, 2001. https://doi.org/10.1109/ICDM.2001.989500.","apa":"Bharat, K., Chang, B.-W., Henzinger, M. H., & Ruhl, M. (2001). Who links to whom: Mining linkage between Web sites. In 1st IEEE International Conference on Data Mining (pp. 51–58). San Jose, CA, United States: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/ICDM.2001.989500","mla":"Bharat, K., et al. “Who Links to Whom: Mining Linkage between Web Sites.” 1st IEEE International Conference on Data Mining, Institute of Electrical and Electronics Engineers, 2001, pp. 51–58, doi:10.1109/ICDM.2001.989500.","short":"K. Bharat, B.-W. Chang, M.H. Henzinger, M. Ruhl, in:, 1st IEEE International Conference on Data Mining, Institute of Electrical and Electronics Engineers, 2001, pp. 51–58."},"title":"Who links to whom: Mining linkage between Web sites","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","type":"conference","month":"12"},{"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","day":"01","type":"book_chapter","title":"Application of the likelihood function in phylogenetic analysis","month":"01","publication":"Handbook of Statistical Genetics","abstract":[{"text":"This chapter contains sections titled:\r\n\r\nIntroduction\r\n\r\n- History\r\n\r\n- Developing an Intuition of Likelihood\r\n\r\n- Method of Maximum Likelihood\r\n\r\n- Bayesian Inference\r\n\r\n- Markov Chain Monte Carlo\r\n\r\n- Assessing Uncertainty of Phylogenies\r\n\r\n- Hypothesis Testing and Model Choice\r\n\r\n- Comparative Analysis\r\n\r\n- Conclusions\r\n\r\n- References","lang":"eng"}],"doi":"10.1002/9780470061619.ch15","citation":{"ieee":"J. Huelsenbeck and J. P. Bollback, “Application of the likelihood function in phylogenetic analysis,” in Handbook of Statistical Genetics, D. Balding, M. Bishop, and C. Cannings, Eds. Wiley-Blackwell, 2001, pp. 415–439.","chicago":"Huelsenbeck, John, and Jonathan P Bollback. “Application of the Likelihood Function in Phylogenetic Analysis.” In Handbook of Statistical Genetics, edited by David Balding, Martin Bishop, and Chriss Cannings, 415–39. Wiley-Blackwell, 2001. https://doi.org/10.1002/9780470061619.ch15.","ista":"Huelsenbeck J, Bollback JP. 2001.Application of the likelihood function in phylogenetic analysis. In: Handbook of Statistical Genetics. , 415–439.","ama":"Huelsenbeck J, Bollback JP. Application of the likelihood function in phylogenetic analysis. In: Balding D, Bishop M, Cannings C, eds. Handbook of Statistical Genetics. Wiley-Blackwell; 2001:415-439. doi:10.1002/9780470061619.ch15","mla":"Huelsenbeck, John, and Jonathan P. Bollback. “Application of the Likelihood Function in Phylogenetic Analysis.” Handbook of Statistical Genetics, edited by David Balding et al., Wiley-Blackwell, 2001, pp. 415–39, doi:10.1002/9780470061619.ch15.","apa":"Huelsenbeck, J., & Bollback, J. P. (2001). Application of the likelihood function in phylogenetic analysis. In D. Balding, M. Bishop, & C. Cannings (Eds.), Handbook of Statistical Genetics (pp. 415–439). Wiley-Blackwell. https://doi.org/10.1002/9780470061619.ch15","short":"J. Huelsenbeck, J.P. Bollback, in:, D. Balding, M. Bishop, C. Cannings (Eds.), Handbook of Statistical Genetics, Wiley-Blackwell, 2001, pp. 415–439."},"editor":[{"first_name":"David","last_name":"Balding","full_name":"Balding, David"},{"full_name":"Bishop, Martin","last_name":"Bishop","first_name":"Martin"},{"first_name":"Chriss","last_name":"Cannings","full_name":"Cannings, Chriss"}],"publist_id":"2966","status":"public","extern":"1","oa_version":"None","_id":"3434","date_created":"2018-12-11T12:03:19Z","language":[{"iso":"eng"}],"article_processing_charge":"No","page":"415 - 439","publisher":"Wiley-Blackwell","author":[{"full_name":"Huelsenbeck, John","last_name":"Huelsenbeck","first_name":"John"},{"orcid":"0000-0002-4624-4612","full_name":"Bollback, Jonathan P","last_name":"Bollback","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","first_name":"Jonathan P"}],"quality_controlled":"1","date_published":"2001-01-01T00:00:00Z","date_updated":"2023-05-15T14:43:39Z","publication_status":"published","year":"2001","publication_identifier":{"isbn":["9781119429142 "]}},{"doi":"10.1126/science.1065889","abstract":[{"text":"As a discipline, phylogenetics is becoming transformed by a flood of molecular data. These data allow broad questions to be asked about the history of life, but also present difficult statistical and computational problems. Bayesian inference of phylogeny brings a new perspective to a number of outstanding issues in evolutionary biology, including the analysis of large phylogenetic trees and complex evolutionary models and the detection of the footprint of natural selection in DNA sequences.","lang":"eng"}],"publication":"Science","title":"Bayesian inference of phylogeny and its impact on evolutionary biology","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"journal_article","publication_status":"published","publication_identifier":{"issn":["0036-8075"]},"year":"2001","date_published":"2001-12-14T00:00:00Z","quality_controlled":"1","publisher":"American Association for the Advancement of Science","page":"2310 - 2314","article_processing_charge":"No","language":[{"iso":"eng"}],"oa_version":"None","status":"public","extern":"1","publist_id":"2962","citation":{"ieee":"J. Huelsenbeck, F. Ronquist, R. Nielsen, and J. P. Bollback, “Bayesian inference of phylogeny and its impact on evolutionary biology,” Science, vol. 294, no. 5550. American Association for the Advancement of Science, pp. 2310–2314, 2001.","chicago":"Huelsenbeck, John, Fredrik Ronquist, Rasmus Nielsen, and Jonathan P Bollback. “Bayesian Inference of Phylogeny and Its Impact on Evolutionary Biology.” Science. American Association for the Advancement of Science, 2001. https://doi.org/10.1126/science.1065889.","ama":"Huelsenbeck J, Ronquist F, Nielsen R, Bollback JP. Bayesian inference of phylogeny and its impact on evolutionary biology. Science. 2001;294(5550):2310-2314. doi:10.1126/science.1065889","ista":"Huelsenbeck J, Ronquist F, Nielsen R, Bollback JP. 2001. Bayesian inference of phylogeny and its impact on evolutionary biology. Science. 294(5550), 2310–2314.","apa":"Huelsenbeck, J., Ronquist, F., Nielsen, R., & Bollback, J. P. (2001). Bayesian inference of phylogeny and its impact on evolutionary biology. Science. American Association for the Advancement of Science. https://doi.org/10.1126/science.1065889","short":"J. Huelsenbeck, F. Ronquist, R. Nielsen, J.P. Bollback, Science 294 (2001) 2310–2314.","mla":"Huelsenbeck, John, et al. “Bayesian Inference of Phylogeny and Its Impact on Evolutionary Biology.” Science, vol. 294, no. 5550, American Association for the Advancement of Science, 2001, pp. 2310–14, doi:10.1126/science.1065889."},"external_id":{"pmid":["11743192 "]},"pmid":1,"month":"12","intvolume":" 294","day":"14","date_updated":"2023-05-15T14:10:13Z","author":[{"last_name":"Huelsenbeck","first_name":"John","full_name":"Huelsenbeck, John"},{"first_name":"Fredrik","last_name":"Ronquist","full_name":"Ronquist, Fredrik"},{"last_name":"Nielsen","first_name":"Rasmus","full_name":"Nielsen, Rasmus"},{"id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","last_name":"Bollback","first_name":"Jonathan P","full_name":"Bollback, Jonathan P","orcid":"0000-0002-4624-4612"}],"date_created":"2018-12-11T12:03:20Z","_id":"3438","volume":294,"issue":"5550"},{"type":"journal_article","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Isolation of polymorphic microsatellite markers from the malaria vector Anopheles darlingi","doi":" 10.1046/j.1471-8278.2001.00078.x","publication":"Molecular Ecology Notes","abstract":[{"lang":"eng","text":"High molecular weight DNA was extracted from the primary Neotropical malaria vector, Anopheles darlingi from Capanema, Pará, Brazil, to create a small insert genomic library, and then a phagemid library. Enriched sublibraries were constructed from the phagemid library using a microsatellite oligo primed second strand synthesis protocol. The resulting 242 760 individual clones were screened. The mean clone size of the positive clones was 302 bp. Flanking primers were designed for each suitable microsatellite sequence. Eight polymorphic loci were optimized and characterized. The allele size ranges are based on 253 samples of A. darlingi from eastern Amazonian and central Brazil."}],"language":[{"iso":"eng"}],"article_processing_charge":"No","publist_id":"2961","extern":"1","status":"public","oa_version":"None","date_published":"2001-12-01T00:00:00Z","publication_status":"published","year":"2001","publication_identifier":{"issn":["1471-8278"]},"page":"223 - 225","publisher":"Wiley-Blackwell","quality_controlled":"1","month":"12","day":"01","intvolume":" 1","citation":{"short":"J. Conn, J.P. Bollback, D. Onyabe, T. Robinson, R. Wilkerson, M. Povoa, Molecular Ecology Notes 1 (2001) 223–225.","mla":"Conn, Jan, et al. “Isolation of Polymorphic Microsatellite Markers from the Malaria Vector Anopheles Darlingi.” Molecular Ecology Notes, vol. 1, no. 4, Wiley-Blackwell, 2001, pp. 223–25, doi: 10.1046/j.1471-8278.2001.00078.x.","apa":"Conn, J., Bollback, J. P., Onyabe, D., Robinson, T., Wilkerson, R., & Povoa, M. (2001). Isolation of polymorphic microsatellite markers from the malaria vector Anopheles darlingi. Molecular Ecology Notes. Wiley-Blackwell. https://doi.org/ 10.1046/j.1471-8278.2001.00078.x","chicago":"Conn, Jan, Jonathan P Bollback, David Onyabe, Tessa Robinson, Richard Wilkerson, and Marinete Povoa. “Isolation of Polymorphic Microsatellite Markers from the Malaria Vector Anopheles Darlingi.” Molecular Ecology Notes. Wiley-Blackwell, 2001. https://doi.org/ 10.1046/j.1471-8278.2001.00078.x.","ista":"Conn J, Bollback JP, Onyabe D, Robinson T, Wilkerson R, Povoa M. 2001. Isolation of polymorphic microsatellite markers from the malaria vector Anopheles darlingi. Molecular Ecology Notes. 1(4), 223–225.","ama":"Conn J, Bollback JP, Onyabe D, Robinson T, Wilkerson R, Povoa M. Isolation of polymorphic microsatellite markers from the malaria vector Anopheles darlingi. Molecular Ecology Notes. 2001;1(4):223-225. doi: 10.1046/j.1471-8278.2001.00078.x","ieee":"J. Conn, J. P. Bollback, D. Onyabe, T. Robinson, R. Wilkerson, and M. Povoa, “Isolation of polymorphic microsatellite markers from the malaria vector Anopheles darlingi,” Molecular Ecology Notes, vol. 1, no. 4. Wiley-Blackwell, pp. 223–225, 2001."},"_id":"3439","date_created":"2018-12-11T12:03:20Z","issue":"4","acknowledgement":"For support in Brazil we thank D. Galiza, R.N.L. Lacerda,E.P. Santa Rosa, M.N.O. Segura, and R.T.L. de Souza. We also thankM.J. Braun for allowing work on the library construction at theLaboratory of Molecular Systematics, Washington. Supported byNIH AI 40116 to JEC and Instituto Evandro Chagas, Belém, Brazil.","volume":1,"date_updated":"2023-05-15T13:58:49Z","author":[{"full_name":"Conn, Jan","last_name":"Conn","first_name":"Jan"},{"first_name":"Jonathan P","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","last_name":"Bollback","full_name":"Bollback, Jonathan P","orcid":"0000-0002-4624-4612"},{"last_name":"Onyabe","first_name":"David","full_name":"Onyabe, David"},{"first_name":"Tessa","last_name":"Robinson","full_name":"Robinson, Tessa"},{"full_name":"Wilkerson, Richard","last_name":"Wilkerson","first_name":"Richard"},{"full_name":"Povoa, Marinete","last_name":"Povoa","first_name":"Marinete"}],"article_type":"original"},{"date_published":"2001-05-01T00:00:00Z","publication_identifier":{"issn":["0039-7989"]},"year":"2001","publication_status":"published","page":"351 - 366","publisher":"Oxford University Press","quality_controlled":"1","language":[{"iso":"eng"}],"article_processing_charge":"No","publist_id":"2960","status":"public","extern":"1","oa_version":"None","doi":"10.1080/10635150119871","publication":"Systematic Biology","abstract":[{"text":"Several methods have been proposed to infer the states at the ancestral nodes on a phylogeny. These methods assume a specific tree and set of branch lengths when estimating the ancestral character state. Inferences of the ancestral states, then, are conditioned on the tree and branch lengths being true. We develop a hierarchical Bayes method for inferring the ancestral states on a tree. The method integrates over uncertainty in the tree, branch lengths, and substitution model parameters by using Markov chain Monte Carlo. We compare the hierarchical Bayes inferences of ancestral states with inferences of ancestral states made under the assumption that a specific tree is correct. We find that the methods are correlated, but that accommodating uncertainty in parameters of the phylogenetic model can make inferences of ancestral states even more uncertain than they would be in an empirical Bayes analysis.\r\n","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"journal_article","title":"Empirical and hierarchical Bayesian estimation of ancestral states","date_updated":"2023-05-15T13:54:01Z","article_type":"original","author":[{"last_name":"Huelsenbeck","first_name":"John","full_name":"Huelsenbeck, John"},{"id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","last_name":"Bollback","first_name":"Jonathan P","full_name":"Bollback, Jonathan P","orcid":"0000-0002-4624-4612"}],"_id":"3440","date_created":"2018-12-11T12:03:20Z","issue":"3","volume":50,"citation":{"ieee":"J. Huelsenbeck and J. P. Bollback, “Empirical and hierarchical Bayesian estimation of ancestral states,” Systematic Biology, vol. 50, no. 3. Oxford University Press, pp. 351–366, 2001.","apa":"Huelsenbeck, J., & Bollback, J. P. (2001). Empirical and hierarchical Bayesian estimation of ancestral states. Systematic Biology. Oxford University Press. https://doi.org/10.1080/10635150119871","short":"J. Huelsenbeck, J.P. Bollback, Systematic Biology 50 (2001) 351–366.","mla":"Huelsenbeck, John, and Jonathan P. Bollback. “Empirical and Hierarchical Bayesian Estimation of Ancestral States.” Systematic Biology, vol. 50, no. 3, Oxford University Press, 2001, pp. 351–66, doi:10.1080/10635150119871.","ista":"Huelsenbeck J, Bollback JP. 2001. Empirical and hierarchical Bayesian estimation of ancestral states. Systematic Biology. 50(3), 351–366.","chicago":"Huelsenbeck, John, and Jonathan P Bollback. “Empirical and Hierarchical Bayesian Estimation of Ancestral States.” Systematic Biology. Oxford University Press, 2001. https://doi.org/10.1080/10635150119871.","ama":"Huelsenbeck J, Bollback JP. Empirical and hierarchical Bayesian estimation of ancestral states. Systematic Biology. 2001;50(3):351-366. doi:10.1080/10635150119871"},"external_id":{"pmid":["12116580"]},"month":"05","pmid":1,"day":"01","intvolume":" 50"}]