--- _id: '4436' abstract: - lang: eng text: We present an assume-guarantee interface algebra for real-time components. In our formalism a component implements a set of task sequences that share a resource. A component interface consists of an arrival rate function and a latency for each task sequence, and a capacity function for the shared resource. The interface specifies that the component guarantees certain task latencies depending on assumptions about task arrival rates and allocated resource capacities. Our algebra defines compatibility and refinement relations on interfaces. Interface compatibility can be checked on partial designs, even when some component interfaces are yet unknown. In this case interface composition computes as new assumptions the weakest constraints on the unknown components that are necessary to satisfy the specified guarantees. Interface refinement is defined in a way that ensures that compatible interfaces can be refined and implemented independently. Our algebra thus formalizes an interface-based design methodology that supports both the incremental addition of new components and the independent stepwise refinement of existing components. We demonstrate the flexibility and efficiency of the framework through simulation experiments. author: - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Slobodan full_name: Matic, Slobodan last_name: Matic citation: ama: 'Henzinger TA, Matic S. An interface algebra for real-time components. In: IEEE; 2006:253-266. doi:10.1109/RTAS.2006.11' apa: 'Henzinger, T. A., & Matic, S. (2006). An interface algebra for real-time components (pp. 253–266). Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, IEEE. https://doi.org/10.1109/RTAS.2006.11' chicago: Henzinger, Thomas A, and Slobodan Matic. “An Interface Algebra for Real-Time Components,” 253–66. IEEE, 2006. https://doi.org/10.1109/RTAS.2006.11. ieee: 'T. A. Henzinger and S. Matic, “An interface algebra for real-time components,” presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, 2006, pp. 253–266.' ista: 'Henzinger TA, Matic S. 2006. An interface algebra for real-time components. RTAS: Real-time and Embedded Technology and Applications Symposium, 253–266.' mla: Henzinger, Thomas A., and Slobodan Matic. An Interface Algebra for Real-Time Components. IEEE, 2006, pp. 253–66, doi:10.1109/RTAS.2006.11. short: T.A. Henzinger, S. Matic, in:, IEEE, 2006, pp. 253–266. conference: name: 'RTAS: Real-time and Embedded Technology and Applications Symposium' date_created: 2018-12-11T12:08:50Z date_published: 2006-04-24T00:00:00Z date_updated: 2021-01-12T07:56:57Z day: '24' doi: 10.1109/RTAS.2006.11 extern: 1 month: '04' page: 253 - 266 publication_status: published publisher: IEEE publist_id: '294' quality_controlled: 0 status: public title: An interface algebra for real-time components type: conference year: '2006' ... --- _id: '4432' abstract: - lang: eng text: We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision. acknowledgement: This research was supported in part by the NSF grants CCR-0208875, CCR-0225610, and CCR-0234690. alternative_title: - LNCS author: - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vinayak full_name: Prabhu, Vinayak S last_name: Prabhu citation: ama: 'Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: Vol 4202. Springer; 2006:1-17. doi:10.1007/11867340_1' apa: 'Henzinger, T. A., & Prabhu, V. (2006). Timed alternating-time temporal logic (Vol. 4202, pp. 1–17). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. https://doi.org/10.1007/11867340_1' chicago: Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal Logic,” 4202:1–17. Springer, 2006. https://doi.org/10.1007/11867340_1. ieee: 'T. A. Henzinger and V. Prabhu, “Timed alternating-time temporal logic,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, vol. 4202, pp. 1–17.' ista: 'Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.' mla: Henzinger, Thomas A., and Vinayak Prabhu. Timed Alternating-Time Temporal Logic. Vol. 4202, Springer, 2006, pp. 1–17, doi:10.1007/11867340_1. short: T.A. Henzinger, V. Prabhu, in:, Springer, 2006, pp. 1–17. conference: name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' date_created: 2018-12-11T12:08:49Z date_published: 2006-09-19T00:00:00Z date_updated: 2021-01-12T07:56:56Z day: '19' doi: 10.1007/11867340_1 extern: 1 intvolume: ' 4202' month: '09' page: 1 - 17 publication_status: published publisher: Springer publist_id: '296' quality_controlled: 0 status: public title: Timed alternating-time temporal logic type: conference volume: 4202 year: '2006' ... --- _id: '4431' abstract: - lang: eng text: 'We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science.' acknowledgement: Supported in part by the ARTIST2 European Network of Excellence on Embedded Systems Design, by the NSF ITR Center on Hybrid and Embedded Software Systems (CHESS), and by the SNSF NCCR on Mobile Information and Communication Systems (MICS). alternative_title: - LNCS author: - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Joseph full_name: Sifakis, Joseph last_name: Sifakis citation: ama: 'Henzinger TA, Sifakis J. The embedded systems design challenge. In: Vol 4085. Springer; 2006:1-15. doi:10.1007/11813040_1' apa: 'Henzinger, T. A., & Sifakis, J. (2006). The embedded systems design challenge (Vol. 4085, pp. 1–15). Presented at the FM: Formal Methods, Springer. https://doi.org/10.1007/11813040_1' chicago: Henzinger, Thomas A, and Joseph Sifakis. “The Embedded Systems Design Challenge,” 4085:1–15. Springer, 2006. https://doi.org/10.1007/11813040_1. ieee: 'T. A. Henzinger and J. Sifakis, “The embedded systems design challenge,” presented at the FM: Formal Methods, 2006, vol. 4085, pp. 1–15.' ista: 'Henzinger TA, Sifakis J. 2006. The embedded systems design challenge. FM: Formal Methods, LNCS, vol. 4085, 1–15.' mla: Henzinger, Thomas A., and Joseph Sifakis. The Embedded Systems Design Challenge. Vol. 4085, Springer, 2006, pp. 1–15, doi:10.1007/11813040_1. short: T.A. Henzinger, J. Sifakis, in:, Springer, 2006, pp. 1–15. conference: name: 'FM: Formal Methods' date_created: 2018-12-11T12:08:49Z date_published: 2006-08-10T00:00:00Z date_updated: 2021-01-12T07:56:55Z day: '10' doi: 10.1007/11813040_1 extern: 1 intvolume: ' 4085' month: '08' page: 1 - 15 publication_status: published publisher: Springer publist_id: '301' quality_controlled: 0 status: public title: The embedded systems design challenge type: conference volume: 4085 year: '2006' ... --- _id: '4451' 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 alternation-free 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. author: - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman - first_name: Ritankar full_name: Majumdar, Ritankar S last_name: Majumdar citation: ama: Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. 2006;354(2):173-186. doi:10.1016/j.tcs.2005.11.015 apa: Henzinger, T. A., Kupferman, O., & Majumdar, R. (2006). On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2005.11.015 chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science. Elsevier, 2006. https://doi.org/10.1016/j.tcs.2005.11.015. ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential fragments of the mu-calculus,” Theoretical Computer Science, vol. 354, no. 2. Elsevier, pp. 173–186, 2006. ista: Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186. mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science, vol. 354, no. 2, Elsevier, 2006, pp. 173–86, doi:10.1016/j.tcs.2005.11.015. short: T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354 (2006) 173–186. date_created: 2018-12-11T12:08:55Z date_published: 2006-03-28T00:00:00Z date_updated: 2021-01-12T07:57:04Z day: '28' doi: 10.1016/j.tcs.2005.11.015 extern: 1 intvolume: ' 354' issue: '2' month: '03' page: 173 - 186 publication: Theoretical Computer Science publication_status: published publisher: Elsevier publist_id: '276' quality_controlled: 0 status: public title: On the universal and existential fragments of the mu-calculus type: journal_article volume: 354 year: '2006' ... --- _id: '4523' abstract: - lang: eng text: We consider the problem if a given program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi. author: - first_name: Bhargav full_name: Gulavani, Bhargav S last_name: Gulavani - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Yamini full_name: Kannan, Yamini last_name: Kannan - first_name: Aditya full_name: Nori, Aditya V last_name: Nori - first_name: Sriram full_name: Rajamani, Sriram K last_name: Rajamani citation: ama: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm for property checking. In: ACM; 2006:117-127. doi:10.1145/1181775.1181790' apa: 'Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., & Rajamani, S. (2006). Synergy: A new algorithm for property checking (pp. 117–127). Presented at the FSE: Foundations of Software Engineering, ACM. https://doi.org/10.1145/1181775.1181790' chicago: 'Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and Sriram Rajamani. “Synergy: A New Algorithm for Property Checking,” 117–27. ACM, 2006. https://doi.org/10.1145/1181775.1181790.' ieee: 'B. Gulavani, T. A. Henzinger, Y. Kannan, A. Nori, and S. Rajamani, “Synergy: A new algorithm for property checking,” presented at the FSE: Foundations of Software Engineering, 2006, pp. 117–127.' ista: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. 2006. Synergy: A new algorithm for property checking. FSE: Foundations of Software Engineering, 117–127.' mla: 'Gulavani, Bhargav, et al. Synergy: A New Algorithm for Property Checking. ACM, 2006, pp. 117–27, doi:10.1145/1181775.1181790.' short: B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, ACM, 2006, pp. 117–127. conference: name: 'FSE: Foundations of Software Engineering' date_created: 2018-12-11T12:09:18Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T07:59:26Z day: '01' doi: 10.1145/1181775.1181790 extern: 1 month: '01' page: 117 - 127 publication_status: published publisher: ACM publist_id: '206' quality_controlled: 0 status: public title: 'Synergy: A new algorithm for property checking' type: conference year: '2006' ... --- _id: '4526' abstract: - lang: eng text: 'We designed and implemented a new programming language called Hierarchical Timing Language (HTL) for hard realtime systems. Critical timing constraints are specified within the language,and ensured by the compiler. Programs in HTL are extensible in two dimensions without changing their timing behavior: new program modules can be added, and individual program tasks can be refined. The mechanism supporting time invariance under parallel composition is that different program modules communicate at specified instances of time. Time invariance under refinement is achieved by conservative scheduling of the top level. HTL is a coordination language, in that individual tasks can be implemented in "foreign" languages. As a case study, we present a distributed HTL implementation of an automotive steer-by-wire controller.' author: - first_name: Arkadeb full_name: Ghosal, Arkadeb last_name: Ghosal - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Daniel full_name: Iercan, Daniel last_name: Iercan - first_name: Christoph full_name: Kirsch, Christoph M last_name: Kirsch - first_name: Alberto full_name: Sangiovanni-Vincentelli, Alberto last_name: Sangiovanni Vincentelli citation: ama: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. A hierarchical coordination language for interacting real-time tasks. In: ACM; 2006:132-141. doi:10.1145/1176887.1176907' apa: 'Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., & Sangiovanni Vincentelli, A. (2006). A hierarchical coordination language for interacting real-time tasks (pp. 132–141). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1176887.1176907' chicago: Ghosal, Arkadeb, Thomas A Henzinger, Daniel Iercan, Christoph Kirsch, and Alberto Sangiovanni Vincentelli. “A Hierarchical Coordination Language for Interacting Real-Time Tasks,” 132–41. ACM, 2006. https://doi.org/10.1145/1176887.1176907. ieee: 'A. Ghosal, T. A. Henzinger, D. Iercan, C. Kirsch, and A. Sangiovanni Vincentelli, “A hierarchical coordination language for interacting real-time tasks,” presented at the EMSOFT: Embedded Software , 2006, pp. 132–141.' ista: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. 2006. A hierarchical coordination language for interacting real-time tasks. EMSOFT: Embedded Software , 132–141.' mla: Ghosal, Arkadeb, et al. A Hierarchical Coordination Language for Interacting Real-Time Tasks. ACM, 2006, pp. 132–41, doi:10.1145/1176887.1176907. short: A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, A. Sangiovanni Vincentelli, in:, ACM, 2006, pp. 132–141. conference: name: 'EMSOFT: Embedded Software ' date_created: 2018-12-11T12:09:18Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T07:59:27Z day: '01' doi: 10.1145/1176887.1176907 extern: 1 month: '01' page: 132 - 141 publication_status: published publisher: ACM publist_id: '201' quality_controlled: 0 status: public title: A hierarchical coordination language for interacting real-time tasks type: conference year: '2006' ... --- _id: '4528' abstract: - lang: eng text: Computational modeling of biological systems is becoming increasingly common as scientists attempt to understand biological phenomena in their full complexity. Here we distinguish between two types of biological models mathematical and computational - according to their different representations of biological phenomena and their diverse potential. We call the approach of constructing computational models of biological systems executable biology, as it focuses on the design of executable computer algorithms that mimic biological phenomena. We give an overview of the main modeling efforts in this direction, and discuss some of the new challenges that executable biology poses for computer science and biology. We argue that for executable biology to reach its full potential as a mainstream biological technique, formal and algorithmic approaches must be integrated into biological research, driving biology towards a more precise engineering discipline. author: - first_name: Jasmin full_name: Fisher, Jasmin last_name: Fisher - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Fisher J, Henzinger TA. Executable biology. In: IEEE; 2006:1675-1682. doi:10.1109/WSC.2006.322942' apa: 'Fisher, J., & Henzinger, T. A. (2006). Executable biology (pp. 1675–1682). Presented at the WSC: Winter Simulation Conference, IEEE. https://doi.org/10.1109/WSC.2006.322942' chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Biology,” 1675–82. IEEE, 2006. https://doi.org/10.1109/WSC.2006.322942. ieee: 'J. Fisher and T. A. Henzinger, “Executable biology,” presented at the WSC: Winter Simulation Conference, 2006, pp. 1675–1682.' ista: 'Fisher J, Henzinger TA. 2006. Executable biology. WSC: Winter Simulation Conference, 1675–1682.' mla: Fisher, Jasmin, and Thomas A. Henzinger. Executable Biology. IEEE, 2006, pp. 1675–82, doi:10.1109/WSC.2006.322942. short: J. Fisher, T.A. Henzinger, in:, IEEE, 2006, pp. 1675–1682. conference: name: 'WSC: Winter Simulation Conference' date_created: 2018-12-11T12:09:19Z date_published: 2006-12-03T00:00:00Z date_updated: 2021-01-12T07:59:28Z day: '03' doi: 10.1109/WSC.2006.322942 extern: 1 month: '12' page: 1675 - 1682 publication_status: published publisher: IEEE publist_id: '197' quality_controlled: 0 status: public title: Executable biology type: conference year: '2006' ... --- _id: '4539' abstract: - lang: eng text: Games on graphs with ω-regular objectives provide a model for the control and synthesis of reactive systems. Every ω-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. While for one-shot liveness (reachability) objectives, classical and finitary liveness coincide, for repeated liveness (Büchi) objectives, the finitary formulation is strictly stronger. In this work we study games with finitary parity and Streett (fairness) objectives. We prove the determinacy of these games, present algorithms for solving these games, and characterize the memory requirements of winning strategies. Our algorithms can be used, for example, for synthesizing controllers that do not let the response time of a system increase without bound. acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327 and the NSF ITR grant CCR-0225610. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Krishnendu Chatterjee id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Chatterjee K, Henzinger TA. Finitary winning in omega-regular games. In: Vol 3920. Springer; 2006:257-271. doi:10.1007/11691372_17' apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Finitary winning in omega-regular games (Vol. 3920, pp. 257–271). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. https://doi.org/10.1007/11691372_17' chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Finitary Winning in Omega-Regular Games,” 3920:257–71. Springer, 2006. https://doi.org/10.1007/11691372_17. ieee: 'K. Chatterjee and T. A. Henzinger, “Finitary winning in omega-regular games,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2006, vol. 3920, pp. 257–271.' ista: 'Chatterjee K, Henzinger TA. 2006. Finitary winning in omega-regular games. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 3920, 257–271.' mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Finitary Winning in Omega-Regular Games. Vol. 3920, Springer, 2006, pp. 257–71, doi:10.1007/11691372_17. short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 257–271. conference: name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' date_created: 2018-12-11T12:09:22Z date_published: 2006-03-15T00:00:00Z date_updated: 2021-01-12T07:59:32Z day: '15' doi: 10.1007/11691372_17 extern: 1 intvolume: ' 3920' month: '03' page: 257 - 271 publication_status: published publisher: Springer publist_id: '183' quality_controlled: 0 status: public title: Finitary winning in omega-regular games type: conference volume: 3920 year: '2006' ... --- _id: '4538' abstract: - lang: eng text: A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy improvement algorithm for stochastic parity games; this is the first non-brute-force algorithm for solving these games. From the strategy improvement algorithm we obtain a randomized subexponential-time algorithm to solve such games. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Krishnendu Chatterjee id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Chatterjee K, Henzinger TA. Strategy improvement and randomized subexponential algorithms for stochastic parity games. In: Vol 3884. Springer; 2006:512-523. doi:10.1007/11672142_42' apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Strategy improvement and randomized subexponential algorithms for stochastic parity games (Vol. 3884, pp. 512–523). Presented at the STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_42' chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games,” 3884:512–23. Springer, 2006. https://doi.org/10.1007/11672142_42. ieee: 'K. Chatterjee and T. A. Henzinger, “Strategy improvement and randomized subexponential algorithms for stochastic parity games,” presented at the STACS: Theoretical Aspects of Computer Science, 2006, vol. 3884, pp. 512–523.' ista: 'Chatterjee K, Henzinger TA. 2006. Strategy improvement and randomized subexponential algorithms for stochastic parity games. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 3884, 512–523.' mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games. Vol. 3884, Springer, 2006, pp. 512–23, doi:10.1007/11672142_42. short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 512–523. conference: name: 'STACS: Theoretical Aspects of Computer Science' date_created: 2018-12-11T12:09:22Z date_published: 2006-02-14T00:00:00Z date_updated: 2021-01-12T07:59:32Z day: '14' doi: 10.1007/11672142_42 extern: 1 intvolume: ' 3884' month: '02' page: 512 - 523 publication_status: published publisher: Springer publist_id: '184' quality_controlled: 0 status: public title: Strategy improvement and randomized subexponential algorithms for stochastic parity games type: conference volume: 3884 year: '2006' ... --- _id: '4551' abstract: - lang: eng text: "We consider Markov decision processes (MDPs) with multiple discounted reward objectives. Such MDPs occur in design problems where one wishes to simultaneously optimize several criteria, for example, latency and power. The possible trade-offs between the different objectives are characterized by the Pareto curve. We show that every Pareto-optimal point can be achieved by a memoryless strategy; however, unlike in the single-objective case, the memoryless strategy may require randomization. Moreover, we show that the Pareto curve can be approximated in polynomial time in the size of the MDP. Additionally, we study the problem if a given value vector is realizable by any strategy, and show that it can be decided in polynomial time; but the question whether it is realizable by a deterministic memoryless strategy is NP-complete. These results provide efficient algorithms for design exploration in MDP models with multiple objectives.\nThis research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202. " acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Krishnendu Chatterjee id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ritankar full_name: Majumdar, Ritankar S last_name: Majumdar - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Chatterjee K, Majumdar R, Henzinger TA. Markov decision processes with multiple objectives. In: Vol 3884. Springer; 2006:325-336. doi:10.1007/11672142_26' apa: 'Chatterjee, K., Majumdar, R., & Henzinger, T. A. (2006). Markov decision processes with multiple objectives (Vol. 3884, pp. 325–336). Presented at the STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_26' chicago: Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. https://doi.org/10.1007/11672142_26. ieee: 'K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Markov decision processes with multiple objectives,” presented at the STACS: Theoretical Aspects of Computer Science, 2006, vol. 3884, pp. 325–336.' ista: 'Chatterjee K, Majumdar R, Henzinger TA. 2006. Markov decision processes with multiple objectives. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 3884, 325–336.' mla: Chatterjee, Krishnendu, et al. Markov Decision Processes with Multiple Objectives. Vol. 3884, Springer, 2006, pp. 325–36, doi:10.1007/11672142_26. short: K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336. conference: name: 'STACS: Theoretical Aspects of Computer Science' date_created: 2018-12-11T12:09:26Z date_published: 2006-02-14T00:00:00Z date_updated: 2021-01-12T07:59:38Z day: '14' doi: 10.1007/11672142_26 extern: 1 intvolume: ' 3884' month: '02' page: 325 - 336 publication_status: published publisher: Springer publist_id: '161' quality_controlled: 0 status: public title: Markov decision processes with multiple objectives type: conference volume: 3884 year: '2006' ... --- _id: '4550' abstract: - lang: eng text: 'In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent''s payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it sometimes suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of ω-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.' author: - first_name: Krishnendu full_name: Krishnendu Chatterjee id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Marcin full_name: Jurdziński, Marcin last_name: Jurdziński citation: ama: Chatterjee K, Henzinger TA, Jurdziński M. Games with secure equilibria. Theoretical Computer Science. 2006;365(1-2):67-82. doi:10.1016/j.tcs.2006.07.032 apa: Chatterjee, K., Henzinger, T. A., & Jurdziński, M. (2006). Games with secure equilibria. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2006.07.032 chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Games with Secure Equilibria.” Theoretical Computer Science. Elsevier, 2006. https://doi.org/10.1016/j.tcs.2006.07.032. ieee: K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Games with secure equilibria,” Theoretical Computer Science, vol. 365, no. 1–2. Elsevier, pp. 67–82, 2006. ista: Chatterjee K, Henzinger TA, Jurdziński M. 2006. Games with secure equilibria. Theoretical Computer Science. 365(1–2), 67–82. mla: Chatterjee, Krishnendu, et al. “Games with Secure Equilibria.” Theoretical Computer Science, vol. 365, no. 1–2, Elsevier, 2006, pp. 67–82, doi:10.1016/j.tcs.2006.07.032. short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science 365 (2006) 67–82. date_created: 2018-12-11T12:09:26Z date_published: 2006-08-07T00:00:00Z date_updated: 2021-01-12T07:59:38Z day: '07' doi: 10.1016/j.tcs.2006.07.032 extern: 1 intvolume: ' 365' issue: 1-2 month: '08' page: 67 - 82 publication: Theoretical Computer Science publication_status: published publisher: Elsevier publist_id: '164' quality_controlled: 0 status: public title: Games with secure equilibria type: journal_article volume: 365 year: '2006' ... --- _id: '4549' abstract: - lang: eng text: We present a compositional theory of system verification, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system properties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports the composition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbered distances between descriptions of a system at different levels of detail. We show that the classical Boolean rules for compositional reasoning have quantitative counterparts in our setting. While our general theory allows costs to be specified by arbitrary cost functions, we also consider a class of linear cost functions, which give rise to an instance of our framework where all operations are computable in polynomial time. acknowledgement: Supported in part by the NSF grants CCR-0234690, CCR-0208875, and CCR-0225610; by the NSF grant CCR-0132780 and ARP grant SC20051123. author: - first_name: Krishnendu full_name: Krishnendu Chatterjee id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: de Alfaro, Luca last_name: De Alfaro - first_name: Marco full_name: Faella, Marco last_name: Faella - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Ritankar full_name: Majumdar, Ritankar S last_name: Majumdar - first_name: Mariëlle full_name: Stoelinga, Mariëlle last_name: Stoelinga citation: ama: 'Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Compositional quantitative reasoning. In: IEEE; 2006:179-188. doi:10.1109/QEST.2006.11' apa: 'Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., & Stoelinga, M. (2006). Compositional quantitative reasoning (pp. 179–188). Presented at the QEST: Quantitative Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.11' chicago: Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and Mariëlle Stoelinga. “Compositional Quantitative Reasoning,” 179–88. IEEE, 2006. https://doi.org/10.1109/QEST.2006.11. ieee: 'K. Chatterjee, L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “Compositional quantitative reasoning,” presented at the QEST: Quantitative Evaluation of Systems, 2006, pp. 179–188.' ista: 'Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2006. Compositional quantitative reasoning. QEST: Quantitative Evaluation of Systems, 179–188.' mla: Chatterjee, Krishnendu, et al. Compositional Quantitative Reasoning. IEEE, 2006, pp. 179–88, doi:10.1109/QEST.2006.11. short: K. Chatterjee, L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:, IEEE, 2006, pp. 179–188. conference: name: 'QEST: Quantitative Evaluation of Systems' date_created: 2018-12-11T12:09:26Z date_published: 2006-09-01T00:00:00Z date_updated: 2021-01-12T07:59:37Z day: '01' doi: 10.1109/QEST.2006.11 extern: 1 month: '09' page: 179 - 188 publication_status: published publisher: IEEE publist_id: '163' quality_controlled: 0 status: public title: Compositional quantitative reasoning type: conference year: '2006' ... --- _id: '4552' abstract: - lang: eng text: 'A concurrent reachability game is a two-player game played on a graph: at each state, the players simultaneously and independently select moves; the two moves determine jointly a probability distribution over the successor states. The objective for player 1 consists in reaching a set of target states; the objective for player 2 is to prevent this, so that the game is zero-sum. Our contributions are two-fold. First, we present a simple proof of the fact that in concurrent reachability games, for all epsilon > 0, memoryless epsilon-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an epsilon-optimal strategy achieves the objective with probability within epsilon of the value of the game. In contrast to previous proofs of this fact, which rely on the limit behavior of discounted games using advanced Puisieux series analysis, our proof is elementary and combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives.' author: - first_name: Krishnendu full_name: Krishnendu Chatterjee id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: de Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent reachability games. In: IEEE; 2006:291-300. doi:10.1109/QEST.2006.48' apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2006). Strategy improvement for concurrent reachability games (pp. 291–300). Presented at the QEST: Quantitative Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.48' chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy Improvement for Concurrent Reachability Games,” 291–300. IEEE, 2006. https://doi.org/10.1109/QEST.2006.48. ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for concurrent reachability games,” presented at the QEST: Quantitative Evaluation of Systems, 2006, pp. 291–300.' ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2006. Strategy improvement for concurrent reachability games. QEST: Quantitative Evaluation of Systems, 291–300.' mla: Chatterjee, Krishnendu, et al. Strategy Improvement for Concurrent Reachability Games. IEEE, 2006, pp. 291–300, doi:10.1109/QEST.2006.48. short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2006, pp. 291–300. conference: name: 'QEST: Quantitative Evaluation of Systems' date_created: 2018-12-11T12:09:26Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T07:59:39Z day: '01' doi: 10.1109/QEST.2006.48 extern: 1 month: '01' page: 291 - 300 publication_status: published publisher: IEEE publist_id: '162' quality_controlled: 0 status: public title: Strategy improvement for concurrent reachability games type: conference year: '2006' ... --- _id: '4574' abstract: - lang: eng text: Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker Blast. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending Blast with calls to Tvla. alternative_title: - LNCS author: - first_name: Dirk full_name: Beyer, Dirk last_name: Beyer - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Grégory full_name: Théoduloz, Grégory last_name: Théoduloz citation: ama: 'Beyer D, Henzinger TA, Théoduloz G. Lazy shape analysis. In: Vol 4144. Springer; 2006:532-546. doi:10.1007/11817963_48' apa: 'Beyer, D., Henzinger, T. A., & Théoduloz, G. (2006). Lazy shape analysis (Vol. 4144, pp. 532–546). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/11817963_48' chicago: Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Lazy Shape Analysis,” 4144:532–46. Springer, 2006. https://doi.org/10.1007/11817963_48. ieee: 'D. Beyer, T. A. Henzinger, and G. Théoduloz, “Lazy shape analysis,” presented at the CAV: Computer Aided Verification, 2006, vol. 4144, pp. 532–546.' ista: 'Beyer D, Henzinger TA, Théoduloz G. 2006. Lazy shape analysis. CAV: Computer Aided Verification, LNCS, vol. 4144, 532–546.' mla: Beyer, Dirk, et al. Lazy Shape Analysis. Vol. 4144, Springer, 2006, pp. 532–46, doi:10.1007/11817963_48. short: D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Springer, 2006, pp. 532–546. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:09:33Z date_published: 2006-08-08T00:00:00Z date_updated: 2021-01-12T07:59:49Z day: '08' doi: 10.1007/11817963_48 extern: 1 intvolume: ' 4144' month: '08' page: 532 - 546 publication_status: published publisher: Springer publist_id: '133' quality_controlled: 0 status: public title: Lazy shape analysis type: conference volume: 4144 year: '2006' ... --- _id: '573' abstract: - lang: eng text: 'Mitchison and Jozsa recently suggested that the "chained-Zeno" counterfactual computation protocol recently proposed by Hosten et al. is counterfactual for only one output of the computer. This claim was based on the existing abstract algebraic definition of counterfactual computation, and indeed according to this definition, their argument is correct. However, a more general definition (physically adequate) for counterfactual computation is implicitly assumed by Hosten et. al. Here we explain in detail why the protocol is counterfactual and how the "history tracking" method of the existing description inadequately represents the physics underlying the protocol. Consequently, we propose a modified definition of counterfactual computation. Finally, we comment on one of the most interesting aspects of the error-correcting protocol. ' article_processing_charge: No author: - first_name: Onur full_name: Hosten, Onur id: 4C02D85E-F248-11E8-B48F-1D18A9856A87 last_name: Hosten orcid: 0000-0002-2031-204X - first_name: Matthew full_name: Rakher, Matthew last_name: Rakher - first_name: Julio full_name: Barreiro, Julio last_name: Barreiro - first_name: Nicholas full_name: Peters, Nicholas last_name: Peters - first_name: Paul full_name: Kwiat, Paul last_name: Kwiat citation: ama: Hosten O, Rakher M, Barreiro J, Peters N, Kwiat P. Counterfactual computation revisited. 2006. apa: Hosten, O., Rakher, M., Barreiro, J., Peters, N., & Kwiat, P. (2006). Counterfactual computation revisited. ArXiv. chicago: Hosten, Onur, Matthew Rakher, Julio Barreiro, Nicholas Peters, and Paul Kwiat. “Counterfactual Computation Revisited.” ArXiv, 2006. ieee: O. Hosten, M. Rakher, J. Barreiro, N. Peters, and P. Kwiat, “Counterfactual computation revisited.” ArXiv, 2006. ista: Hosten O, Rakher M, Barreiro J, Peters N, Kwiat P. 2006. Counterfactual computation revisited. mla: Hosten, Onur, et al. Counterfactual Computation Revisited. ArXiv, 2006. short: O. Hosten, M. Rakher, J. Barreiro, N. Peters, P. Kwiat, (2006). date_created: 2018-12-11T11:47:16Z date_published: 2006-08-06T00:00:00Z date_updated: 2020-05-12T08:23:52Z day: '06' extern: '1' external_id: arxiv: - '0607101' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/quant-ph/0607101 month: '08' oa: 1 oa_version: Preprint page: '12' publication_status: published publisher: ArXiv publist_id: '7241' status: public title: Counterfactual computation revisited type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2006' ... --- _id: '574' abstract: - lang: eng text: 'Vaidman, in a recent article adopts the method of ''quantum weak measurements in pre- and postselected ensembles'' to ascertain whether or not the chained-Zeno counterfactual computation scheme proposed by Hosten et al. is counterfactual; which has been the topic of a debate on the definition of counterfactuality. We disagree with his conclusion, which brings up some interesting aspects of quantum weak measurements and some concerns about the way they are interpreted. ' article_processing_charge: No author: - first_name: Onur full_name: Hosten, Onur id: 4C02D85E-F248-11E8-B48F-1D18A9856A87 last_name: Hosten orcid: 0000-0002-2031-204X - first_name: Paul full_name: Kwiat, Paul last_name: Kwiat citation: ama: Hosten O, Kwiat P. Weak measurements and counterfactual computation. 2006. apa: Hosten, O., & Kwiat, P. (2006). Weak measurements and counterfactual computation. ArXiv. chicago: Hosten, Onur, and Paul Kwiat. “Weak Measurements and Counterfactual Computation.” ArXiv, 2006. ieee: O. Hosten and P. Kwiat, “Weak measurements and counterfactual computation.” ArXiv, 2006. ista: Hosten O, Kwiat P. 2006. Weak measurements and counterfactual computation. mla: Hosten, Onur, and Paul Kwiat. Weak Measurements and Counterfactual Computation. ArXiv, 2006. short: O. Hosten, P. Kwiat, (2006). date_created: 2018-12-11T11:47:16Z date_published: 2006-12-19T00:00:00Z date_updated: 2020-05-12T08:18:01Z day: '19' extern: '1' external_id: arxiv: - '0612159' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/quant-ph/0612159 month: '12' oa: 1 oa_version: Preprint page: '2' publication_status: published publisher: ArXiv publist_id: '7240' status: public title: Weak measurements and counterfactual computation type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2006' ... --- _id: '578' abstract: - lang: eng text: A source of single photons allows secure quantum key distribution, in addition, to being a critical resource for linear optics quantum computing. We describe our progress on deterministically creating single photons from spontaneous parametric downconversion, an extension of the Pittman, Jacobs and Franson scheme [Phys. Rev A, v66, 042303 (2002)]. Their idea was to conditionally prepare single photons by measuring one member of a spontaneously emitted photon pair and storing the remaining conditionally prepared photon until a predetermined time, when it would be "deterministically" released from storage. Our approach attempts to improve upon this by recycling the pump pulse in order to decrease the possibility of multiple-pair generation, while maintaining a high probability of producing a single pair. Many of the challenges we discuss are central to other quantum information technologies, including the need for low-loss optical storage, switching and detection, and fast feed-forward control. alternative_title: - Proc. SPIE author: - first_name: Nicholas full_name: Peters, Nicholas A last_name: Peters - first_name: Keith full_name: Arnold, Keith J last_name: Arnold - first_name: Aaron full_name: VanDevender, Aaron P last_name: Vandevender - first_name: Evan full_name: Jeffrey, Evan R last_name: Jeffrey - first_name: Radhika full_name: Rangarajan, Radhika last_name: Rangarajan - first_name: Onur full_name: Onur Hosten id: 4C02D85E-F248-11E8-B48F-1D18A9856A87 last_name: Hosten orcid: 0000-0002-2031-204X - first_name: Julio full_name: Barreiro, Julio T last_name: Barreiro - first_name: Joseph full_name: Altepeter, Joseph B last_name: Altepeter - first_name: Paul full_name: Kwiat, Paul G last_name: Kwiat citation: ama: 'Peters N, Arnold K, Vandevender A, et al. Towards a quasi-deterministic single-photon source. In: Vol 6305. SPIE; 2006. doi:10.1117/12.684702' apa: Peters, N., Arnold, K., Vandevender, A., Jeffrey, E., Rangarajan, R., Hosten, O., … Kwiat, P. (2006). Towards a quasi-deterministic single-photon source (Vol. 6305). Presented at the Quantum Communications and Quantum Imaging, SPIE. https://doi.org/10.1117/12.684702 chicago: Peters, Nicholas, Keith Arnold, Aaron Vandevender, Evan Jeffrey, Radhika Rangarajan, Onur Hosten, Julio Barreiro, Joseph Altepeter, and Paul Kwiat. “Towards a Quasi-Deterministic Single-Photon Source,” Vol. 6305. SPIE, 2006. https://doi.org/10.1117/12.684702. ieee: N. Peters et al., “Towards a quasi-deterministic single-photon source,” presented at the Quantum Communications and Quantum Imaging, 2006, vol. 6305. ista: Peters N, Arnold K, Vandevender A, Jeffrey E, Rangarajan R, Hosten O, Barreiro J, Altepeter J, Kwiat P. 2006. Towards a quasi-deterministic single-photon source. Quantum Communications and Quantum Imaging, Proc. SPIE, vol. 6305. mla: Peters, Nicholas, et al. Towards a Quasi-Deterministic Single-Photon Source. Vol. 6305, SPIE, 2006, doi:10.1117/12.684702. short: N. Peters, K. Arnold, A. Vandevender, E. Jeffrey, R. Rangarajan, O. Hosten, J. Barreiro, J. Altepeter, P. Kwiat, in:, SPIE, 2006. conference: name: Quantum Communications and Quantum Imaging date_created: 2018-12-11T11:47:17Z date_published: 2006-01-01T00:00:00Z date_updated: 2020-07-14T12:47:11Z day: '01' doi: 10.1117/12.684702 extern: 1 intvolume: ' 6305' month: '01' publication_status: published publisher: SPIE publist_id: '7234' quality_controlled: 0 status: public title: Towards a quasi-deterministic single-photon source type: conference volume: 6305 year: '2006' ... --- _id: '577' abstract: - lang: eng text: Visible light photon counters (VLPCs) and solid-state photomultipliers (SSPMs) are high-efficiency single-photon detectors which have multi-photon counting capability. While both the VLPCs and the SSPMs have inferred internal quantum efficiencies above 93%, the actual measured values for both the detectors were in fact limited to less than 88%, attributed to in-coupling losses. We are currently improving this overall detection efficiency via a) custom anti-reflection coating the detectors and the in-coupling fibers, b) implementing a novel cryogenic design to reduce transmission losses and, c) using low-noise electronics to obtain a better signal-to-noise ratio. alternative_title: - Proceedings of SPIE author: - first_name: Radhika full_name: Rangarajan, Radhika last_name: Rangarajan - first_name: Joseph full_name: Altepeter, Joseph B last_name: Altepeter - first_name: Evan full_name: Jeffrey, Evan R last_name: Jeffrey - first_name: Micah full_name: Stoutimore, Micah J last_name: Stoutimore - first_name: Nicholas full_name: Peters, Nicholas A last_name: Peters - first_name: Onur full_name: Onur Hosten id: 4C02D85E-F248-11E8-B48F-1D18A9856A87 last_name: Hosten orcid: 0000-0002-2031-204X - first_name: Paul full_name: Kwiat, Paul G last_name: Kwiat citation: ama: 'Rangarajan R, Altepeter J, Jeffrey E, et al. High-efficiency single-photon detectors. In: Vol 6372. SPIE; 2006. doi:10.1117/12.686117' apa: Rangarajan, R., Altepeter, J., Jeffrey, E., Stoutimore, M., Peters, N., Hosten, O., & Kwiat, P. (2006). High-efficiency single-photon detectors (Vol. 6372). Presented at the Unknown (978-081946470-5), SPIE. https://doi.org/10.1117/12.686117 chicago: Rangarajan, Radhika, Joseph Altepeter, Evan Jeffrey, Micah Stoutimore, Nicholas Peters, Onur Hosten, and Paul Kwiat. “High-Efficiency Single-Photon Detectors,” Vol. 6372. SPIE, 2006. https://doi.org/10.1117/12.686117. ieee: R. Rangarajan et al., “High-efficiency single-photon detectors,” presented at the Unknown (978-081946470-5), 2006, vol. 6372. ista: Rangarajan R, Altepeter J, Jeffrey E, Stoutimore M, Peters N, Hosten O, Kwiat P. 2006. High-efficiency single-photon detectors. Unknown (978-081946470-5), Proceedings of SPIE, vol. 6372. mla: Rangarajan, Radhika, et al. High-Efficiency Single-Photon Detectors. Vol. 6372, SPIE, 2006, doi:10.1117/12.686117. short: R. Rangarajan, J. Altepeter, E. Jeffrey, M. Stoutimore, N. Peters, O. Hosten, P. Kwiat, in:, SPIE, 2006. conference: name: Unknown (978-081946470-5) date_created: 2018-12-11T11:47:17Z date_published: 2006-01-01T00:00:00Z date_updated: 2020-07-14T12:47:11Z day: '01' doi: 10.1117/12.686117 extern: 1 intvolume: ' 6372' month: '01' publication_status: published publisher: SPIE publist_id: '7233' quality_controlled: 0 status: public title: High-efficiency single-photon detectors type: conference volume: 6372 year: '2006' ... --- _id: '579' abstract: - lang: eng text: 'The logic underlying the coherent nature of quantum information processing often deviates from intuitive reasoning, leading to surprising effects. Counterfactual computation constitutes a striking example: the potential outcome of a quantum computation can be inferred, even if the computer is not run 1. Relying on similar arguments to interaction-free measurements 2 (or quantum interrogation3), counterfactual computation is accomplished by putting the computer in a superposition of ''running'' and ''not running'' states, and then interfering the two histories. Conditional on the as-yet-unknown outcome of the computation, it is sometimes possible to counterfactually infer information about the solution. Here we demonstrate counterfactual computation, implementing Grover''s search algorithm with an all-optical approach4. It was believed that the overall probability of such counterfactual inference is intrinsically limited1,5, so that it could not perform better on average than random guesses. However, using a novel ''chained'' version of the quantum Zeno effect6, we show how to boost the counterfactual inference probability to unity, thereby beating the random guessing limit. Our methods are general and apply to any physical system, as illustrated by a discussion of trapped-ion systems. Finally, we briefly show that, in certain circumstances, counterfactual computation can eliminate errors induced by decoherence. ' author: - first_name: Onur full_name: Onur Hosten id: 4C02D85E-F248-11E8-B48F-1D18A9856A87 last_name: Hosten orcid: 0000-0002-2031-204X - first_name: Matthew full_name: Rakher, Matthew T last_name: Rakher - first_name: Julio full_name: Barreiro, Julio T last_name: Barreiro - first_name: Nicholas full_name: Peters, Nicholas A last_name: Peters - first_name: Paul full_name: Kwiat, Paul G last_name: Kwiat citation: ama: Hosten O, Rakher M, Barreiro J, Peters N, Kwiat P. Counterfactual quantum computation through quantum interrogation. Nature. 2006;439(7079):949-952. doi:10.1038/nature04523 apa: Hosten, O., Rakher, M., Barreiro, J., Peters, N., & Kwiat, P. (2006). Counterfactual quantum computation through quantum interrogation. Nature. Nature Publishing Group. https://doi.org/10.1038/nature04523 chicago: Hosten, Onur, Matthew Rakher, Julio Barreiro, Nicholas Peters, and Paul Kwiat. “Counterfactual Quantum Computation through Quantum Interrogation.” Nature. Nature Publishing Group, 2006. https://doi.org/10.1038/nature04523. ieee: O. Hosten, M. Rakher, J. Barreiro, N. Peters, and P. Kwiat, “Counterfactual quantum computation through quantum interrogation,” Nature, vol. 439, no. 7079. Nature Publishing Group, pp. 949–952, 2006. ista: Hosten O, Rakher M, Barreiro J, Peters N, Kwiat P. 2006. Counterfactual quantum computation through quantum interrogation. Nature. 439(7079), 949–952. mla: Hosten, Onur, et al. “Counterfactual Quantum Computation through Quantum Interrogation.” Nature, vol. 439, no. 7079, Nature Publishing Group, 2006, pp. 949–52, doi:10.1038/nature04523. short: O. Hosten, M. Rakher, J. Barreiro, N. Peters, P. Kwiat, Nature 439 (2006) 949–952. date_created: 2018-12-11T11:47:18Z date_published: 2006-02-23T00:00:00Z date_updated: 2021-01-12T08:03:29Z day: '23' doi: 10.1038/nature04523 extern: 1 intvolume: ' 439' issue: '7079' month: '02' page: 949 - 952 publication: Nature publication_status: published publisher: Nature Publishing Group publist_id: '7235' quality_controlled: 0 status: public title: Counterfactual quantum computation through quantum interrogation type: journal_article volume: 439 year: '2006' ... --- _id: '583' abstract: - lang: eng text: Visible light photon counters (VLPCs) and solid-state photomultipliers (SSPMs) facilitate efficient single-photon detection. We are attempting to improve their efficiency, previously limited to < 88% by coupling losses, via anti-reflection coatings, better electronics and cryogenics. author: - first_name: Radhika full_name: Rangarajan, Radhika last_name: Rangarajan - first_name: Nicholas full_name: Peters, Nicholas A last_name: Peters - first_name: Onur full_name: Onur Hosten id: 4C02D85E-F248-11E8-B48F-1D18A9856A87 last_name: Hosten orcid: 0000-0002-2031-204X - first_name: Joseph full_name: Altepeter, Joseph B last_name: Altepeter - first_name: Evan full_name: Jeffrey, Evan R last_name: Jeffrey - first_name: Paul full_name: Kwiat, Paul G last_name: Kwiat citation: ama: 'Rangarajan R, Peters N, Hosten O, Altepeter J, Jeffrey E, Kwiat P. Improved single-photon detection. In: IEEE; 2006. doi:10.1109/CLEO.2006.4628641' apa: 'Rangarajan, R., Peters, N., Hosten, O., Altepeter, J., Jeffrey, E., & Kwiat, P. (2006). Improved single-photon detection. Presented at the CLEO/QELS: Conference on Lasers and Electro-Optics / Quantum Electronics and Laser Science Conference, IEEE. https://doi.org/10.1109/CLEO.2006.4628641' chicago: Rangarajan, Radhika, Nicholas Peters, Onur Hosten, Joseph Altepeter, Evan Jeffrey, and Paul Kwiat. “Improved Single-Photon Detection.” IEEE, 2006. https://doi.org/10.1109/CLEO.2006.4628641. ieee: 'R. Rangarajan, N. Peters, O. Hosten, J. Altepeter, E. Jeffrey, and P. Kwiat, “Improved single-photon detection,” presented at the CLEO/QELS: Conference on Lasers and Electro-Optics / Quantum Electronics and Laser Science Conference, 2006.' ista: 'Rangarajan R, Peters N, Hosten O, Altepeter J, Jeffrey E, Kwiat P. 2006. Improved single-photon detection. CLEO/QELS: Conference on Lasers and Electro-Optics / Quantum Electronics and Laser Science Conference.' mla: Rangarajan, Radhika, et al. Improved Single-Photon Detection. IEEE, 2006, doi:10.1109/CLEO.2006.4628641. short: R. Rangarajan, N. Peters, O. Hosten, J. Altepeter, E. Jeffrey, P. Kwiat, in:, IEEE, 2006. conference: name: 'CLEO/QELS: Conference on Lasers and Electro-Optics / Quantum Electronics and Laser Science Conference' date_created: 2018-12-11T11:47:19Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T08:03:43Z day: '01' doi: 10.1109/CLEO.2006.4628641 extern: 1 month: '01' publication_status: published publisher: IEEE publist_id: '7232' quality_controlled: 0 status: public title: Improved single-photon detection type: conference year: '2006' ...