[{"publisher":"Springer","volume":2719,"month":"06","conference":{"start_date":"2003-06-30","location":"Eindhoven, The Netherlands","name":"ICALP: Automata, Languages and Programming","end_date":"2003-07-04"},"date_created":"2018-12-11T12:08:58Z","status":"public","intvolume":"      2719","publist_id":"265","year":"2003","citation":{"ama":"Henzinger TA, Jhala R, Majumdar R. Counterexample-guided control. In: <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>. Vol 2719. Springer; 2003:886-902. doi:<a href=\"https://doi.org/10.1007/3-540-45061-0_69\">10.1007/3-540-45061-0_69</a>","ieee":"T. A. Henzinger, R. Jhala, and R. Majumdar, “Counterexample-guided control,” in <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>, Eindhoven, The Netherlands, 2003, vol. 2719, pp. 886–902.","ista":"Henzinger TA, Jhala R, Majumdar R. 2003. Counterexample-guided control. Proceedings of the 30th International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2719, 886–902.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the 30th International Colloquium on Automata, Languages and Programming, Springer, 2003, pp. 886–902.","chicago":"Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Counterexample-Guided Control.” In <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>, 2719:886–902. Springer, 2003. <a href=\"https://doi.org/10.1007/3-540-45061-0_69\">https://doi.org/10.1007/3-540-45061-0_69</a>.","apa":"Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2003). Counterexample-guided control. In <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i> (Vol. 2719, pp. 886–902). Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/3-540-45061-0_69\">https://doi.org/10.1007/3-540-45061-0_69</a>","mla":"Henzinger, Thomas A., et al. “Counterexample-Guided Control.” <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>, vol. 2719, Springer, 2003, pp. 886–902, doi:<a href=\"https://doi.org/10.1007/3-540-45061-0_69\">10.1007/3-540-45061-0_69</a>."},"quality_controlled":"1","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"}],"extern":"1","abstract":[{"text":"A major hurdle in the algorithmic verification and control of systems is the need to find suitable abstract models, which omit enough details to overcome the state-explosion problem, but retain enough details to exhibit satisfaction or controllability with respect to the specification. The paradigm of counterexample-guided abstraction refinement suggests a fully automatic way of finding suitable abstract models: one starts with a coarse abstraction, attempts to verify or control the abstract model, and if this attempt fails and the abstract counterexample does not correspond to a concrete counterexample, then one uses the spurious counterexample to guide the refinement of the abstract model. We present a counterexample-guided refinement algorithm for solving ω-regular control objectives. The main difficulty is that in control, unlike in verification, counterexamples are strategies in a game between system and controller. In the case that the controller has no choices, our scheme subsumes known counterexample-guided refinement algorithms for the verification of ω-regular specifications. Our algorithm is useful in all situations where ω-regular games need to be solved, such as supervisory control, sequential and program synthesis, and modular verification. The algorithm is fully symbolic, and therefore applicable also to infinite-state systems.","lang":"eng"}],"publication_status":"published","title":"Counterexample-guided control","publication":"Proceedings of the 30th International Colloquium on Automata, Languages and Programming","_id":"4462","date_published":"2003-06-25T00:00:00Z","page":"886 - 902","alternative_title":["LNCS"],"scopus_import":"1","publication_identifier":{"isbn":["9783540404934"]},"oa_version":"None","type":"conference","date_updated":"2024-01-10T11:19:41Z","day":"25","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This research was supported in part by the DARPA SEC grant F33615-C-98-3614, the ONR grant N00014-02-1-0671, and the NSF grants CCR-9988172, CCR-0085949, and CCR-0225610.","doi":"10.1007/3-540-45061-0_69","language":[{"iso":"eng"}]},{"day":"27","oa_version":"None","type":"conference","date_updated":"2024-01-10T11:05:53Z","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This work was supported in part by the NSF grants CCR-0085949 and CCR-0234690, the DARPA grant F33615-00-C-1693, and the MARCO grant 98-DT-660.","language":[{"iso":"eng"}],"doi":"10.1007/978-3-540-45069-6_27","page":"262 - 274","date_published":"2003-06-27T00:00:00Z","publication_identifier":{"isbn":["9783540405245"]},"alternative_title":["LNCS"],"year":"2003","extern":"1","quality_controlled":"1","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"}],"citation":{"apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Qadeer, S. (2003). Thread-modular abstraction refinement. In <i>Proceedings of the 15th International Conference on Computer Aided Verification</i> (Vol. 2725, pp. 262–274). Boulder, CO, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-540-45069-6_27\">https://doi.org/10.1007/978-3-540-45069-6_27</a>","mla":"Henzinger, Thomas A., et al. “Thread-Modular Abstraction Refinement.” <i>Proceedings of the 15th International Conference on Computer Aided Verification</i>, vol. 2725, Springer, 2003, pp. 262–74, doi:<a href=\"https://doi.org/10.1007/978-3-540-45069-6_27\">10.1007/978-3-540-45069-6_27</a>.","ama":"Henzinger TA, Jhala R, Majumdar R, Qadeer S. Thread-modular abstraction refinement. In: <i>Proceedings of the 15th International Conference on Computer Aided Verification</i>. Vol 2725. Springer; 2003:262-274. doi:<a href=\"https://doi.org/10.1007/978-3-540-45069-6_27\">10.1007/978-3-540-45069-6_27</a>","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer, “Thread-modular abstraction refinement,” in <i>Proceedings of the 15th International Conference on Computer Aided Verification</i>, Boulder, CO, USA, 2003, vol. 2725, pp. 262–274.","ista":"Henzinger TA, Jhala R, Majumdar R, Qadeer S. 2003. Thread-modular abstraction refinement. Proceedings of the 15th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2725, 262–274.","chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Shaz Qadeer. “Thread-Modular Abstraction Refinement.” In <i>Proceedings of the 15th International Conference on Computer Aided Verification</i>, 2725:262–74. Springer, 2003. <a href=\"https://doi.org/10.1007/978-3-540-45069-6_27\">https://doi.org/10.1007/978-3-540-45069-6_27</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, S. Qadeer, in:, Proceedings of the 15th International Conference on Computer Aided Verification, Springer, 2003, pp. 262–274."},"abstract":[{"text":"We present an algorithm called TAR (“Thread-modular Abstraction Refinement”) for model checking safety properties of concurrent software. The TAR algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that TAR explores the state space of one thread at a time, making assumptions about how the environment can interfere. The TAR algorithm uses counterexample-guided predicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at the same time environment assumptions are approximated from below. In our software verification tool BLAST we have implemented a fully automatic race checker for multithreaded C programs which is based on the TAR algorithm. This tool has verified a wide variety of commonly used locking idioms, including locking schemes that are not amenable to existing dynamic and static race checkers such as ERASER or WARLOCK.","lang":"eng"}],"publication_status":"published","_id":"4463","title":"Thread-modular abstraction refinement","publication":"Proceedings of the 15th International Conference on Computer Aided Verification","publisher":"Springer","volume":2725,"status":"public","month":"06","conference":{"location":"Boulder, CO, USA","start_date":"2003-07-08","end_date":"2003-07-12","name":"CAV: Computer Aided Verification"},"date_created":"2018-12-11T12:08:59Z","publist_id":"266","intvolume":"      2725"},{"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","day":"29","oa_version":"None","date_updated":"2024-01-10T11:33:57Z","type":"conference","language":[{"iso":"eng"}],"doi":"10.1007/978-3-540-45212-6_16","acknowledgement":"This work was supported by the AFOSR MURI grant F49620-00-1-0327, the California MICRO grant 01-037, the DARPA grant F33615-C-98-3614, the MARCO grant 98-DT-660, and the NSF grants CCR-0208875, CCR-0085949, and CCR-0225610.","page":"241 - 256","date_published":"2003-09-29T00:00:00Z","scopus_import":"1","publication_identifier":{"isbn":["9783540202233"]},"alternative_title":["LNCS"],"quality_controlled":"1","extern":"1","author":[{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"},{"last_name":"Matic","first_name":"Slobodan","full_name":"Matic, Slobodan"}],"citation":{"ista":"Henzinger TA, Kirsch C, Matic S. 2003. Schedule-carrying code. Proceedings of the 3rd International Conference on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2855, 241–256.","chicago":"Henzinger, Thomas A, Christoph Kirsch, and Slobodan Matic. “Schedule-Carrying Code.” In <i>Proceedings of the 3rd International Conference on Embedded Software</i>, 2855:241–56. ACM, 2003. <a href=\"https://doi.org/10.1007/978-3-540-45212-6_16\">https://doi.org/10.1007/978-3-540-45212-6_16</a>.","short":"T.A. Henzinger, C. Kirsch, S. Matic, in:, Proceedings of the 3rd International Conference on Embedded Software, ACM, 2003, pp. 241–256.","ieee":"T. A. Henzinger, C. Kirsch, and S. Matic, “Schedule-carrying code,” in <i>Proceedings of the 3rd International Conference on Embedded Software</i>, Philadelphia, PA, USA, 2003, vol. 2855, pp. 241–256.","ama":"Henzinger TA, Kirsch C, Matic S. Schedule-carrying code. In: <i>Proceedings of the 3rd International Conference on Embedded Software</i>. Vol 2855. ACM; 2003:241-256. doi:<a href=\"https://doi.org/10.1007/978-3-540-45212-6_16\">10.1007/978-3-540-45212-6_16</a>","mla":"Henzinger, Thomas A., et al. “Schedule-Carrying Code.” <i>Proceedings of the 3rd International Conference on Embedded Software</i>, vol. 2855, ACM, 2003, pp. 241–56, doi:<a href=\"https://doi.org/10.1007/978-3-540-45212-6_16\">10.1007/978-3-540-45212-6_16</a>.","apa":"Henzinger, T. A., Kirsch, C., &#38; Matic, S. (2003). Schedule-carrying code. In <i>Proceedings of the 3rd International Conference on Embedded Software</i> (Vol. 2855, pp. 241–256). Philadelphia, PA, USA: ACM. <a href=\"https://doi.org/10.1007/978-3-540-45212-6_16\">https://doi.org/10.1007/978-3-540-45212-6_16</a>"},"year":"2003","_id":"4464","publication":"Proceedings of the 3rd International Conference on Embedded Software","title":"Schedule-carrying code","abstract":[{"text":"We introduce the paradigm of schedule-carrying code (SCC). A hard real-time program can be executed on a given platform only if there exists a feasible schedule for the real-time tasks of the program. Traditionally, a scheduler determines the existence of a feasible schedule according to some scheduling strategy. With SCC, a compiler proves the existence of a feasible schedule by generating executable code that is attached to the program and represents its schedule. An SCC executable is a real-time program that carries its schedule as code, which is produced once and can be revalidated and executed with each use. We evaluate SCC both in theory and practice. In theory, we give two scenarios, of nonpreemptive and distributed scheduling for Giotto programs, where the generation of a feasible schedule is hard, while the validation of scheduling instructions that are attached to the programs is easy. In practice, we implement SCC and show that explicit scheduling instructions can reduce the scheduling overhead up to 35% and can provide an efficient, flexible, and verifiable means for compiling Giotto programs on complex architectures, such as the TTA.","lang":"eng"}],"publication_status":"published","volume":2855,"publisher":"ACM","publist_id":"267","intvolume":"      2855","status":"public","conference":{"end_date":"2003-10-15","name":"EMSOFT: Embedded Software ","location":"Philadelphia, PA, USA","start_date":"2003-10-13"},"month":"09","date_created":"2018-12-11T12:08:59Z"},{"page":"123 - 146","date_published":"2003-05-20T00:00:00Z","publisher":"Wiley-Blackwell","publication_identifier":{"isbn":["9780471234364 "]},"publist_id":"262","status":"public","month":"05","date_created":"2018-12-11T12:08:59Z","quality_controlled":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","article_processing_charge":"No","author":[{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Horowitz, Benjamin","first_name":"Benjamin","last_name":"Horowitz"},{"full_name":"Kirsch, Christoph","last_name":"Kirsch","first_name":"Christoph"}],"citation":{"short":"T.A. Henzinger, B. Horowitz, C. Kirsch, in:, Software-Enabled Control: Information Technology for Dynamical Systems, Wiley-Blackwell, 2003, pp. 123–146.","chicago":"Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Embedded Control Systems Development with Giotto.” In <i>Software-Enabled Control: Information Technology for Dynamical Systems</i>, 123–46. Wiley-Blackwell, 2003. <a href=\"https://doi.org/10.1002/047172288X.ch8\">https://doi.org/10.1002/047172288X.ch8</a>.","ista":"Henzinger TA, Horowitz B, Kirsch C. 2003.Embedded control systems development with Giotto. In: Software-Enabled Control: Information Technology for Dynamical Systems. , 123–146.","ieee":"T. A. Henzinger, B. Horowitz, and C. Kirsch, “Embedded control systems development with Giotto,” in <i>Software-Enabled Control: Information Technology for Dynamical Systems</i>, Wiley-Blackwell, 2003, pp. 123–146.","ama":"Henzinger TA, Horowitz B, Kirsch C. Embedded control systems development with Giotto. In: <i>Software-Enabled Control: Information Technology for Dynamical Systems</i>. Wiley-Blackwell; 2003:123-146. doi:<a href=\"https://doi.org/10.1002/047172288X.ch8\">10.1002/047172288X.ch8</a>","apa":"Henzinger, T. A., Horowitz, B., &#38; Kirsch, C. (2003). Embedded control systems development with Giotto. In <i>Software-Enabled Control: Information Technology for Dynamical Systems</i> (pp. 123–146). Wiley-Blackwell. <a href=\"https://doi.org/10.1002/047172288X.ch8\">https://doi.org/10.1002/047172288X.ch8</a>","mla":"Henzinger, Thomas A., et al. “Embedded Control Systems Development with Giotto.” <i>Software-Enabled Control: Information Technology for Dynamical Systems</i>, Wiley-Blackwell, 2003, pp. 123–46, doi:<a href=\"https://doi.org/10.1002/047172288X.ch8\">10.1002/047172288X.ch8</a>."},"year":"2003","day":"20","oa_version":"None","type":"book_chapter","date_updated":"2024-01-08T12:24:01Z","_id":"4465","doi":"10.1002/047172288X.ch8","language":[{"iso":"eng"}],"publication":"Software-Enabled Control: Information Technology for Dynamical Systems","title":"Embedded control systems development with Giotto","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"},{"publication_status":"published","abstract":[{"lang":"eng","text":"One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternationfree fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment."}],"_id":"4466","publication":"Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ","title":"On the universal and existential fragments of the mu-calculus","year":"2003","extern":"1","quality_controlled":"1","author":[{"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":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"}],"citation":{"mla":"Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of the Mu-Calculus.” <i>Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, vol. 2619, Springer, 2003, pp. 49–64, doi:<a href=\"https://doi.org/10.1007/3-540-36577-X_5\">10.1007/3-540-36577-X_5</a>.","apa":"Henzinger, T. A., Kupferman, O., &#38; Majumdar, R. (2003). On the universal and existential fragments of the mu-calculus. In <i>Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i> (Vol. 2619, pp. 49–64). Warsaw, Poland: Springer. <a href=\"https://doi.org/10.1007/3-540-36577-X_5\">https://doi.org/10.1007/3-540-36577-X_5</a>","chicago":"Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal and Existential Fragments of the Mu-Calculus.” In <i>Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, 2619:49–64. Springer, 2003. <a href=\"https://doi.org/10.1007/3-540-36577-X_5\">https://doi.org/10.1007/3-540-36577-X_5</a>.","short":"T.A. Henzinger, O. Kupferman, R. Majumdar, in:, Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Springer, 2003, pp. 49–64.","ista":"Henzinger TA, Kupferman O, Majumdar R. 2003. On the universal and existential fragments of the mu-calculus. Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 2619, 49–64.","ama":"Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments of the mu-calculus. In: <i>Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 2619. Springer; 2003:49-64. doi:<a href=\"https://doi.org/10.1007/3-540-36577-X_5\">10.1007/3-540-36577-X_5</a>","ieee":"T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential fragments of the mu-calculus,” in <i>Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, Warsaw, Poland, 2003, vol. 2619, pp. 49–64."},"status":"public","date_created":"2018-12-11T12:08:59Z","conference":{"start_date":"2003-04-07","location":"Warsaw, Poland","end_date":"2003-04-11","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"month":"03","publist_id":"263","intvolume":"      2619","publisher":"Springer","volume":2619,"acknowledgement":"This work was supported in part by NSF grant CCR-9988172, the AFOSR MURI grant F49620-00-1-0327, and a Microsoft Research Fellowship.","language":[{"iso":"eng"}],"doi":"10.1007/3-540-36577-X_5","day":"14","type":"conference","date_updated":"2024-01-08T13:17:35Z","oa_version":"None","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_identifier":{"isbn":["9783540008989"]},"alternative_title":["LNCS"],"page":"49 - 64","date_published":"2003-03-14T00:00:00Z"},{"volume":2648,"publisher":"Springer","intvolume":"      2648","publist_id":"264","date_created":"2018-12-11T12:09:00Z","month":"04","conference":{"location":"Portland, OR, USA","start_date":"2003-05-09","name":"SPIN: Model Checking Software","end_date":"2003-05-10"},"status":"public","citation":{"chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre. “Software Verification with BLAST.” In <i>Proceedings of the 10th International SPIN Workshop </i>, 2648:235–39. Springer, 2003. <a href=\"https://doi.org/10.1007/3-540-44829-2_17\">https://doi.org/10.1007/3-540-44829-2_17</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the 10th International SPIN Workshop , Springer, 2003, pp. 235–239.","ista":"Henzinger TA, Jhala R, Majumdar R, Sutre G. 2003. Software verification with BLAST. Proceedings of the 10th International SPIN Workshop . SPIN: Model Checking Software, LNCS, vol. 2648, 235–239.","ama":"Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with BLAST. In: <i>Proceedings of the 10th International SPIN Workshop </i>. Vol 2648. Springer; 2003:235-239. doi:<a href=\"https://doi.org/10.1007/3-540-44829-2_17\">10.1007/3-540-44829-2_17</a>","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Software verification with BLAST,” in <i>Proceedings of the 10th International SPIN Workshop </i>, Portland, OR, USA, 2003, vol. 2648, pp. 235–239.","mla":"Henzinger, Thomas A., et al. “Software Verification with BLAST.” <i>Proceedings of the 10th International SPIN Workshop </i>, vol. 2648, Springer, 2003, pp. 235–39, doi:<a href=\"https://doi.org/10.1007/3-540-44829-2_17\">10.1007/3-540-44829-2_17</a>.","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Sutre, G. (2003). Software verification with BLAST. In <i>Proceedings of the 10th International SPIN Workshop </i> (Vol. 2648, pp. 235–239). Portland, OR, USA: Springer. <a href=\"https://doi.org/10.1007/3-540-44829-2_17\">https://doi.org/10.1007/3-540-44829-2_17</a>"},"extern":"1","author":[{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"full_name":"Sutre, Grégoire","first_name":"Grégoire","last_name":"Sutre"}],"quality_controlled":"1","year":"2003","publication":"Proceedings of the 10th International SPIN Workshop ","title":"Software verification with BLAST","_id":"4467","publication_status":"published","abstract":[{"text":"BLAST (the Berkeley Lazy Abstraction Software verification Tool) is a verification system for checking safety properties of C programs using automatic property-driven construction and model checking of software abstractions. Blast implements an abstract-model check-refine loop to check for reachability of a specified label in the program. The abstract model is built on the fly using predicate abstraction. This model is then checked for reachability. If there is no (abstract) path to the specified error label, Blast reports that the system is safe and produces a succinct proof. Otherwise, it checks if the path is feasible using symbolic execution of the program. If the path is feasible, Blast outputs the path as an error trace, otherwise, it uses the infeasibility of the path to refine the abstract model. Blast short-circuits the loop from abstraction to verification to refinement, integrating the three steps tightly through “lazy abstraction” [5]. This integration can offer significant advantages in performance by avoiding the repetition of work from one iteration of the loop to the next. ","lang":"eng"}],"date_published":"2003-04-28T00:00:00Z","page":"235 - 239","alternative_title":["LNCS"],"publication_identifier":{"isbn":["9783540401179"]},"scopus_import":"1","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2024-01-08T14:05:29Z","type":"conference","oa_version":"None","day":"28","doi":"10.1007/3-540-44829-2_17","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the NSF grants CCR-0085949 and CCR-9988172, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, and a Microsoft Research Fellowship."},{"_id":"4468","title":"From control models to real-time code using Giotto","publication":"IEEE Control Systems Magazine","publication_status":"published","abstract":[{"text":"Giotto is a high-level programming language for time-triggered control applications. The authors begin with a conceptual overview of its methodology, discuss the Giotto helicopter project, and summarize available Giotto implementations.","lang":"eng"}],"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":"Kirsch, Christoph","last_name":"Kirsch","first_name":"Christoph"},{"full_name":"Sanvido, Marco","last_name":"Sanvido","first_name":"Marco"},{"last_name":"Pree","first_name":"Wolfgang","full_name":"Pree, Wolfgang"}],"quality_controlled":"1","extern":"1","citation":{"ama":"Henzinger TA, Kirsch C, Sanvido M, Pree W. From control models to real-time code using Giotto. <i>IEEE Control Systems Magazine</i>. 2003;23(1):50-64. doi:<a href=\"https://doi.org/10.1109/MCS.2003.1172829\">10.1109/MCS.2003.1172829</a>","ieee":"T. A. Henzinger, C. Kirsch, M. Sanvido, and W. Pree, “From control models to real-time code using Giotto,” <i>IEEE Control Systems Magazine</i>, vol. 23, no. 1. IEEE, pp. 50–64, 2003.","ista":"Henzinger TA, Kirsch C, Sanvido M, Pree W. 2003. From control models to real-time code using Giotto. IEEE Control Systems Magazine. 23(1), 50–64.","short":"T.A. Henzinger, C. Kirsch, M. Sanvido, W. Pree, IEEE Control Systems Magazine 23 (2003) 50–64.","chicago":"Henzinger, Thomas A, Christoph Kirsch, Marco Sanvido, and Wolfgang Pree. “From Control Models to Real-Time Code Using Giotto.” <i>IEEE Control Systems Magazine</i>. IEEE, 2003. <a href=\"https://doi.org/10.1109/MCS.2003.1172829\">https://doi.org/10.1109/MCS.2003.1172829</a>.","mla":"Henzinger, Thomas A., et al. “From Control Models to Real-Time Code Using Giotto.” <i>IEEE Control Systems Magazine</i>, vol. 23, no. 1, IEEE, 2003, pp. 50–64, doi:<a href=\"https://doi.org/10.1109/MCS.2003.1172829\">10.1109/MCS.2003.1172829</a>.","apa":"Henzinger, T. A., Kirsch, C., Sanvido, M., &#38; Pree, W. (2003). From control models to real-time code using Giotto. <i>IEEE Control Systems Magazine</i>. IEEE. <a href=\"https://doi.org/10.1109/MCS.2003.1172829\">https://doi.org/10.1109/MCS.2003.1172829</a>"},"year":"2003","publist_id":"260","intvolume":"        23","status":"public","date_created":"2018-12-11T12:09:00Z","month":"01","issue":"1","volume":23,"article_type":"original","publisher":"IEEE","language":[{"iso":"eng"}],"doi":"10.1109/MCS.2003.1172829","acknowledgement":"We thank Niklaus Wirth and Walter Schaufelberger for their advice and support of the reengineering effort of the ETH Zurich helicopter control system using Giotto. This research was supported in part by DARPA SEC grant F33615-C-98–3614, MARCO GSRC grant 98-DT-660, and AFOSR MURI grant F49620–00-1–0327. A preliminary version of this article appeared as [1].","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","day":"29","type":"journal_article","date_updated":"2024-01-08T10:54:53Z","oa_version":"None","publication_identifier":{"issn":["1066-033X "]},"scopus_import":"1","page":"50 - 64","date_published":"2003-01-29T00:00:00Z"},{"issue":"1","volume":91,"article_type":"original","publisher":"IEEE","intvolume":"        91","publist_id":"261","month":"01","date_created":"2018-12-11T12:09:00Z","status":"public","citation":{"ista":"Henzinger TA, Horowitz B, Kirsch C. 2003. Giotto: A time-triggered language for embedded programming. Proceedings of the IEEE. 91(1), 84–99.","chicago":"Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Giotto: A Time-Triggered Language for Embedded Programming.” <i>Proceedings of the IEEE</i>. IEEE, 2003. <a href=\"https://doi.org/10.1109/JPROC.2002.805825\">https://doi.org/10.1109/JPROC.2002.805825</a>.","short":"T.A. Henzinger, B. Horowitz, C. Kirsch, Proceedings of the IEEE 91 (2003) 84–99.","ieee":"T. A. Henzinger, B. Horowitz, and C. Kirsch, “Giotto: A time-triggered language for embedded programming,” <i>Proceedings of the IEEE</i>, vol. 91, no. 1. IEEE, pp. 84–99, 2003.","ama":"Henzinger TA, Horowitz B, Kirsch C. Giotto: A time-triggered language for embedded programming. <i>Proceedings of the IEEE</i>. 2003;91(1):84-99. doi:<a href=\"https://doi.org/10.1109/JPROC.2002.805825\">10.1109/JPROC.2002.805825</a>","apa":"Henzinger, T. A., Horowitz, B., &#38; Kirsch, C. (2003). Giotto: A time-triggered language for embedded programming. <i>Proceedings of the IEEE</i>. IEEE. <a href=\"https://doi.org/10.1109/JPROC.2002.805825\">https://doi.org/10.1109/JPROC.2002.805825</a>","mla":"Henzinger, Thomas A., et al. “Giotto: A Time-Triggered Language for Embedded Programming.” <i>Proceedings of the IEEE</i>, vol. 91, no. 1, IEEE, 2003, pp. 84–99, doi:<a href=\"https://doi.org/10.1109/JPROC.2002.805825\">10.1109/JPROC.2002.805825</a>."},"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Benjamin","last_name":"Horowitz","full_name":"Horowitz, Benjamin"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"}],"extern":"1","quality_controlled":"1","year":"2003","publication":"Proceedings of the IEEE","title":"Giotto: A time-triggered language for embedded programming","_id":"4469","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, actuator updates, 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","date_published":"2003-01-29T00:00:00Z","page":"84 - 99","scopus_import":"1","publication_identifier":{"issn":["0018-9219 "]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","oa_version":"None","date_updated":"2024-01-10T11:55:18Z","type":"journal_article","day":"29","language":[{"iso":"eng"}],"doi":"10.1109/JPROC.2002.805825","acknowledgement":"The authors would like to thank R. Majumdar for implementing a prototype Giotto compiler for Lego Mindstorms robots. They would like to thank D. Derevyanko and W. Williams for building the Intel x86 robots; and E. Lee and X. Liu for help with implementing Giotto as a “model of computation” in Ptolemy II [26]. Finally, they would also like to thank M. Sanvido for his suggestions on the design of the Giotto drivers; and P. Griffiths for implementing the functionality code of the electronic throttle controller."},{"volume":2855,"publisher":"ACM","publist_id":"148","intvolume":"      2855","status":"public","date_created":"2018-12-11T12:09:29Z","conference":{"location":"Philadelphia, PA, USA","start_date":"2003-10-13","end_date":"2003-10-15","name":"EMSOFT: Embedded Software "},"month":"09","author":[{"first_name":"Arindam","last_name":"Chakrabarti","full_name":"Chakrabarti, Arindam"},{"full_name":"De Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Stoelinga","first_name":"Mariëlle","full_name":"Stoelinga, Mariëlle"}],"quality_controlled":"1","extern":"1","citation":{"ama":"Chakrabarti A, De Alfaro L, Henzinger TA, Stoelinga M. Resource interfaces. In: <i>Third International Conference on Embedded Software</i>. Vol 2855. ACM; 2003:117-133. doi:<a href=\"https://doi.org/10.1007/978-3-540-45212-6_9\">10.1007/978-3-540-45212-6_9</a>","ieee":"A. Chakrabarti, L. De Alfaro, T. A. Henzinger, and M. Stoelinga, “Resource interfaces,” in <i>Third International Conference on Embedded Software</i>, Philadelphia, PA, USA, 2003, vol. 2855, pp. 117–133.","chicago":"Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, and Mariëlle Stoelinga. “Resource Interfaces.” In <i>Third International Conference on Embedded Software</i>, 2855:117–33. ACM, 2003. <a href=\"https://doi.org/10.1007/978-3-540-45212-6_9\">https://doi.org/10.1007/978-3-540-45212-6_9</a>.","short":"A. Chakrabarti, L. De Alfaro, T.A. Henzinger, M. Stoelinga, in:, Third International Conference on Embedded Software, ACM, 2003, pp. 117–133.","ista":"Chakrabarti A, De Alfaro L, Henzinger TA, Stoelinga M. 2003. Resource interfaces. Third International Conference on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2855, 117–133.","mla":"Chakrabarti, Arindam, et al. “Resource Interfaces.” <i>Third International Conference on Embedded Software</i>, vol. 2855, ACM, 2003, pp. 117–33, doi:<a href=\"https://doi.org/10.1007/978-3-540-45212-6_9\">10.1007/978-3-540-45212-6_9</a>.","apa":"Chakrabarti, A., De Alfaro, L., Henzinger, T. A., &#38; Stoelinga, M. (2003). Resource interfaces. In <i>Third International Conference on Embedded Software</i> (Vol. 2855, pp. 117–133). Philadelphia, PA, USA: ACM. <a href=\"https://doi.org/10.1007/978-3-540-45212-6_9\">https://doi.org/10.1007/978-3-540-45212-6_9</a>"},"year":"2003","_id":"4561","publication":"Third International Conference on Embedded Software","title":"Resource interfaces","publication_status":"published","abstract":[{"lang":"eng","text":"We present a formalism for specifying component interfaces that expose component requirements on limited resources. The formalism permits an algorithmic check if two or more components, when put together, exceed the available resources. Moreover, the formalism can be used to compute the quantity of resources necessary for satisfying the requirements of a collection of components. The formalism can be instantiated in several ways. For example, several components may draw power from the same source. Then, the formalism supports compatibility checks such as: can two components, when put together, achieve their tasks without ever exceeding the available amount of peak power? or, can they achieve their tasks by using no more than the initially available amount of energy (i.e., power accumulated over time)? The corresponding quantitative questions that our algorithms answer are the following: what is the amount of peak power needed for two components to be put together? what is the corresponding amount of initial energy? To solve these questions, we model interfaces with resource requirements as games with quantitative objectives. The games are played on state spaces where each state is labeled by a number (representing, e.g., power consumption), and a play produces an infinite path of labels. The objective may be, for example, to minimize the largest label that occurs during a play. We illustrate our approach by modeling compatibility questions for the components of robot control software, and of wireless sensor networks."}],"page":"117 - 133","date_published":"2003-09-29T00:00:00Z","publication_identifier":{"isbn":["9783540202233"]},"scopus_import":"1","alternative_title":["LNCS"],"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","day":"29","type":"conference","date_updated":"2024-01-08T10:48:11Z","oa_version":"None","language":[{"iso":"eng"}],"doi":"10.1007/978-3-540-45212-6_9","acknowledgement":"This research was supported in part by the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the ONR grant N00014-02-1-0671, and the NSF grants CCR-0085949, CCR-0132780, CCR-0234690, and CCR-9988172."},{"acknowledgement":"This research was supported in part by the NSF CAREER award CCR-0132780, the DARPA grant F33615-C-98-3614, the NSF grants CCR-9988172, CCR-0234690 and CCR-0225610, and the ONR grant N00014-02-1-0671.","language":[{"iso":"eng"}],"doi":"10.1007/3-540-45061-0_79","type":"conference","date_updated":"2023-07-26T13:07:31Z","oa_version":"None","day":"25","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","alternative_title":["LNCS"],"publication_identifier":{"isbn":["9783540404934"]},"scopus_import":"1","date_published":"2003-06-25T00:00:00Z","page":"1022 - 1037","publication_status":"published","abstract":[{"lang":"eng","text":"Discounting the future means that the value, today, of a unit payoffis 1 if the payoffo ccurs today, a if it occurs tomorrow, a 2 if it occurs the day after tomorrow, and so on, for some real-valued discount factor 0 &lt; a &lt; 1. Discounting (or inflation) is a key paradigm in economics and has been studied in Markov decision processes as well as game theory. We submit that discounting also has a natural place in systems engineering: for nonterminating systems, a potential bug in the far-away future is less troubling than a potential bug today. We therefore develop a systems theory with discounting. Our theory includes several basic elements: discounted versions of system properties that correspond to the ω-regular properties, fixpoint-based algorithms for checking discounted properties, and a quantitative notion of bisimilarity for capturing the difference between two states with respect to discounted properties. We present the theory in a general form that applies to probabilistic systems as well as multicomponent systems (games), but it readily specializes to classical transition systems. We show that discounting, besides its natural practical appeal, has also several mathematical benefits. First, the resulting theory is robust, in that small perturbations of a system can cause only small changes in the properties of the system. Second, the theory is computational, in that the values of discounted properties, as well as the discounted bisimilarity distance between states, can be computed to any desired degree of precision."}],"publication":"Proceedings of the 30th International Colloquium on Automata, Languages and Programming","title":"Discounting the future in systems theory","_id":"4628","year":"2003","citation":{"mla":"De Alfaro, Luca, et al. “Discounting the Future in Systems Theory.” <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>, vol. 2719, Springer, 2003, pp. 1022–37, doi:<a href=\"https://doi.org/10.1007/3-540-45061-0_79\">10.1007/3-540-45061-0_79</a>.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Majumdar, R. (2003). Discounting the future in systems theory. In <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i> (Vol. 2719, pp. 1022–1037). Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/3-540-45061-0_79\">https://doi.org/10.1007/3-540-45061-0_79</a>","ista":"De Alfaro L, Henzinger TA, Majumdar R. 2003. Discounting the future in systems theory. Proceedings of the 30th International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2719, 1022–1037.","short":"L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 30th International Colloquium on Automata, Languages and Programming, Springer, 2003, pp. 1022–1037.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Discounting the Future in Systems Theory.” In <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>, 2719:1022–37. Springer, 2003. <a href=\"https://doi.org/10.1007/3-540-45061-0_79\">https://doi.org/10.1007/3-540-45061-0_79</a>.","ama":"De Alfaro L, Henzinger TA, Majumdar R. Discounting the future in systems theory. In: <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>. Vol 2719. Springer; 2003:1022-1037. doi:<a href=\"https://doi.org/10.1007/3-540-45061-0_79\">10.1007/3-540-45061-0_79</a>","ieee":"L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Discounting the future in systems theory,” in <i>Proceedings of the 30th International Colloquium on Automata, Languages and Programming</i>, Eindhoven, The Netherlands, 2003, vol. 2719, pp. 1022–1037."},"extern":"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","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Majumdar, Ritankar","last_name":"Majumdar","first_name":"Ritankar"}],"quality_controlled":"1","date_created":"2018-12-11T12:09:50Z","month":"06","conference":{"name":"ICALP: Automata, Languages and Programming","end_date":"2003-07-04","location":"Eindhoven, The Netherlands","start_date":"2003-06-30"},"status":"public","intvolume":"      2719","publist_id":"77","publisher":"Springer","volume":2719},{"year":"2003","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"full_name":"Faella, Marco","last_name":"Faella","first_name":"Marco"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"},{"first_name":"Mariëlle","last_name":"Stoelinga","full_name":"Stoelinga, Mariëlle"}],"quality_controlled":"1","extern":"1","citation":{"mla":"De Alfaro, Luca, et al. “The Element of Surprise in Timed Games.” <i>Proceedings of the 14th International Conference on Concurrency Theory</i>, vol. 2761, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2003, pp. 144–58, doi:<a href=\"https://doi.org/10.1007/978-3-540-45187-7_9\">10.1007/978-3-540-45187-7_9</a>.","apa":"De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., &#38; Stoelinga, M. (2003). The element of surprise in timed games. In <i>Proceedings of the 14th International Conference on Concurrency Theory</i> (Vol. 2761, pp. 144–158). Marseille, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-540-45187-7_9\">https://doi.org/10.1007/978-3-540-45187-7_9</a>","short":"L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:, Proceedings of the 14th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2003, pp. 144–158.","chicago":"De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and Mariëlle Stoelinga. “The Element of Surprise in Timed Games.” In <i>Proceedings of the 14th International Conference on Concurrency Theory</i>, 2761:144–58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2003. <a href=\"https://doi.org/10.1007/978-3-540-45187-7_9\">https://doi.org/10.1007/978-3-540-45187-7_9</a>.","ista":"De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2003. The element of surprise in timed games. Proceedings of the 14th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2761, 144–158.","ama":"De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. The element of surprise in timed games. In: <i>Proceedings of the 14th International Conference on Concurrency Theory</i>. Vol 2761. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2003:144-158. doi:<a href=\"https://doi.org/10.1007/978-3-540-45187-7_9\">10.1007/978-3-540-45187-7_9</a>","ieee":"L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “The element of surprise in timed games,” in <i>Proceedings of the 14th International Conference on Concurrency Theory</i>, Marseille, France, 2003, vol. 2761, pp. 144–158."},"publication_status":"published","abstract":[{"lang":"eng","text":"We consider concurrent two-person games played in real time, in which the players decide both which action to play, and when to play it. Such timed games differ from untimed games in two essential ways. First, players can take each other by surprise, because actions are played with delays that cannot be anticipated by the opponent. Second, a player should not be able to win the game by preventing time from diverging. We present a model of timed games that preserves the element of surprise and accounts for time divergence in a way that treats both players symmetrically and applies to all ω-regular winning conditions. We prove that the ability to take each other by surprise adds extra power to the players. For the case that the games are specified in the style of timed automata, we provide symbolic algorithms for their solution with respect to all ω-regular winning conditions. We also show that for these timed games, memory strategies are more powerful than memoryless strategies already in the case of reachability objectives."}],"_id":"4630","title":"The element of surprise in timed games","publication":"Proceedings of the 14th International Conference on Concurrency Theory","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":2761,"status":"public","date_created":"2018-12-11T12:09:51Z","conference":{"end_date":"2003-09-05","name":"CONCUR: Concurrency Theory","location":"Marseille, France","start_date":"2003-09-03"},"month":"08","publist_id":"78","intvolume":"      2761","day":"21","type":"conference","date_updated":"2024-01-08T10:05:30Z","oa_version":"None","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"Supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA grant F33615-C-98-3614, the MARCO grant 98-DT-660, -the ONR grant N00014-02-1-0671, the NSF grants CCR-9988172, CCR-0225610, and CCR-0234690, the NSF CAREER award CCR-0132780, and the MIUR grant MEFISTO.","language":[{"iso":"eng"}],"doi":"10.1007/978-3-540-45187-7_9","page":"144 - 158","date_published":"2003-08-21T00:00:00Z","publication_identifier":{"isbn":["9783540407539"]},"scopus_import":"1","alternative_title":["LNCS"]},{"doi":"10.2166/nh.2002.0004","language":[{"iso":"eng"}],"day":"01","oa_version":"Published Version","date_updated":"2023-02-20T08:30:15Z","type":"journal_article","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","publication_identifier":{"eissn":["2224-7955"],"issn":["0029-1277"]},"page":"47-74","date_published":"2002-02-01T00:00:00Z","abstract":[{"text":"For many years considerable efforts have been put into investigating and modelling hydrological processes of mountainous catchments. On the one hand, the complexity and intrinsically high variability of the involved processes as well as insufficient knowledge of the underlying physical mechanisms still induce large uncertainties in understanding observed phenomena and predicting the behaviour of the system. On the other hand, the demand for models that are able to simulate mountainous water resource systems is increasing because of the needs related to both water exploitation and water conservation, which clearly call for an integrated vision and modelling of these systems.\r\nAccordingly, this paper moves from a brief survey of the most significant achievements in mountain hydrology to discuss what could be future challenging issues related to the broader spectrum of questions, which hydrologic modelling of mountainous river systems may face in the next decades. Firstly, reference is made to existing methodologies for modelling alpine water systems, focussing on some specific aspects that provide a basis for the discussion of the weaknesses and perspectives of present simulation tools. The future is thus discussed, delineating some of the research challenges that may foster a comprehensive and integrated vision of water related issues in mountainous regions.","lang":"eng"}],"publication_status":"published","_id":"12659","oa":1,"title":"Modelling mountainous water systems between learning and speculating looking for challenges","publication":"Hydrology Research","year":"2002","quality_controlled":"1","extern":"1","author":[{"last_name":"Burlando","first_name":"Paolo","full_name":"Burlando, Paolo"},{"last_name":"Pellicciotti","first_name":"Francesca","full_name":"Pellicciotti, Francesca","id":"b28f055a-81ea-11ed-b70c-a9fe7f7b0e70"},{"first_name":"Ulrich","last_name":"Strasser","full_name":"Strasser, Ulrich"}],"citation":{"ieee":"P. Burlando, F. Pellicciotti, and U. Strasser, “Modelling mountainous water systems between learning and speculating looking for challenges,” <i>Hydrology Research</i>, vol. 33, no. 1. IWA Publishing, pp. 47–74, 2002.","ama":"Burlando P, Pellicciotti F, Strasser U. Modelling mountainous water systems between learning and speculating looking for challenges. <i>Hydrology Research</i>. 2002;33(1):47-74. doi:<a href=\"https://doi.org/10.2166/nh.2002.0004\">10.2166/nh.2002.0004</a>","short":"P. Burlando, F. Pellicciotti, U. Strasser, Hydrology Research 33 (2002) 47–74.","chicago":"Burlando, Paolo, Francesca Pellicciotti, and Ulrich Strasser. “Modelling Mountainous Water Systems between Learning and Speculating Looking for Challenges.” <i>Hydrology Research</i>. IWA Publishing, 2002. <a href=\"https://doi.org/10.2166/nh.2002.0004\">https://doi.org/10.2166/nh.2002.0004</a>.","ista":"Burlando P, Pellicciotti F, Strasser U. 2002. Modelling mountainous water systems between learning and speculating looking for challenges. Hydrology Research. 33(1), 47–74.","apa":"Burlando, P., Pellicciotti, F., &#38; Strasser, U. (2002). Modelling mountainous water systems between learning and speculating looking for challenges. <i>Hydrology Research</i>. IWA Publishing. <a href=\"https://doi.org/10.2166/nh.2002.0004\">https://doi.org/10.2166/nh.2002.0004</a>","mla":"Burlando, Paolo, et al. “Modelling Mountainous Water Systems between Learning and Speculating Looking for Challenges.” <i>Hydrology Research</i>, vol. 33, no. 1, IWA Publishing, 2002, pp. 47–74, doi:<a href=\"https://doi.org/10.2166/nh.2002.0004\">10.2166/nh.2002.0004</a>."},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.2166/nh.2002.0004"}],"status":"public","month":"02","date_created":"2023-02-20T08:19:02Z","intvolume":"        33","article_type":"original","publisher":"IWA Publishing","volume":33,"issue":"1"},{"volume":55,"issue":"2","publisher":"Springer","article_type":"original","publist_id":"6787","intvolume":"        55","status":"public","date_created":"2018-12-11T11:48:53Z","month":"01","quality_controlled":"1","extern":"1","author":[{"full_name":"Perelygin, Andrey","last_name":"Perelygin","first_name":"Andrey"},{"orcid":"0000-0001-8243-4694","full_name":"Kondrashov, Fyodor","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","first_name":"Fyodor","last_name":"Kondrashov"},{"first_name":"Igor","last_name":"Rogozin","full_name":"Rogozin, Igor"},{"last_name":"Brinton","first_name":"Margo","full_name":"Brinton, Margo"}],"citation":{"chicago":"Perelygin, Andrey, Fyodor Kondrashov, Igor Rogozin, and Margo Brinton. “Evolution of the Mouse Polyubiquitin C Gene.” <i>Journal of Molecular Evolution</i>. Springer, 2002. <a href=\"https://doi.org/10.1007/s00239-002-2318-0\">https://doi.org/10.1007/s00239-002-2318-0</a>.","short":"A. Perelygin, F. Kondrashov, I. Rogozin, M. Brinton, Journal of Molecular Evolution 55 (2002) 202–210.","ista":"Perelygin A, Kondrashov F, Rogozin I, Brinton M. 2002. Evolution of the mouse polyubiquitin C gene. Journal of Molecular Evolution. 55(2), 202–210.","ieee":"A. Perelygin, F. Kondrashov, I. Rogozin, and M. Brinton, “Evolution of the mouse polyubiquitin C gene,” <i>Journal of Molecular Evolution</i>, vol. 55, no. 2. Springer, pp. 202–210, 2002.","ama":"Perelygin A, Kondrashov F, Rogozin I, Brinton M. Evolution of the mouse polyubiquitin C gene. <i>Journal of Molecular Evolution</i>. 2002;55(2):202-210. doi:<a href=\"https://doi.org/10.1007/s00239-002-2318-0\">10.1007/s00239-002-2318-0</a>","mla":"Perelygin, Andrey, et al. “Evolution of the Mouse Polyubiquitin C Gene.” <i>Journal of Molecular Evolution</i>, vol. 55, no. 2, Springer, 2002, pp. 202–10, doi:<a href=\"https://doi.org/10.1007/s00239-002-2318-0\">10.1007/s00239-002-2318-0</a>.","apa":"Perelygin, A., Kondrashov, F., Rogozin, I., &#38; Brinton, M. (2002). Evolution of the mouse polyubiquitin C gene. <i>Journal of Molecular Evolution</i>. Springer. <a href=\"https://doi.org/10.1007/s00239-002-2318-0\">https://doi.org/10.1007/s00239-002-2318-0</a>"},"year":"2002","_id":"859","publication":"Journal of Molecular Evolution","title":"Evolution of the mouse polyubiquitin C gene","pmid":1,"publication_status":"published","abstract":[{"lang":"eng","text":"The polymeric ubiquitin (poly-u) genes are composed of tandem 228-bp repeats with no spacer sequences between individual monomer units. Ubiquitin is one of the most conserved proteins known to date, and the individual units within a number of poly-u genes are significantly more similar to each other than would be expected if each unit evolved independently. It has been proposed that the rather striking similarity among poly-u monomers in some lineages is caused by a series of homogenization events. Here we report the sequences of the polyubiquitin-C (Ubc) genes in two mouse strains. Analysis of these sequences, as well as those of the previously reported Chinese hamster and rat poly-u genes, supports the assertion that the homogenization of the ubiquitin-C gene in rodents is due to unequal crossing-over events. The sequence divergence of noncoding DNA was used to estimate the frequency of unequal crossing-over events (6.3 x 10-5 events per generation) in the Ubc gene, as well as to provide evidence of apparent selection in the poly-u gene."}],"page":"202 - 210","date_published":"2002-01-01T00:00:00Z","external_id":{"pmid":["12107596"]},"publication_identifier":{"issn":["0022-2844"]},"scopus_import":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","day":"01","type":"journal_article","date_updated":"2023-07-26T12:01:34Z","oa_version":"None","doi":"10.1007/s00239-002-2318-0","language":[{"iso":"eng"}],"acknowledgement":"We are thankful to J.A. Southerland and P.L. Jiang for technical assistance in DNA sequencing, as well as to Y.I. Pavlov for helpful discussions. This work was supported by public Health Service Research Grant AI45135 from the Institute of Allergy and Infectious Diseases, National Institutes of Health."},{"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","oa_version":"Published Version","type":"journal_article","date_updated":"2023-07-26T11:48:27Z","day":"01","doi":"10.1186/gb-2002-3-2-research0008","language":[{"iso":"eng"}],"acknowledgement":"We are grateful to A.S. Kondrashov for numerous helpful suggestions, to I. King Jordan, M.A. Roytberg, J.L. Spouge and D.A. Kondrashov for useful discussions and to A.S. Kondrashov, I. King Jordan and D.J. Lipman for critical reading of the manuscript.","external_id":{"pmid":["11864370"]},"date_published":"2002-01-01T00:00:00Z","scopus_import":"1","publication_identifier":{"issn":["1465-6906"]},"main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC65685/"}],"citation":{"ama":"Kondrashov F, Rogozin I, Wolf Y, Koonin E. Selection in the evolution of gene duplications . <i>Genome Biology</i>. 2002;3(2). doi:<a href=\"https://doi.org/10.1186/gb-2002-3-2-research0008\">10.1186/gb-2002-3-2-research0008</a>","ieee":"F. Kondrashov, I. Rogozin, Y. Wolf, and E. Koonin, “Selection in the evolution of gene duplications ,” <i>Genome Biology</i>, vol. 3, no. 2. BioMed Central, 2002.","short":"F. Kondrashov, I. Rogozin, Y. Wolf, E. Koonin, Genome Biology 3 (2002).","chicago":"Kondrashov, Fyodor, Igor Rogozin, Yuri Wolf, and Eugene Koonin. “Selection in the Evolution of Gene Duplications .” <i>Genome Biology</i>. BioMed Central, 2002. <a href=\"https://doi.org/10.1186/gb-2002-3-2-research0008\">https://doi.org/10.1186/gb-2002-3-2-research0008</a>.","ista":"Kondrashov F, Rogozin I, Wolf Y, Koonin E. 2002. Selection in the evolution of gene duplications . Genome Biology. 3(2).","apa":"Kondrashov, F., Rogozin, I., Wolf, Y., &#38; Koonin, E. (2002). Selection in the evolution of gene duplications . <i>Genome Biology</i>. BioMed Central. <a href=\"https://doi.org/10.1186/gb-2002-3-2-research0008\">https://doi.org/10.1186/gb-2002-3-2-research0008</a>","mla":"Kondrashov, Fyodor, et al. “Selection in the Evolution of Gene Duplications .” <i>Genome Biology</i>, vol. 3, no. 2, BioMed Central, 2002, doi:<a href=\"https://doi.org/10.1186/gb-2002-3-2-research0008\">10.1186/gb-2002-3-2-research0008</a>."},"extern":"1","quality_controlled":"1","author":[{"last_name":"Kondrashov","first_name":"Fyodor","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","full_name":"Kondrashov, Fyodor","orcid":"0000-0001-8243-4694"},{"full_name":"Rogozin, Igor","first_name":"Igor","last_name":"Rogozin"},{"last_name":"Wolf","first_name":"Yuri","full_name":"Wolf, Yuri"},{"last_name":"Koonin","first_name":"Eugene","full_name":"Koonin, Eugene"}],"year":"2002","pmid":1,"publication":"Genome Biology","title":"Selection in the evolution of gene duplications ","_id":"871","oa":1,"abstract":[{"text":"BACKGROUND: Gene duplications have a major role in the evolution of new biological functions. Theoretical studies often assume that a duplication per se is selectively neutral and that, following a duplication, one of the gene copies is freed from purifying (stabilizing) selection, which creates the potential for evolution of a new function. RESULTS: In search of systematic evidence of accelerated evolution after duplication, we used data from 26 bacterial, six archaeal, and seven eukaryotic genomes to compare the mode and strength of selection acting on recently duplicated genes (paralogs) and on similarly diverged, unduplicated orthologous genes in different species. We find that the ratio of nonsynonymous to synonymous substitutions (Kn/Ks) in most paralogous pairs is &lt;&lt;1 and that paralogs typically evolve at similar rates, without significant asymmetry, indicating that both paralogs produced by a duplication are subject to purifying selection. This selection is, however, substantially weaker than the purifying selection affecting unduplicated orthologs that have diverged to the same extent as the analyzed paralogs. Most of the recently duplicated genes appear to be involved in various forms of environmental response; in particular, many of them encode membrane and secreted proteins. CONCLUSIONS: The results of this analysis indicate that recently duplicated paralogs evolve faster than orthologs with the same level of divergence and similar functions, but apparently do not experience a phase of neutral evolution. We hypothesize that gene duplications that persist in an evolving lineage are beneficial from the time of their origin, due primarily to a protein dosage effect in response to variable environmental conditions; duplications are likely to give rise to new functions at a later phase of their evolution once a higher level of divergence is reached.","lang":"eng"}],"publication_status":"published","issue":"2","volume":3,"article_type":"original","publisher":"BioMed Central","intvolume":"         3","publist_id":"6781","month":"01","date_created":"2018-12-11T11:48:57Z","status":"public"},{"publisher":"National Academy of Sciences","article_type":"original","volume":99,"issue":"23","month":"11","date_created":"2018-12-11T11:49:01Z","status":"public","intvolume":"        99","publist_id":"6763","year":"2002","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC137512/"}],"citation":{"apa":"Kondrashov, A., Sunyaev, S., &#38; Kondrashov, F. (2002). Dobzhansky-Muller incompatibilities in protein evolution. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.232565499\">https://doi.org/10.1073/pnas.232565499</a>","mla":"Kondrashov, Alexey, et al. “Dobzhansky-Muller Incompatibilities in Protein Evolution.” <i>PNAS</i>, vol. 99, no. 23, National Academy of Sciences, 2002, pp. 14878–83, doi:<a href=\"https://doi.org/10.1073/pnas.232565499\">10.1073/pnas.232565499</a>.","ista":"Kondrashov A, Sunyaev S, Kondrashov F. 2002. Dobzhansky-Muller incompatibilities in protein evolution. PNAS. 99(23), 14878–14883.","chicago":"Kondrashov, Alexey, Shamil Sunyaev, and Fyodor Kondrashov. “Dobzhansky-Muller Incompatibilities in Protein Evolution.” <i>PNAS</i>. National Academy of Sciences, 2002. <a href=\"https://doi.org/10.1073/pnas.232565499\">https://doi.org/10.1073/pnas.232565499</a>.","short":"A. Kondrashov, S. Sunyaev, F. Kondrashov, PNAS 99 (2002) 14878–14883.","ieee":"A. Kondrashov, S. Sunyaev, and F. Kondrashov, “Dobzhansky-Muller incompatibilities in protein evolution,” <i>PNAS</i>, vol. 99, no. 23. National Academy of Sciences, pp. 14878–14883, 2002.","ama":"Kondrashov A, Sunyaev S, Kondrashov F. Dobzhansky-Muller incompatibilities in protein evolution. <i>PNAS</i>. 2002;99(23):14878-14883. doi:<a href=\"https://doi.org/10.1073/pnas.232565499\">10.1073/pnas.232565499</a>"},"quality_controlled":"1","author":[{"last_name":"Kondrashov","first_name":"Alexey","full_name":"Kondrashov, Alexey"},{"last_name":"Sunyaev","first_name":"Shamil","full_name":"Sunyaev, Shamil"},{"first_name":"Fyodor","last_name":"Kondrashov","full_name":"Kondrashov, Fyodor","orcid":"0000-0001-8243-4694","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87"}],"extern":"1","abstract":[{"lang":"eng","text":"We study fitness landscape in the space of protein sequences by relating sets of human pathogenic missense mutations in 32 proteins to amino acid substitutions that occurred in the course of evolution of these proteins. On average, ≈10% of deviations of a nonhuman protein from its human ortholog are compensated pathogenic deviations (CPDs), i.e., are caused by an amino acid substitution that, at this site, would be pathogenic to humans. Normal functioning of a CPD-containing protein must be caused by other, compensatory deviations of the nonhuman species from humans. Together, a CPD and the corresponding compensatory deviation form a Dobzhansky-Muller incompatibility that can be visualized as the corner on a fitness ridge. Thus, proteins evolve along fitness ridges which contain only ≈10 steps between sucessive corners. The fraction of CPDs among all deviations of a protein from its human ortholog does not increase with the evolutionary distance between the proteins, indicating that subtitutions that carry evolving proteins around these corners occur in rapid succession, driven by positive selection. Data on fitness of interspecies hybrids suggest that the compensatory change that makes a CPD fit usually occurs within the same protein. Data on protein structures and on cooccurrence of amino acids at different sites of multiple orthologous proteins often make it possible to provisionally identify the substitution that compensates a partiCUlar CPD."}],"publication_status":"published","pmid":1,"title":"Dobzhansky-Muller incompatibilities in protein evolution","publication":"PNAS","_id":"885","oa":1,"external_id":{"pmid":["12403824"]},"date_published":"2002-11-12T00:00:00Z","page":"14878 - 14883","scopus_import":"1","publication_identifier":{"issn":["0027-8424"]},"oa_version":"Published Version","date_updated":"2023-07-26T09:48:37Z","type":"journal_article","day":"12","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","language":[{"iso":"eng"}],"doi":"10.1073/pnas.232565499"},{"oa_version":"None","date_updated":"2023-07-26T09:45:30Z","type":"journal_article","day":"01","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"We are grateful to A. Kondrashov, I. Rogozin and A. Feldman for reading the manuscript and P. Bouman, J. Cherry, J. Blumensteil and T. Kim for discussion.","doi":"10.1038/ng940","language":[{"iso":"eng"}],"external_id":{"pmid":["12134150"]},"date_published":"2002-08-01T00:00:00Z","page":"415 - 418","scopus_import":"1","year":"2002","citation":{"mla":"Castillo Davis, Cristian, et al. “Selection for Short Introns in Highly Expressed Genes.” <i>Nature Genetics</i>, vol. 31, no. 4, Nature Publishing Group, 2002, pp. 415–18, doi:<a href=\"https://doi.org/10.1038/ng940\">10.1038/ng940</a>.","apa":"Castillo Davis, C., Mekhedov, S., Hartl, D., Koonin, E., &#38; Kondrashov, F. (2002). Selection for short introns in highly expressed genes. <i>Nature Genetics</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/ng940\">https://doi.org/10.1038/ng940</a>","ista":"Castillo Davis C, Mekhedov S, Hartl D, Koonin E, Kondrashov F. 2002. Selection for short introns in highly expressed genes. Nature Genetics. 31(4), 415–418.","chicago":"Castillo Davis, Cristian, Sergei Mekhedov, Daniel Hartl, Eugene Koonin, and Fyodor Kondrashov. “Selection for Short Introns in Highly Expressed Genes.” <i>Nature Genetics</i>. Nature Publishing Group, 2002. <a href=\"https://doi.org/10.1038/ng940\">https://doi.org/10.1038/ng940</a>.","short":"C. Castillo Davis, S. Mekhedov, D. Hartl, E. Koonin, F. Kondrashov, Nature Genetics 31 (2002) 415–418.","ieee":"C. Castillo Davis, S. Mekhedov, D. Hartl, E. Koonin, and F. Kondrashov, “Selection for short introns in highly expressed genes,” <i>Nature Genetics</i>, vol. 31, no. 4. Nature Publishing Group, pp. 415–418, 2002.","ama":"Castillo Davis C, Mekhedov S, Hartl D, Koonin E, Kondrashov F. Selection for short introns in highly expressed genes. <i>Nature Genetics</i>. 2002;31(4):415-418. doi:<a href=\"https://doi.org/10.1038/ng940\">10.1038/ng940</a>"},"quality_controlled":"1","extern":"1","author":[{"last_name":"Castillo Davis","first_name":"Cristian","full_name":"Castillo Davis, Cristian"},{"last_name":"Mekhedov","first_name":"Sergei","full_name":"Mekhedov, Sergei"},{"full_name":"Hartl, Daniel","last_name":"Hartl","first_name":"Daniel"},{"full_name":"Koonin, Eugene","last_name":"Koonin","first_name":"Eugene"},{"id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8243-4694","full_name":"Kondrashov, Fyodor","last_name":"Kondrashov","first_name":"Fyodor"}],"abstract":[{"lang":"eng","text":"Transcription is a slow and expensive process: in eukaryotes, approximately 20 nucleotides can be transcribed per second at the expense of at least two ATP molecules per nucleotide. Thus, at least for highly expressed genes, transcription of long introns, which are particularly common in mammals, is costly. Using data on the expression of genes that encode proteins in Caenorhabditis elegans and Homo sapiens, we show that introns in highly expressed genes are substantially shorter than those in genes that are expressed at low levels. This difference is greater in humans, such that introns are, on average, 14 times shorter in highly expressed genes than in genes with low expression, whereas in C. Elegans the difference in intron length is only twofold. In contrast, the density of introns in a gene does not strongly depend on the level of gene expression. Thus, natural selection appears to favor short introns in highly expressed genes to minimize the cost of transcription and other molecular processes, such as splicing.\r\n"}],"publication_status":"published","pmid":1,"publication":"Nature Genetics","title":"Selection for short introns in highly expressed genes","_id":"897","article_type":"original","publisher":"Nature Publishing Group","volume":31,"issue":"4","month":"08","date_created":"2018-12-11T11:49:05Z","status":"public","intvolume":"        31","publist_id":"6751"},{"publication_identifier":{"issn":["1010-6030"]},"publist_id":"5387","intvolume":"       149","status":"public","date_created":"2018-12-11T11:53:44Z","month":"06","volume":149,"page":"191 - 198","issue":"1-3","date_published":"2002-06-28T00:00:00Z","publisher":"Elsevier","doi":"10.1016/S1010-6030(02)00027-8","language":[{"iso":"eng"}],"_id":"1737","publication":"Journal of Photochemistry and Photobiology A: Chemistry","title":"A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency solid-state dye-sensitized solar cells","publication_status":"published","abstract":[{"lang":"eng","text":"A new solvent-free composite polymer electrolyte consisting of high-molecular mass polyethylene oxide (PEO) filled with titanium oxide and containing LiI and I2 was developed. The introduction of the inorganic filler (TiO2 Degussa P25) into the polymer matrix produces dramatic morphological changes to the host polymer structure. Upon addition of the inorganic oxide, the surface roughness increases, with respect to the original polymer and in parallel, the fractal dimension decreases. Both the thermograms and the atomic force microscope (AFM) pictures confirm the amorphicity of the composite electrolyte. The polymer sub-units are held together in a parallel orientation, forming straight long chains of about 500 nm in width, along which TiO2 spherical particles of about 20-25 nm in diameter are distributed. The polymer chains separated by the titania particles are arranged in a three-dimensional, mechanically stable network, that creates free space and voids into which the iodide/triodide anions can easily migrate. All solid-state dye-sensitized solar cells fabricated using this composite electrolyte present high efficiencies (typical maximum incident photon to current efficiency (IPCE) as high as 40% at 520 nm and overall conversion efficiency (η) of 0.96% (Voc = 0.67 V, Jsc = 2.050 mA/cm2, FF = 39%) under direct solar irradiation. Further improvement of the photovoltaic performance is expected by optimization of the electrolyte parameters and of the cell assembly."}],"acknowledgement":"Financial support from NCSR “Demokritos” (Dimoerevna 598 project), Empeirikeion Foundation and General Secretariat for Research and Technology of Greece (EPET II, Greece–France and Greece–Czech Republic bilateral collaboration projects) is also greatly acknowledged. G. Katsaros thanks the Greek State Scholarships Foundation (IKY) for fellowship allowance","article_processing_charge":"No","author":[{"first_name":"Georgios","last_name":"Katsaros","full_name":"Katsaros, Georgios","id":"38DB5788-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas","last_name":"Stergiopoulos","full_name":"Stergiopoulos, Thomas"},{"last_name":"Arabatzis","first_name":"Iannis","full_name":"Arabatzis, Iannis"},{"last_name":"Papadokostaki","first_name":"Kyriaki","full_name":"Papadokostaki, Kyriaki"},{"full_name":"Falaras, Polycarpos","last_name":"Falaras","first_name":"Polycarpos"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","citation":{"mla":"Katsaros, Georgios, et al. “A Solvent-Free Composite Polymer/Inorganic Oxide Electrolyte for High Efficiency Solid-State Dye-Sensitized Solar Cells.” <i>Journal of Photochemistry and Photobiology A: Chemistry</i>, vol. 149, no. 1–3, Elsevier, 2002, pp. 191–98, doi:<a href=\"https://doi.org/10.1016/S1010-6030(02)00027-8\">10.1016/S1010-6030(02)00027-8</a>.","apa":"Katsaros, G., Stergiopoulos, T., Arabatzis, I., Papadokostaki, K., &#38; Falaras, P. (2002). A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency solid-state dye-sensitized solar cells. <i>Journal of Photochemistry and Photobiology A: Chemistry</i>. Elsevier. <a href=\"https://doi.org/10.1016/S1010-6030(02)00027-8\">https://doi.org/10.1016/S1010-6030(02)00027-8</a>","ieee":"G. Katsaros, T. Stergiopoulos, I. Arabatzis, K. Papadokostaki, and P. Falaras, “A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency solid-state dye-sensitized solar cells,” <i>Journal of Photochemistry and Photobiology A: Chemistry</i>, vol. 149, no. 1–3. Elsevier, pp. 191–198, 2002.","ama":"Katsaros G, Stergiopoulos T, Arabatzis I, Papadokostaki K, Falaras P. A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency solid-state dye-sensitized solar cells. <i>Journal of Photochemistry and Photobiology A: Chemistry</i>. 2002;149(1-3):191-198. doi:<a href=\"https://doi.org/10.1016/S1010-6030(02)00027-8\">10.1016/S1010-6030(02)00027-8</a>","ista":"Katsaros G, Stergiopoulos T, Arabatzis I, Papadokostaki K, Falaras P. 2002. A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency solid-state dye-sensitized solar cells. Journal of Photochemistry and Photobiology A: Chemistry. 149(1–3), 191–198.","chicago":"Katsaros, Georgios, Thomas Stergiopoulos, Iannis Arabatzis, Kyriaki Papadokostaki, and Polycarpos Falaras. “A Solvent-Free Composite Polymer/Inorganic Oxide Electrolyte for High Efficiency Solid-State Dye-Sensitized Solar Cells.” <i>Journal of Photochemistry and Photobiology A: Chemistry</i>. Elsevier, 2002. <a href=\"https://doi.org/10.1016/S1010-6030(02)00027-8\">https://doi.org/10.1016/S1010-6030(02)00027-8</a>.","short":"G. Katsaros, T. Stergiopoulos, I. Arabatzis, K. Papadokostaki, P. Falaras, Journal of Photochemistry and Photobiology A: Chemistry 149 (2002) 191–198."},"day":"28","year":"2002","date_updated":"2023-07-26T08:56:55Z","type":"journal_article","oa_version":"None"},{"author":[{"full_name":"Falaras, Polycarpos","first_name":"Polycarpos","last_name":"Falaras"},{"first_name":"Katerina","last_name":"Chryssou","full_name":"Chryssou, Katerina"},{"last_name":"Stergiopoulos","first_name":"Thomas","full_name":"Stergiopoulos, Thomas"},{"last_name":"Arabatzis","first_name":"Ioannis","full_name":"Arabatzis, Ioannis M"},{"full_name":"Georgios Katsaros","id":"38DB5788-F248-11E8-B48F-1D18A9856A87","first_name":"Georgios","last_name":"Katsaros"},{"last_name":"Catalano","first_name":"Vincent","full_name":"Catalano, Vincent J"},{"first_name":"Raif","last_name":"Kurtaran","full_name":"Kurtaran, Raif"},{"last_name":"Hugot Le Goff","first_name":"Anne","full_name":"Hugot-Le Goff, Anne"},{"last_name":"Bernard","first_name":"Marie","full_name":"Bernard, Marie C"}],"quality_controlled":0,"extern":1,"citation":{"ista":"Falaras P, Chryssou K, Stergiopoulos T, Arabatzis I, Katsaros G, Catalano V, Kurtaran R, Hugot Le Goff A, Bernard M. 2002. Dye-sensitization of titanium dioxide thin films by Ru(II)-bpp-bpy complexes. Organic Photovoltaics vol. 4801, 125–135.","chicago":"Falaras, Polycarpos, Katerina Chryssou, Thomas Stergiopoulos, Ioannis Arabatzis, Georgios Katsaros, Vincent Catalano, Raif Kurtaran, Anne Hugot Le Goff, and Marie Bernard. “Dye-Sensitization of Titanium Dioxide Thin Films by Ru(II)-Bpp-Bpy Complexes,” 4801:125–35. SPIE, 2002. <a href=\"https://doi.org/10.1117/12.452446\">https://doi.org/10.1117/12.452446</a>.","short":"P. Falaras, K. Chryssou, T. Stergiopoulos, I. Arabatzis, G. Katsaros, V. Catalano, R. Kurtaran, A. Hugot Le Goff, M. Bernard, in:, SPIE, 2002, pp. 125–135.","ama":"Falaras P, Chryssou K, Stergiopoulos T, et al. Dye-sensitization of titanium dioxide thin films by Ru(II)-bpp-bpy complexes. In: Vol 4801. SPIE; 2002:125-135. doi:<a href=\"https://doi.org/10.1117/12.452446\">10.1117/12.452446</a>","ieee":"P. Falaras <i>et al.</i>, “Dye-sensitization of titanium dioxide thin films by Ru(II)-bpp-bpy complexes,” presented at the Organic Photovoltaics, 2002, vol. 4801, pp. 125–135.","apa":"Falaras, P., Chryssou, K., Stergiopoulos, T., Arabatzis, I., Katsaros, G., Catalano, V., … Bernard, M. (2002). Dye-sensitization of titanium dioxide thin films by Ru(II)-bpp-bpy complexes (Vol. 4801, pp. 125–135). Presented at the Organic Photovoltaics, SPIE. <a href=\"https://doi.org/10.1117/12.452446\">https://doi.org/10.1117/12.452446</a>","mla":"Falaras, Polycarpos, et al. <i>Dye-Sensitization of Titanium Dioxide Thin Films by Ru(II)-Bpp-Bpy Complexes</i>. Vol. 4801, SPIE, 2002, pp. 125–35, doi:<a href=\"https://doi.org/10.1117/12.452446\">10.1117/12.452446</a>."},"year":"2002","day":"01","date_updated":"2021-01-12T06:52:53Z","type":"conference","_id":"1738","doi":"10.1117/12.452446","title":"Dye-sensitization of titanium dioxide thin films by Ru(II)-bpp-bpy complexes","abstract":[{"text":"New dyes of the type Ru(II)(bdmpp)(bpy) [where bdmpp is 2,6-bis(3,5-dimethyl-N-pyrazoyl)pyridine and bpy is 2,2′-bipyridine-4,4′-dicarboxylic acid] are prepared and characterized by infra-red (IR), mass (MS) and electrospray mass spectroscopy (ES-MS) as well as 1H NMR (1D and 2D) spectroscopies. The compounds present broad and very high intensity MLCT absorption bands in the visible and can be chemically anchored on TiO2 films via ester-like linkage involving carboxylato groups. These complexes have been tested with success as potential molecular antennas in dye-sensitized solar cells. Both opaque and transparent nanocrystalline TiO2 thin film electrodes obtained by a doctor blade technique sensitized by these complexes were incorporated in a sandwich type regenerative photoelectrochemical solar cell containing 0.1M LiI +0.01M I2 in propylene carbonate as well as a platinized conductive glass counter electrode. The cell was characterized by Raman spectroscopy under anodic and cathodic bias. Two new vibration bands were observed in the lower frequency region. The first one at 112 cm-1 is due to tri-iodide formed on the photoactive electrode, and the second one at 167 cm-1 is a sign of the dye/iodide interaction and corresponds to a vibration in a chemically stable &quot;DI&quot; intermediate species. Under direct sunlight illumination (solar irradiance of 60 mW/cm2) by using a composite polymer solid state electrolyte, the cell ITO/TiO2/[Ru(II)(bdmpp)(bpy)(NCS)](PF6)/electrolyte/Pt-ITO produced a continuous photocurrent as high as 4.29mA/cm2, and gave IPCE values about half of the corresponding values obtained by the standard N3 dye under the same conditions. The photovoltage is about 600 mV and the overall energy conversion cell's efficiency is as high as 1.72%.","lang":"eng"}],"publication_status":"published","page":"125 - 135","volume":4801,"date_published":"2002-01-01T00:00:00Z","publisher":"SPIE","publist_id":"5385","intvolume":"      4801","status":"public","month":"01","conference":{"name":"Organic Photovoltaics"},"date_created":"2018-12-11T11:53:45Z"},{"citation":{"mla":"Stergiopoulos, Thomas, et al. “Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells.” <i>Nano Letters</i>, vol. 2, no. 11, American Chemical Society, 2002, pp. 1259–61, doi:<a href=\"https://doi.org/10.1021/nl025798u\">10.1021/nl025798u</a>.","apa":"Stergiopoulos, T., Arabatzis, I., Katsaros, G., &#38; Falaras, P. (2002). Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells. <i>Nano Letters</i>. American Chemical Society. <a href=\"https://doi.org/10.1021/nl025798u\">https://doi.org/10.1021/nl025798u</a>","ieee":"T. Stergiopoulos, I. Arabatzis, G. Katsaros, and P. Falaras, “Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells,” <i>Nano Letters</i>, vol. 2, no. 11. American Chemical Society, pp. 1259–1261, 2002.","ama":"Stergiopoulos T, Arabatzis I, Katsaros G, Falaras P. Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells. <i>Nano Letters</i>. 2002;2(11):1259-1261. doi:<a href=\"https://doi.org/10.1021/nl025798u\">10.1021/nl025798u</a>","ista":"Stergiopoulos T, Arabatzis I, Katsaros G, Falaras P. 2002. Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells. Nano Letters. 2(11), 1259–1261.","short":"T. Stergiopoulos, I. Arabatzis, G. Katsaros, P. Falaras, Nano Letters 2 (2002) 1259–1261.","chicago":"Stergiopoulos, Thomas, Iannis Arabatzis, Georgios Katsaros, and Polycarpos Falaras. “Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells.” <i>Nano Letters</i>. American Chemical Society, 2002. <a href=\"https://doi.org/10.1021/nl025798u\">https://doi.org/10.1021/nl025798u</a>."},"author":[{"full_name":"Stergiopoulos, Thomas","last_name":"Stergiopoulos","first_name":"Thomas"},{"first_name":"Iannis","last_name":"Arabatzis","full_name":"Arabatzis, Iannis M"},{"full_name":"Georgios Katsaros","id":"38DB5788-F248-11E8-B48F-1D18A9856A87","last_name":"Katsaros","first_name":"Georgios"},{"last_name":"Falaras","first_name":"Polycarpos","full_name":"Falaras, Polycarpos"}],"extern":1,"quality_controlled":0,"date_updated":"2021-01-12T06:52:53Z","type":"journal_article","year":"2002","day":"01","publication":"Nano Letters","title":"Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells","_id":"1739","doi":"10.1021/nl025798u","acknowledgement":"Financial support from NCSR “Demokritos” and GSRT-Greece is greatly acknowledged. ","abstract":[{"text":"Poly(ethylene oxide)/titania polymer electrolyte based photoelectrochemical cells have been fabricated with Ru(dcbpy)2(NCS)2 complex as the sensitizer and nanoporous TiO2 films as photoanodes. The introduction of the titania filler into the poly(ethylene oxide) matrix reduces the crystallinity of the polymer and enhances the mobility of the 1-/13 - redox couple, resulting in outstanding overall conversion efficiency (4.2% under direct sunlight illumination) of the corresponding dye-sensitized nanocrystalline TiO2 solar cell, one of the best efficiencies reported to date for a solid-state device.","lang":"eng"}],"publication_status":"published","date_published":"2002-11-01T00:00:00Z","page":"1259 - 1261","issue":"11","volume":2,"publisher":"American Chemical Society","intvolume":"         2","publist_id":"5386","month":"11","date_created":"2018-12-11T11:53:45Z","status":"public"},{"date_published":"2002-10-02T00:00:00Z","page":"293 - 318","scopus_import":"1","publication_identifier":{"issn":["0022-314X"]},"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"Published Version","date_updated":"2023-07-26T12:15:14Z","type":"journal_article","day":"02","language":[{"iso":"eng"}],"doi":"10.1006/jnth.2002.2800","volume":96,"issue":"2","publisher":"Academic Press","article_type":"original","intvolume":"        96","publist_id":"7708","month":"10","date_created":"2018-12-11T11:45:11Z","status":"public","citation":{"apa":"Browning, T. D. (2002). Equal Sums of Two kth Powers. <i>Journal of Number Theory</i>. Academic Press. <a href=\"https://doi.org/10.1006/jnth.2002.2800\">https://doi.org/10.1006/jnth.2002.2800</a>","mla":"Browning, Timothy D. “Equal Sums of Two Kth Powers.” <i>Journal of Number Theory</i>, vol. 96, no. 2, Academic Press, 2002, pp. 293–318, doi:<a href=\"https://doi.org/10.1006/jnth.2002.2800\">10.1006/jnth.2002.2800</a>.","ieee":"T. D. Browning, “Equal Sums of Two kth Powers,” <i>Journal of Number Theory</i>, vol. 96, no. 2. Academic Press, pp. 293–318, 2002.","ama":"Browning TD. Equal Sums of Two kth Powers. <i>Journal of Number Theory</i>. 2002;96(2):293-318. doi:<a href=\"https://doi.org/10.1006/jnth.2002.2800\">10.1006/jnth.2002.2800</a>","ista":"Browning TD. 2002. Equal Sums of Two kth Powers. Journal of Number Theory. 96(2), 293–318.","short":"T.D. Browning, Journal of Number Theory 96 (2002) 293–318.","chicago":"Browning, Timothy D. “Equal Sums of Two Kth Powers.” <i>Journal of Number Theory</i>. Academic Press, 2002. <a href=\"https://doi.org/10.1006/jnth.2002.2800\">https://doi.org/10.1006/jnth.2002.2800</a>."},"author":[{"orcid":"0000-0002-8314-0177","full_name":"Browning, Timothy D","id":"35827D50-F248-11E8-B48F-1D18A9856A87","last_name":"Browning","first_name":"Timothy D"}],"extern":"1","quality_controlled":"1","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"year":"2002","publication":"Journal of Number Theory","title":"Equal Sums of Two kth Powers","_id":"204","abstract":[{"text":"Let k⩾5 be an integer, and let x⩾1 be an arbitrary real number. We derive a bound[Formula presented] for the number of positive integers less than or equal to x which can be represented as a sum of two non-negative coprime kth powers, in essentially more than one way.","lang":"eng"}],"publication_status":"published"}]