--- _id: '6158' abstract: - lang: eng text: Wild isolates of Caenorhabditis elegans can feed either alone or in groups1,2. This natural variation in behaviour is associated with a single residue difference in NPR-1, a predicted G-protein-coupled neuropeptide receptor related to Neuropeptide Y receptors2. Here we show that the NPR-1 isoform associated with solitary feeding acts in neurons exposed to the body fluid to inhibit social feeding. Furthermore, suppressing the activity of these neurons, called AQR, PQR and URX, using an activated K+ channel, inhibits social feeding. NPR-1 activity in AQR, PQR and URX neurons seems to suppress social feeding by antagonizing signalling through a cyclic GMP-gated ion channel encoded by tax-2 and tax-4. We show that mutations in tax-2 or tax-4 disrupt social feeding, and that tax-4 is required in several neurons for social feeding, including one or more of AQR, PQR and URX. The AQR, PQR and URX neurons are unusual in C. elegans because they are directly exposed to the pseudocoelomic body fluid3. Our data suggest a model in which these neurons integrate antagonistic signals to control the choice between social and solitary feeding behaviour. author: - first_name: Juliet C. full_name: Coates, Juliet C. last_name: Coates - first_name: Mario full_name: de Bono, Mario id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87 last_name: de Bono orcid: 0000-0001-8347-0443 citation: ama: Coates JC, de Bono M. Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans. Nature. 2002;419(6910):925-929. doi:10.1038/nature01170 apa: Coates, J. C., & de Bono, M. (2002). Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans. Nature. Springer Nature. https://doi.org/10.1038/nature01170 chicago: Coates, Juliet C., and Mario de Bono. “Antagonistic Pathways in Neurons Exposed to Body Fluid Regulate Social Feeding in Caenorhabditis Elegans.” Nature. Springer Nature, 2002. https://doi.org/10.1038/nature01170. ieee: J. C. Coates and M. de Bono, “Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans,” Nature, vol. 419, no. 6910. Springer Nature, pp. 925–929, 2002. ista: Coates JC, de Bono M. 2002. Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans. Nature. 419(6910), 925–929. mla: Coates, Juliet C., and Mario de Bono. “Antagonistic Pathways in Neurons Exposed to Body Fluid Regulate Social Feeding in Caenorhabditis Elegans.” Nature, vol. 419, no. 6910, Springer Nature, 2002, pp. 925–29, doi:10.1038/nature01170. short: J.C. Coates, M. de Bono, Nature 419 (2002) 925–929. date_created: 2019-03-21T10:09:20Z date_published: 2002-10-31T00:00:00Z date_updated: 2021-01-12T08:06:26Z day: '31' doi: 10.1038/nature01170 extern: '1' external_id: pmid: - '12410311' intvolume: ' 419' issue: '6910' language: - iso: eng month: '10' oa_version: None page: 925-929 pmid: 1 publication: Nature publication_identifier: issn: - 0028-0836 publication_status: published publisher: Springer Nature quality_controlled: '1' status: public title: Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 419 year: '2002' ... --- _id: '6159' abstract: - lang: eng text: 'Natural Caenorhabditis elegans isolates exhibit either social or solitary feeding on bacteria. We show here that social feeding is induced by nociceptive neurons that detect adverse or stressful conditions. Ablation of the nociceptive neurons ASH and ADL transforms social animals into solitary feeders. Social feeding is probably due to the sensation of noxious chemicals by ASH and ADL neurons; it requires the genes ocr-2 and osm-9, which encode TRP-related transduction channels, and odr-4 and odr-8, which are required to localize sensory chemoreceptors to cilia. Other sensory neurons may suppress social feeding, as social feeding in ocr-2 and odr-4 mutants is restored by mutations in osm-3, a gene required for the development of 26 ciliated sensory neurons. Our data suggest a model for regulation of social feeding by opposing sensory inputs: aversive inputs to nociceptive neurons promote social feeding, whereas antagonistic inputs from neurons that express osm-3 inhibit aggregation.' author: - first_name: Mario full_name: de Bono, Mario id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87 last_name: de Bono orcid: 0000-0001-8347-0443 - first_name: David M. full_name: Tobin, David M. last_name: Tobin - first_name: M. Wayne full_name: Davis, M. Wayne last_name: Davis - first_name: Leon full_name: Avery, Leon last_name: Avery - first_name: Cornelia I. full_name: Bargmann, Cornelia I. last_name: Bargmann citation: ama: de Bono M, Tobin DM, Davis MW, Avery L, Bargmann CI. Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli. Nature. 2002;419(6910):899-903. doi:10.1038/nature01169 apa: de Bono, M., Tobin, D. M., Davis, M. W., Avery, L., & Bargmann, C. I. (2002). Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli. Nature. Springer Nature. https://doi.org/10.1038/nature01169 chicago: Bono, Mario de, David M. Tobin, M. Wayne Davis, Leon Avery, and Cornelia I. Bargmann. “Social Feeding in Caenorhabditis Elegans Is Induced by Neurons That Detect Aversive Stimuli.” Nature. Springer Nature, 2002. https://doi.org/10.1038/nature01169. ieee: M. de Bono, D. M. Tobin, M. W. Davis, L. Avery, and C. I. Bargmann, “Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli,” Nature, vol. 419, no. 6910. Springer Nature, pp. 899–903, 2002. ista: de Bono M, Tobin DM, Davis MW, Avery L, Bargmann CI. 2002. Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli. Nature. 419(6910), 899–903. mla: de Bono, Mario, et al. “Social Feeding in Caenorhabditis Elegans Is Induced by Neurons That Detect Aversive Stimuli.” Nature, vol. 419, no. 6910, Springer Nature, 2002, pp. 899–903, doi:10.1038/nature01169. short: M. de Bono, D.M. Tobin, M.W. Davis, L. Avery, C.I. Bargmann, Nature 419 (2002) 899–903. date_created: 2019-03-21T10:27:04Z date_published: 2002-10-31T00:00:00Z date_updated: 2021-01-12T08:06:27Z day: '31' doi: 10.1038/nature01169 extern: '1' external_id: pmid: - '12410303' intvolume: ' 419' issue: '6910' language: - iso: eng month: '10' oa_version: None page: 899-903 pmid: 1 publication: Nature publication_identifier: issn: - 0028-0836 publication_status: published publisher: Springer Nature quality_controlled: '1' status: public title: Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 419 year: '2002' ... --- _id: '4631' abstract: - lang: eng text: We present a theory of timed interfaces, which is capable of specifying both the timing of the inputs a component expects from the environment, and the timing of the outputs it can produce. Two timed interfaces are compatible if there is a way to use them together such that their timing expectations are met. Our theory provides algorithms for checking the compatibility between two interfaces and for deriving the composite interface; the theory can thus be viewed as a type system for real-time interaction. Technically, a timed interface is encoded as a timed game between two players, representing the inputs and outputs of the component. The algorithms for compatibility checking and interface composition are thus derived from algorithms for solving timed games. acknowledgement: This research was supported in part by the NSF CAREER award CCR-0132780, the NSF grant CCR-9988172 the AFOSR MURI grant F49620-00-1-0327, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, and the ONR grant N00014-02-1-0671. alternative_title: - LNCS article_processing_charge: No author: - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Mariëlle full_name: Stoelinga, Mariëlle last_name: Stoelinga citation: ama: 'De Alfaro L, Henzinger TA, Stoelinga M. Timed interfaces. In: Proceedings of the 2nd International Conference on Embedded Software. Vol 2491. ACM; 2002:108-122. doi:10.1007/3-540-45828-X_9' apa: 'De Alfaro, L., Henzinger, T. A., & Stoelinga, M. (2002). Timed interfaces. In Proceedings of the 2nd International Conference on Embedded Software (Vol. 2491, pp. 108–122). Grenoble, France: ACM. https://doi.org/10.1007/3-540-45828-X_9' chicago: De Alfaro, Luca, Thomas A Henzinger, and Mariëlle Stoelinga. “Timed Interfaces.” In Proceedings of the 2nd International Conference on Embedded Software, 2491:108–22. ACM, 2002. https://doi.org/10.1007/3-540-45828-X_9. ieee: L. De Alfaro, T. A. Henzinger, and M. Stoelinga, “Timed interfaces,” in Proceedings of the 2nd International Conference on Embedded Software, Grenoble, France, 2002, vol. 2491, pp. 108–122. ista: 'De Alfaro L, Henzinger TA, Stoelinga M. 2002. Timed interfaces. Proceedings of the 2nd International Conference on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2491, 108–122.' mla: De Alfaro, Luca, et al. “Timed Interfaces.” Proceedings of the 2nd International Conference on Embedded Software, vol. 2491, ACM, 2002, pp. 108–22, doi:10.1007/3-540-45828-X_9. short: L. De Alfaro, T.A. Henzinger, M. Stoelinga, in:, Proceedings of the 2nd International Conference on Embedded Software, ACM, 2002, pp. 108–122. conference: end_date: 2002-10-09 location: Grenoble, France name: 'EMSOFT: Embedded Software ' start_date: 2002-10-07 date_created: 2018-12-11T12:09:51Z date_published: 2002-10-24T00:00:00Z date_updated: 2023-06-02T10:00:32Z day: '24' doi: 10.1007/3-540-45828-X_9 extern: '1' intvolume: ' 2491' language: - iso: eng month: '10' oa_version: None page: 108 - 122 publication: Proceedings of the 2nd International Conference on Embedded Software publication_identifier: isbn: - '9783540443070' publication_status: published publisher: ACM publist_id: '76' quality_controlled: '1' status: public title: Timed interfaces type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2491 year: '2002' ... --- _id: '4562' abstract: - lang: eng text: We present interface models that describe both the input assumptions of a component, and its output behavior. By enabling us to check that the input assumptions of a component are met in a design, interface models provide a compatibility check for component-based design. When refining a design into an implementation, interface models require that the output behavior of a component satisfies the design specification only when the input assumptions of the specification are satisfied, yielding greater flexibility in the choice of implementations. Technically, our interface models are games between two players, Input and Output; the duality of the players accounts for the dual roles of inputs and outputs in composition and refinement. We present two interface models in detail, one for a simple synchronous form of interaction between components typical in hardware, and the other for more complex synchronous interactions on bidirectional connections. As an example, we specify the interface of a bidirectional bus, with the input assumption that at any time at most one component has write access to the bus. For these interface models, we present algorithms for compatibility and refinement checking, and we describe efficient symbolic implementations. acknowledgement: This research was supported in part by the AFOSR grant F49620-00-1-0327, the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the NSF grant CCR-9988172, the SRC grant 99-TJ-683.003, and the NSF CAREER award CCR-0132780. alternative_title: - LNCS article_processing_charge: No author: - first_name: Arindam full_name: Chakrabarti, Arindam last_name: Chakrabarti - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Freddy full_name: Mang, Freddy last_name: Mang citation: ama: 'Chakrabarti A, De Alfaro L, Henzinger TA, Mang F. Synchronous and bidirectional component interfaces. In: Proceedings of the 14th International Conference on Computer Aided Verification. Vol 2404. Springer; 2002:414-427. doi:10.1007/3-540-45657-0_34' apa: 'Chakrabarti, A., De Alfaro, L., Henzinger, T. A., & Mang, F. (2002). Synchronous and bidirectional component interfaces. In Proceedings of the 14th International Conference on Computer Aided Verification (Vol. 2404, pp. 414–427). Copenhagen, Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_34' chicago: Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, and Freddy Mang. “Synchronous and Bidirectional Component Interfaces.” In Proceedings of the 14th International Conference on Computer Aided Verification, 2404:414–27. Springer, 2002. https://doi.org/10.1007/3-540-45657-0_34. ieee: A. Chakrabarti, L. De Alfaro, T. A. Henzinger, and F. Mang, “Synchronous and bidirectional component interfaces,” in Proceedings of the 14th International Conference on Computer Aided Verification, Copenhagen, Denmark, 2002, vol. 2404, pp. 414–427. ista: 'Chakrabarti A, De Alfaro L, Henzinger TA, Mang F. 2002. Synchronous and bidirectional component interfaces. Proceedings of the 14th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 414–427.' mla: Chakrabarti, Arindam, et al. “Synchronous and Bidirectional Component Interfaces.” Proceedings of the 14th International Conference on Computer Aided Verification, vol. 2404, Springer, 2002, pp. 414–27, doi:10.1007/3-540-45657-0_34. short: A. Chakrabarti, L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 14th International Conference on Computer Aided Verification, Springer, 2002, pp. 414–427. conference: end_date: 2002-07-31 location: Copenhagen, Denmark name: 'CAV: Computer Aided Verification' start_date: 2002-07-27 date_created: 2018-12-11T12:09:29Z date_published: 2002-06-19T00:00:00Z date_updated: 2023-06-02T12:01:22Z day: '19' doi: 10.1007/3-540-45657-0_34 extern: '1' intvolume: ' 2404' language: - iso: eng month: '06' oa_version: None page: 414 - 427 publication: Proceedings of the 14th International Conference on Computer Aided Verification publication_identifier: isbn: - '9783540439974' publication_status: published publisher: Springer publist_id: '146' quality_controlled: '1' scopus_import: '1' status: public title: Synchronous and bidirectional component interfaces type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2404 year: '2002' ... --- _id: '4565' abstract: - lang: eng text: "In the literature, we find several formulations of the control\r\nproblem for timed and hybrid systems. We argue that formulations where\r\na controller can cause an action at any point in dense (rational or real)\r\ntime are problematic, by presenting an example where the controller\r\nmust act faster and faster, yet causes no Zeno effects (say, the control\r\nactions are at times 0, 1/2, 1, 1 1/4, 2, 2 1/8, 3, 3 1/16 ,...). Such a controller is,\r\nof course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well- understood if the time unit, or “sampling rate” of the controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We prove that this problem is undecidable even in the special case of timed automata." acknowledgement: "Partially supported by the FNRS, Belgium, under grant 1.5.096.01.\r\nPartially supported by the DARPA SEC grant F33615-C-98-3614, the AFOSR MURI grant F49620-00-1-0327, the NSF Theory grant CCR-9988172, and the MARCO GSRC grant 98-DT-660.\r\nPartially supported by a “Crédit aux chercheurs” from the Belgian National Fund for Scientific Research." alternative_title: - LNCS article_processing_charge: No author: - first_name: Franck full_name: Cassez, Franck last_name: Cassez - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jean full_name: Raskin, Jean last_name: Raskin citation: ama: 'Cassez F, Henzinger TA, Raskin J. A comparison of control problems for timed and hybrid systems. In: Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control. Vol 2289. Springer; 2002:134-148. doi:10.1007/3-540-45873-5_13' apa: 'Cassez, F., Henzinger, T. A., & Raskin, J. (2002). A comparison of control problems for timed and hybrid systems. In Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control (Vol. 2289, pp. 134–148). Stanford, CA, USA: Springer. https://doi.org/10.1007/3-540-45873-5_13' chicago: 'Cassez, Franck, Thomas A Henzinger, and Jean Raskin. “A Comparison of Control Problems for Timed and Hybrid Systems.” In Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, 2289:134–48. Springer, 2002. https://doi.org/10.1007/3-540-45873-5_13.' ieee: 'F. Cassez, T. A. Henzinger, and J. Raskin, “A comparison of control problems for timed and hybrid systems,” in Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, Stanford, CA, USA, 2002, vol. 2289, pp. 134–148.' ista: 'Cassez F, Henzinger TA, Raskin J. 2002. A comparison of control problems for timed and hybrid systems. Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 2289, 134–148.' mla: 'Cassez, Franck, et al. “A Comparison of Control Problems for Timed and Hybrid Systems.” Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, vol. 2289, Springer, 2002, pp. 134–48, doi:10.1007/3-540-45873-5_13.' short: 'F. Cassez, T.A. Henzinger, J. Raskin, in:, Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, Springer, 2002, pp. 134–148.' conference: end_date: 2002-03-27 location: Stanford, CA, USA name: 'HSCC: Hybrid Systems - Computation and Control' start_date: 2002-03-25 date_created: 2018-12-11T12:09:30Z date_published: 2002-03-14T00:00:00Z date_updated: 2023-06-02T10:29:10Z day: '14' doi: 10.1007/3-540-45873-5_13 extern: '1' intvolume: ' 2289' language: - iso: eng month: '03' oa_version: None page: 134 - 148 publication: 'Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control' publication_identifier: isbn: - '9783540433217' publication_status: published publisher: Springer publist_id: '144' quality_controlled: '1' scopus_import: '1' status: public title: A comparison of control problems for timed and hybrid systems type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2289 year: '2002' ... --- _id: '4595' abstract: - lang: eng text: 'Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures. Every state transition of a concurrent game structure results from a choice of moves, one for each player. The players represent individual components and the environment of an open system. Concurrent game structures can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. Over structures without fairness constraints, the model-checking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic model-checking algorithm for CTL extends with few modifications to ATL. Over structures with weak-fairness constraints, ATL model checking requires the solution of 1-pair Rabin games, and can be done in polynomial time. Over structures with strong-fairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. In the case of ATL*, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time.' acknowledgement: We thank Luca de Alfaro, Kousha Etessami, Salvatore La Torre, P. Madhusudan, Amir Pnueli, Moshe Vardi, Thomas Wilke, and Mihalis Yannakakis for helpful discussions. We also thank Freddy Mang for comments on a draft of this manuscript. article_processing_charge: No article_type: original author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman citation: ama: Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. Journal of the ACM. 2002;49(5):672-713. doi:10.1145/585265.585270 apa: Alur, R., Henzinger, T. A., & Kupferman, O. (2002). Alternating-time temporal logic. Journal of the ACM. ACM. https://doi.org/10.1145/585265.585270 chicago: Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time Temporal Logic.” Journal of the ACM. ACM, 2002. https://doi.org/10.1145/585265.585270. ieee: R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,” Journal of the ACM, vol. 49, no. 5. ACM, pp. 672–713, 2002. ista: Alur R, Henzinger TA, Kupferman O. 2002. Alternating-time temporal logic. Journal of the ACM. 49(5), 672–713. mla: Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” Journal of the ACM, vol. 49, no. 5, ACM, 2002, pp. 672–713, doi:10.1145/585265.585270. short: R. Alur, T.A. Henzinger, O. Kupferman, Journal of the ACM 49 (2002) 672–713. date_created: 2018-12-11T12:09:40Z date_published: 2002-09-01T00:00:00Z date_updated: 2023-06-02T10:07:22Z day: '01' doi: 10.1145/585265.585270 extern: '1' intvolume: ' 49' issue: '5' language: - iso: eng month: '09' oa_version: None page: 672 - 713 publication: Journal of the ACM publication_identifier: issn: - 0004-5411 publication_status: published publisher: ACM publist_id: '110' quality_controlled: '1' scopus_import: '1' status: public title: Alternating-time temporal logic type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 49 year: '2002' ... --- _id: '4471' abstract: - lang: eng text: The sequential synthesis problem, which is closely related to Church’s solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. In this paper we solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Büchi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. We also study the problem of deciding whether a given specification is uninitialized, that is, if its uninitialized and initialized synthesis problems coincide. We show that this problem has, for each specification formalism, the same complexity as the equivalence problem. acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003, the DARPA contract NAG2-1214, and the NSF grant CCR-9988172. alternative_title: - LNCS article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Sriram full_name: Krishnan, Sriram last_name: Krishnan - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman - first_name: Freddy full_name: Mang, Freddy last_name: Mang citation: ama: 'Henzinger TA, Krishnan S, Kupferman O, Mang F. Synthesis of uninitialized systems. In: Proceedings of the 29th International Colloquium on Automata, Languages and Programming. Vol 2380. Springer; 2002:644-656. doi:10.1007/3-540-45465-9_55' apa: 'Henzinger, T. A., Krishnan, S., Kupferman, O., & Mang, F. (2002). Synthesis of uninitialized systems. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (Vol. 2380, pp. 644–656). Malaga, Spain: Springer. https://doi.org/10.1007/3-540-45465-9_55' chicago: Henzinger, Thomas A, Sriram Krishnan, Orna Kupferman, and Freddy Mang. “Synthesis of Uninitialized Systems.” In Proceedings of the 29th International Colloquium on Automata, Languages and Programming, 2380:644–56. Springer, 2002. https://doi.org/10.1007/3-540-45465-9_55. ieee: T. A. Henzinger, S. Krishnan, O. Kupferman, and F. Mang, “Synthesis of uninitialized systems,” in Proceedings of the 29th International Colloquium on Automata, Languages and Programming, Malaga, Spain, 2002, vol. 2380, pp. 644–656. ista: 'Henzinger TA, Krishnan S, Kupferman O, Mang F. 2002. Synthesis of uninitialized systems. Proceedings of the 29th International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2380, 644–656.' mla: Henzinger, Thomas A., et al. “Synthesis of Uninitialized Systems.” Proceedings of the 29th International Colloquium on Automata, Languages and Programming, vol. 2380, Springer, 2002, pp. 644–56, doi:10.1007/3-540-45465-9_55. short: T.A. Henzinger, S. Krishnan, O. Kupferman, F. Mang, in:, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, Springer, 2002, pp. 644–656. conference: end_date: 2002-07-13 location: Malaga, Spain name: 'ICALP: Automata, Languages and Programming' start_date: 2002-07-08 date_created: 2018-12-11T12:09:01Z date_published: 2002-06-26T00:00:00Z date_updated: 2023-06-05T08:05:13Z day: '26' doi: 10.1007/3-540-45465-9_55 extern: '1' intvolume: ' 2380' language: - iso: eng month: '06' oa_version: None page: 644 - 656 publication: Proceedings of the 29th International Colloquium on Automata, Languages and Programming publication_identifier: isbn: - '9783540438649' publication_status: published publisher: Springer publist_id: '257' quality_controlled: '1' scopus_import: '1' status: public title: Synthesis of uninitialized systems type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2380 year: '2002' ... --- _id: '4474' abstract: - lang: eng text: 'The simulation preorder for labeled transition systems is defined locally, and operationally, as a game that relates states with their immediate successor states. Simulation enjoys many appealing properties. First, simulation has a denotational characterization: system S simulates system I iff every computation tree embedded in the unrolling of I can be embedded also in the unrolling of S. Second, simulation has a logical characterization: S simulates I iff every universal branching-time formula satisfied by S is satisfied also by I. It follows that simulation is a suitable notion of implementation, and it is the coarsest abstraction of a system that preserves universal branching-time properties. Third, based on its local definition, simulation between finite-state systems can be checked in polynomial time. Finally, simulation implies trace containment, which cannot be defined locally and requires polynomial space for verification. Hence simulation is widely used both in manual and in automatic verification. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We propose a new view of fair simulation by extending the local definition of simulation to account for fairness: system View the MathML sourcefairly simulates system View the MathML source iff in the simulation game, there is a strategy that matches with each fair computation of View the MathML source a fair computation of View the MathML source. Our definition enjoys a denotational characterization and has a logical characterization: View the MathML source fairly simulates View the MathML source iff every fair computation tree (whose infinite paths are fair) embedded in the unrolling of View the MathML source can be embedded also in the unrolling of View the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by View the MathML source is satisfied also by View the MathML source (∀AFMC is the universal fragment of the alternation-free μ-calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace containment and is therefore useful as an efficiently computable local criterion for proving linear-time abstraction hierarchies of fair systems.' acknowledgement: We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers for their comments on this paper. article_processing_charge: No article_type: original author: - first_name: Thomas A full_name: Henzinger, Thomas A 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: Sriram full_name: Rajamani, Sriram last_name: Rajamani citation: ama: Henzinger TA, Kupferman O, Rajamani S. Fair simulation. Information and Computation. 2002;173(1):64-81. doi:10.1006/inco.2001.3085 apa: Henzinger, T. A., Kupferman, O., & Rajamani, S. (2002). Fair simulation. Information and Computation. Elsevier. https://doi.org/10.1006/inco.2001.3085 chicago: Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.” Information and Computation. Elsevier, 2002. https://doi.org/10.1006/inco.2001.3085. ieee: T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” Information and Computation, vol. 173, no. 1. Elsevier, pp. 64–81, 2002. ista: Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information and Computation. 173(1), 64–81. mla: Henzinger, Thomas A., et al. “Fair Simulation.” Information and Computation, vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:10.1006/inco.2001.3085. short: T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173 (2002) 64–81. date_created: 2018-12-11T12:09:02Z date_published: 2002-02-25T00:00:00Z date_updated: 2023-06-05T07:53:27Z day: '25' doi: 10.1006/inco.2001.3085 extern: '1' intvolume: ' 173' issue: '1' language: - iso: eng main_file_link: - open_access: '1' url: https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub month: '02' oa: 1 oa_version: Published Version page: 64 - 81 publication: Information and Computation publication_identifier: issn: - 0890-5401 publication_status: published publisher: Elsevier publist_id: '255' quality_controlled: '1' scopus_import: '1' status: public title: Fair simulation type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 173 year: '2002' ... --- _id: '4563' abstract: - lang: eng text: We present a formal methodology and tool for uncovering errors in the interaction of software modules. Our methodology consists of a suite of languages for defining software interfaces, and algorithms for checking interface compatibility. We focus on interfaces that explain the method-call dependencies between software modules. Such an interface makes assumptions about the environment in the form of call and availability constraints. A call constraint restricts the accessibility of local methods to certain external methods. An availability constraint restricts the accessibility of local methods to certain states of the module. For example, the interface for a file server with local methods open and read may assert that a file cannot be read without having been opened. Checking interface compatibility requires the solution of games, and in the presence of availability constraints, of pushdown games. Based on this methodology, we have implemented a tool that has uncovered incompatibilities in TinyOS, a small operating system for sensor nodes in adhoc networks. acknowledgement: This research was supported in part by the AFOSR grant F49620-00-1-0327, the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the NSF grants CCR-9988172, CCR-0085949, CCR-0132780, the SRC grant 99-TJ-683, and the Polish KBN grant 7-T11C-027-20. alternative_title: - LNCS article_processing_charge: No author: - first_name: Arindam full_name: Chakrabarti, Arindam last_name: Chakrabarti - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Henzinger, Thomas A 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 - first_name: Freddy full_name: Mang, Freddy last_name: Mang citation: ama: 'Chakrabarti A, De Alfaro L, Henzinger TA, Jurdziński M, Mang F. Interface compatibility checking for software modules. In: Proceedings of the 14th International Conference on Computer Aided Verification. Vol 2404. Springer; 2002:428-441. doi:10.1007/3-540-45657-0_35' apa: 'Chakrabarti, A., De Alfaro, L., Henzinger, T. A., Jurdziński, M., & Mang, F. (2002). Interface compatibility checking for software modules. In Proceedings of the 14th International Conference on Computer Aided Verification (Vol. 2404, pp. 428–441). Copenhagen, Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_35' chicago: Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, Marcin Jurdziński, and Freddy Mang. “Interface Compatibility Checking for Software Modules.” In Proceedings of the 14th International Conference on Computer Aided Verification, 2404:428–41. Springer, 2002. https://doi.org/10.1007/3-540-45657-0_35. ieee: A. Chakrabarti, L. De Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang, “Interface compatibility checking for software modules,” in Proceedings of the 14th International Conference on Computer Aided Verification, Copenhagen, Denmark, 2002, vol. 2404, pp. 428–441. ista: 'Chakrabarti A, De Alfaro L, Henzinger TA, Jurdziński M, Mang F. 2002. Interface compatibility checking for software modules. Proceedings of the 14th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 428–441.' mla: Chakrabarti, Arindam, et al. “Interface Compatibility Checking for Software Modules.” Proceedings of the 14th International Conference on Computer Aided Verification, vol. 2404, Springer, 2002, pp. 428–41, doi:10.1007/3-540-45657-0_35. short: A. Chakrabarti, L. De Alfaro, T.A. Henzinger, M. Jurdziński, F. Mang, in:, Proceedings of the 14th International Conference on Computer Aided Verification, Springer, 2002, pp. 428–441. conference: end_date: 2002-07-31 location: Copenhagen, Denmark name: 'CAV: Computer Aided Verification' start_date: 2002-07-27 date_created: 2018-12-11T12:09:30Z date_published: 2002-06-19T00:00:00Z date_updated: 2023-06-05T07:38:10Z day: '19' doi: 10.1007/3-540-45657-0_35 extern: '1' intvolume: ' 2404' language: - iso: eng month: '06' oa_version: None page: 428 - 441 publication: Proceedings of the 14th International Conference on Computer Aided Verification publication_identifier: isbn: - ' 9783540439974' publication_status: published publisher: Springer publist_id: '147' quality_controlled: '1' scopus_import: '1' status: public title: Interface compatibility checking for software modules type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2404 year: '2002' ... --- _id: '4472' abstract: - lang: eng text: 'We present a methodology and tool for verifying and certifying systems code. The verification is based on the lazy-abstraction paradigm for intertwining the following three logical steps: construct a predicate abstraction from the code, model check the abstraction, and automatically refine the abstraction based on counterexample analysis. The certification is based on the proof-carrying code paradigm. Lazy abstraction enables the automatic construction of small proof certificates. The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software verification Tool. We describe our experience applying Blast to Linux and Windows device drivers. Given the C code for a driver and for a temporal-safety monitor, Blast automatically generates an easily checkable correctness certificate if the driver satisfies the specification, and an error trace otherwise.' acknowledgement: This work was supported in part by the NSF ITR grants CCR-0085949, CCR-0081588, the NSF Career grant CCR-9875171, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, the SRC contract 99-TJ-683, a Microsoft fellowship, and gifts from AT&T Research and Microsoft Research. alternative_title: - LNCS article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: George full_name: Necula, George last_name: Necula - first_name: Ranjit full_name: Jhala, Ranjit last_name: Jhala - first_name: Grégoire full_name: Sutre, Grégoire last_name: Sutre - first_name: Ritankar full_name: Majumdar, Ritankar last_name: Majumdar - first_name: Westley full_name: Weimer, Westley last_name: Weimer citation: ama: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. Temporal safety proofs for systems code. In: Proceedings of the 14th International Conference on Computer Aided Verification. Vol 2404. Springer; 2002:526-538. doi:10.1007/3-540-45657-0_45' apa: 'Henzinger, T. A., Necula, G., Jhala, R., Sutre, G., Majumdar, R., & Weimer, W. (2002). Temporal safety proofs for systems code. In Proceedings of the 14th International Conference on Computer Aided Verification (Vol. 2404, pp. 526–538). Copenhagen, Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_45' chicago: Henzinger, Thomas A, George Necula, Ranjit Jhala, Grégoire Sutre, Ritankar Majumdar, and Westley Weimer. “Temporal Safety Proofs for Systems Code.” In Proceedings of the 14th International Conference on Computer Aided Verification, 2404:526–38. Springer, 2002. https://doi.org/10.1007/3-540-45657-0_45. ieee: T. A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, and W. Weimer, “Temporal safety proofs for systems code,” in Proceedings of the 14th International Conference on Computer Aided Verification, Copenhagen, Denmark, 2002, vol. 2404, pp. 526–538. ista: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. 2002. Temporal safety proofs for systems code. Proceedings of the 14th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 526–538.' mla: Henzinger, Thomas A., et al. “Temporal Safety Proofs for Systems Code.” Proceedings of the 14th International Conference on Computer Aided Verification, vol. 2404, Springer, 2002, pp. 526–38, doi:10.1007/3-540-45657-0_45. short: T.A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, W. Weimer, in:, Proceedings of the 14th International Conference on Computer Aided Verification, Springer, 2002, pp. 526–538. conference: end_date: 2002-07-31 location: Copenhagen, Denmark name: 'CAV: Computer Aided Verification' start_date: 2002-07-27 date_created: 2018-12-11T12:09:01Z date_published: 2002-06-19T00:00:00Z date_updated: 2023-06-05T08:11:32Z day: '19' doi: 10.1007/3-540-45657-0_45 extern: '1' intvolume: ' 2404' language: - iso: eng month: '06' oa_version: None page: 526 - 538 publication: Proceedings of the 14th International Conference on Computer Aided Verification publication_identifier: isbn: - '9783540439974' publication_status: published publisher: Springer publist_id: '258' quality_controlled: '1' scopus_import: '1' status: public title: Temporal safety proofs for systems code type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2404 year: '2002' ... --- _id: '4470' abstract: - lang: eng text: Giotto is a platform-independent language for specifying software for high-performance control applications. In this paper we present a new approach to the compilation of Giotto. Following this approach, the Giotto compiler generates code for a virtual machine, called the E machine, which can be ported to different platforms. The Giotto compiler also checks if the generated E code is time safe for a given platform, that is, if the platform offers sufficient performance to ensure that the E code is executed in a timely fashion that conforms with the Giotto semantics. Time-safety checking requires a schedulability analysis. We show that while for arbitrary E code, the analysis is exponential, for E code generated from typical Giotto programs, the analysis is polynomial. This supports our claim that Giotto identifies a useful fragment of embedded programs. acknowledgement: Supported in part by the DARPA SEC grant F33615-C-98-3614, MARCO GSRC grant 98-DT-660, AFOSR MURI grant F49620-00-1-0327, NSF grant CCR-9988172, and a Microsoft Research Fellowship. alternative_title: - LNCS article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Christoph full_name: Kirsch, Christoph last_name: Kirsch - first_name: Ritankar full_name: Majumdar, Ritankar last_name: Majumdar - first_name: Slobodan full_name: Matic, Slobodan last_name: Matic citation: ama: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. Time-safety checking for embedded programs. In: Proceedings of the 2nd International Conference on Embedded Software. Vol 2491. ACM; 2002:76-92. doi:10.1007/3-540-45828-X_7' apa: 'Henzinger, T. A., Kirsch, C., Majumdar, R., & Matic, S. (2002). Time-safety checking for embedded programs. In Proceedings of the 2nd International Conference on Embedded Software (Vol. 2491, pp. 76–92). Grenoble, France: ACM. https://doi.org/10.1007/3-540-45828-X_7' chicago: Henzinger, Thomas A, Christoph Kirsch, Ritankar Majumdar, and Slobodan Matic. “Time-Safety Checking for Embedded Programs.” In Proceedings of the 2nd International Conference on Embedded Software, 2491:76–92. ACM, 2002. https://doi.org/10.1007/3-540-45828-X_7. ieee: T. A. Henzinger, C. Kirsch, R. Majumdar, and S. Matic, “Time-safety checking for embedded programs,” in Proceedings of the 2nd International Conference on Embedded Software, Grenoble, France, 2002, vol. 2491, pp. 76–92. ista: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. 2002. Time-safety checking for embedded programs. Proceedings of the 2nd International Conference on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2491, 76–92.' mla: Henzinger, Thomas A., et al. “Time-Safety Checking for Embedded Programs.” Proceedings of the 2nd International Conference on Embedded Software, vol. 2491, ACM, 2002, pp. 76–92, doi:10.1007/3-540-45828-X_7. short: T.A. Henzinger, C. Kirsch, R. Majumdar, S. Matic, in:, Proceedings of the 2nd International Conference on Embedded Software, ACM, 2002, pp. 76–92. conference: end_date: 2002-10-09 location: Grenoble, France name: 'EMSOFT: Embedded Software ' start_date: 2002-10-07 date_created: 2018-12-11T12:09:01Z date_published: 2002-09-25T00:00:00Z date_updated: 2023-06-05T08:50:59Z day: '25' doi: 10.1007/3-540-45828-X_7 extern: '1' intvolume: ' 2491' language: - iso: eng month: '09' oa_version: None page: 76 - 92 publication: Proceedings of the 2nd International Conference on Embedded Software publication_identifier: isbn: - '9783540443070' publication_status: published publisher: ACM publist_id: '259' quality_controlled: '1' scopus_import: '1' status: public title: Time-safety checking for embedded programs type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2491 year: '2002' ... --- _id: '4444' abstract: - lang: eng text: The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first, platform-independent compiler phase generates E code (code executed by the Embedded Machine), which supervises the timing ---not the scheduling--- of application tasks relative to external events, such as clock ticks and sensor interrupts. E~code is portable and exhibits, given an input behavior, predictable (i.e., deterministic) timing and output behavior. The second, platform-dependent compiler phase checks the time safety of the E code, that is, whether platform performance (determined by the hardware) and platform utilization (determined by the scheduler of the operating system) enable its timely execution. We have used the Embedded Machine to compile and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter. acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT- 660, the AFOSR MURI grant F49620-00-1-0327, and the NSF ITR grant CCR-0085949. article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Christoph full_name: Kirsch, Christoph last_name: Kirsch citation: ama: 'Henzinger TA, Kirsch C. The embedded machine: predictable, portable real-time code. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. ACM; 2002:315-326. doi:10.1145/512529.512567' apa: 'Henzinger, T. A., & Kirsch, C. (2002). The embedded machine: predictable, portable real-time code. In Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation (pp. 315–326). Berlin, Germany: ACM. https://doi.org/10.1145/512529.512567' chicago: 'Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 315–26. ACM, 2002. https://doi.org/10.1145/512529.512567.' ieee: 'T. A. Henzinger and C. Kirsch, “The embedded machine: predictable, portable real-time code,” in Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation, Berlin, Germany, 2002, pp. 315–326.' ista: 'Henzinger TA, Kirsch C. 2002. The embedded machine: predictable, portable real-time code. Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation. PLDI: Programming Languages Design and Implementation, 315–326.' mla: 'Henzinger, Thomas A., and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, ACM, 2002, pp. 315–26, doi:10.1145/512529.512567.' short: T.A. Henzinger, C. Kirsch, in:, Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, ACM, 2002, pp. 315–326. conference: end_date: 2002-06-19 location: Berlin, Germany name: 'PLDI: Programming Languages Design and Implementation' start_date: 2002-06-17 date_created: 2018-12-11T12:08:53Z date_published: 2002-06-01T00:00:00Z date_updated: 2023-06-05T09:02:23Z day: '01' doi: 10.1145/512529.512567 extern: '1' language: - iso: eng month: '06' oa_version: None page: 315 - 326 publication: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation publication_identifier: isbn: - '9781581134636' publication_status: published publisher: ACM publist_id: '284' quality_controlled: '1' scopus_import: '1' status: public title: 'The embedded machine: predictable, portable real-time code' type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '2002' ... --- _id: '4476' abstract: - lang: eng text: 'One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.' acknowledgement: "We thank Wes Weimer and Jeff Foster for many useful discussions. \r\n" article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Ranjit full_name: Jhala, Ranjit last_name: Jhala - first_name: Ritankar full_name: Majumdar, Ritankar last_name: Majumdar - first_name: Grégoire full_name: Sutre, Grégoire last_name: Sutre citation: ama: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM; 2002:58-70. doi:10.1145/503272.503279' apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Sutre, G. (2002). Lazy abstraction. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 58–70). Portland, OR, USA: ACM. https://doi.org/10.1145/503272.503279' chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre. “Lazy Abstraction.” In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 58–70. ACM, 2002. https://doi.org/10.1145/503272.503279. ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy abstraction,” in Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Portland, OR, USA, 2002, pp. 58–70. ista: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. 2002. Lazy abstraction. Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL: Principles of Programming Languages, 58–70.' mla: Henzinger, Thomas A., et al. “Lazy Abstraction.” Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 2002, pp. 58–70, doi:10.1145/503272.503279. short: T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 2002, pp. 58–70. conference: end_date: 2002-01-18 location: Portland, OR, USA name: 'POPL: Principles of Programming Languages' start_date: 2002-01-16 date_created: 2018-12-11T12:09:03Z date_published: 2002-01-01T00:00:00Z date_updated: 2023-06-05T07:45:53Z day: '01' doi: 10.1145/503272.503279 extern: '1' language: - iso: eng month: '01' oa_version: None page: 58 - 70 publication: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages publication_identifier: isbn: - '9781581134506' publication_status: published publisher: ACM publist_id: '254' quality_controlled: '1' scopus_import: '1' status: public title: Lazy abstraction type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '2002' ... --- _id: '4473' abstract: - lang: eng text: 'The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P ≤s Q, denoting "P is simulated by Q," into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also extend our assume-guarantee rule to account for fairness constraints on transition systems.' article_processing_charge: No article_type: original author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Shaz full_name: Qadeer, Shaz last_name: Qadeer - first_name: Sriram full_name: Rajamani, Sriram last_name: Rajamani - first_name: Serdar full_name: Tasiran, Serdar last_name: Tasiran citation: ama: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems (TOPLAS). 2002;24(1):51-64. doi:10.1145/509705.509707 apa: Henzinger, T. A., Qadeer, S., Rajamani, S., & Tasiran, S. (2002). An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems (TOPLAS). ACM. https://doi.org/10.1145/509705.509707 chicago: Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “An Assume-Guarantee Rule for Checking Simulation.” ACM Transactions on Programming Languages and Systems (TOPLAS). ACM, 2002. https://doi.org/10.1145/509705.509707. ieee: T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee rule for checking simulation,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 24, no. 1. ACM, pp. 51–64, 2002. ista: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 2002. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems (TOPLAS). 24(1), 51–64. mla: Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 24, no. 1, ACM, 2002, pp. 51–64, doi:10.1145/509705.509707. short: T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming Languages and Systems (TOPLAS) 24 (2002) 51–64. date_created: 2018-12-11T12:09:02Z date_published: 2002-01-01T00:00:00Z date_updated: 2023-06-05T07:59:47Z day: '01' doi: 10.1145/509705.509707 extern: '1' intvolume: ' 24' issue: '1' language: - iso: eng month: '01' oa_version: None page: 51 - 64 publication: ACM Transactions on Programming Languages and Systems (TOPLAS) publication_identifier: issn: - 0164-0925 publication_status: published publisher: ACM publist_id: '256' quality_controlled: '1' scopus_import: '1' status: public title: An assume-guarantee rule for checking simulation type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 24 year: '2002' ... --- _id: '4423' abstract: - lang: eng text: Automation control systems typically incorporate legacy code and components that were originally designed to operate independently. Furthermore, they operate under stringent safety and timing constraints. Current design strategies deal with these requirements and characteristics with ad hoc approaches. In particular, when designing control laws, implementation constraints are often ignored or cursorily estimated. Indeed, costly redesigns are needed after a prototype of the control system is built due to missed timing constraints and subtle transient errors. In this paper, we use the concepts of platform-based design, and the Giotto programming language, to develop a methodology for the design of automation control systems that builds in modularity and correct-by-construction procedures. We illustrate our strategy by describing the (successful) application of the methodology to the design of a time-based control system for a rotorcraft Uninhabited Aerial Vehicle (UAV). acknowledgement: "Research supported in part by DARPA under contract no.F33615-98-C-3614, Software Enabled Control, administered by\r\nAFRL, Dayton OH." article_processing_charge: No author: - first_name: Benjamin full_name: Horowitz, Benjamin last_name: Horowitz - first_name: Judith full_name: Liebman, Judith last_name: Liebman - first_name: Cedric full_name: Ma, Cedric last_name: Ma - first_name: T John full_name: Koo, T John last_name: Koo - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Alberto full_name: Sangiovanni Vincentelli, Alberto last_name: Sangiovanni Vincentelli - first_name: Shankar full_name: Sastry, Shankar last_name: Sastry citation: ama: 'Horowitz B, Liebman J, Ma C, et al. Embedded software design and system integration for rotorcraft UAV using platforms. In: Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control. Vol 15. Elsevier; 2002. doi:10.3182/20020721-6-ES-1901.01628' apa: 'Horowitz, B., Liebman, J., Ma, C., Koo, T. J., Henzinger, T. A., Sangiovanni Vincentelli, A., & Sastry, S. (2002). Embedded software design and system integration for rotorcraft UAV using platforms. In Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control (Vol. 15). Barcelona, Spain: Elsevier. https://doi.org/10.3182/20020721-6-ES-1901.01628' chicago: Horowitz, Benjamin, Judith Liebman, Cedric Ma, T John Koo, Thomas A Henzinger, Alberto Sangiovanni Vincentelli, and Shankar Sastry. “Embedded Software Design and System Integration for Rotorcraft UAV Using Platforms.” In Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control, Vol. 15. Elsevier, 2002. https://doi.org/10.3182/20020721-6-ES-1901.01628. ieee: B. Horowitz et al., “Embedded software design and system integration for rotorcraft UAV using platforms,” in Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control, Barcelona, Spain, 2002, vol. 15, no. 1. ista: 'Horowitz B, Liebman J, Ma C, Koo TJ, Henzinger TA, Sangiovanni Vincentelli A, Sastry S. 2002. Embedded software design and system integration for rotorcraft UAV using platforms. Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control. IFAC: World Congress on Automatic Control vol. 15.' mla: Horowitz, Benjamin, et al. “Embedded Software Design and System Integration for Rotorcraft UAV Using Platforms.” Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control, vol. 15, no. 1, Elsevier, 2002, doi:10.3182/20020721-6-ES-1901.01628. short: B. Horowitz, J. Liebman, C. Ma, T.J. Koo, T.A. Henzinger, A. Sangiovanni Vincentelli, S. Sastry, in:, Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control, Elsevier, 2002. conference: end_date: 2002-07-26 location: Barcelona, Spain name: 'IFAC: World Congress on Automatic Control' start_date: 2002-07-21 date_created: 2018-12-11T12:08:47Z date_published: 2002-07-01T00:00:00Z date_updated: 2023-06-05T09:55:10Z day: '01' doi: 10.3182/20020721-6-ES-1901.01628 extern: '1' intvolume: ' 15' issue: '1' language: - iso: eng month: '07' oa_version: None publication: Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control publication_identifier: issn: - 1474-6670 publication_status: published publisher: Elsevier publist_id: '306' quality_controlled: '1' scopus_import: '1' status: public title: Embedded software design and system integration for rotorcraft UAV using platforms type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 15 year: '2002' ... --- _id: '4421' abstract: - lang: eng text: We demonstrate the feasibility and benefits of Giotto-based control software development by reimplementing the autopilot system of an autonomously flying model helicopter. Giotto offers a clean separation between the platform-independent concerns of software functionality and I/O timing, and the platform-dependent concerns of software scheduling and execution. Functionality code such as code computing control laws can be generated automatically from Simulink models or, as in the case of this project, inherited from a legacy system. I/O timing code is generated automatically from Giotto models that specify real-time requirements such as task frequencies and actuator update rates. We extend Simulink to support the design of Giotto models, and from these models, the automatic generation of Giotto code that supervises the interaction of the functionality code with the physical environment. The Giotto compiler performs a schedulability analysis on the Giotto code, and generates timing code for the helicopter platform. The Giotto methodology guarantees the stringent hard real-time requirements of the autopilot system, and at the same time supports the automation of the software development process in a way that produces a transparent software architecture with predictable behavior and reusable components. acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, and the AFOSR MURI grant F49620-00-1-0327. alternative_title: - LNCS article_processing_charge: No author: - first_name: Christoph full_name: Kirsch, Christoph last_name: Kirsch - first_name: Marco full_name: Sanvido, Marco last_name: Sanvido - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Wolfgang full_name: Pree, Wolfgang last_name: Pree citation: ama: 'Kirsch C, Sanvido M, Henzinger TA, Pree W. A Giotto-based helicopter control system. In: Proceedings of the 2nd International Conference on Embedded Software. Vol 2491. ACM; 2002:46-60. doi:10.1007/3-540-45828-X_5' apa: 'Kirsch, C., Sanvido, M., Henzinger, T. A., & Pree, W. (2002). A Giotto-based helicopter control system. In Proceedings of the 2nd International Conference on Embedded Software (Vol. 2491, pp. 46–60). Grenoble, France: ACM. https://doi.org/10.1007/3-540-45828-X_5' chicago: Kirsch, Christoph, Marco Sanvido, Thomas A Henzinger, and Wolfgang Pree. “A Giotto-Based Helicopter Control System.” In Proceedings of the 2nd International Conference on Embedded Software, 2491:46–60. ACM, 2002. https://doi.org/10.1007/3-540-45828-X_5. ieee: C. Kirsch, M. Sanvido, T. A. Henzinger, and W. Pree, “A Giotto-based helicopter control system,” in Proceedings of the 2nd International Conference on Embedded Software, Grenoble, France, 2002, vol. 2491, pp. 46–60. ista: 'Kirsch C, Sanvido M, Henzinger TA, Pree W. 2002. A Giotto-based helicopter control system. Proceedings of the 2nd International Conference on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2491, 46–60.' mla: Kirsch, Christoph, et al. “A Giotto-Based Helicopter Control System.” Proceedings of the 2nd International Conference on Embedded Software, vol. 2491, ACM, 2002, pp. 46–60, doi:10.1007/3-540-45828-X_5. short: C. Kirsch, M. Sanvido, T.A. Henzinger, W. Pree, in:, Proceedings of the 2nd International Conference on Embedded Software, ACM, 2002, pp. 46–60. conference: end_date: 2002-10-09 location: Grenoble, France name: 'EMSOFT: Embedded Software ' start_date: 2002-10-07 date_created: 2018-12-11T12:08:46Z date_published: 2002-09-25T00:00:00Z date_updated: 2023-06-05T13:07:20Z day: '25' doi: 10.1007/3-540-45828-X_5 extern: '1' intvolume: ' 2491' language: - iso: eng month: '09' oa_version: None page: 46 - 60 publication: Proceedings of the 2nd International Conference on Embedded Software publication_identifier: isbn: - '9783540443070' publication_status: published publisher: ACM publist_id: '310' quality_controlled: '1' scopus_import: '1' status: public title: A Giotto-based helicopter control system type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2491 year: '2002' ... --- _id: '4422' abstract: - lang: eng text: "Behavioral properties of open systems can be formalized as objectives in two-player games. Turn-based games model asynchronous interaction between the players (the system and its environment) by interleaving their moves. Concurrent games model synchronous interaction: the players always move simultaneously. Infinitary winning criteria are considered: Büchi, co-Büchi, and more general parity conditions. A generalization of determinacy for parity games to concurrent parity games demands probabilistic (mixed) strategies: either player 1 has a mixed strategy to win with probability 1 (almost-sure winning), or player 2 has a mixed strategy to win with positive probability.\r\nThis work provides efficient reductions of concurrent probabilistic Büchi and co-Büchi games to turn-based games with Büchi condition and parity winning condition with three priorities, respectively. From a theoretical point of view, the latter reduction shows that one can trade the probabilistic nature of almost-sure winning for a more general parity (fairness) condition. The reductions improve understanding of concurrent games and provide an alternative simple proof of determinacy of concurrent Büchi and co-Büchi games. From a practical point of view, the reductions turn solvers of turn-based games into solvers of concurrent probabilistic games. Thus improvements in the well-studied algorithms for the former carry over immediately to the latter. In particular, a recent improvement in the complexity of solving turn-based parity games yields an improvement in time complexity of solving concurrent probabilistic co-Büchi games from cubic to quadratic." acknowledgement: This research was supported in part by the Polish KBN grant 7-T11C-027-20, the AFOSR MURI grant F49620-00-1-0327, and the NSF Theory grant CCR-9988172. alternative_title: - LNCS article_processing_charge: No author: - first_name: Marcin full_name: Jurdziński, Marcin last_name: Jurdziński - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Jurdziński M, Kupferman O, Henzinger TA. Trading probability for fairness. In: Proceedings of the 16th International Workshop on Computer Science Logic. Vol 2471. Springer; 2002:292-305. doi:10.1007/3-540-45793-3_20' apa: 'Jurdziński, M., Kupferman, O., & Henzinger, T. A. (2002). Trading probability for fairness. In Proceedings of the 16th International Workshop on Computer Science Logic (Vol. 2471, pp. 292–305). Edinburgh, Scotland: Springer. https://doi.org/10.1007/3-540-45793-3_20' chicago: Jurdziński, Marcin, Orna Kupferman, and Thomas A Henzinger. “Trading Probability for Fairness.” In Proceedings of the 16th International Workshop on Computer Science Logic, 2471:292–305. Springer, 2002. https://doi.org/10.1007/3-540-45793-3_20. ieee: M. Jurdziński, O. Kupferman, and T. A. Henzinger, “Trading probability for fairness,” in Proceedings of the 16th International Workshop on Computer Science Logic, Edinburgh, Scotland, 2002, vol. 2471, pp. 292–305. ista: 'Jurdziński M, Kupferman O, Henzinger TA. 2002. Trading probability for fairness. Proceedings of the 16th International Workshop on Computer Science Logic. CSL: Computer Science Logic, LNCS, vol. 2471, 292–305.' mla: Jurdziński, Marcin, et al. “Trading Probability for Fairness.” Proceedings of the 16th International Workshop on Computer Science Logic, vol. 2471, Springer, 2002, pp. 292–305, doi:10.1007/3-540-45793-3_20. short: M. Jurdziński, O. Kupferman, T.A. Henzinger, in:, Proceedings of the 16th International Workshop on Computer Science Logic, Springer, 2002, pp. 292–305. conference: location: Edinburgh, Scotland name: 'CSL: Computer Science Logic' date_created: 2018-12-11T12:08:46Z date_published: 2002-09-09T00:00:00Z date_updated: 2023-06-05T10:02:54Z day: '09' doi: 10.1007/3-540-45793-3_20 extern: '1' intvolume: ' 2471' language: - iso: eng month: '09' oa_version: None page: 292 - 305 publication: Proceedings of the 16th International Workshop on Computer Science Logic publication_identifier: isbn: - '9783540442400' publication_status: published publisher: Springer publist_id: '308' quality_controlled: '1' scopus_import: '1' status: public title: Trading probability for fairness type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 2471 year: '2002' ... --- _id: '4413' abstract: - lang: eng text: 'An essential problem in component-based design is how to compose components designed in isolation. Several approaches have been proposed for specifying component interfaces that capture behavioral aspects such as interaction protocols, and for verifying interface compatibility. Likewise, several approaches have been developed for synthesizing converters between incompatible protocols. In this paper, we introduce the notion of adaptability as the property that two interfaces have when they can be made compatible by communicating through a converter that meets specified requirements. We show that verifying adaptability and synthesizing an appropriate converter are two faces of the same coin: adaptability can be formalized and solved using a game-theoretic framework, and then the converter can be synthesized as a strategy that always wins the game. Finally we show that this framework can be related to the rectification problem in trace theory.' acknowledgement: "The authors would like to thank Jerry Burch of the Cadence Berkeley Labs for many insightful discussions and suggestions.\r\n" article_processing_charge: No author: - first_name: Roberto full_name: Passerone, Roberto last_name: Passerone - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Alberto full_name: Sangiovanni Vincentelli, Alberto last_name: Sangiovanni Vincentelli citation: ama: 'Passerone R, De Alfaro L, Henzinger TA, Sangiovanni Vincentelli A. Convertibility verification and converter synthesis: Two faces of the same coin. In: Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design. IEEE; 2002:132-139. doi:10.1145/774572.774592' apa: 'Passerone, R., De Alfaro, L., Henzinger, T. A., & Sangiovanni Vincentelli, A. (2002). Convertibility verification and converter synthesis: Two faces of the same coin. In Proceedings of the 11th IEEE/ACM international conference on Computer-aided design (pp. 132–139). San Jose, CA, USA: IEEE. https://doi.org/10.1145/774572.774592' chicago: 'Passerone, Roberto, Luca De Alfaro, Thomas A Henzinger, and Alberto Sangiovanni Vincentelli. “Convertibility Verification and Converter Synthesis: Two Faces of the Same Coin.” In Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design, 132–39. IEEE, 2002. https://doi.org/10.1145/774572.774592.' ieee: 'R. Passerone, L. De Alfaro, T. A. Henzinger, and A. Sangiovanni Vincentelli, “Convertibility verification and converter synthesis: Two faces of the same coin,” in Proceedings of the 11th IEEE/ACM international conference on Computer-aided design, San Jose, CA, USA, 2002, pp. 132–139.' ista: 'Passerone R, De Alfaro L, Henzinger TA, Sangiovanni Vincentelli A. 2002. Convertibility verification and converter synthesis: Two faces of the same coin. Proceedings of the 11th IEEE/ACM international conference on Computer-aided design. ICCAD: Computer-Aided Design, 132–139.' mla: 'Passerone, Roberto, et al. “Convertibility Verification and Converter Synthesis: Two Faces of the Same Coin.” Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design, IEEE, 2002, pp. 132–39, doi:10.1145/774572.774592.' short: R. Passerone, L. De Alfaro, T.A. Henzinger, A. Sangiovanni Vincentelli, in:, Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design, IEEE, 2002, pp. 132–139. conference: end_date: 2002-11-14 location: San Jose, CA, USA name: 'ICCAD: Computer-Aided Design' start_date: 2002-11-10 date_created: 2018-12-11T12:08:44Z date_published: 2002-11-01T00:00:00Z date_updated: 2023-06-05T14:21:46Z day: '01' doi: 10.1145/774572.774592 extern: '1' language: - iso: eng month: '11' oa_version: None page: 132 - 139 publication: Proceedings of the 11th IEEE/ACM international conference on Computer-aided design publication_identifier: isbn: - '9780780376076' publication_status: published publisher: IEEE publist_id: '318' quality_controlled: '1' scopus_import: '1' status: public title: 'Convertibility verification and converter synthesis: Two faces of the same coin' type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '2002' ... --- _id: '4262' abstract: - lang: eng text: Natural populations are structured spatially into local populations and genetically into diverse ‘genetic backgrounds’ defined by different combinations of selected alleles. If selection maintains genetic backgrounds at constant frequency then neutral diversity is enhanced. By contrast, if background frequencies fluctuate then diversity is reduced. Provided that the population size of each background is large enough, these effects can be described by the structured coalescent process. Almost all the extant results based on the coalescent deal with a single selected locus. Yet we know that very large numbers of genes are under selection and that any substantial effects are likely to be due to the cumulative effects of many loci. Here, we set up a general framework for the extension of the coalescent to multilocus scenarios and we use it to study the simplest model, where strong balancing selection acting on a set of n loci maintains 2n backgrounds at constant frequencies and at linkage equilibrium. Analytical results show that the expected linked neutral diversity increases exponentially with the number of selected loci and can become extremely large. However, simulation results reveal that the structured coalescent approach breaks down when the number of backgrounds approaches the population size, because of stochastic fluctuations in background frequencies. A new method is needed to extend the structured coalescent to cases with large numbers of backgrounds. acknowledgement: "We thank B. Charlesworth, D. Charlesworth and F. Depaulis for valuable discussion and criticism. We are also\r\ngrateful to an anonymous reviewer, who pointed out an imprecision in the original manuscript. This work was\r\nsupported by the BBSRC." article_processing_charge: No article_type: original author: - first_name: Nicholas H full_name: Barton, Nicholas H id: 4880FE40-F248-11E8-B48F-1D18A9856A87 last_name: Barton orcid: 0000-0002-8548-5240 - first_name: Arcadio full_name: Navarro, Arcadio last_name: Navarro citation: ama: 'Barton NH, Navarro A. Extending the coalescent to multilocus systems: the case of balancing selection. Genetical Research. 2002;79(2):129-139. doi:10.1017/S0016672301005493' apa: 'Barton, N. H., & Navarro, A. (2002). Extending the coalescent to multilocus systems: the case of balancing selection. Genetical Research. Cambridge University Press. https://doi.org/10.1017/S0016672301005493' chicago: 'Barton, Nicholas H, and Arcadio Navarro. “Extending the Coalescent to Multilocus Systems: The Case of Balancing Selection.” Genetical Research. Cambridge University Press, 2002. https://doi.org/10.1017/S0016672301005493.' ieee: 'N. H. Barton and A. Navarro, “Extending the coalescent to multilocus systems: the case of balancing selection,” Genetical Research, vol. 79, no. 2. Cambridge University Press, pp. 129–139, 2002.' ista: 'Barton NH, Navarro A. 2002. Extending the coalescent to multilocus systems: the case of balancing selection. Genetical Research. 79(2), 129–139.' mla: 'Barton, Nicholas H., and Arcadio Navarro. “Extending the Coalescent to Multilocus Systems: The Case of Balancing Selection.” Genetical Research, vol. 79, no. 2, Cambridge University Press, 2002, pp. 129–39, doi:10.1017/S0016672301005493.' short: N.H. Barton, A. Navarro, Genetical Research 79 (2002) 129–139. date_created: 2018-12-11T12:07:55Z date_published: 2002-05-23T00:00:00Z date_updated: 2023-06-06T11:23:19Z day: '23' doi: 10.1017/S0016672301005493 extern: '1' external_id: pmid: - '12073551' intvolume: ' 79' issue: '2' language: - iso: eng month: '05' oa_version: None page: 129 - 139 pmid: 1 publication: Genetical Research publication_identifier: issn: - 0016-6723 publication_status: published publisher: Cambridge University Press publist_id: '1832' quality_controlled: '1' scopus_import: '1' status: public title: 'Extending the coalescent to multilocus systems: the case of balancing selection' type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 79 year: '2002' ... --- _id: '4260' abstract: - lang: eng text: 'We calculate the fixation probability of a beneficial allele that arises as the result of a unique mutation in an asexual population that is subject to recurrent deleterious mutation at rate U. Our analysis is an extension of previous works, which make a biologically restrictive assumption that selection against deleterious alleles is stronger than that on the beneficial allele of interest. We show that when selection against deleterious alleles is weak, beneficial alleles that confer a selective advantage that is small relative to U have greatly reduced probabilities of fixation. We discuss the consequences of this effect for the distribution of effects of alleles fixed during adaptation. We show that a selective sweep will increase the fixation probabilities of other beneficial mutations arising during some short interval afterward. We use the calculated fixation probabilities to estimate the expected rate of fitness improvement in an asexual population when beneficial alleles arise continually at some low rate proportional to U. We estimate the rate of mutation that is optimal in the sense that it maximizes this rate of fitness improvement. Again, this analysis relaxes the assumption made previously that selection against deleterious alleles is stronger than on beneficial alleles. ' acknowledgement: "We thank Brian Charlesworth, Arcadi Navarro, Allen Orr, Sally Otto, Mario Pineda-Krch, Rosie Redfield, Olivier Tenaillon, and two anonymous reviewers for discussions and/or helpful comments on the\r\nmanuscript. T.J. is supported by Wellcome Trust International Prize Travelling Research Fellowship no. 061530. N.B. is supported by the Biotechnology and Biological Sciences Research Council and by the Natural Environment Research Council." article_processing_charge: No article_type: original author: - first_name: Toby full_name: Johnson, Toby last_name: Johnson - first_name: Nicholas H full_name: Barton, Nicholas H id: 4880FE40-F248-11E8-B48F-1D18A9856A87 last_name: Barton orcid: 0000-0002-8548-5240 citation: ama: Johnson T, Barton NH. The effect of deleterious alleles on adaptation in asexual populations. Genetics. 2002;162(1):395-411. doi:10.1093/genetics/162.1.395 apa: Johnson, T., & Barton, N. H. (2002). The effect of deleterious alleles on adaptation in asexual populations. Genetics. Genetics Society of America. https://doi.org/10.1093/genetics/162.1.395 chicago: Johnson, Toby, and Nicholas H Barton. “The Effect of Deleterious Alleles on Adaptation in Asexual Populations.” Genetics. Genetics Society of America, 2002. https://doi.org/10.1093/genetics/162.1.395. ieee: T. Johnson and N. H. Barton, “The effect of deleterious alleles on adaptation in asexual populations,” Genetics, vol. 162, no. 1. Genetics Society of America, pp. 395–411, 2002. ista: Johnson T, Barton NH. 2002. The effect of deleterious alleles on adaptation in asexual populations. Genetics. 162(1), 395–411. mla: Johnson, Toby, and Nicholas H. Barton. “The Effect of Deleterious Alleles on Adaptation in Asexual Populations.” Genetics, vol. 162, no. 1, Genetics Society of America, 2002, pp. 395–411, doi:10.1093/genetics/162.1.395. short: T. Johnson, N.H. Barton, Genetics 162 (2002) 395–411. date_created: 2018-12-11T12:07:54Z date_published: 2002-09-01T00:00:00Z date_updated: 2023-06-06T11:45:48Z day: '01' doi: 10.1093/genetics/162.1.395 extern: '1' external_id: pmid: - '12242249' intvolume: ' 162' issue: '1' language: - iso: eng main_file_link: - open_access: '1' url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC1462245/ month: '09' oa: 1 oa_version: None page: 395 - 411 pmid: 1 publication: Genetics publication_identifier: issn: - 0016-6731 publication_status: published publisher: Genetics Society of America publist_id: '1833' quality_controlled: '1' scopus_import: '1' status: public title: The effect of deleterious alleles on adaptation in asexual populations type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 162 year: '2002' ...