[{"main_file_link":[{"url":"https://www.nhbs.com/dispersal-book"}],"citation":{"short":"N.H. Barton, in:, Dispersal, Oxford University Press, 2001.","chicago":"Barton, Nicholas H. “The Evolutionary Consequences of Gene Flow and Local Adaptation: Future Approaches.” In <i>Dispersal</i>. Oxford University Press, 2001.","ista":"Barton NH. 2001.The evolutionary consequences of gene flow and local adaptation: Future approaches. In: Dispersal. .","ama":"Barton NH. The evolutionary consequences of gene flow and local adaptation: Future approaches. In: <i>Dispersal</i>. Oxford University Press; 2001.","ieee":"N. H. Barton, “The evolutionary consequences of gene flow and local adaptation: Future approaches,” in <i>Dispersal</i>, Oxford University Press, 2001.","mla":"Barton, Nicholas H. “The Evolutionary Consequences of Gene Flow and Local Adaptation: Future Approaches.” <i>Dispersal</i>, Oxford University Press, 2001.","apa":"Barton, N. H. (2001). The evolutionary consequences of gene flow and local adaptation: Future approaches. In <i>Dispersal</i>. Oxford University Press."},"article_processing_charge":"No","extern":"1","quality_controlled":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","author":[{"orcid":"0000-0002-8548-5240","full_name":"Barton, Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","last_name":"Barton","first_name":"Nicholas H"}],"oa_version":"None","type":"book_chapter","date_updated":"2023-05-10T09:57:10Z","year":"2001","day":"01","publication":"Dispersal","title":"The evolutionary consequences of gene flow and local adaptation: Future approaches","_id":"4278","language":[{"iso":"eng"}],"abstract":[{"text":"The ability of species to migrate that has interested ecologists for many years. Now that so many species and ecosystems face major environmental change, the ability of species to adapt to these changes by dispersing, migrating, or moving between different patches of habitat can be crucial to ensuring their survivial. This book provides a timely and wide-ranging overview of the study of dispersal and incorporates much of the latest research. The causes, mechanisms, and consequences of dispersal at the individual, population, species and community levels are considered. The potential of new techniques and models for studying dispersal, drawn from molecular biology and demography, is also explored. Perspectives and insights are offered from the fields of evolution, conservation biology and genetics. Throughout the book, theoretical approaches are combined with empirical data, and care has been taken to include examples from as wide a range of species as possible. ","lang":"eng"}],"publication_status":"published","date_published":"2001-04-01T00:00:00Z","publisher":"Oxford University Press","publist_id":"1812","publication_identifier":{"isbn":["9780198506591"]},"month":"04","date_created":"2018-12-11T12:08:00Z","status":"public"},{"title":"EMSOFT: Embedded Software","_id":"4449","doi":"10.1007/3-540-45449-7","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Embedded software is software that interacts with physical processes. As em- bedded systems increasingly permeate our daily lives on all levels, from micros- copic devices to international networks, the cost-efficient development of reliable embedded software is one of the grand challenges in computer science today. The purpose of the workshop is to bring together researchers in all areas of computer science that are traditionally distinct but relevant to embedded software develop- ment, and to incubate a research community in this way. The workshop aims to cover all aspects of the design and implementation of embedded software, inclu- ding operating systems and middleware, programming languages and compilers, modeling and validation, software engineering and programming methodologies, scheduling and execution time analysis, networking and fault tolerance, as well as application areas, such as embedded control, real-time signal processing, and telecommunications."}],"publication_status":"published","citation":{"ama":"Henzinger TA, ed. <i>EMSOFT: Embedded Software</i>. Vol 2211. ACM; 2001. doi:<a href=\"https://doi.org/10.1007/3-540-45449-7\">10.1007/3-540-45449-7</a>","ieee":"T. A. Henzinger, Ed., <i>EMSOFT: Embedded Software</i>, vol. 2211. ACM, 2001.","chicago":"Henzinger, Thomas A, ed. <i>EMSOFT: Embedded Software</i>. Vol. 2211. ACM, 2001. <a href=\"https://doi.org/10.1007/3-540-45449-7\">https://doi.org/10.1007/3-540-45449-7</a>.","short":"T.A. Henzinger, ed., EMSOFT: Embedded Software, ACM, 2001.","ista":"Henzinger TA ed. 2001. EMSOFT: Embedded Software, ACM,p.","apa":"Henzinger, T. A. (Ed.). (2001). <i>EMSOFT: Embedded Software</i> (Vol. 2211). Presented at the EMSOFT 2001: Embedded Software, Tahoe City, CA, USA: ACM. <a href=\"https://doi.org/10.1007/3-540-45449-7\">https://doi.org/10.1007/3-540-45449-7</a>","mla":"Henzinger, Thomas A., editor. <i>EMSOFT: Embedded Software</i>. Vol. 2211, ACM, 2001, doi:<a href=\"https://doi.org/10.1007/3-540-45449-7\">10.1007/3-540-45449-7</a>."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","quality_controlled":"1","article_processing_charge":"No","oa_version":"None","type":"conference_editor","date_updated":"2023-05-10T09:53:17Z","year":"2001","day":"26","alternative_title":["LNCS"],"intvolume":"      2211","publication_identifier":{"isbn":["9783540426738"]},"publist_id":"283","conference":{"start_date":"2001-10-08","location":"Tahoe City, CA, USA","end_date":"2001-10-10","name":"EMSOFT 2001: Embedded Software"},"month":"09","date_created":"2018-12-11T12:08:54Z","status":"public","date_published":"2001-09-26T00:00:00Z","volume":2211,"editor":[{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"}],"publisher":"ACM"},{"publication_status":"published","abstract":[{"text":"We provide an overview of the current status of HYTECH, and reflect on some of the lessons learned from our experiences with the tool. HYTECH is a symbolic model checker for mixed discrete-continuous systems that are modeled as automata with piecewise-constant polyhedral differential inclusions. The use of a formal input language and automated procedures for state-space traversal lay the foundation for formally verifying properties of hybrid dynamical systems. We describe some recent experiences analyzing three hybrid systems. We point out the successes and limitations of the tool. The analysis procedure has been extended in a number of ways to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems.","lang":"eng"}],"title":"Some lessons from the HYTECH experience","publication":"Proceedings of the 40th IEEE Conference on Decision and Control","doi":"10.1109/.2001.980714","language":[{"iso":"eng"}],"_id":"4475","type":"conference","date_updated":"2023-05-10T09:47:20Z","oa_version":"None","day":"01","year":"2001","citation":{"ama":"Henzinger TA, Preussig J, Wong Toi H. Some lessons from the HYTECH experience. In: <i>Proceedings of the 40th IEEE Conference on Decision and Control</i>. Vol 3. IEEE; 2001:2887-2892. doi:<a href=\"https://doi.org/10.1109/.2001.980714\">10.1109/.2001.980714</a>","ieee":"T. A. Henzinger, J. Preussig, and H. Wong Toi, “Some lessons from the HYTECH experience,” in <i>Proceedings of the 40th IEEE Conference on Decision and Control</i>, Orlando, FL, USA, 2001, vol. 3, pp. 2887–2892.","ista":"Henzinger TA, Preussig J, Wong Toi H. 2001. Some lessons from the HYTECH experience. Proceedings of the 40th IEEE Conference on Decision and Control. CDC: Decision and Control vol. 3, 2887–2892.","chicago":"Henzinger, Thomas A, Joerg Preussig, and Howard Wong Toi. “Some Lessons from the HYTECH Experience.” In <i>Proceedings of the 40th IEEE Conference on Decision and Control</i>, 3:2887–92. IEEE, 2001. <a href=\"https://doi.org/10.1109/.2001.980714\">https://doi.org/10.1109/.2001.980714</a>.","short":"T.A. Henzinger, J. Preussig, H. Wong Toi, in:, Proceedings of the 40th IEEE Conference on Decision and Control, IEEE, 2001, pp. 2887–2892.","apa":"Henzinger, T. A., Preussig, J., &#38; Wong Toi, H. (2001). Some lessons from the HYTECH experience. In <i>Proceedings of the 40th IEEE Conference on Decision and Control</i> (Vol. 3, pp. 2887–2892). Orlando, FL, USA: IEEE. <a href=\"https://doi.org/10.1109/.2001.980714\">https://doi.org/10.1109/.2001.980714</a>","mla":"Henzinger, Thomas A., et al. “Some Lessons from the HYTECH Experience.” <i>Proceedings of the 40th IEEE Conference on Decision and Control</i>, vol. 3, IEEE, 2001, pp. 2887–92, doi:<a href=\"https://doi.org/10.1109/.2001.980714\">10.1109/.2001.980714</a>."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","quality_controlled":"1","author":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"first_name":"Joerg","last_name":"Preussig","full_name":"Preussig, Joerg"},{"full_name":"Wong Toi, Howard","last_name":"Wong Toi","first_name":"Howard"}],"article_processing_charge":"No","date_created":"2018-12-11T12:09:02Z","month":"05","conference":{"end_date":"2001-12-07","name":"CDC: Decision and Control","start_date":"2001-12-04","location":"Orlando, FL, USA"},"status":"public","intvolume":"         3","publist_id":"253","publication_identifier":{"isbn":["0780370619"]},"scopus_import":"1","publisher":"IEEE","date_published":"2001-05-01T00:00:00Z","volume":3,"page":"2887 - 2892"},{"publisher":"Springer","volume":2034,"status":"public","conference":{"location":"Rome, Italy","start_date":"2001-03-28","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2001-03-30"},"month":"03","date_created":"2018-12-11T12:09:03Z","publist_id":"250","intvolume":"      2034","year":"2001","extern":"1","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Minea, Marius","last_name":"Minea","first_name":"Marius"},{"first_name":"Vinayak","last_name":"Prabhu","full_name":"Prabhu, Vinayak"}],"quality_controlled":"1","citation":{"chicago":"Henzinger, Thomas A, Marius Minea, and Vinayak Prabhu. “Assume-Guarantee Reasoning for Hierarchical Hybrid Systems.” In <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>, 2034:275–90. Springer, 2001. <a href=\"https://doi.org/10.1007/3-540-45351-2_24\">https://doi.org/10.1007/3-540-45351-2_24</a>.","short":"T.A. Henzinger, M. Minea, V. Prabhu, in:, Proceedings of the 4th International Workshop on Hybrid Systems, Springer, 2001, pp. 275–290.","ista":"Henzinger TA, Minea M, Prabhu V. 2001. Assume-guarantee reasoning for hierarchical hybrid systems. Proceedings of the 4th International Workshop on Hybrid Systems. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 2034, 275–290.","ieee":"T. A. Henzinger, M. Minea, and V. Prabhu, “Assume-guarantee reasoning for hierarchical hybrid systems,” in <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>, Rome, Italy, 2001, vol. 2034, pp. 275–290.","ama":"Henzinger TA, Minea M, Prabhu V. Assume-guarantee reasoning for hierarchical hybrid systems. In: <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>. Vol 2034. Springer; 2001:275-290. doi:<a href=\"https://doi.org/10.1007/3-540-45351-2_24\">10.1007/3-540-45351-2_24</a>","mla":"Henzinger, Thomas A., et al. “Assume-Guarantee Reasoning for Hierarchical Hybrid Systems.” <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>, vol. 2034, Springer, 2001, pp. 275–90, doi:<a href=\"https://doi.org/10.1007/3-540-45351-2_24\">10.1007/3-540-45351-2_24</a>.","apa":"Henzinger, T. A., Minea, M., &#38; Prabhu, V. (2001). Assume-guarantee reasoning for hierarchical hybrid systems. In <i>Proceedings of the 4th International Workshop on Hybrid Systems</i> (Vol. 2034, pp. 275–290). Rome, Italy: Springer. <a href=\"https://doi.org/10.1007/3-540-45351-2_24\">https://doi.org/10.1007/3-540-45351-2_24</a>"},"abstract":[{"lang":"eng","text":"The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for decomposing a verification task about a system into subtasks about the individual components of the system. The key to assume-guarantee reasoning is to consider each component not in isolation, but in conjunction with assumptions about the context of the component. Assume-guarantee principles are known for purely concurrent contexts, which constrain the input data of a component, as well as for purely sequential contexts, which constrain the entry configurations of a component. We present a model for hierarchical system design which permits the arbitrary nesting of parallel as well as serial composition, and which supports an assume-guarantee principle for mixed parallel-serial contexts. Our model also supports both discrete and continuous processes, and is therefore well-suited for the modeling and analysis of embedded software systems which interact with real-world environments. Using an example of two cooperating robots, we show refinement between a high-level model which specifies continuous timing constraints and an implementation which relies on discrete sampling."}],"publication_status":"published","_id":"4477","publication":"Proceedings of the 4th International Workshop on Hybrid Systems","title":"Assume-guarantee reasoning for hierarchical hybrid systems","page":"275 - 290","date_published":"2001-03-14T00:00:00Z","scopus_import":"1","publication_identifier":{"isbn":["9783540418665"]},"alternative_title":["LNCS"],"day":"14","oa_version":"None","date_updated":"2023-05-09T14:47:37Z","type":"conference","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"Support for this research was provided in part by the AFOSR MURI grant F49620- 00-1-0327, and the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF ITR grant CCR-0085949.","language":[{"iso":"eng"}],"doi":"10.1007/3-540-45351-2_24"},{"abstract":[{"lang":"eng","text":"Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. We illustrate the platform-independence and time-triggered execution of Giotto by coordinating a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots."}],"publication_status":"published","acknowledgement":"We thank Rupak Majumdar for implementing a prototype Giotto compiler for Lego Mindstorms robots. We thank Dmitry Derevyanko and Winthrop Williams for building our Intel x86 robots. We thank Edward Lee and Xiaojun Liu for help with a Ptolemy II [4] implementation of Giotto. This research was supported in part by the DARPA SEC grant F33615-C-98-3614, the DARPA MoBIES grant F33615- 00-C-1703, the MARCO GSRC grant 98-DT-660, the AFOSR MURI grant F49620-00-1-0327, and the NSF ITR grant CCR-0085949.","_id":"4478","doi":"10.1145/384197.384208","language":[{"iso":"eng"}],"title":"Embedded control systems development with Giotto","publication":"Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems","year":"2001","day":"01","oa_version":"None","date_updated":"2023-05-10T09:37:20Z","type":"conference","author":[{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Horowitz, Benjamin","last_name":"Horowitz","first_name":"Benjamin"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","quality_controlled":"1","extern":"1","citation":{"ista":"Henzinger TA, Horowitz B, Kirsch C. 2001. Embedded control systems development with Giotto. Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems. LCTES: Languages, Compilers, and Tools for Embedded Systems, 64–72.","short":"T.A. Henzinger, B. Horowitz, C. Kirsch, in:, Proceedings of the 2nd ACM SIGPLAN Workshop on Languages, Compilers and Tools for Embedded Systems, ACM, 2001, pp. 64–72.","chicago":"Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Embedded Control Systems Development with Giotto.” In <i>Proceedings of the 2nd ACM SIGPLAN Workshop on Languages, Compilers and Tools for Embedded Systems</i>, 64–72. ACM, 2001. <a href=\"https://doi.org/10.1145/384197.384208\">https://doi.org/10.1145/384197.384208</a>.","ieee":"T. A. Henzinger, B. Horowitz, and C. Kirsch, “Embedded control systems development with Giotto,” in <i>Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems</i>, New York, NY, United States, 2001, pp. 64–72.","ama":"Henzinger TA, Horowitz B, Kirsch C. Embedded control systems development with Giotto. In: <i>Proceedings of the 2nd ACM SIGPLAN Workshop on Languages, Compilers and Tools for Embedded Systems</i>. ACM; 2001:64-72. doi:<a href=\"https://doi.org/10.1145/384197.384208\">10.1145/384197.384208</a>","apa":"Henzinger, T. A., Horowitz, B., &#38; Kirsch, C. (2001). Embedded control systems development with Giotto. In <i>Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems</i> (pp. 64–72). New York, NY, United States: ACM. <a href=\"https://doi.org/10.1145/384197.384208\">https://doi.org/10.1145/384197.384208</a>","mla":"Henzinger, Thomas A., et al. “Embedded Control Systems Development with Giotto.” <i>Proceedings of the 2nd ACM SIGPLAN Workshop on Languages, Compilers and Tools for Embedded Systems</i>, ACM, 2001, pp. 64–72, doi:<a href=\"https://doi.org/10.1145/384197.384208\">10.1145/384197.384208</a>."},"status":"public","month":"06","conference":{"location":"New York, NY, United States","name":"LCTES: Languages, Compilers, and Tools for Embedded Systems"},"date_created":"2018-12-11T12:09:03Z","scopus_import":"1","publist_id":"251","publication_identifier":{"isbn":["9781581134254"]},"publisher":"ACM","page":"64 - 72","date_published":"2001-06-01T00:00:00Z"},{"quality_controlled":"1","extern":"1","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Horowitz, Benjamin","last_name":"Horowitz","first_name":"Benjamin"},{"full_name":"Kirsch, Christoph","first_name":"Christoph","last_name":"Kirsch"}],"citation":{"apa":"Henzinger, T. A., Horowitz, B., &#38; Kirsch, C. (2001). Giotto: A time-triggered language for embedded programming. In <i>Proceedings of the 1st International Workshop on Embedded Software</i> (Vol. 2211, pp. 166–184). Tahoe City, CA, USA: ACM. <a href=\"https://doi.org/10.1007/3-540-45449-7_12\">https://doi.org/10.1007/3-540-45449-7_12</a>","mla":"Henzinger, Thomas A., et al. “Giotto: A Time-Triggered Language for Embedded Programming.” <i>Proceedings of the 1st International Workshop on Embedded Software</i>, vol. 2211, ACM, 2001, pp. 166–84, doi:<a href=\"https://doi.org/10.1007/3-540-45449-7_12\">10.1007/3-540-45449-7_12</a>.","ama":"Henzinger TA, Horowitz B, Kirsch C. Giotto: A time-triggered language for embedded programming. In: <i>Proceedings of the 1st International Workshop on Embedded Software</i>. Vol 2211. ACM; 2001:166-184. doi:<a href=\"https://doi.org/10.1007/3-540-45449-7_12\">10.1007/3-540-45449-7_12</a>","ieee":"T. A. Henzinger, B. Horowitz, and C. Kirsch, “Giotto: A time-triggered language for embedded programming,” in <i>Proceedings of the 1st International Workshop on Embedded Software</i>, Tahoe City, CA, USA, 2001, vol. 2211, pp. 166–184.","ista":"Henzinger TA, Horowitz B, Kirsch C. 2001. Giotto: A time-triggered language for embedded programming. Proceedings of the 1st International Workshop on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2211, 166–184.","chicago":"Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Giotto: A Time-Triggered Language for Embedded Programming.” In <i>Proceedings of the 1st International Workshop on Embedded Software</i>, 2211:166–84. ACM, 2001. <a href=\"https://doi.org/10.1007/3-540-45449-7_12\">https://doi.org/10.1007/3-540-45449-7_12</a>.","short":"T.A. Henzinger, B. Horowitz, C. Kirsch, in:, Proceedings of the 1st International Workshop on Embedded Software, ACM, 2001, pp. 166–184."},"year":"2001","_id":"4479","title":"Giotto: A time-triggered language for embedded programming","publication":"Proceedings of the 1st International Workshop on Embedded Software","abstract":[{"text":"Giotto provides an abstract programmer’s model for the implementation of embedded control systems with hard real-time constraints. A typical control application consists of periodic software tasks together with a mode switching logic for enabling and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations, and mode switches independent of any implementation platform. Giotto can be annotated with platform constraints such as task-to-host mappings, and task and communication schedules. The annotations are directives for the Giotto compiler, but they do not alter the functionality and timing of a Giotto program. By separating the platform-independent from the platform-dependent concerns, Giotto enables a great deal of flexibility in choosing control platforms as well as a great deal of automation in the validation and synthesis of control software. The time-triggered nature of Giotto achieves timing predictability, which makes Giotto particularly suitable for safety-critical applications.","lang":"eng"}],"publication_status":"published","volume":2211,"publisher":"ACM","publist_id":"252","intvolume":"      2211","status":"public","month":"09","conference":{"name":"EMSOFT: Embedded Software ","end_date":"2001-10-10","start_date":"2001-10-08","location":"Tahoe City, CA, USA"},"date_created":"2018-12-11T12:09:04Z","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","day":"26","oa_version":"None","type":"conference","date_updated":"2023-05-10T09:42:10Z","doi":"10.1007/3-540-45449-7_12","language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the DARPA SEC grant F33615-C-98-3614 and by the MARCO GSRC grant 98-DT-660.","page":"166 - 184","date_published":"2001-09-26T00:00:00Z","scopus_import":"1","publication_identifier":{"isbn":["9783540426738"]},"alternative_title":["LNCS"]},{"language":[{"iso":"eng"}],"doi":"10.1109/DASC.2001.964169","_id":"4564","publication":"Proceedings of the 20th Digital Avionics Systems Conference","title":"A reusable and platform-independent framework for distributed control systems","publication_status":"published","abstract":[{"lang":"eng","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."}],"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. ","quality_controlled":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","extern":"1","author":[{"full_name":"Brown, Timothy","first_name":"Timothy","last_name":"Brown"},{"last_name":"Pasetti","first_name":"Alessandro","full_name":"Pasetti, Alessandro"},{"last_name":"Pree","first_name":"Wolfgang","full_name":"Pree, Wolfgang"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"}],"citation":{"mla":"Brown, Timothy, et al. “A Reusable and Platform-Independent Framework for Distributed Control Systems.” <i>Proceedings of the 20th Digital Avionics Systems Conference</i>, IEEE, 2001, pp. 1–11, doi:<a href=\"https://doi.org/10.1109/DASC.2001.964169\">10.1109/DASC.2001.964169</a>.","apa":"Brown, T., Pasetti, A., Pree, W., Henzinger, T. A., &#38; Kirsch, C. (2001). A reusable and platform-independent framework for distributed control systems. In <i>Proceedings of the 20th Digital Avionics Systems Conference</i> (pp. 1–11). Daytona Beach, FL, USA: IEEE. <a href=\"https://doi.org/10.1109/DASC.2001.964169\">https://doi.org/10.1109/DASC.2001.964169</a>","ieee":"T. Brown, A. Pasetti, W. Pree, T. A. Henzinger, and C. Kirsch, “A reusable and platform-independent framework for distributed control systems,” in <i>Proceedings of the 20th Digital Avionics Systems Conference</i>, Daytona Beach, FL, USA, 2001, pp. 1–11.","ama":"Brown T, Pasetti A, Pree W, Henzinger TA, Kirsch C. A reusable and platform-independent framework for distributed control systems. In: <i>Proceedings of the 20th Digital Avionics Systems Conference</i>. IEEE; 2001:1-11. doi:<a href=\"https://doi.org/10.1109/DASC.2001.964169\">10.1109/DASC.2001.964169</a>","chicago":"Brown, Timothy, Alessandro Pasetti, Wolfgang Pree, Thomas A Henzinger, and Christoph Kirsch. “A Reusable and Platform-Independent Framework for Distributed Control Systems.” In <i>Proceedings of the 20th Digital Avionics Systems Conference</i>, 1–11. IEEE, 2001. <a href=\"https://doi.org/10.1109/DASC.2001.964169\">https://doi.org/10.1109/DASC.2001.964169</a>.","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.","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."},"day":"06","year":"2001","type":"conference","date_updated":"2023-05-09T12:23:16Z","oa_version":"None","publication_identifier":{"isbn":["0780370341"]},"publist_id":"143","scopus_import":"1","status":"public","date_created":"2018-12-11T12:09:30Z","month":"08","conference":{"name":"DASC: Digital Avionics Systems Conference","end_date":"2001-10-18","location":"Daytona Beach, FL, USA","start_date":"2001-10-14"},"page":"1 - 11","date_published":"2001-08-06T00:00:00Z","publisher":"IEEE"},{"date_published":"2001-03-01T00:00:00Z","page":"97 - 116","scopus_import":"1","publication_identifier":{"issn":["0925-9856"]},"oa_version":"None","date_updated":"2023-05-08T12:22:38Z","type":"journal_article","day":"01","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","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.","language":[{"iso":"eng"}],"doi":"10.1023/A:1008767206905","article_type":"original","publisher":"Springer","volume":18,"issue":"2","month":"03","date_created":"2018-12-11T12:09:41Z","status":"public","intvolume":"        18","publist_id":"108","year":"2001","citation":{"chicago":"Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” <i>Formal Methods in System Design</i>. Springer, 2001. <a href=\"https://doi.org/10.1023/A:1008767206905\">https://doi.org/10.1023/A:1008767206905</a>.","short":"R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, Formal Methods in System Design 18 (2001) 97–116.","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. <i>Formal Methods in System Design</i>. 2001;18(2):97-116. doi:<a href=\"https://doi.org/10.1023/A:1008767206905\">10.1023/A:1008767206905</a>","ieee":"R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order reduction in symbolic state-space exploration,” <i>Formal Methods in System Design</i>, vol. 18, no. 2. Springer, pp. 97–116, 2001.","apa":"Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (2001). Partial-order reduction in symbolic state-space exploration. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1023/A:1008767206905\">https://doi.org/10.1023/A:1008767206905</a>","mla":"Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.” <i>Formal Methods in System Design</i>, vol. 18, no. 2, Springer, 2001, pp. 97–116, doi:<a href=\"https://doi.org/10.1023/A:1008767206905\">10.1023/A:1008767206905</a>."},"extern":"1","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"last_name":"Brayton","first_name":"Robert","full_name":"Brayton, Robert"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","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"}],"quality_controlled":"1","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"}],"publication_status":"published","title":"Partial-order reduction in symbolic state-space exploration","publication":"Formal Methods in System Design","_id":"4599"},{"status":"public","date_created":"2018-12-11T12:09:41Z","conference":{"name":"ICSE: Software Engineering"},"month":"08","publication_identifier":{"isbn":["0769510507"]},"publist_id":"109","publisher":"IEEE","page":"835 - 836","date_published":"2001-08-07T00:00:00Z","publication_status":"published","abstract":[{"lang":"eng","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."}],"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. ","language":[{"iso":"eng"}],"doi":"10.1109/ICSE.2001.919196","_id":"4600","publication":"Proceedings of the 23rd International Conference on Software Engineering","title":"jMocha: A model-checking tool that exploits design structure","day":"07","year":"2001","date_updated":"2023-05-08T14:06:55Z","type":"conference","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Kang","first_name":"Myong","full_name":"Kang, Myong"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"first_name":"Freddy","last_name":"Mang","full_name":"Mang, Freddy"},{"last_name":"Wang","first_name":"Bow","full_name":"Wang, Bow"}],"article_processing_charge":"No","extern":"1","quality_controlled":"1","citation":{"ama":"Alur R, De Alfaro L, Grosu R, et al. jMocha: A model-checking tool that exploits design structure. In: <i>Proceedings of the 23rd International Conference on Software Engineering</i>. IEEE; 2001:835-836. doi:<a href=\"https://doi.org/10.1109/ICSE.2001.919196\">10.1109/ICSE.2001.919196</a>","ieee":"R. Alur <i>et al.</i>, “jMocha: A model-checking tool that exploits design structure,” in <i>Proceedings of the 23rd International Conference on Software Engineering</i>, 2001, pp. 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 <i>Proceedings of the 23rd International Conference on Software Engineering</i>, 835–36. IEEE, 2001. <a href=\"https://doi.org/10.1109/ICSE.2001.919196\">https://doi.org/10.1109/ICSE.2001.919196</a>.","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.","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.","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 <i>Proceedings of the 23rd International Conference on Software Engineering</i> (pp. 835–836). IEEE. <a href=\"https://doi.org/10.1109/ICSE.2001.919196\">https://doi.org/10.1109/ICSE.2001.919196</a>","mla":"Alur, Rajeev, et al. “JMocha: A Model-Checking Tool That Exploits Design Structure.” <i>Proceedings of the 23rd International Conference on Software Engineering</i>, IEEE, 2001, pp. 835–36, doi:<a href=\"https://doi.org/10.1109/ICSE.2001.919196\">10.1109/ICSE.2001.919196</a>."}},{"day":"01","year":"2001","type":"conference","date_updated":"2023-05-08T12:01:02Z","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","author":[{"full_name":"De Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"}],"article_processing_charge":"No","extern":"1","quality_controlled":"1","citation":{"ieee":"L. De Alfaro and T. A. Henzinger, “Interface automata,” in <i>Proceedings of the 8th European software engineering conference</i>, Vienna, Austria, 2001, pp. 109–120.","ama":"De Alfaro L, Henzinger TA. Interface automata. In: <i>Proceedings of the 8th European Software Engineering Conference</i>. ACM; 2001:109-120. doi:<a href=\"https://doi.org/10.1145/503209.503226\">10.1145/503209.503226</a>","ista":"De Alfaro L, Henzinger TA. 2001. Interface automata. Proceedings of the 8th European software engineering conference. FSE: Foundations of Software Engineering, 109–120.","short":"L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 8th European Software Engineering Conference, ACM, 2001, pp. 109–120.","chicago":"De Alfaro, Luca, and Thomas A Henzinger. “Interface Automata.” In <i>Proceedings of the 8th European Software Engineering Conference</i>, 109–20. ACM, 2001. <a href=\"https://doi.org/10.1145/503209.503226\">https://doi.org/10.1145/503209.503226</a>.","mla":"De Alfaro, Luca, and Thomas A. Henzinger. “Interface Automata.” <i>Proceedings of the 8th European Software Engineering Conference</i>, ACM, 2001, pp. 109–20, doi:<a href=\"https://doi.org/10.1145/503209.503226\">10.1145/503209.503226</a>.","apa":"De Alfaro, L., &#38; Henzinger, T. A. (2001). Interface automata. In <i>Proceedings of the 8th European software engineering conference</i> (pp. 109–120). Vienna, Austria: ACM. <a href=\"https://doi.org/10.1145/503209.503226\">https://doi.org/10.1145/503209.503226</a>"},"publication_status":"published","abstract":[{"lang":"eng","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."}],"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.","doi":"10.1145/503209.503226","language":[{"iso":"eng"}],"_id":"4622","publication":"Proceedings of the 8th European software engineering conference","title":"Interface automata","publisher":"ACM","page":"109 - 120","date_published":"2001-06-01T00:00:00Z","status":"public","date_created":"2018-12-11T12:09:48Z","conference":{"location":"Vienna, Austria","start_date":"2001-09-10","name":"FSE: Foundations of Software Engineering","end_date":"2001-09-14"},"month":"06","publist_id":"83","publication_identifier":{"isbn":["9781581133905"]},"scopus_import":"1"},{"publication":"Proceedings of the 1st International Workshop on Embedded Software","title":"Interface theories for component-based design","_id":"4623","publication_status":"published","abstract":[{"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.","lang":"eng"}],"citation":{"ama":"De Alfaro L, Henzinger TA. Interface theories for component-based design. In: <i>Proceedings of the 1st International Workshop on Embedded Software</i>. Vol 2211. ACM; 2001:148-165. doi:<a href=\"https://doi.org/10.1007/3-540-45449-7_11\">10.1007/3-540-45449-7_11</a>","ieee":"L. De Alfaro and T. A. Henzinger, “Interface theories for component-based design,” in <i>Proceedings of the 1st International Workshop on Embedded Software</i>, Tahoe City, CA, USA, 2001, vol. 2211, pp. 148–165.","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.","chicago":"De Alfaro, Luca, and Thomas A Henzinger. “Interface Theories for Component-Based Design.” In <i>Proceedings of the 1st International Workshop on Embedded Software</i>, 2211:148–65. ACM, 2001. <a href=\"https://doi.org/10.1007/3-540-45449-7_11\">https://doi.org/10.1007/3-540-45449-7_11</a>.","short":"L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 1st International Workshop on Embedded Software, ACM, 2001, pp. 148–165.","mla":"De Alfaro, Luca, and Thomas A. Henzinger. “Interface Theories for Component-Based Design.” <i>Proceedings of the 1st International Workshop on Embedded Software</i>, vol. 2211, ACM, 2001, pp. 148–65, doi:<a href=\"https://doi.org/10.1007/3-540-45449-7_11\">10.1007/3-540-45449-7_11</a>.","apa":"De Alfaro, L., &#38; Henzinger, T. A. (2001). Interface theories for component-based design. In <i>Proceedings of the 1st International Workshop on Embedded Software</i> (Vol. 2211, pp. 148–165). Tahoe City, CA, USA: ACM. <a href=\"https://doi.org/10.1007/3-540-45449-7_11\">https://doi.org/10.1007/3-540-45449-7_11</a>"},"extern":"1","quality_controlled":"1","author":[{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"}],"year":"2001","intvolume":"      2211","publist_id":"84","date_created":"2018-12-11T12:09:48Z","month":"09","conference":{"name":"EMSOFT: Embedded Software ","end_date":"2001-10-10","start_date":"2001-10-08","location":"Tahoe City, CA, USA"},"status":"public","volume":2211,"publisher":"ACM","doi":"10.1007/3-540-45449-7_11","language":[{"iso":"eng"}],"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.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","date_updated":"2023-05-08T12:11:20Z","type":"conference","oa_version":"None","day":"26","alternative_title":["LNCS"],"publication_identifier":{"isbn":["9783540426738"]},"scopus_import":"1","date_published":"2001-09-26T00:00:00Z","page":"148 - 165"},{"oa_version":"None","date_updated":"2023-05-08T10:24:59Z","type":"conference","day":"13","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","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","language":[{"iso":"eng"}],"date_published":"2001-08-13T00:00:00Z","page":"351 - 365","alternative_title":["LNCS"],"scopus_import":"1","publication_identifier":{"isbn":["9783540424970"]},"year":"2001","citation":{"ama":"De Alfaro L, Henzinger TA, Jhala R. Compositional methods for probabilistic systems. In: <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:351-365. doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_24\">10.1007/3-540-44685-0_24</a>","ieee":"L. De Alfaro, T. A. Henzinger, and R. Jhala, “Compositional methods for probabilistic systems,” in <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, Aalborg, Denmark, 2001, vol. 2154, 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.","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.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ranjit Jhala. “Compositional Methods for Probabilistic Systems.” In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, 2154:351–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. <a href=\"https://doi.org/10.1007/3-540-44685-0_24\">https://doi.org/10.1007/3-540-44685-0_24</a>.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Jhala, R. (2001). Compositional methods for probabilistic systems. In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i> (Vol. 2154, pp. 351–365). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-44685-0_24\">https://doi.org/10.1007/3-540-44685-0_24</a>","mla":"De Alfaro, Luca, et al. “Compositional Methods for Probabilistic Systems.” <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–65, doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_24\">10.1007/3-540-44685-0_24</a>."},"quality_controlled":"1","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"}],"extern":"1","abstract":[{"lang":"eng","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."}],"publication_status":"published","title":"Compositional methods for probabilistic systems","publication":"Proceedings of the 12th International Conference on on Concurrency Theory","_id":"4632","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":2154,"conference":{"start_date":"2001-08-20","location":"Aalborg, Denmark","name":"CONCUR: Concurrency Theory","end_date":"2001-08-25"},"month":"08","date_created":"2018-12-11T12:09:51Z","status":"public","intvolume":"      2154","publist_id":"75"},{"page":"536 - 550","date_published":"2001-08-13T00:00:00Z","publication_identifier":{"isbn":["9783540424970"]},"scopus_import":"1","alternative_title":["LNCS"],"day":"13","type":"conference","date_updated":"2023-05-08T09:57:31Z","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","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.","doi":"10.1007/3-540-44685-0_36","language":[{"iso":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":2154,"status":"public","date_created":"2018-12-11T12:09:52Z","month":"08","conference":{"location":"Aalborg, Denmark","start_date":"2001-08-20","name":"CONCUR: Concurrency Theory","end_date":"2001-08-25"},"publist_id":"73","intvolume":"      2154","year":"2001","author":[{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"}],"extern":"1","quality_controlled":"1","citation":{"mla":"De Alfaro, Luca, et al. “Symbolic Algorithms for Infinite-State Games.” <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–50, doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_36\">10.1007/3-540-44685-0_36</a>.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Majumdar, R. (2001). Symbolic algorithms for infinite-state games. In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i> (Vol. 2154, pp. 536–550). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-44685-0_36\">https://doi.org/10.1007/3-540-44685-0_36</a>","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Symbolic Algorithms for Infinite-State Games.” In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, 2154:536–50. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. <a href=\"https://doi.org/10.1007/3-540-44685-0_36\">https://doi.org/10.1007/3-540-44685-0_36</a>.","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.","ieee":"L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Symbolic algorithms for infinite-state games,” in <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 536–550.","ama":"De Alfaro L, Henzinger TA, Majumdar R. Symbolic algorithms for infinite-state games. In: <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:536-550. doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_36\">10.1007/3-540-44685-0_36</a>"},"publication_status":"published","abstract":[{"lang":"eng","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."}],"_id":"4633","title":"Symbolic algorithms for infinite-state games","publication":"Proceedings of the 12th International Conference on on Concurrency Theory"},{"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.","doi":"10.1007/3-540-44685-0_38","language":[{"iso":"eng"}],"day":"13","oa_version":"None","type":"conference","date_updated":"2023-05-08T10:20:19Z","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","publication_identifier":{"isbn":["9783540424970"]},"alternative_title":["LNCS"],"page":"566 - 581","date_published":"2001-08-13T00:00:00Z","abstract":[{"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.","lang":"eng"}],"publication_status":"published","_id":"4634","title":"The control of synchronous systems, Part II","publication":"Proceedings of the 12th International Conference on on Concurrency Theory","year":"2001","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Mang, Freddy","first_name":"Freddy","last_name":"Mang"}],"quality_controlled":"1","extern":"1","citation":{"apa":"De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (2001). The control of synchronous systems, Part II. In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i> (Vol. 2154, pp. 566–581). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-44685-0_38\">https://doi.org/10.1007/3-540-44685-0_38</a>","mla":"De Alfaro, Luca, et al. “The Control of Synchronous Systems, Part II.” <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–81, doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_38\">10.1007/3-540-44685-0_38</a>.","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.","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.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous Systems, Part II.” In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, 2154:566–81. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. <a href=\"https://doi.org/10.1007/3-540-44685-0_38\">https://doi.org/10.1007/3-540-44685-0_38</a>.","ama":"De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems, Part II. In: <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:566-581. doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_38\">10.1007/3-540-44685-0_38</a>","ieee":"L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems, Part II,” in <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 566–581."},"status":"public","month":"08","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","publist_id":"74","intvolume":"      2154","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":2154},{"page":"86 - 87","date_published":"2001-05-01T00:00:00Z","publisher":"ACM","publist_id":"71","publication_identifier":{"isbn":["9781581133486"]},"status":"public","conference":{"end_date":"2000-05-05","name":"WWW: World Wide Web Conference","location":"Hong Kong, Hong Kong","start_date":"2001-05-01"},"month":"05","date_created":"2018-12-11T12:09:52Z","extern":"1","article_processing_charge":"No","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Mang","first_name":"Freddy","full_name":"Mang, Freddy"}],"quality_controlled":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"mla":"De Alfaro, Luca, et al. “MCWEB: A Model-Checking Tool for Web-Site Debugging.” <i>Proceedings of the 10th International Conference on World Wide Web</i>, ACM, 2001, pp. 86–87.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (2001). MCWEB: A model-checking tool for web-site debugging. In <i>Proceedings of the 10th international conference on World Wide Web</i> (pp. 86–87). Hong Kong, Hong Kong: ACM.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “MCWEB: A Model-Checking Tool for Web-Site Debugging.” In <i>Proceedings of the 10th International Conference on World Wide Web</i>, 86–87. ACM, 2001.","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.","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.","ieee":"L. De Alfaro, T. A. Henzinger, and F. Mang, “MCWEB: A model-checking tool for web-site debugging,” in <i>Proceedings of the 10th international conference on World Wide Web</i>, Hong Kong, Hong Kong, 2001, pp. 86–87.","ama":"De Alfaro L, Henzinger TA, Mang F. MCWEB: A model-checking tool for web-site debugging. In: <i>Proceedings of the 10th International Conference on World Wide Web</i>. ACM; 2001:86-87."},"main_file_link":[{"url":"https://ir.webis.de/anthology/2001.wwwconf_conference-2001p.57/"}],"year":"2001","day":"01","oa_version":"None","date_updated":"2023-05-08T09:39:02Z","type":"conference","_id":"4635","language":[{"iso":"eng"}],"publication":"Proceedings of the 10th international conference on World Wide Web","title":"MCWEB: A model-checking tool for web-site debugging","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"}],"publication_status":"published"},{"month":"08","conference":{"end_date":"2001-06-19","name":"LICS: Logic in Computer Science","start_date":"2001-06-16","location":"Boston, MA, USA"},"date_created":"2018-12-11T12:09:52Z","status":"public","publist_id":"72","publication_identifier":{"isbn":["076951281X"]},"publisher":"IEEE","date_published":"2001-08-07T00:00:00Z","page":"279 - 290","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"}],"publication_status":"published","publication":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science","title":"From verification to control: dynamic programs for omega-regular objectives","_id":"4636","doi":"10.1109/LICS.2001.932504","language":[{"iso":"eng"}],"oa_version":"None","type":"conference","date_updated":"2023-05-08T09:48:06Z","year":"2001","day":"07","citation":{"mla":"De Alfaro, Luca, et al. “From Verification to Control: Dynamic Programs for Omega-Regular Objectives.” <i>Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science</i>, IEEE, 2001, pp. 279–90, doi:<a href=\"https://doi.org/10.1109/LICS.2001.932504\">10.1109/LICS.2001.932504</a>.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Majumdar, R. (2001). From verification to control: dynamic programs for omega-regular objectives. In <i>Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science</i> (pp. 279–290). Boston, MA, USA: IEEE. <a href=\"https://doi.org/10.1109/LICS.2001.932504\">https://doi.org/10.1109/LICS.2001.932504</a>","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.","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.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “From Verification to Control: Dynamic Programs for Omega-Regular Objectives.” In <i>Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science</i>, 279–90. IEEE, 2001. <a href=\"https://doi.org/10.1109/LICS.2001.932504\">https://doi.org/10.1109/LICS.2001.932504</a>.","ama":"De Alfaro L, Henzinger TA, Majumdar R. From verification to control: dynamic programs for omega-regular objectives. In: <i>Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science</i>. IEEE; 2001:279-290. doi:<a href=\"https://doi.org/10.1109/LICS.2001.932504\">10.1109/LICS.2001.932504</a>","ieee":"L. De Alfaro, T. A. Henzinger, and R. Majumdar, “From verification to control: dynamic programs for omega-regular objectives,” in <i>Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science</i>, Boston, MA, USA, 2001, pp. 279–290."},"article_processing_charge":"No","author":[{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Majumdar, Ritankar","last_name":"Majumdar","first_name":"Ritankar"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","quality_controlled":"1","extern":"1"},{"_id":"12925","title":"Structure and Function of the Ion Channel ICln","publication":"Cellular Physiology and Biochemistry","pmid":1,"publication_status":"published","abstract":[{"lang":"eng","text":"Normal function of organs and cells is tightly linked to the cytoarchitecture. Control of the cell volume is therefore vital for the organism. A widely established strategy of cells to counteract swelling is the activation of chloride and potassium channels, which leads to a net efflux of salt followed by water - a process termed regulatory volume decrease. Since there is evidence for swelling-dependent chloride channels (IClswell) being activated also during pathological processes, the identification of the molecular entity underlying IClswell is of utmost importance. Several proteins are discussed as the channel forming IClswell, i.e. phospholemman, p-glycoprotein, CLC-3 and ICln. In this review we would like to focus on the properties of ICln, a protein cloned from a Madin Darby canine kidney (MDCK) cell library whose expression in Xenopus laevis oocytes resulted in a nucleotide sensitive outwardly rectifying chloride current closely resembling the biophysical properties of IClswell."}],"quality_controlled":"1","extern":"1","author":[{"full_name":"Fürst, Johannes","last_name":"Fürst","first_name":"Johannes"},{"full_name":"Jakab, Martin","first_name":"Martin","last_name":"Jakab"},{"last_name":"König","first_name":"Matthias","full_name":"König, Matthias"},{"full_name":"Ritter, Markus","last_name":"Ritter","first_name":"Markus"},{"last_name":"Gschwentner","first_name":"Martin","full_name":"Gschwentner, Martin"},{"full_name":"Rudzki, Jakob","last_name":"Rudzki","first_name":"Jakob"},{"last_name":"Danzl","first_name":"Johann G","orcid":"0000-0001-8559-3973","full_name":"Danzl, Johann G","id":"42EFD3B6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mayer, Michael","last_name":"Mayer","first_name":"Michael"},{"full_name":"Burtscher, Carmen M.","first_name":"Carmen M.","last_name":"Burtscher"},{"last_name":"Schirmer","first_name":"Julia","full_name":"Schirmer, Julia"},{"first_name":"Brigitte","last_name":"Maier","full_name":"Maier, Brigitte"},{"full_name":"Nairz, Manfred","last_name":"Nairz","first_name":"Manfred"},{"full_name":"Chwatal, Sabine","first_name":"Sabine","last_name":"Chwatal"},{"full_name":"Paulmichl, Markus","first_name":"Markus","last_name":"Paulmichl"}],"citation":{"ama":"Fürst J, Jakab M, König M, et al. Structure and Function of the Ion Channel ICln. <i>Cellular Physiology and Biochemistry</i>. 2000;10(5-6):329-334. doi:<a href=\"https://doi.org/10.1159/000016374\">10.1159/000016374</a>","ieee":"J. Fürst <i>et al.</i>, “Structure and Function of the Ion Channel ICln,” <i>Cellular Physiology and Biochemistry</i>, vol. 10, no. 5–6. S. Karger AG, pp. 329–334, 2000.","short":"J. Fürst, M. Jakab, M. König, M. Ritter, M. Gschwentner, J. Rudzki, J.G. Danzl, M. Mayer, C.M. Burtscher, J. Schirmer, B. Maier, M. Nairz, S. Chwatal, M. Paulmichl, Cellular Physiology and Biochemistry 10 (2000) 329–334.","chicago":"Fürst, Johannes, Martin Jakab, Matthias König, Markus Ritter, Martin Gschwentner, Jakob Rudzki, Johann G Danzl, et al. “Structure and Function of the Ion Channel ICln.” <i>Cellular Physiology and Biochemistry</i>. S. Karger AG, 2000. <a href=\"https://doi.org/10.1159/000016374\">https://doi.org/10.1159/000016374</a>.","ista":"Fürst J, Jakab M, König M, Ritter M, Gschwentner M, Rudzki J, Danzl JG, Mayer M, Burtscher CM, Schirmer J, Maier B, Nairz M, Chwatal S, Paulmichl M. 2000. Structure and Function of the Ion Channel ICln. Cellular Physiology and Biochemistry. 10(5–6), 329–334.","apa":"Fürst, J., Jakab, M., König, M., Ritter, M., Gschwentner, M., Rudzki, J., … Paulmichl, M. (2000). Structure and Function of the Ion Channel ICln. <i>Cellular Physiology and Biochemistry</i>. S. Karger AG. <a href=\"https://doi.org/10.1159/000016374\">https://doi.org/10.1159/000016374</a>","mla":"Fürst, Johannes, et al. “Structure and Function of the Ion Channel ICln.” <i>Cellular Physiology and Biochemistry</i>, vol. 10, no. 5–6, S. Karger AG, 2000, pp. 329–34, doi:<a href=\"https://doi.org/10.1159/000016374\">10.1159/000016374</a>."},"year":"2000","intvolume":"        10","status":"public","date_created":"2023-05-08T09:04:58Z","issue":"5-6","volume":10,"article_type":"original","publisher":"S. Karger AG","language":[{"iso":"eng"}],"doi":"10.1159/000016374","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","date_updated":"2023-05-08T10:07:10Z","oa_version":"None","publication_identifier":{"issn":["1015-8987","1421-9778"]},"scopus_import":"1","page":"329-334","date_published":"2000-01-01T00:00:00Z","keyword":["Physiology"],"external_id":{"pmid":["11125213"]}},{"day":"01","type":"journal_article","date_updated":"2023-05-08T09:22:03Z","oa_version":"None","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","doi":"10.1016/S0168-9525(00)02059-X","language":[{"iso":"eng"}],"page":"333 - 334","date_published":"2000-08-01T00:00:00Z","external_id":{"pmid":["10904260 "]},"publication_identifier":{"issn":["0168-9479"]},"scopus_import":"1","year":"2000","author":[{"first_name":"Yuri","last_name":"Wolf","full_name":"Wolf, Yuri"},{"id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","full_name":"Kondrashov, Fyodor","orcid":"0000-0001-8243-4694","first_name":"Fyodor","last_name":"Kondrashov"},{"last_name":"Koonin","first_name":"Eugene","full_name":"Koonin, Eugene"}],"quality_controlled":"1","extern":"1","citation":{"mla":"Wolf, Yuri, et al. “No Footprints of Primordial Introns in a Eukaryotic Genome.” <i>Trends in Genetics</i>, vol. 16, no. 8, Elsevier, 2000, pp. 333–34, doi:<a href=\"https://doi.org/10.1016/S0168-9525(00)02059-X\">10.1016/S0168-9525(00)02059-X</a>.","apa":"Wolf, Y., Kondrashov, F., &#38; Koonin, E. (2000). No footprints of primordial introns in a eukaryotic genome. <i>Trends in Genetics</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0168-9525(00)02059-X\">https://doi.org/10.1016/S0168-9525(00)02059-X</a>","ieee":"Y. Wolf, F. Kondrashov, and E. Koonin, “No footprints of primordial introns in a eukaryotic genome,” <i>Trends in Genetics</i>, vol. 16, no. 8. Elsevier, pp. 333–334, 2000.","ama":"Wolf Y, Kondrashov F, Koonin E. No footprints of primordial introns in a eukaryotic genome. <i>Trends in Genetics</i>. 2000;16(8):333-334. doi:<a href=\"https://doi.org/10.1016/S0168-9525(00)02059-X\">10.1016/S0168-9525(00)02059-X</a>","ista":"Wolf Y, Kondrashov F, Koonin E. 2000. No footprints of primordial introns in a eukaryotic genome. Trends in Genetics. 16(8), 333–334.","short":"Y. Wolf, F. Kondrashov, E. Koonin, Trends in Genetics 16 (2000) 333–334.","chicago":"Wolf, Yuri, Fyodor Kondrashov, and Eugene Koonin. “No Footprints of Primordial Introns in a Eukaryotic Genome.” <i>Trends in Genetics</i>. Elsevier, 2000. <a href=\"https://doi.org/10.1016/S0168-9525(00)02059-X\">https://doi.org/10.1016/S0168-9525(00)02059-X</a>."},"publication_status":"published","_id":"842","publication":"Trends in Genetics","title":"No footprints of primordial introns in a eukaryotic genome","pmid":1,"publisher":"Elsevier","article_type":"original","issue":"8","volume":16,"status":"public","date_created":"2018-12-11T11:48:48Z","month":"08","publist_id":"6806","intvolume":"        16"},{"_id":"8525","doi":"10.1007/s002200050811","language":[{"iso":"eng"}],"title":"Generic diffeomorphisms with superexponential growth of number of periodic orbits","publication":"Communications in Mathematical Physics","abstract":[{"lang":"eng","text":"Let M be a smooth compact manifold of dimension at least 2 and Diffr(M) be the space of C r smooth diffeomorphisms of M. Associate to each diffeomorphism f;isin; Diffr(M) the sequence P n (f) of the number of isolated periodic points for f of period n. In this paper we exhibit an open set N in the space of diffeomorphisms Diffr(M) such for a Baire generic diffeomorphism f∈N the number of periodic points P n f grows with a period n faster than any following sequence of numbers {a n } n ∈ Z + along a subsequence, i.e. P n (f)>a ni for some n i →∞ with i→∞. In the cases of surface diffeomorphisms, i.e. dim M≡2, an open set N with a supergrowth of the number of periodic points is a Newhouse domain. A proof of the man result is based on the Gontchenko–Shilnikov–Turaev Theorem [GST]. A complete proof of that theorem is also presented."}],"publication_status":"published","quality_controlled":"1","extern":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"id":"FE553552-CDE8-11E9-B324-C0EBE5697425","full_name":"Kaloshin, Vadim","orcid":"0000-0002-6051-2628","last_name":"Kaloshin","first_name":"Vadim"}],"citation":{"ieee":"V. Kaloshin, “Generic diffeomorphisms with superexponential growth of number of periodic orbits,” <i>Communications in Mathematical Physics</i>, vol. 211. Springer Nature, pp. 253–271, 2000.","ama":"Kaloshin V. Generic diffeomorphisms with superexponential growth of number of periodic orbits. <i>Communications in Mathematical Physics</i>. 2000;211:253-271. doi:<a href=\"https://doi.org/10.1007/s002200050811\">10.1007/s002200050811</a>","chicago":"Kaloshin, Vadim. “Generic Diffeomorphisms with Superexponential Growth of Number of Periodic Orbits.” <i>Communications in Mathematical Physics</i>. Springer Nature, 2000. <a href=\"https://doi.org/10.1007/s002200050811\">https://doi.org/10.1007/s002200050811</a>.","short":"V. Kaloshin, Communications in Mathematical Physics 211 (2000) 253–271.","ista":"Kaloshin V. 2000. Generic diffeomorphisms with superexponential growth of number of periodic orbits. Communications in Mathematical Physics. 211, 253–271.","mla":"Kaloshin, Vadim. “Generic Diffeomorphisms with Superexponential Growth of Number of Periodic Orbits.” <i>Communications in Mathematical Physics</i>, vol. 211, Springer Nature, 2000, pp. 253–71, doi:<a href=\"https://doi.org/10.1007/s002200050811\">10.1007/s002200050811</a>.","apa":"Kaloshin, V. (2000). Generic diffeomorphisms with superexponential growth of number of periodic orbits. <i>Communications in Mathematical Physics</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s002200050811\">https://doi.org/10.1007/s002200050811</a>"},"year":"2000","day":"01","oa_version":"None","type":"journal_article","date_updated":"2021-01-12T08:19:52Z","publication_identifier":{"issn":["0010-3616","1432-0916"]},"intvolume":"       211","status":"public","month":"04","date_created":"2020-09-18T10:50:20Z","volume":211,"page":"253-271","keyword":["Mathematical Physics","Statistical and Nonlinear Physics"],"date_published":"2000-04-01T00:00:00Z","publisher":"Springer Nature","article_type":"original"},{"date_published":"2000-01-01T00:00:00Z","page":"27 - 28","alternative_title":["LEOS"],"scopus_import":"1","publication_identifier":{"isbn":["078035947X"]},"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","date_updated":"2023-05-04T14:46:21Z","type":"conference","day":"01","language":[{"iso":"eng"}],"doi":"10.1109/LEOS.2000.890656","volume":1,"publisher":"IEEE","intvolume":"         1","publist_id":"5388","month":"01","conference":{"start_date":"2000-11-13","location":"Rio Grande, PR, USA","end_date":"2000-11-16","name":"Lasers and Electro Optics Society Annual Meeting"},"date_created":"2018-12-11T11:53:44Z","status":"public","citation":{"ista":"Katsaros G, Lane P, Murphy M. 2000. Comparison of the impact of FWM on binary, duobinary and dicode modulation in DWDM systems. Proceedings of the 2000 IEEE Annual Meeting Conference . Lasers and Electro Optics Society Annual Meeting, LEOS, vol. 1, 27–28.","short":"G. Katsaros, P. Lane, M. Murphy, in:, Proceedings of the 2000 IEEE Annual Meeting Conference , IEEE, 2000, pp. 27–28.","chicago":"Katsaros, Georgios, Phil Lane, and Michelle Murphy. “Comparison of the Impact of FWM on Binary, Duobinary and Dicode Modulation in DWDM Systems.” In <i>Proceedings of the 2000 IEEE Annual Meeting Conference </i>, 1:27–28. IEEE, 2000. <a href=\"https://doi.org/10.1109/LEOS.2000.890656\">https://doi.org/10.1109/LEOS.2000.890656</a>.","ama":"Katsaros G, Lane P, Murphy M. Comparison of the impact of FWM on binary, duobinary and dicode modulation in DWDM systems. In: <i>Proceedings of the 2000 IEEE Annual Meeting Conference </i>. Vol 1. IEEE; 2000:27-28. doi:<a href=\"https://doi.org/10.1109/LEOS.2000.890656\">10.1109/LEOS.2000.890656</a>","ieee":"G. Katsaros, P. Lane, and M. Murphy, “Comparison of the impact of FWM on binary, duobinary and dicode modulation in DWDM systems,” in <i>Proceedings of the 2000 IEEE Annual Meeting Conference </i>, Rio Grande, PR, USA, 2000, vol. 1, pp. 27–28.","mla":"Katsaros, Georgios, et al. “Comparison of the Impact of FWM on Binary, Duobinary and Dicode Modulation in DWDM Systems.” <i>Proceedings of the 2000 IEEE Annual Meeting Conference </i>, vol. 1, IEEE, 2000, pp. 27–28, doi:<a href=\"https://doi.org/10.1109/LEOS.2000.890656\">10.1109/LEOS.2000.890656</a>.","apa":"Katsaros, G., Lane, P., &#38; Murphy, M. (2000). Comparison of the impact of FWM on binary, duobinary and dicode modulation in DWDM systems. In <i>Proceedings of the 2000 IEEE Annual Meeting Conference </i> (Vol. 1, pp. 27–28). Rio Grande, PR, USA: IEEE. <a href=\"https://doi.org/10.1109/LEOS.2000.890656\">https://doi.org/10.1109/LEOS.2000.890656</a>"},"quality_controlled":"1","extern":"1","author":[{"id":"38DB5788-F248-11E8-B48F-1D18A9856A87","full_name":"Katsaros, Georgios","last_name":"Katsaros","first_name":"Georgios"},{"first_name":"Phil","last_name":"Lane","full_name":"Lane, Phil"},{"first_name":"Michelle","last_name":"Murphy","full_name":"Murphy, Michelle"}],"year":"2000","publication":"Proceedings of the 2000 IEEE Annual Meeting Conference ","title":"Comparison of the impact of FWM on binary, duobinary and dicode modulation in DWDM systems","_id":"1736","abstract":[{"lang":"eng","text":"A coding scheme called diode is compared with duobinary signalling and with normal binary transmission. It is shown that the diode coding suppresses the FWM products of a three channel DWDM system and this reduction against that achieved with duobinary coding is presented. The results presented show how the average level of the FWM products relative to the average levels of the three optical carriers vary over the channel spacing range. The suppression observed is about / dB more than that achieved with duobinary modulation and is greater for narrow channel spacing."}],"publication_status":"published"}]