--- _id: '4237' abstract: - lang: eng text: The growth function of populations is central in biomathematics. The main dogma is the existence of density-dependence mechanisms, which can be modelled with distinct functional forms that depend on the size of the Population. One important class of regulatory functions is the theta-logistic, which generalizes the logistic equation. Using this model as a motivation, this paper introduces a simple dynamical reformulation that generalizes many growth functions. The reformulation consists of two equations, one for population size, and one for the growth rate. Furthermore, the model shows that although population is density-dependent, the dynamics of the growth rate does not depend either on population size, nor on the carrying capacity. Actually, the growth equation is uncoupled from the population size equation, and the model has only two parameters, a Malthusian parameter rho and a competition coefficient theta. Distinct sign combinations of these parameters reproduce not only the family of theta-logistics, but also the van Bertalanffy, Gompertz and Potential Growth equations, among other possibilities. It is also shown that, except for two critical points, there is a general size-scaling relation that includes those appearing in the most important allometric theories, including the recently proposed Metabolic Theory of Ecology. With this model, several issues of general interest are discussed such as the growth of animal population, extinctions, cell growth and allometry, and the effect of environment over a population. (c) 2005 Elsevier Ltd. All rights reserved. article_processing_charge: No author: - first_name: Harold full_name: de Vladar, Harold id: 2A181218-F248-11E8-B48F-1D18A9856A87 last_name: de Vladar orcid: 0000-0002-5985-7653 citation: ama: de Vladar H. Density-dependence as a size-independent regulatory mechanism. Journal of Theoretical Biology. 2006;238(2):245-256. doi:3802 apa: de Vladar, H. (2006). Density-dependence as a size-independent regulatory mechanism. Journal of Theoretical Biology. Elsevier. https://doi.org/3802 chicago: Vladar, Harold de. “Density-Dependence as a Size-Independent Regulatory Mechanism.” Journal of Theoretical Biology. Elsevier, 2006. https://doi.org/3802. ieee: H. de Vladar, “Density-dependence as a size-independent regulatory mechanism,” Journal of Theoretical Biology, vol. 238, no. 2. Elsevier, pp. 245–256, 2006. ista: de Vladar H. 2006. Density-dependence as a size-independent regulatory mechanism. Journal of Theoretical Biology. 238(2), 245–256. mla: de Vladar, Harold. “Density-Dependence as a Size-Independent Regulatory Mechanism.” Journal of Theoretical Biology, vol. 238, no. 2, Elsevier, 2006, pp. 245–56, doi:3802. short: H. de Vladar, Journal of Theoretical Biology 238 (2006) 245–256. date_created: 2018-12-11T12:07:46Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T07:55:31Z day: '01' doi: '3802' extern: '1' intvolume: ' 238' issue: '2' language: - iso: eng month: '01' oa_version: None page: 245 - 256 publication: Journal of Theoretical Biology publication_status: published publisher: Elsevier publist_id: '1878' status: public title: Density-dependence as a size-independent regulatory mechanism type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 238 year: '2006' ... --- _id: '4235' author: - first_name: Harold full_name: Harold Vladar id: 2A181218-F248-11E8-B48F-1D18A9856A87 last_name: Vladar orcid: 0000-0002-5985-7653 - first_name: J. full_name: González,J. A last_name: González citation: ama: de Vladar H, González J. Dynamic response of cancer under the influence of immunological activity and therapy. Journal of Theoretical Biology. 2006:91-109. apa: de Vladar, H., & González, J. (2006). Dynamic response of cancer under the influence of immunological activity and therapy. Journal of Theoretical Biology. Elsevier. chicago: Vladar, Harold de, and J. González. “Dynamic Response of Cancer under the Influence of Immunological Activity and Therapy.” Journal of Theoretical Biology. Elsevier, 2006. ieee: H. de Vladar and J. González, “Dynamic response of cancer under the influence of immunological activity and therapy,” Journal of Theoretical Biology. Elsevier, pp. 91–109, 2006. ista: de Vladar H, González J. 2006. Dynamic response of cancer under the influence of immunological activity and therapy. Journal of Theoretical Biology., 91–109. mla: de Vladar, Harold, and J. González. “Dynamic Response of Cancer under the Influence of Immunological Activity and Therapy.” Journal of Theoretical Biology, Elsevier, 2006, pp. 91–109. short: H. de Vladar, J. González, Journal of Theoretical Biology (2006) 91–109. date_created: 2018-12-11T12:07:45Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T07:55:30Z day: '01' extern: 1 month: '01' page: 91 - 109 publication: Journal of Theoretical Biology publication_status: published publisher: Elsevier publist_id: '1879' quality_controlled: 0 status: public title: Dynamic response of cancer under the influence of immunological activity and therapy type: journal_article year: '2006' ... --- _id: '4248' abstract: - lang: eng text: 'In finite populations, genetic drift generates interference between selected loci, causing advantageous alleles to be found more often on different chromosomes than on the same chromosome, which reduces the rate of adaptation. This “Hill–Robertson effect” generates indirect selection to increase recombination rates. We present a new method to quantify the strength of this selection. Our model represents a new beneficial allele (A) entering a population as a single copy, while another beneficial allele (B) is sweeping at another locus. A third locus affects the recombination rate between selected loci. Using a branching process model, we calculate the probability distribution of the number of copies of A on the different genetic backgrounds, after it is established but while it is still rare. Then, we use a deterministic model to express the change in frequency of the recombination modifier, due to hitchhiking, as A goes to fixation. We show that this method can give good estimates of selection for recombination. Moreover, it shows that recombination is selected through two different effects: it increases the fixation probability of new alleles, and it accelerates selective sweeps. The relative importance of these two effects depends on the relative times of occurrence of the beneficial alleles.' author: - first_name: Denis full_name: Roze, Denis last_name: Roze - first_name: Nicholas H full_name: Nicholas Barton id: 4880FE40-F248-11E8-B48F-1D18A9856A87 last_name: Barton orcid: 0000-0002-8548-5240 citation: ama: Roze D, Barton NH. The Hill-Robertson effect and the evolution of recombination. Genetics. 2006;173(3):1793-1811. doi:10.1534/genetics.106.058586 apa: Roze, D., & Barton, N. H. (2006). The Hill-Robertson effect and the evolution of recombination. Genetics. Genetics Society of America. https://doi.org/10.1534/genetics.106.058586 chicago: Roze, Denis, and Nicholas H Barton. “The Hill-Robertson Effect and the Evolution of Recombination.” Genetics. Genetics Society of America, 2006. https://doi.org/10.1534/genetics.106.058586 . ieee: D. Roze and N. H. Barton, “The Hill-Robertson effect and the evolution of recombination,” Genetics, vol. 173, no. 3. Genetics Society of America, pp. 1793–1811, 2006. ista: Roze D, Barton NH. 2006. The Hill-Robertson effect and the evolution of recombination. Genetics. 173(3), 1793–1811. mla: Roze, Denis, and Nicholas H. Barton. “The Hill-Robertson Effect and the Evolution of Recombination.” Genetics, vol. 173, no. 3, Genetics Society of America, 2006, pp. 1793–811, doi:10.1534/genetics.106.058586 . short: D. Roze, N.H. Barton, Genetics 173 (2006) 1793–1811. date_created: 2018-12-11T12:07:50Z date_published: 2006-07-01T00:00:00Z date_updated: 2021-01-12T07:55:36Z day: '01' doi: '10.1534/genetics.106.058586 ' extern: 1 intvolume: ' 173' issue: '3' month: '07' page: 1793 - 1811 publication: Genetics publication_status: published publisher: Genetics Society of America publist_id: '1854' quality_controlled: 0 status: public title: The Hill-Robertson effect and the evolution of recombination type: journal_article volume: 173 year: '2006' ... --- _id: '4250' abstract: - lang: eng text: A recent analysis has shown that divergence between human and chimpanzee varies greatly across the genome. Although this is consistent with ‘hybridisation’ between the diverging human and chimp lineages, such observations can be explained more simply by the null model of allopatric speciation. author: - first_name: Nicholas H full_name: Nicholas Barton id: 4880FE40-F248-11E8-B48F-1D18A9856A87 last_name: Barton orcid: 0000-0002-8548-5240 citation: ama: 'Barton NH. Evolutionary Biology: How did the human species form? Current Biology. 2006;16(16):647-650. doi:10.1016/j.cub.2006.07.032' apa: 'Barton, N. H. (2006). Evolutionary Biology: How did the human species form? Current Biology. Cell Press. https://doi.org/10.1016/j.cub.2006.07.032' chicago: 'Barton, Nicholas H. “Evolutionary Biology: How Did the Human Species Form?” Current Biology. Cell Press, 2006. https://doi.org/10.1016/j.cub.2006.07.032.' ieee: 'N. H. Barton, “Evolutionary Biology: How did the human species form?,” Current Biology, vol. 16, no. 16. Cell Press, pp. 647–650, 2006.' ista: 'Barton NH. 2006. Evolutionary Biology: How did the human species form? Current Biology. 16(16), 647–650.' mla: 'Barton, Nicholas H. “Evolutionary Biology: How Did the Human Species Form?” Current Biology, vol. 16, no. 16, Cell Press, 2006, pp. 647–50, doi:10.1016/j.cub.2006.07.032.' short: N.H. Barton, Current Biology 16 (2006) 647–650. date_created: 2018-12-11T12:07:51Z date_published: 2006-08-22T00:00:00Z date_updated: 2019-04-26T07:22:41Z day: '22' doi: 10.1016/j.cub.2006.07.032 extern: 1 intvolume: ' 16' issue: '16' month: '08' page: 647 - 650 publication: Current Biology publication_status: published publisher: Cell Press publist_id: '1850' quality_controlled: 0 status: public title: 'Evolutionary Biology: How did the human species form?' type: review volume: 16 year: '2006' ... --- _id: '4359' alternative_title: - LNCS 3855 author: - first_name: Thomas full_name: Thomas Wies id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Viktor full_name: Kuncak, Viktor last_name: Kuncak - first_name: Patrick full_name: Lam,Patrick last_name: Lam - first_name: Andreas full_name: Podelski,Andreas last_name: Podelski - first_name: Martin full_name: Rinard,Martin last_name: Rinard citation: ama: 'Wies T, Kuncak V, Lam P, Podelski A, Rinard M. Field Constraint Analysis. In: Springer; 2006:157-173. doi:1551' apa: 'Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. (2006). Field Constraint Analysis (pp. 157–173). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. https://doi.org/1551' chicago: Wies, Thomas, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard. “Field Constraint Analysis,” 157–73. Springer, 2006. https://doi.org/1551. ieee: 'T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard, “Field Constraint Analysis,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, 2006, pp. 157–173.' ista: 'Wies T, Kuncak V, Lam P, Podelski A, Rinard M. 2006. Field Constraint Analysis. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS 3855, , 157–173.' mla: Wies, Thomas, et al. Field Constraint Analysis. Springer, 2006, pp. 157–73, doi:1551. short: T. Wies, V. Kuncak, P. Lam, A. Podelski, M. Rinard, in:, Springer, 2006, pp. 157–173. conference: name: 'VMCAI: Verification, Model Checking and Abstract Interpretation' date_created: 2018-12-11T12:08:27Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T07:56:23Z day: '01' doi: '1551' extern: 1 month: '01' page: 157 - 173 publication_status: published publisher: Springer publist_id: '1097' quality_controlled: 0 status: public title: Field Constraint Analysis type: conference year: '2006' ... --- _id: '4373' alternative_title: - LNCS author: - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Dejan full_name: Dejan Nickovic id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Amir full_name: Pnueli,Amir last_name: Pnueli citation: ama: 'Maler O, Nickovic D, Pnueli A. Real Time Temporal Logic: Past, Present, Future. In: Springer; 2006:2-16. doi:1571' apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). Real Time Temporal Logic: Past, Present, Future (pp. 2–16). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. https://doi.org/1571' chicago: 'Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Real Time Temporal Logic: Past, Present, Future,” 2–16. Springer, 2006. https://doi.org/1571.' ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “Real Time Temporal Logic: Past, Present, Future,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, pp. 2–16.' ista: 'Maler O, Nickovic D, Pnueli A. 2006. Real Time Temporal Logic: Past, Present, Future. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 2–16.' mla: 'Maler, Oded, et al. Real Time Temporal Logic: Past, Present, Future. Springer, 2006, pp. 2–16, doi:1571.' short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 2–16. conference: name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' date_created: 2018-12-11T12:08:31Z date_published: 2006-01-23T00:00:00Z date_updated: 2021-01-12T07:56:29Z day: '23' doi: '1571' extern: 1 month: '01' page: 2 - 16 publication_status: published publisher: Springer publist_id: '1084' quality_controlled: 0 status: public title: 'Real Time Temporal Logic: Past, Present, Future' type: conference year: '2006' ... --- _id: '4374' alternative_title: - LNCS author: - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Dejan full_name: Dejan Nickovic id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Amir full_name: Pnueli,Amir last_name: Pnueli citation: ama: 'Maler O, Nickovic D, Pnueli A. From MITL to Timed Automata. In: Springer; 2006:274-289. doi:1570' apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). From MITL to Timed Automata (pp. 274–289). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. https://doi.org/1570' chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “From MITL to Timed Automata,” 274–89. Springer, 2006. https://doi.org/1570. ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “From MITL to Timed Automata,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, pp. 274–289.' ista: 'Maler O, Nickovic D, Pnueli A. 2006. From MITL to Timed Automata. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 274–289.' mla: Maler, Oded, et al. From MITL to Timed Automata. Springer, 2006, pp. 274–89, doi:1570. short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2006, pp. 274–289. conference: name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' date_created: 2018-12-11T12:08:31Z date_published: 2006-10-19T00:00:00Z date_updated: 2021-01-12T07:56:30Z day: '19' doi: '1570' extern: 1 month: '10' page: 274 - 289 publication_status: published publisher: Springer publist_id: '1085' quality_controlled: 0 status: public title: From MITL to Timed Automata type: conference year: '2006' ... --- _id: '4406' abstract: - lang: eng text: We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata. acknowledgement: This research was supported in part by the NSF grants CCR-0234690 and CCR-0225610, and the Belgian FNRS grant 2.4530.02 of the FRFC project “Centre Fédéré en Vérification.” alternative_title: - LNCS author: - first_name: Martin full_name: De Wulf, Martin last_name: De Wulf - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jean full_name: Raskin, Jean-François last_name: Raskin citation: ama: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. Antichains: A new algorithm for checking universality of finite automata. In: Vol 4144. Springer; 2006:17-30. doi:10.1007/11817963_5' apa: 'De Wulf, M., Doyen, L., Henzinger, T. A., & Raskin, J. (2006). Antichains: A new algorithm for checking universality of finite automata (Vol. 4144, pp. 17–30). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/11817963_5' chicago: 'De Wulf, Martin, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Antichains: A New Algorithm for Checking Universality of Finite Automata,” 4144:17–30. Springer, 2006. https://doi.org/10.1007/11817963_5.' ieee: 'M. De Wulf, L. Doyen, T. A. Henzinger, and J. Raskin, “Antichains: A new algorithm for checking universality of finite automata,” presented at the CAV: Computer Aided Verification, 2006, vol. 4144, pp. 17–30.' ista: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. 2006. Antichains: A new algorithm for checking universality of finite automata. CAV: Computer Aided Verification, LNCS, vol. 4144, 17–30.' mla: 'De Wulf, Martin, et al. Antichains: A New Algorithm for Checking Universality of Finite Automata. Vol. 4144, Springer, 2006, pp. 17–30, doi:10.1007/11817963_5.' short: M. De Wulf, L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2006, pp. 17–30. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:08:41Z date_published: 2006-08-08T00:00:00Z date_updated: 2021-01-12T07:56:45Z day: '08' doi: 10.1007/11817963_5 extern: 1 intvolume: ' 4144' month: '08' page: 17 - 30 publication_status: published publisher: Springer publist_id: '326' quality_controlled: 0 status: public title: 'Antichains: A new algorithm for checking universality of finite automata' type: conference volume: 4144 year: '2006' ... --- _id: '4401' alternative_title: - LNCS author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Pavol full_name: Pavol Cerny id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 last_name: Cerny - first_name: Steve full_name: Zdancewic,Steve last_name: Zdancewic citation: ama: 'Alur R, Cerny P, Zdancewic S. Preserving Secrecy Under Refinement. In: Springer; 2006:107-118. doi:1543' apa: 'Alur, R., Cerny, P., & Zdancewic, S. (2006). Preserving Secrecy Under Refinement (pp. 107–118). Presented at the ICALP: Automata, Languages and Programming, Springer. https://doi.org/1543' chicago: Alur, Rajeev, Pavol Cerny, and Steve Zdancewic. “Preserving Secrecy Under Refinement,” 107–18. Springer, 2006. https://doi.org/1543. ieee: 'R. Alur, P. Cerny, and S. Zdancewic, “Preserving Secrecy Under Refinement,” presented at the ICALP: Automata, Languages and Programming, 2006, pp. 107–118.' ista: 'Alur R, Cerny P, Zdancewic S. 2006. Preserving Secrecy Under Refinement. ICALP: Automata, Languages and Programming, LNCS, , 107–118.' mla: Alur, Rajeev, et al. Preserving Secrecy Under Refinement. Springer, 2006, pp. 107–18, doi:1543. short: R. Alur, P. Cerny, S. Zdancewic, in:, Springer, 2006, pp. 107–118. conference: name: 'ICALP: Automata, Languages and Programming' date_created: 2018-12-11T12:08:40Z date_published: 2006-01-01T00:00:00Z date_updated: 2021-01-12T07:56:42Z day: '01' doi: '1543' extern: 1 month: '01' page: 107 - 118 publication_status: published publisher: Springer publist_id: '1054' quality_controlled: 0 status: public title: Preserving Secrecy Under Refinement type: conference year: '2006' ... --- _id: '4437' abstract: - lang: eng text: The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies. acknowledgement: This research was supported in part by the Swiss National Science Foundation. 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: Nir full_name: Piterman, Nir last_name: Piterman citation: ama: 'Henzinger TA, Piterman N. Solving games without determinization. In: Vol 4207. Springer; 2006:395-410. doi:10.1007/11874683_26' apa: 'Henzinger, T. A., & Piterman, N. (2006). Solving games without determinization (Vol. 4207, pp. 395–410). Presented at the CSL: Computer Science Logic, Springer. https://doi.org/10.1007/11874683_26' chicago: Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization,” 4207:395–410. Springer, 2006. https://doi.org/10.1007/11874683_26. ieee: 'T. A. Henzinger and N. Piterman, “Solving games without determinization,” presented at the CSL: Computer Science Logic, 2006, vol. 4207, pp. 395–410.' ista: 'Henzinger TA, Piterman N. 2006. Solving games without determinization. CSL: Computer Science Logic, LNCS, vol. 4207, 395–410.' mla: Henzinger, Thomas A., and Nir Piterman. Solving Games without Determinization. Vol. 4207, Springer, 2006, pp. 395–410, doi:10.1007/11874683_26. short: T.A. Henzinger, N. Piterman, in:, Springer, 2006, pp. 395–410. conference: name: 'CSL: Computer Science Logic' date_created: 2018-12-11T12:08:51Z date_published: 2006-09-20T00:00:00Z date_updated: 2021-01-12T07:56:58Z day: '20' doi: 10.1007/11874683_26 extern: 1 intvolume: ' 4207' month: '09' page: 395 - 410 publication_status: published publisher: Springer publist_id: '295' quality_controlled: 0 status: public title: Solving games without determinization type: conference volume: 4207 year: '2006' ... --- _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' ...