[{"doi":"10.1006/tpbi.2001.1557","quality_controlled":"1","publication_identifier":{"issn":["0040-5809"]},"issue":"1","language":[{"iso":"eng"}],"title":"Neutral evolution in spatially continuous populations","publist_id":"1830","author":[{"first_name":"Nicholas H","last_name":"Barton","full_name":"Barton, Nicholas H","orcid":"0000-0002-8548-5240","id":"4880FE40-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Depaulis, Frantz","last_name":"Depaulis","first_name":"Frantz"},{"full_name":"Etheridge, Alison","last_name":"Etheridge","first_name":"Alison"}],"day":"01","publication":"Theoretical Population Biology","article_type":"original","article_processing_charge":"No","scopus_import":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Academic Press","pmid":1,"date_published":"2002-02-01T00:00:00Z","publication_status":"published","extern":"1","intvolume":"        61","citation":{"ama":"Barton NH, Depaulis F, Etheridge A. Neutral evolution in spatially continuous populations. <i>Theoretical Population Biology</i>. 2002;61(1):31-48. doi:<a href=\"https://doi.org/10.1006/tpbi.2001.1557\">10.1006/tpbi.2001.1557</a>","mla":"Barton, Nicholas H., et al. “Neutral Evolution in Spatially Continuous Populations.” <i>Theoretical Population Biology</i>, vol. 61, no. 1, Academic Press, 2002, pp. 31–48, doi:<a href=\"https://doi.org/10.1006/tpbi.2001.1557\">10.1006/tpbi.2001.1557</a>.","ista":"Barton NH, Depaulis F, Etheridge A. 2002. Neutral evolution in spatially continuous populations. Theoretical Population Biology. 61(1), 31–48.","apa":"Barton, N. H., Depaulis, F., &#38; Etheridge, A. (2002). Neutral evolution in spatially continuous populations. <i>Theoretical Population Biology</i>. Academic Press. <a href=\"https://doi.org/10.1006/tpbi.2001.1557\">https://doi.org/10.1006/tpbi.2001.1557</a>","ieee":"N. H. Barton, F. Depaulis, and A. Etheridge, “Neutral evolution in spatially continuous populations,” <i>Theoretical Population Biology</i>, vol. 61, no. 1. Academic Press, pp. 31–48, 2002.","chicago":"Barton, Nicholas H, Frantz Depaulis, and Alison Etheridge. “Neutral Evolution in Spatially Continuous Populations.” <i>Theoretical Population Biology</i>. Academic Press, 2002. <a href=\"https://doi.org/10.1006/tpbi.2001.1557\">https://doi.org/10.1006/tpbi.2001.1557</a>.","short":"N.H. Barton, F. Depaulis, A. Etheridge, Theoretical Population Biology 61 (2002) 31–48."},"external_id":{"pmid":["11895381"]},"status":"public","volume":61,"date_created":"2018-12-11T12:07:55Z","page":"31 - 48","oa_version":"None","month":"02","type":"journal_article","abstract":[{"text":"We introduce a general recursion for the probability of identity in state of two individuals sampled from a population subject to mutation, migration, and random drift in a two-dimensional continuum. The recursion allows for the interactions induced by density-dependent regulation of the population, which are inevitable in a continuous population. We give explicit series expansions for large neighbourhood size and for low mutation rates respectively and investigate the accuracy of the classical Malécot formula for these general models. When neighbourhood size is small, this formula does not give the identity even over large scales. However, for large neighbourhood size, it is an accurate approximation which summarises the local population structure in terms of three quantities: the effective dispersal rate, σe; the effective population density, ρe; and a local scale, κ, at which local interactions become significant. The results are illustrated by simulations.","lang":"eng"}],"date_updated":"2023-06-06T09:57:49Z","_id":"4263","acknowledgement":"This work was supported by grants from the EPSRC (GR/L10048 and an advanced fellowship for A.M.E.) and NERC (GR3/11635) and by the Darwin Trust of Edinburgh. We thank Anja Sturm for her assistance with the project and anonymous reviewers for helpful comments. This paper is dedicated to Charlotte, A.M.E.’s daughter born during the gestation of the manuscript.","year":"2002"},{"citation":{"short":"J. Huelsenbeck, J.P. Bollback, A. Levine, Systematic Biology 51 (2002) 32–43.","chicago":"Huelsenbeck, John, Jonathan P Bollback, and Amy Levine. “Inferring the Root of a Phylogenetic Tree.” <i>Systematic Biology</i>. Oxford University Press, 2002. <a href=\"https://doi.org/10.1080/106351502753475862\">https://doi.org/10.1080/106351502753475862</a>.","ieee":"J. Huelsenbeck, J. P. Bollback, and A. Levine, “Inferring the root of a phylogenetic tree,” <i>Systematic Biology</i>, vol. 51, no. 1. Oxford University Press, pp. 32–43, 2002.","apa":"Huelsenbeck, J., Bollback, J. P., &#38; Levine, A. (2002). Inferring the root of a phylogenetic tree. <i>Systematic Biology</i>. Oxford University Press. <a href=\"https://doi.org/10.1080/106351502753475862\">https://doi.org/10.1080/106351502753475862</a>","mla":"Huelsenbeck, John, et al. “Inferring the Root of a Phylogenetic Tree.” <i>Systematic Biology</i>, vol. 51, no. 1, Oxford University Press, 2002, pp. 32–43, doi:<a href=\"https://doi.org/10.1080/106351502753475862\">10.1080/106351502753475862</a>.","ista":"Huelsenbeck J, Bollback JP, Levine A. 2002. Inferring the root of a phylogenetic tree. Systematic Biology. 51(1), 32–43.","ama":"Huelsenbeck J, Bollback JP, Levine A. Inferring the root of a phylogenetic tree. <i>Systematic Biology</i>. 2002;51(1):32-43. doi:<a href=\"https://doi.org/10.1080/106351502753475862\">10.1080/106351502753475862</a>"},"intvolume":"        51","extern":"1","status":"public","external_id":{"pmid":["11943091"]},"date_published":"2002-02-01T00:00:00Z","publication_status":"published","_id":"4347","year":"2002","date_created":"2018-12-11T12:08:23Z","volume":51,"date_updated":"2023-06-06T09:53:27Z","abstract":[{"lang":"eng","text":"Phylogenetic trees can be rooted by a number of criteria. Here, we introduce a Bayesian method for inferring the root of a phylogenetic tree by using one of several criteria: the outgroup, molecular clock, and nonreversible model of DNA substitution. We perform simulation analyses to examine the relative ability of these three criteria to correctly identify the root of the tree. The outgroup and molecular clock criteria were best able to identify the root of the tree, whereas the nonreversible model was able to identify the root only when the substitution process was highly nonreversible. We also examined the performance of the criteria for a tree of four species for which the topology and root position are well supported. Results of the analyses of these data are consistent with the simulation results."}],"month":"02","type":"journal_article","oa_version":"None","page":"32 - 43","language":[{"iso":"eng"}],"issue":"1","quality_controlled":"1","doi":"10.1080/106351502753475862","publication_identifier":{"issn":["0039-7989"]},"article_processing_charge":"No","scopus_import":"1","article_type":"original","publication":"Systematic Biology","pmid":1,"publisher":"Oxford University Press","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"1113","title":"Inferring the root of a phylogenetic tree","day":"01","author":[{"last_name":"Huelsenbeck","first_name":"John","full_name":"Huelsenbeck, John"},{"id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4624-4612","full_name":"Bollback, Jonathan P","last_name":"Bollback","first_name":"Jonathan P"},{"last_name":"Levine","first_name":"Amy","full_name":"Levine, Amy"}]},{"author":[{"full_name":"Bollback, Jonathan P","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4624-4612","first_name":"Jonathan P","last_name":"Bollback"}],"day":"25","title":"Bayesian model adequacy and choice in phylogenetics","publist_id":"1112","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Oxford University Press","pmid":1,"publication":"Molecular Biology and Evolution","article_type":"original","scopus_import":"1","article_processing_charge":"No","publication_identifier":{"issn":["0737-4038"]},"doi":"10.1093/oxfordjournals.molbev.a004175","quality_controlled":"1","issue":"7","language":[{"iso":"eng"}],"page":"1171 - 80","type":"journal_article","month":"03","oa_version":"None","date_updated":"2023-06-06T09:18:18Z","abstract":[{"lang":"eng","text":"Bayesian inference is becoming a common statistical approach to phylogenetic estimation because, among other reasons, it allows for rapid analysis of large data sets with complex evolutionary models. Conveniently, Bayesian phylogenetic methods use currently available stochastic models of sequence evolution. However, as with other model-based approaches, the results of Bayesian inference are conditional on the assumed model of evolution: inadequate models (models that poorly fit the data) may result in erroneous inferences. In this article, I present a Bayesian phylogenetic method that evaluates the adequacy of evolutionary models using posterior predictive distributions. By evaluating a model's posterior predictive performance, an adequate model can be selected for a Bayesian phylogenetic study. Although I present a single test statistic that assesses the overall (global) performance of a phylogenetic model, a variety of test statistics can be tailored to evaluate specific features (local performance) of evolutionary models to identify sources failure. The method presented here, unlike the likelihood-ratio test and parametric bootstrap, accounts for uncertainty in the phylogeny and model parameters."}],"volume":19,"date_created":"2018-12-11T12:08:24Z","acknowledgement":"This work was supported by grants from the NSF to John Huelsenbeck (MCB-0075404 and DEB0075406), to whom I am grateful for his support throughout this project. Also, I would like to express my deep thanks to Andrea Betancourt, John Huelsenbeck, Kelly Dyer, Rasmus Nielsen, and Frederick Ronquist for taking the time to read early versions of the\r\nmanuscript. Each and every one of them provided invaluable comments, that ultimately made the manuscript better. John Huelsenbeck, Bret Larget, Rasmus Nielsen, Ken Karol, and Andrea Betancourt patiently listened to me drone on about this project, and offered insightful comments that benefited this work, and for this they have my deepest gratitude. And finally, I would like to thank two anonymous reviewers who gave critical attention to the manuscript and provided valuable comments.","year":"2002","_id":"4349","publication_status":"published","date_published":"2002-03-25T00:00:00Z","external_id":{"pmid":["12082136 "]},"status":"public","extern":"1","intvolume":"        19","citation":{"ieee":"J. P. Bollback, “Bayesian model adequacy and choice in phylogenetics,” <i>Molecular Biology and Evolution</i>, vol. 19, no. 7. Oxford University Press, pp. 1171–80, 2002.","chicago":"Bollback, Jonathan P. “Bayesian Model Adequacy and Choice in Phylogenetics.” <i>Molecular Biology and Evolution</i>. Oxford University Press, 2002. <a href=\"https://doi.org/10.1093/oxfordjournals.molbev.a004175\">https://doi.org/10.1093/oxfordjournals.molbev.a004175</a>.","short":"J.P. Bollback, Molecular Biology and Evolution 19 (2002) 1171–80.","ama":"Bollback JP. Bayesian model adequacy and choice in phylogenetics. <i>Molecular Biology and Evolution</i>. 2002;19(7):1171-1180. doi:<a href=\"https://doi.org/10.1093/oxfordjournals.molbev.a004175\">10.1093/oxfordjournals.molbev.a004175</a>","ista":"Bollback JP. 2002. Bayesian model adequacy and choice in phylogenetics. Molecular Biology and Evolution. 19(7), 1171–80.","mla":"Bollback, Jonathan P. “Bayesian Model Adequacy and Choice in Phylogenetics.” <i>Molecular Biology and Evolution</i>, vol. 19, no. 7, Oxford University Press, 2002, pp. 1171–80, doi:<a href=\"https://doi.org/10.1093/oxfordjournals.molbev.a004175\">10.1093/oxfordjournals.molbev.a004175</a>.","apa":"Bollback, J. P. (2002). Bayesian model adequacy and choice in phylogenetics. <i>Molecular Biology and Evolution</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/oxfordjournals.molbev.a004175\">https://doi.org/10.1093/oxfordjournals.molbev.a004175</a>"}},{"_id":"4407","year":"2002","volume":274,"date_created":"2018-12-11T12:08:42Z","page":"151 - 182","date_updated":"2023-06-06T09:10:56Z","abstract":[{"lang":"eng","text":"This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MetricIntervalTL formulae into EventClockTL formulae, the two logics being equally expressive. Our proof is structured to yield axiomatizations also for interesting fragments of these logics, such as the linear temporal logic of the real numbers (TLR)."}],"month":"03","type":"journal_article","oa_version":"None","extern":"1","intvolume":"       274","citation":{"mla":"Raskin, Jean, et al. “Axioms for Real-Time Logics.” <i>Theoretical Computer Science</i>, vol. 274, no. 1–2, Elsevier, 2002, pp. 151–82, doi:<a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">10.1016/S0304-3975(00)00308-X</a>.","ista":"Raskin J, Schobbens P, Henzinger TA. 2002. Axioms for real-time logics. Theoretical Computer Science. 274(1–2), 151–182.","apa":"Raskin, J., Schobbens, P., &#38; Henzinger, T. A. (2002). Axioms for real-time logics. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">https://doi.org/10.1016/S0304-3975(00)00308-X</a>","ama":"Raskin J, Schobbens P, Henzinger TA. Axioms for real-time logics. <i>Theoretical Computer Science</i>. 2002;274(1-2):151-182. doi:<a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">10.1016/S0304-3975(00)00308-X</a>","short":"J. Raskin, P. Schobbens, T.A. Henzinger, Theoretical Computer Science 274 (2002) 151–182.","ieee":"J. Raskin, P. Schobbens, and T. A. Henzinger, “Axioms for real-time logics,” <i>Theoretical Computer Science</i>, vol. 274, no. 1–2. Elsevier, pp. 151–182, 2002.","chicago":"Raskin, Jean, Pierre Schobbens, and Thomas A Henzinger. “Axioms for Real-Time Logics.” <i>Theoretical Computer Science</i>. Elsevier, 2002. <a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">https://doi.org/10.1016/S0304-3975(00)00308-X</a>."},"status":"public","date_published":"2002-03-01T00:00:00Z","publication_status":"published","publication":"Theoretical Computer Science","scopus_import":"1","article_processing_charge":"No","article_type":"original","publisher":"Elsevier","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Axioms for real-time logics","publist_id":"324","author":[{"full_name":"Raskin, Jean","last_name":"Raskin","first_name":"Jean"},{"full_name":"Schobbens, Pierre","last_name":"Schobbens","first_name":"Pierre"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"}],"day":"01","language":[{"iso":"eng"}],"issue":"1-2","doi":"10.1016/S0304-3975(00)00308-X","quality_controlled":"1","publication_identifier":{"issn":["0304-3975"]}},{"status":"public","conference":{"end_date":"2002-11-14","location":"San Jose, CA, USA","name":"ICCAD: Computer-Aided Design","start_date":"2002-11-10"},"extern":"1","language":[{"iso":"eng"}],"citation":{"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.","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 <i>Proceedings of the 11th IEEE/ACM international conference on Computer-aided design</i>, San Jose, CA, USA, 2002, pp. 132–139.","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 <i>Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design</i>, 132–39. IEEE, 2002. <a href=\"https://doi.org/10.1145/774572.774592\">https://doi.org/10.1145/774572.774592</a>.","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.” <i>Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design</i>, IEEE, 2002, pp. 132–39, doi:<a href=\"https://doi.org/10.1145/774572.774592\">10.1145/774572.774592</a>.","apa":"Passerone, R., De Alfaro, L., Henzinger, T. A., &#38; Sangiovanni Vincentelli, A. (2002). Convertibility verification and converter synthesis: Two faces of the same coin. In <i>Proceedings of the 11th IEEE/ACM international conference on Computer-aided design</i> (pp. 132–139). San Jose, CA, USA: IEEE. <a href=\"https://doi.org/10.1145/774572.774592\">https://doi.org/10.1145/774572.774592</a>","ama":"Passerone R, De Alfaro L, Henzinger TA, Sangiovanni Vincentelli A. Convertibility verification and converter synthesis: Two faces of the same coin. In: <i>Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design</i>. IEEE; 2002:132-139. doi:<a href=\"https://doi.org/10.1145/774572.774592\">10.1145/774572.774592</a>"},"publication_identifier":{"isbn":["9780780376076"]},"publication_status":"published","doi":"10.1145/774572.774592","date_published":"2002-11-01T00:00:00Z","quality_controlled":"1","acknowledgement":"The authors would like to thank Jerry Burch of the Cadence Berkeley Labs for many insightful discussions and suggestions.\r\n","publisher":"IEEE","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","year":"2002","_id":"4413","publication":"Proceedings of the 11th IEEE/ACM international conference on Computer-aided design","scopus_import":"1","article_processing_charge":"No","author":[{"full_name":"Passerone, Roberto","first_name":"Roberto","last_name":"Passerone"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Sangiovanni Vincentelli","first_name":"Alberto","full_name":"Sangiovanni Vincentelli, Alberto"}],"page":"132 - 139","type":"conference","oa_version":"None","month":"11","day":"01","abstract":[{"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.","lang":"eng"}],"date_updated":"2023-06-05T14:21:46Z","title":"Convertibility verification and converter synthesis: Two faces of the same coin","publist_id":"318","date_created":"2018-12-11T12:08:44Z"},{"_id":"4414","article_processing_charge":"No","publisher":"University of California, Berkeley","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2002","title":"Games in open systems verification and synthesis","date_created":"2018-12-11T12:08:44Z","publist_id":"315","page":"1 - 116","author":[{"full_name":"Mang, Freddy","last_name":"Mang","first_name":"Freddy"}],"abstract":[{"lang":"eng","text":"This dissertation investigates game-theoretic approaches to the algorithmic analysis of concurrent, reactive systems. A concurrent system comprises a number of components working concurrently; a reactive system maintains an ongoing interaction with its environment. Traditional approaches to the formal analysis of concurrent reactive systems usually view the system as an unstructured state-transition graphs; instead, we view them as collections of interacting components, where each one is an open system which accepts inputs from the other components. The interactions among the components are naturally modeled as games.\r\n\r\nAdopting this game-theoretic view, we study three related problems pertaining to the verification and synthesis of systems. Firstly, we propose two novel game-theoretic techniques for the model-checking of concurrent reactive systems, and improve the performance of model-checking. The first technique discovers an error as soon as it cannot be prevented, which can be long before it actually occurs. This technique is based on the key observation that &quot;unpreventability&quot; is a local property to a module: an error is unpreventable in a module state if no environment can prevent it. The second technique attempts to decompose a model-checking proof into smaller proof obligations by constructing abstract modules automatically, using reachability and &quot;unpreventability&quot; information about the concrete modules. Three increasingly powerful proof decomposition rules are proposed and we show that in practice, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification. Both techniques fall into the category of compositional reasoning.\r\n\r\nSecondly, we investigate the composition and control of synchronous systems. An essential property of synchronous systems for compositional reasoning is non-blocking. In the composition of synchronous systems, however, due to circular causal dependency of input and output signals, non-blocking is not always guaranteed. Blocking compositions of systems can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping systems with types, which make the dependencies between input and output signals transparent. We characterize various typing mechanisms in game-theoretic terms, and study their effects on the controller synthesis problem. We show that our typing systems are general enough to capture interesting real-life synchronous systems such as all delay-insensitive digital circuits. We then study their corresponding single-step control problems --a restricted form of controller synthesis problem whose solutions can be iterated in appropriate manners to solve all LTL controller synthesis problems. We also consider versions of the controller synthesis problem in which the type of the controller is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions.\r\n\r\nThirdly, we study the synthesis of a class of open systems, namely, uninitialized state machines. 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. 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 Buechi 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. The lower bound proofs require nontrivial generic reductions."}],"day":"01","date_updated":"2021-01-12T07:56:48Z","month":"05","oa_version":"None","type":"dissertation","extern":"1","citation":{"short":"F. Mang, Games in Open Systems Verification and Synthesis, University of California, Berkeley, 2002.","ieee":"F. Mang, “Games in open systems verification and synthesis,” University of California, Berkeley, 2002.","chicago":"Mang, Freddy. “Games in Open Systems Verification and Synthesis.” University of California, Berkeley, 2002.","mla":"Mang, Freddy. <i>Games in Open Systems Verification and Synthesis</i>. University of California, Berkeley, 2002, pp. 1–116.","ista":"Mang F. 2002. Games in open systems verification and synthesis. University of California, Berkeley.","apa":"Mang, F. (2002). <i>Games in open systems verification and synthesis</i>. University of California, Berkeley.","ama":"Mang F. Games in open systems verification and synthesis. 2002:1-116."},"language":[{"iso":"eng"}],"status":"public","supervisor":[{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"}],"date_published":"2002-05-01T00:00:00Z","publication_status":"published"},{"_id":"4421","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.","year":"2002","volume":2491,"date_created":"2018-12-11T12:08:46Z","page":"46 - 60","oa_version":"None","type":"conference","month":"09","date_updated":"2023-06-05T13:07:20Z","abstract":[{"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.","lang":"eng"}],"intvolume":"      2491","extern":"1","citation":{"ama":"Kirsch C, Sanvido M, Henzinger TA, Pree W. A Giotto-based helicopter control system. In: <i>Proceedings of the 2nd International Conference on Embedded Software</i>. Vol 2491. ACM; 2002:46-60. doi:<a href=\"https://doi.org/10.1007/3-540-45828-X_5\">10.1007/3-540-45828-X_5</a>","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.” <i>Proceedings of the 2nd International Conference on Embedded Software</i>, vol. 2491, ACM, 2002, pp. 46–60, doi:<a href=\"https://doi.org/10.1007/3-540-45828-X_5\">10.1007/3-540-45828-X_5</a>.","apa":"Kirsch, C., Sanvido, M., Henzinger, T. A., &#38; Pree, W. (2002). A Giotto-based helicopter control system. In <i>Proceedings of the 2nd International Conference on Embedded Software</i> (Vol. 2491, pp. 46–60). Grenoble, France: ACM. <a href=\"https://doi.org/10.1007/3-540-45828-X_5\">https://doi.org/10.1007/3-540-45828-X_5</a>","ieee":"C. Kirsch, M. Sanvido, T. A. Henzinger, and W. Pree, “A Giotto-based helicopter control system,” in <i>Proceedings of the 2nd International Conference on Embedded Software</i>, Grenoble, France, 2002, vol. 2491, pp. 46–60.","chicago":"Kirsch, Christoph, Marco Sanvido, Thomas A Henzinger, and Wolfgang Pree. “A Giotto-Based Helicopter Control System.” In <i>Proceedings of the 2nd International Conference on Embedded Software</i>, 2491:46–60. ACM, 2002. <a href=\"https://doi.org/10.1007/3-540-45828-X_5\">https://doi.org/10.1007/3-540-45828-X_5</a>.","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."},"alternative_title":["LNCS"],"status":"public","date_published":"2002-09-25T00:00:00Z","publication_status":"published","publication":"Proceedings of the 2nd International Conference on Embedded Software","scopus_import":"1","article_processing_charge":"No","publisher":"ACM","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"A Giotto-based helicopter control system","publist_id":"310","author":[{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph"},{"full_name":"Sanvido, Marco","first_name":"Marco","last_name":"Sanvido"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Pree","first_name":"Wolfgang","full_name":"Pree, Wolfgang"}],"day":"25","conference":{"start_date":"2002-10-07","location":"Grenoble, France","name":"EMSOFT: Embedded Software ","end_date":"2002-10-09"},"language":[{"iso":"eng"}],"doi":"10.1007/3-540-45828-X_5","quality_controlled":"1","publication_identifier":{"isbn":["9783540443070"]}},{"date_created":"2018-12-11T12:08:46Z","volume":2471,"oa_version":"None","month":"09","type":"conference","date_updated":"2023-06-05T10:02:54Z","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."}],"page":"292 - 305","_id":"4422","year":"2002","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.","date_published":"2002-09-09T00:00:00Z","publication_status":"published","citation":{"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.","chicago":"Jurdziński, Marcin, Orna Kupferman, and Thomas A Henzinger. “Trading Probability for Fairness.” In <i>Proceedings of the 16th International Workshop on Computer Science Logic</i>, 2471:292–305. Springer, 2002. <a href=\"https://doi.org/10.1007/3-540-45793-3_20\">https://doi.org/10.1007/3-540-45793-3_20</a>.","ieee":"M. Jurdziński, O. Kupferman, and T. A. Henzinger, “Trading probability for fairness,” in <i>Proceedings of the 16th International Workshop on Computer Science Logic</i>, Edinburgh, Scotland, 2002, vol. 2471, pp. 292–305.","apa":"Jurdziński, M., Kupferman, O., &#38; Henzinger, T. A. (2002). Trading probability for fairness. In <i>Proceedings of the 16th International Workshop on Computer Science Logic</i> (Vol. 2471, pp. 292–305). Edinburgh, Scotland: Springer. <a href=\"https://doi.org/10.1007/3-540-45793-3_20\">https://doi.org/10.1007/3-540-45793-3_20</a>","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.” <i>Proceedings of the 16th International Workshop on Computer Science Logic</i>, vol. 2471, Springer, 2002, pp. 292–305, doi:<a href=\"https://doi.org/10.1007/3-540-45793-3_20\">10.1007/3-540-45793-3_20</a>.","ama":"Jurdziński M, Kupferman O, Henzinger TA. Trading probability for fairness. In: <i>Proceedings of the 16th International Workshop on Computer Science Logic</i>. Vol 2471. Springer; 2002:292-305. doi:<a href=\"https://doi.org/10.1007/3-540-45793-3_20\">10.1007/3-540-45793-3_20</a>"},"extern":"1","intvolume":"      2471","status":"public","alternative_title":["LNCS"],"publist_id":"308","title":"Trading probability for fairness","day":"09","author":[{"full_name":"Jurdziński, Marcin","first_name":"Marcin","last_name":"Jurdziński"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"}],"scopus_import":"1","article_processing_charge":"No","publication":"Proceedings of the 16th International Workshop on Computer Science Logic","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Springer","quality_controlled":"1","doi":"10.1007/3-540-45793-3_20","publication_identifier":{"isbn":["9783540442400"]},"language":[{"iso":"eng"}],"conference":{"name":"CSL: Computer Science Logic","location":"Edinburgh, Scotland"}},{"title":"Embedded software design and system integration for rotorcraft UAV using platforms","publist_id":"306","author":[{"full_name":"Horowitz, Benjamin","last_name":"Horowitz","first_name":"Benjamin"},{"full_name":"Liebman, Judith","first_name":"Judith","last_name":"Liebman"},{"full_name":"Ma, Cedric","first_name":"Cedric","last_name":"Ma"},{"full_name":"Koo, T John","last_name":"Koo","first_name":"T John"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Sangiovanni Vincentelli, Alberto","first_name":"Alberto","last_name":"Sangiovanni Vincentelli"},{"first_name":"Shankar","last_name":"Sastry","full_name":"Sastry, Shankar"}],"day":"01","publication":"Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control","article_processing_charge":"No","scopus_import":"1","publisher":"Elsevier","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","doi":"10.3182/20020721-6-ES-1901.01628","quality_controlled":"1","publication_identifier":{"issn":["1474-6670"]},"conference":{"location":"Barcelona, Spain","name":"IFAC: World Congress on Automatic Control","start_date":"2002-07-21","end_date":"2002-07-26"},"language":[{"iso":"eng"}],"issue":"1","volume":15,"date_created":"2018-12-11T12:08:47Z","date_updated":"2023-06-05T09:55:10Z","abstract":[{"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).","lang":"eng"}],"month":"07","oa_version":"None","type":"conference","_id":"4423","acknowledgement":"Research supported in part by DARPA under contract no.F33615-98-C-3614, Software Enabled Control, administered by\r\nAFRL, Dayton OH.","year":"2002","date_published":"2002-07-01T00:00:00Z","publication_status":"published","extern":"1","intvolume":"        15","citation":{"apa":"Horowitz, B., Liebman, J., Ma, C., Koo, T. J., Henzinger, T. A., Sangiovanni Vincentelli, A., &#38; Sastry, S. (2002). Embedded software design and system integration for rotorcraft UAV using platforms. In <i>Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control</i> (Vol. 15). Barcelona, Spain: Elsevier. <a href=\"https://doi.org/10.3182/20020721-6-ES-1901.01628\">https://doi.org/10.3182/20020721-6-ES-1901.01628</a>","mla":"Horowitz, Benjamin, et al. “Embedded Software Design and System Integration for Rotorcraft UAV Using Platforms.” <i>Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control</i>, vol. 15, no. 1, Elsevier, 2002, doi:<a href=\"https://doi.org/10.3182/20020721-6-ES-1901.01628\">10.3182/20020721-6-ES-1901.01628</a>.","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.","ama":"Horowitz B, Liebman J, Ma C, et al. Embedded software design and system integration for rotorcraft UAV using platforms. In: <i>Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control</i>. Vol 15. Elsevier; 2002. doi:<a href=\"https://doi.org/10.3182/20020721-6-ES-1901.01628\">10.3182/20020721-6-ES-1901.01628</a>","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.","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 <i>Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control</i>, Vol. 15. Elsevier, 2002. <a href=\"https://doi.org/10.3182/20020721-6-ES-1901.01628\">https://doi.org/10.3182/20020721-6-ES-1901.01628</a>.","ieee":"B. Horowitz <i>et al.</i>, “Embedded software design and system integration for rotorcraft UAV using platforms,” in <i>Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control</i>, Barcelona, Spain, 2002, vol. 15, no. 1."},"status":"public"},{"page":"315 - 326","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Kirsch, Christoph","first_name":"Christoph","last_name":"Kirsch"}],"day":"01","abstract":[{"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.","lang":"eng"}],"date_updated":"2023-06-05T09:02:23Z","month":"06","oa_version":"None","type":"conference","title":"The embedded machine: predictable, portable real-time code","date_created":"2018-12-11T12:08:53Z","publist_id":"284","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"ACM","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.","year":"2002","publication":"Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation","_id":"4444","scopus_import":"1","article_processing_charge":"No","publication_status":"published","publication_identifier":{"isbn":["9781581134636"]},"doi":"10.1145/512529.512567","date_published":"2002-06-01T00:00:00Z","quality_controlled":"1","status":"public","extern":"1","conference":{"end_date":"2002-06-19","start_date":"2002-06-17","location":"Berlin, Germany","name":"PLDI: Programming Languages Design and Implementation"},"language":[{"iso":"eng"}],"citation":{"apa":"Henzinger, T. A., &#38; Kirsch, C. (2002). The embedded machine: predictable, portable real-time code. In <i>Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation</i> (pp. 315–326). Berlin, Germany: ACM. <a href=\"https://doi.org/10.1145/512529.512567\">https://doi.org/10.1145/512529.512567</a>","mla":"Henzinger, Thomas A., and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” <i>Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation</i>, ACM, 2002, pp. 315–26, doi:<a href=\"https://doi.org/10.1145/512529.512567\">10.1145/512529.512567</a>.","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.","ama":"Henzinger TA, Kirsch C. The embedded machine: predictable, portable real-time code. In: <i>Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation</i>. ACM; 2002:315-326. doi:<a href=\"https://doi.org/10.1145/512529.512567\">10.1145/512529.512567</a>","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.","chicago":"Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” In <i>Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation</i>, 315–26. ACM, 2002. <a href=\"https://doi.org/10.1145/512529.512567\">https://doi.org/10.1145/512529.512567</a>.","ieee":"T. A. Henzinger and C. Kirsch, “The embedded machine: predictable, portable real-time code,” in <i>Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation</i>, Berlin, Germany, 2002, pp. 315–326."}},{"publication":"Proceedings of the 2nd International Conference on Embedded Software","scopus_import":"1","article_processing_charge":"No","publisher":"ACM","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Time-safety checking for embedded programs","publist_id":"259","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Kirsch, Christoph","last_name":"Kirsch","first_name":"Christoph"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"first_name":"Slobodan","last_name":"Matic","full_name":"Matic, Slobodan"}],"day":"25","conference":{"end_date":"2002-10-09","start_date":"2002-10-07","location":"Grenoble, France","name":"EMSOFT: Embedded Software "},"language":[{"iso":"eng"}],"doi":"10.1007/3-540-45828-X_7","quality_controlled":"1","publication_identifier":{"isbn":["9783540443070"]},"_id":"4470","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.","year":"2002","volume":2491,"date_created":"2018-12-11T12:09:01Z","page":"76 - 92","date_updated":"2023-06-05T08:50:59Z","abstract":[{"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.","lang":"eng"}],"oa_version":"None","month":"09","type":"conference","extern":"1","intvolume":"      2491","citation":{"ama":"Henzinger TA, Kirsch C, Majumdar R, Matic S. Time-safety checking for embedded programs. In: <i>Proceedings of the 2nd International Conference on Embedded Software</i>. Vol 2491. ACM; 2002:76-92. doi:<a href=\"https://doi.org/10.1007/3-540-45828-X_7\">10.1007/3-540-45828-X_7</a>","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.” <i>Proceedings of the 2nd International Conference on Embedded Software</i>, vol. 2491, ACM, 2002, pp. 76–92, doi:<a href=\"https://doi.org/10.1007/3-540-45828-X_7\">10.1007/3-540-45828-X_7</a>.","apa":"Henzinger, T. A., Kirsch, C., Majumdar, R., &#38; Matic, S. (2002). Time-safety checking for embedded programs. In <i>Proceedings of the 2nd International Conference on Embedded Software</i> (Vol. 2491, pp. 76–92). Grenoble, France: ACM. <a href=\"https://doi.org/10.1007/3-540-45828-X_7\">https://doi.org/10.1007/3-540-45828-X_7</a>","ieee":"T. A. Henzinger, C. Kirsch, R. Majumdar, and S. Matic, “Time-safety checking for embedded programs,” in <i>Proceedings of the 2nd International Conference on Embedded Software</i>, Grenoble, France, 2002, vol. 2491, pp. 76–92.","chicago":"Henzinger, Thomas A, Christoph Kirsch, Ritankar Majumdar, and Slobodan Matic. “Time-Safety Checking for Embedded Programs.” In <i>Proceedings of the 2nd International Conference on Embedded Software</i>, 2491:76–92. ACM, 2002. <a href=\"https://doi.org/10.1007/3-540-45828-X_7\">https://doi.org/10.1007/3-540-45828-X_7</a>.","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."},"alternative_title":["LNCS"],"status":"public","date_published":"2002-09-25T00:00:00Z","publication_status":"published"},{"language":[{"iso":"eng"}],"conference":{"end_date":"2002-07-13","start_date":"2002-07-08","name":"ICALP: Automata, Languages and Programming","location":"Malaga, Spain"},"quality_controlled":"1","doi":"10.1007/3-540-45465-9_55","publication_identifier":{"isbn":["9783540438649"]},"article_processing_charge":"No","scopus_import":"1","publication":"Proceedings of the 29th International Colloquium on Automata, Languages and Programming","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Springer","publist_id":"257","title":"Synthesis of uninitialized systems","day":"26","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Krishnan, Sriram","last_name":"Krishnan","first_name":"Sriram"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"},{"full_name":"Mang, Freddy","first_name":"Freddy","last_name":"Mang"}],"citation":{"ama":"Henzinger TA, Krishnan S, Kupferman O, Mang F. Synthesis of uninitialized systems. In: <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>. Vol 2380. Springer; 2002:644-656. doi:<a href=\"https://doi.org/10.1007/3-540-45465-9_55\">10.1007/3-540-45465-9_55</a>","apa":"Henzinger, T. A., Krishnan, S., Kupferman, O., &#38; Mang, F. (2002). Synthesis of uninitialized systems. In <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i> (Vol. 2380, pp. 644–656). Malaga, Spain: Springer. <a href=\"https://doi.org/10.1007/3-540-45465-9_55\">https://doi.org/10.1007/3-540-45465-9_55</a>","mla":"Henzinger, Thomas A., et al. “Synthesis of Uninitialized Systems.” <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>, vol. 2380, Springer, 2002, pp. 644–56, doi:<a href=\"https://doi.org/10.1007/3-540-45465-9_55\">10.1007/3-540-45465-9_55</a>.","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.","chicago":"Henzinger, Thomas A, Sriram Krishnan, Orna Kupferman, and Freddy Mang. “Synthesis of Uninitialized Systems.” In <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>, 2380:644–56. Springer, 2002. <a href=\"https://doi.org/10.1007/3-540-45465-9_55\">https://doi.org/10.1007/3-540-45465-9_55</a>.","ieee":"T. A. Henzinger, S. Krishnan, O. Kupferman, and F. Mang, “Synthesis of uninitialized systems,” in <i>Proceedings of the 29th International Colloquium on Automata, Languages and Programming</i>, Malaga, Spain, 2002, vol. 2380, pp. 644–656.","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."},"extern":"1","intvolume":"      2380","status":"public","alternative_title":["LNCS"],"date_published":"2002-06-26T00:00:00Z","publication_status":"published","_id":"4471","year":"2002","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.","date_created":"2018-12-11T12:09:01Z","volume":2380,"abstract":[{"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.","lang":"eng"}],"date_updated":"2023-06-05T08:05:13Z","month":"06","type":"conference","oa_version":"None","page":"644 - 656"},{"date_created":"2018-12-11T12:09:01Z","volume":2404,"type":"conference","oa_version":"None","month":"06","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."}],"date_updated":"2023-06-05T08:11:32Z","page":"526 - 538","_id":"4472","year":"2002","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.","date_published":"2002-06-19T00:00:00Z","publication_status":"published","citation":{"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.","chicago":"Henzinger, Thomas A, George Necula, Ranjit Jhala, Grégoire Sutre, Ritankar Majumdar, and Westley Weimer. “Temporal Safety Proofs for Systems Code.” In <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>, 2404:526–38. Springer, 2002. <a href=\"https://doi.org/10.1007/3-540-45657-0_45\">https://doi.org/10.1007/3-540-45657-0_45</a>.","ieee":"T. A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, and W. Weimer, “Temporal safety proofs for systems code,” in <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>, Copenhagen, Denmark, 2002, vol. 2404, pp. 526–538.","apa":"Henzinger, T. A., Necula, G., Jhala, R., Sutre, G., Majumdar, R., &#38; Weimer, W. (2002). Temporal safety proofs for systems code. In <i>Proceedings of the 14th International Conference on Computer Aided Verification</i> (Vol. 2404, pp. 526–538). Copenhagen, Denmark: Springer. <a href=\"https://doi.org/10.1007/3-540-45657-0_45\">https://doi.org/10.1007/3-540-45657-0_45</a>","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.” <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>, vol. 2404, Springer, 2002, pp. 526–38, doi:<a href=\"https://doi.org/10.1007/3-540-45657-0_45\">10.1007/3-540-45657-0_45</a>.","ama":"Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. Temporal safety proofs for systems code. In: <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>. Vol 2404. Springer; 2002:526-538. doi:<a href=\"https://doi.org/10.1007/3-540-45657-0_45\">10.1007/3-540-45657-0_45</a>"},"intvolume":"      2404","extern":"1","status":"public","alternative_title":["LNCS"],"publist_id":"258","title":"Temporal safety proofs for systems code","day":"19","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Necula, George","first_name":"George","last_name":"Necula"},{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"last_name":"Sutre","first_name":"Grégoire","full_name":"Sutre, Grégoire"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"},{"full_name":"Weimer, Westley","first_name":"Westley","last_name":"Weimer"}],"scopus_import":"1","article_processing_charge":"No","publication":"Proceedings of the 14th International Conference on Computer Aided Verification","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Springer","quality_controlled":"1","doi":"10.1007/3-540-45657-0_45","publication_identifier":{"isbn":["9783540439974"]},"language":[{"iso":"eng"}],"conference":{"end_date":"2002-07-31","start_date":"2002-07-27","location":"Copenhagen, Denmark","name":"CAV: Computer Aided Verification"}},{"language":[{"iso":"eng"}],"issue":"1","publication_identifier":{"issn":["0164-0925"]},"quality_controlled":"1","doi":"10.1145/509705.509707","publisher":"ACM","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","scopus_import":"1","article_type":"original","publication":"ACM Transactions on Programming Languages and Systems (TOPLAS)","day":"01","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"},{"full_name":"Tasiran, Serdar","first_name":"Serdar","last_name":"Tasiran"}],"publist_id":"256","title":"An assume-guarantee rule for checking simulation","status":"public","citation":{"ama":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for checking simulation. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. 2002;24(1):51-64. doi:<a href=\"https://doi.org/10.1145/509705.509707\">10.1145/509705.509707</a>","apa":"Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (2002). An assume-guarantee rule for checking simulation. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM. <a href=\"https://doi.org/10.1145/509705.509707\">https://doi.org/10.1145/509705.509707</a>","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.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24, no. 1, ACM, 2002, pp. 51–64, doi:<a href=\"https://doi.org/10.1145/509705.509707\">10.1145/509705.509707</a>.","chicago":"Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM, 2002. <a href=\"https://doi.org/10.1145/509705.509707\">https://doi.org/10.1145/509705.509707</a>.","ieee":"T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee rule for checking simulation,” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24, no. 1. ACM, pp. 51–64, 2002.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming Languages and Systems (TOPLAS) 24 (2002) 51–64."},"intvolume":"        24","extern":"1","publication_status":"published","date_published":"2002-01-01T00:00:00Z","year":"2002","_id":"4473","abstract":[{"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 &quot;P is simulated by Q,&quot; 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.","lang":"eng"}],"date_updated":"2023-06-05T07:59:47Z","oa_version":"None","type":"journal_article","month":"01","page":"51 - 64","date_created":"2018-12-11T12:09:02Z","volume":24},{"language":[{"iso":"eng"}],"issue":"1","quality_controlled":"1","doi":"10.1006/inco.2001.3085","publication_identifier":{"issn":["0890-5401"]},"article_processing_charge":"No","scopus_import":"1","article_type":"original","publication":"Information and Computation","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Elsevier","publist_id":"255","title":"Fair simulation","day":"25","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"},{"last_name":"Rajamani","first_name":"Sriram","full_name":"Rajamani, Sriram"}],"citation":{"short":"T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173 (2002) 64–81.","ieee":"T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” <i>Information and Computation</i>, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.","chicago":"Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.” <i>Information and Computation</i>. Elsevier, 2002. <a href=\"https://doi.org/10.1006/inco.2001.3085\">https://doi.org/10.1006/inco.2001.3085</a>.","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.” <i>Information and Computation</i>, vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:<a href=\"https://doi.org/10.1006/inco.2001.3085\">10.1006/inco.2001.3085</a>.","apa":"Henzinger, T. A., Kupferman, O., &#38; Rajamani, S. (2002). Fair simulation. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.2001.3085\">https://doi.org/10.1006/inco.2001.3085</a>","ama":"Henzinger TA, Kupferman O, Rajamani S. Fair simulation. <i>Information and Computation</i>. 2002;173(1):64-81. doi:<a href=\"https://doi.org/10.1006/inco.2001.3085\">10.1006/inco.2001.3085</a>"},"intvolume":"       173","extern":"1","status":"public","main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub"}],"date_published":"2002-02-25T00:00:00Z","oa":1,"publication_status":"published","_id":"4474","year":"2002","acknowledgement":"We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers for their comments on this paper.","date_created":"2018-12-11T12:09:02Z","volume":173,"date_updated":"2023-06-05T07:53:27Z","abstract":[{"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.","lang":"eng"}],"month":"02","type":"journal_article","oa_version":"Published Version","page":"64 - 81"},{"citation":{"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.” <i>Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, ACM, 2002, pp. 58–70, doi:<a href=\"https://doi.org/10.1145/503272.503279\">10.1145/503272.503279</a>.","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Sutre, G. (2002). Lazy abstraction. In <i>Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i> (pp. 58–70). Portland, OR, USA: ACM. <a href=\"https://doi.org/10.1145/503272.503279\">https://doi.org/10.1145/503272.503279</a>","ama":"Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: <i>Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>. ACM; 2002:58-70. doi:<a href=\"https://doi.org/10.1145/503272.503279\">10.1145/503272.503279</a>","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.","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy abstraction,” in <i>Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i>, Portland, OR, USA, 2002, pp. 58–70.","chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre. “Lazy Abstraction.” In <i>Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, 58–70. ACM, 2002. <a href=\"https://doi.org/10.1145/503272.503279\">https://doi.org/10.1145/503272.503279</a>."},"language":[{"iso":"eng"}],"conference":{"end_date":"2002-01-18","start_date":"2002-01-16","name":"POPL: Principles of Programming Languages","location":"Portland, OR, USA"},"extern":"1","status":"public","quality_controlled":"1","doi":"10.1145/503272.503279","date_published":"2002-01-01T00:00:00Z","publication_identifier":{"isbn":["9781581134506"]},"publication_status":"published","article_processing_charge":"No","scopus_import":"1","_id":"4476","publication":"Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","year":"2002","acknowledgement":"We thank Wes Weimer and Jeff Foster for many useful discussions. \r\n","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"ACM","date_created":"2018-12-11T12:09:03Z","publist_id":"254","title":"Lazy abstraction","type":"conference","month":"01","oa_version":"None","date_updated":"2023-06-05T07:45:53Z","day":"01","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."}],"author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Jhala","first_name":"Ranjit","full_name":"Jhala, Ranjit"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"},{"first_name":"Grégoire","last_name":"Sutre","full_name":"Sutre, Grégoire"}],"page":"58 - 70"},{"extern":"1","intvolume":"       432","citation":{"ista":"Ruocco I, Cuello A, Shigemoto R, Ribeiro Da Silva A. 2001. Light and electron microscopic study of the distribution of substance P-immunoreactive fibers and neurokinin-1 receptors in the skin of the rat lower lip. Journal of Comparative Neurology. 432(4), 466–480.","mla":"Ruocco, Isabella, et al. “Light and Electron Microscopic Study of the Distribution of Substance P-Immunoreactive Fibers and Neurokinin-1 Receptors in the Skin of the Rat Lower Lip.” <i>Journal of Comparative Neurology</i>, vol. 432, no. 4, Wiley-Blackwell, 2001, pp. 466–80, doi:<a href=\"https://doi.org/10.1002/cne.1114\">10.1002/cne.1114</a>.","apa":"Ruocco, I., Cuello, A., Shigemoto, R., &#38; Ribeiro Da Silva, A. (2001). Light and electron microscopic study of the distribution of substance P-immunoreactive fibers and neurokinin-1 receptors in the skin of the rat lower lip. <i>Journal of Comparative Neurology</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/cne.1114\">https://doi.org/10.1002/cne.1114</a>","ama":"Ruocco I, Cuello A, Shigemoto R, Ribeiro Da Silva A. Light and electron microscopic study of the distribution of substance P-immunoreactive fibers and neurokinin-1 receptors in the skin of the rat lower lip. <i>Journal of Comparative Neurology</i>. 2001;432(4):466-480. doi:<a href=\"https://doi.org/10.1002/cne.1114\">10.1002/cne.1114</a>","short":"I. Ruocco, A. Cuello, R. Shigemoto, A. Ribeiro Da Silva, Journal of Comparative Neurology 432 (2001) 466–480.","ieee":"I. Ruocco, A. Cuello, R. Shigemoto, and A. Ribeiro Da Silva, “Light and electron microscopic study of the distribution of substance P-immunoreactive fibers and neurokinin-1 receptors in the skin of the rat lower lip,” <i>Journal of Comparative Neurology</i>, vol. 432, no. 4. Wiley-Blackwell, pp. 466–480, 2001.","chicago":"Ruocco, Isabella, Augusto Cuello, Ryuichi Shigemoto, and Alfredo Ribeiro Da Silva. “Light and Electron Microscopic Study of the Distribution of Substance P-Immunoreactive Fibers and Neurokinin-1 Receptors in the Skin of the Rat Lower Lip.” <i>Journal of Comparative Neurology</i>. Wiley-Blackwell, 2001. <a href=\"https://doi.org/10.1002/cne.1114\">https://doi.org/10.1002/cne.1114</a>."},"status":"public","external_id":{"pmid":["11268009"]},"date_published":"2001-04-16T00:00:00Z","publication_status":"published","_id":"2604","acknowledgement":"This work was sponsored by grant MT-12170 from the Canadian Medical Research Council. The authors thank Marie Ballak for electron microscopy assistance, Alan Forster  for  photographic  expertise,  and  Sid  Parkinson  for editorial assistance.","year":"2001","volume":432,"date_created":"2018-12-11T11:58:37Z","page":"466 - 480","month":"04","oa_version":"None","type":"journal_article","abstract":[{"text":"Cutaneous antidromic vasodilatation and plasma extravasation, two phenomena that occur in neurogenic inflammation, are partially blocked by substance P (SP) receptor antagonists and are known to be mediated in part by mast cell-released substances, such as histamine, serotonin, and nitric oxide. In an attempt to provide a morphological substrate for the above phenomena, we applied light and electron microscopic immunocytochemistry to investigate the pattern of SP innervation of blood vessels and its relationship to mast cells in the skin of the rat lower lip. Furthermore, we examined the distribution of SP (neurokinin-1) receptors and their relationship to SP-immunoreactive (IR) fibers. Our results confirmed that SP-IR fibers are found in cutaneous nerves and that terminal branches are observed around blood vessels and penetrating the epidermis. SP-IR fibers also innervated hair follicles and sebaceous glands. At the ultrastructural level, SP-IR varicosities were observed adjacent to arterioles, capillaries, venules, and mast cells. The varicosities possessed both dense core vesicles and agranular synaptic vesicles. We quantified the distance between SP-IR varicosities and blood vessel endothelial cells. SP-IR terminals were located within 0.23-5.99 μm from the endothelial cell layer in 82.7% of arterioles, in 90.2% of capillaries, and in 86.9% of venules. Although there was a trend for SP-IR fibers to be located closer to the endothelium of venules, this difference was not significant. Neurokinin-1 receptor (NK-1r) immunoreactivity was most abundant in the upper dermis and was associated with the wall of blood vessels. NK-1r were located in equal amounts on the walls of arterioles, capillaries, and venules that were innervated by SP-IR fibers. The present results favor the concept of a participation of SP in cutaneous neurogenic vasodilatation and plasma extravasation both by an action on blood vessels after binding to the NK-1r and by causing the release of substances from mast cells after diffusion through the connective tissue.","lang":"eng"}],"date_updated":"2023-05-24T13:03:51Z","issue":"4","language":[{"iso":"eng"}],"doi":"10.1002/cne.1114","quality_controlled":"1","publication_identifier":{"issn":["0021-9967"]},"publication":"Journal of Comparative Neurology","article_type":"original","scopus_import":"1","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Wiley-Blackwell","pmid":1,"title":"Light and electron microscopic study of the distribution of substance P-immunoreactive fibers and neurokinin-1 receptors in the skin of the rat lower lip","publist_id":"4294","author":[{"full_name":"Ruocco, Isabella","last_name":"Ruocco","first_name":"Isabella"},{"last_name":"Cuello","first_name":"Augusto","full_name":"Cuello, Augusto"},{"full_name":"Shigemoto, Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444","first_name":"Ryuichi","last_name":"Shigemoto"},{"full_name":"Ribeiro Da Silva, Alfredo","last_name":"Ribeiro Da Silva","first_name":"Alfredo"}],"day":"16"},{"title":"Morphological and neurochemical differentiation of large granular layer interneurons in the adult rat cerebellum","publist_id":"4292","author":[{"last_name":"Geurts","first_name":"Frederik","full_name":"Geurts, Frederik"},{"first_name":"Jean","last_name":"Timmermans","full_name":"Timmermans, Jean"},{"id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi","first_name":"Ryuichi","last_name":"Shigemoto"},{"full_name":"De Schutter, Erik","last_name":"De Schutter","first_name":"Erik"}],"day":"10","publication":"Neuroscience","article_type":"original","article_processing_charge":"No","scopus_import":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"Elsevier","pmid":1,"doi":"10.1016/S0306-4522(01)00058-6","quality_controlled":"1","publication_identifier":{"issn":["0306-4522"]},"issue":"2","language":[{"iso":"eng"}],"volume":104,"date_created":"2018-12-11T11:58:38Z","page":"499 - 512","type":"journal_article","oa_version":"None","month":"05","abstract":[{"text":"The granular layer of the cerebellar cortex consists of densely packed neuronal cells, classified into granule cells and large interneurons. In this study, we provide a comparative survey of large granular layer interneurons in the adult rat cerebellum based on both morphological and neurochemical criteria. To this end, double immunofluorescence histochemistry was performed by combining antibodies against the cytoplasmic antigen Rat-303, calretinin, the metabotropic glutamate receptor mGluR2 and somatostatin. Based on Rat-303/calretinin double immunohistochemistry, three distinct populations of large granular layer interneurons could be discerned: cells immunopositive for Rat-303, calretinin or both. Rat-303 or calretinin single-labeled cells represented Golgi cells and unipolar brush cells, respectively. Rat-303/calretinin double-labeled cells located just underneath the Purkinje cell layer represented Lugaro cells. Morphometrical analysis distinguished two populations of Rat-303-positive Golgi cells according to their location: vermis versus hemisphere. Immunostaining for the metabotropic glutamate receptor mGluR2 combined with Rat-303 or calretinin revealed that the majority of Golgi cells (about 90%) appeared to be mGluR2 positive. Lugaro cells were mGluR2 negative. In addition, a limited population of large polymorphous interneurons in the depth of the granular layer with morphological features resembling Golgi cells also displayed Rat-303/calretinin immunoreactivity and were mGluR2 negative. Double immunohistochemistry for Rat-303 and somatostatin revealed three populations of labeled cells in the depth of the granular layer. Besides double-labeled Golgi cells, Rat-303 or somatostatin single-labeled cells were present. Based on mGluR2/somatostatin and calretinin/somatostatin double immunostainings, Rat-303 single-labeled cells were found to correspond to Rat-303/calretinin-positive, mGluR2-negative Golgi-like cells, while the identity of somatostatin single-labeled cells remained unclear. The data presented in this article elaborate previous reports on the morphological and neurochemical differentiation of large interneurons in the rat cerebellar granular layer. In addition, they indicate that the current classification of these cells into Golgi cells, Lugaro cells and unipolar brush cells does not describe the observed neurochemical heterogeneity.","lang":"eng"}],"date_updated":"2023-05-24T12:45:30Z","_id":"2605","year":"2001","date_published":"2001-05-10T00:00:00Z","publication_status":"published","extern":"1","intvolume":"       104","citation":{"short":"F. Geurts, J. Timmermans, R. Shigemoto, E. De Schutter, Neuroscience 104 (2001) 499–512.","chicago":"Geurts, Frederik, Jean Timmermans, Ryuichi Shigemoto, and Erik De Schutter. “Morphological and Neurochemical Differentiation of Large Granular Layer Interneurons in the Adult Rat Cerebellum.” <i>Neuroscience</i>. Elsevier, 2001. <a href=\"https://doi.org/10.1016/S0306-4522(01)00058-6\">https://doi.org/10.1016/S0306-4522(01)00058-6</a>.","ieee":"F. Geurts, J. Timmermans, R. Shigemoto, and E. De Schutter, “Morphological and neurochemical differentiation of large granular layer interneurons in the adult rat cerebellum,” <i>Neuroscience</i>, vol. 104, no. 2. Elsevier, pp. 499–512, 2001.","apa":"Geurts, F., Timmermans, J., Shigemoto, R., &#38; De Schutter, E. (2001). Morphological and neurochemical differentiation of large granular layer interneurons in the adult rat cerebellum. <i>Neuroscience</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0306-4522(01)00058-6\">https://doi.org/10.1016/S0306-4522(01)00058-6</a>","mla":"Geurts, Frederik, et al. “Morphological and Neurochemical Differentiation of Large Granular Layer Interneurons in the Adult Rat Cerebellum.” <i>Neuroscience</i>, vol. 104, no. 2, Elsevier, 2001, pp. 499–512, doi:<a href=\"https://doi.org/10.1016/S0306-4522(01)00058-6\">10.1016/S0306-4522(01)00058-6</a>.","ista":"Geurts F, Timmermans J, Shigemoto R, De Schutter E. 2001. Morphological and neurochemical differentiation of large granular layer interneurons in the adult rat cerebellum. Neuroscience. 104(2), 499–512.","ama":"Geurts F, Timmermans J, Shigemoto R, De Schutter E. Morphological and neurochemical differentiation of large granular layer interneurons in the adult rat cerebellum. <i>Neuroscience</i>. 2001;104(2):499-512. doi:<a href=\"https://doi.org/10.1016/S0306-4522(01)00058-6\">10.1016/S0306-4522(01)00058-6</a>"},"status":"public","external_id":{"pmid":["11377850"]}},{"_id":"2606","year":"2001","acknowledgement":"MV  and  AF  are  senior  coauthors  of  this  work,  which  was  supported  by Ministerio de Educacion y Cultura, grants SAF97/0195 and SAF 2000-0152-C02-02 to M.V; PB94-0219-CO2-01 and PB97-0582-CO2-01 to A.F., Accio Especial  de  R+D  AE98-18  from  Generalitat  Valenciana,  and  a  Fellowship from Bancaixa-C.S.I.C. to J.R.M.-G. We wish to thank Andre M. Goffinet for his  G10  antireelin  antibody  and  Roberto  Gallego,  Juan  M.  Luque  and  Felix Viana for their constructive criticisms on previous versions of the manuscript.","date_created":"2018-12-11T11:58:38Z","volume":13,"month":"03","type":"journal_article","oa_version":"None","abstract":[{"text":"Glutamate receptors have been linked to the regulation of several developmental events in the CNS. By using cortical slices of early postnatal mice, we show that in layer I cells, glutamate produces intracellular calcium ([Ca2+]i) elevations mediated by ionotropic and metabotropic glutamate receptors (mGluRs). The contribution of mGluRs to these responses was demonstrated by application of tACPD, an agonist to groups I and II mGluRs, which evoked [Ca2+]i increases that could be reversibly blocked by MCPG, an antagonist to groups I and II mGluRs. In the absence of extracellular Ca2+, repetitive applications of tACPD or quisqualate, an agonist to group I mGluRs, elicited decreasing [Ca2+]i responses that were restored by refilling a thapsigargin-sensitive Ca2+ store. The use of specific group I mGluR agonists CHPG and DHPG indicated that the functional mGluR in layer I was of the mGluR1 subtype. Subtype specific antibodies confirmed the presence of mGlur1α, but not mGluR5, in Cajal-Retzius (Reelin-immunoreactive) neurons.","lang":"eng"}],"date_updated":"2023-05-24T12:53:46Z","page":"1147 - 1154","citation":{"chicago":"Martínez, Galán, Guillermina López Bendito, Rafael Luján, Ryuichi Shigemoto, Alfonso Fairén, and Miguel Valdeolmillos. “Cajal-Retzius Cells in Early Postnatal Mouse Cortex Selectively Express Functional Metabotropic Glutamate Receptors.” <i>European Journal of Neuroscience</i>. Wiley-Blackwell, 2001. <a href=\"https://doi.org/10.1046/j.0953-816X.2001.01494.x\">https://doi.org/10.1046/j.0953-816X.2001.01494.x</a>.","ieee":"G. Martínez, G. López Bendito, R. Luján, R. Shigemoto, A. Fairén, and M. Valdeolmillos, “Cajal-Retzius cells in early postnatal mouse cortex selectively express functional metabotropic glutamate receptors,” <i>European Journal of Neuroscience</i>, vol. 13, no. 6. Wiley-Blackwell, pp. 1147–1154, 2001.","short":"G. Martínez, G. López Bendito, R. Luján, R. Shigemoto, A. Fairén, M. Valdeolmillos, European Journal of Neuroscience 13 (2001) 1147–1154.","ama":"Martínez G, López Bendito G, Luján R, Shigemoto R, Fairén A, Valdeolmillos M. Cajal-Retzius cells in early postnatal mouse cortex selectively express functional metabotropic glutamate receptors. <i>European Journal of Neuroscience</i>. 2001;13(6):1147-1154. doi:<a href=\"https://doi.org/10.1046/j.0953-816X.2001.01494.x\">10.1046/j.0953-816X.2001.01494.x</a>","apa":"Martínez, G., López Bendito, G., Luján, R., Shigemoto, R., Fairén, A., &#38; Valdeolmillos, M. (2001). Cajal-Retzius cells in early postnatal mouse cortex selectively express functional metabotropic glutamate receptors. <i>European Journal of Neuroscience</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1046/j.0953-816X.2001.01494.x\">https://doi.org/10.1046/j.0953-816X.2001.01494.x</a>","ista":"Martínez G, López Bendito G, Luján R, Shigemoto R, Fairén A, Valdeolmillos M. 2001. Cajal-Retzius cells in early postnatal mouse cortex selectively express functional metabotropic glutamate receptors. European Journal of Neuroscience. 13(6), 1147–1154.","mla":"Martínez, Galán, et al. “Cajal-Retzius Cells in Early Postnatal Mouse Cortex Selectively Express Functional Metabotropic Glutamate Receptors.” <i>European Journal of Neuroscience</i>, vol. 13, no. 6, Wiley-Blackwell, 2001, pp. 1147–54, doi:<a href=\"https://doi.org/10.1046/j.0953-816X.2001.01494.x\">10.1046/j.0953-816X.2001.01494.x</a>."},"intvolume":"        13","extern":"1","external_id":{"pmid":["11285012"]},"status":"public","date_published":"2001-03-01T00:00:00Z","publication_status":"published","article_type":"original","scopus_import":"1","article_processing_charge":"No","publication":"European Journal of Neuroscience","pmid":1,"publisher":"Wiley-Blackwell","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"4293","title":"Cajal-Retzius cells in early postnatal mouse cortex selectively express functional metabotropic glutamate receptors","day":"01","author":[{"first_name":"Galán","last_name":"Martínez","full_name":"Martínez, Galán"},{"full_name":"López Bendito, Guillermina","last_name":"López Bendito","first_name":"Guillermina"},{"full_name":"Luján, Rafael","last_name":"Luján","first_name":"Rafael"},{"full_name":"Shigemoto, Ryuichi","orcid":"0000-0001-8761-9444","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","last_name":"Shigemoto","first_name":"Ryuichi"},{"full_name":"Fairén, Alfonso","last_name":"Fairén","first_name":"Alfonso"},{"full_name":"Valdeolmillos, Miguel","last_name":"Valdeolmillos","first_name":"Miguel"}],"issue":"6","language":[{"iso":"eng"}],"quality_controlled":"1","doi":"10.1046/j.0953-816X.2001.01494.x","publication_identifier":{"issn":["0953-816X"]}},{"intvolume":"        17","extern":"1","citation":{"short":"S. Mion, C. Corti, A. Neki, R. Shigemoto, M. Corsi, G. Fumagalli, F. Ferraguti, Molecular and Cellular Neuroscience 17 (2001) 957–972.","chicago":"Mion, Silvia, Corrado Corti, Akio Neki, Ryuichi Shigemoto, Mauro Corsi, Guido Fumagalli, and Francesco Ferraguti. “Bidirectional Regulation of Neurite Elaboration by Alternatively Spliced Metabotropic Glutamate Receptor 5 (MGluR5) Isoforms.” <i>Molecular and Cellular Neuroscience</i>. Academic Press, 2001. <a href=\"https://doi.org/10.1006/mcne.2001.0993\">https://doi.org/10.1006/mcne.2001.0993</a>.","ieee":"S. Mion <i>et al.</i>, “Bidirectional regulation of neurite elaboration by alternatively spliced metabotropic glutamate receptor 5 (mGluR5) isoforms,” <i>Molecular and Cellular Neuroscience</i>, vol. 17, no. 6. Academic Press, pp. 957–972, 2001.","apa":"Mion, S., Corti, C., Neki, A., Shigemoto, R., Corsi, M., Fumagalli, G., &#38; Ferraguti, F. (2001). Bidirectional regulation of neurite elaboration by alternatively spliced metabotropic glutamate receptor 5 (mGluR5) isoforms. <i>Molecular and Cellular Neuroscience</i>. Academic Press. <a href=\"https://doi.org/10.1006/mcne.2001.0993\">https://doi.org/10.1006/mcne.2001.0993</a>","ista":"Mion S, Corti C, Neki A, Shigemoto R, Corsi M, Fumagalli G, Ferraguti F. 2001. Bidirectional regulation of neurite elaboration by alternatively spliced metabotropic glutamate receptor 5 (mGluR5) isoforms. Molecular and Cellular Neuroscience. 17(6), 957–972.","mla":"Mion, Silvia, et al. “Bidirectional Regulation of Neurite Elaboration by Alternatively Spliced Metabotropic Glutamate Receptor 5 (MGluR5) Isoforms.” <i>Molecular and Cellular Neuroscience</i>, vol. 17, no. 6, Academic Press, 2001, pp. 957–72, doi:<a href=\"https://doi.org/10.1006/mcne.2001.0993\">10.1006/mcne.2001.0993</a>.","ama":"Mion S, Corti C, Neki A, et al. Bidirectional regulation of neurite elaboration by alternatively spliced metabotropic glutamate receptor 5 (mGluR5) isoforms. <i>Molecular and Cellular Neuroscience</i>. 2001;17(6):957-972. doi:<a href=\"https://doi.org/10.1006/mcne.2001.0993\">10.1006/mcne.2001.0993</a>"},"external_id":{"pmid":["11414786"]},"status":"public","date_published":"2001-06-01T00:00:00Z","publication_status":"published","_id":"2607","acknowledgement":"The authors thank: Dr. J. M. Rimland and M. T. Scupoli for their technical help with X. oocytes recordings and FAC sorting, respectively; Dr. Y. Dalezios for helping with the statistical analyses; and Dr. G. Varani for helping with the analyses of mRNA and genomic sequences. We are also grateful to Professor F. Benfenati, Dr. F. Conquet, Dr. Rafael Lujan, Dr. J. McIlhinney, Professor P. Somogyi, Dr. J. H. Xuereb, and Dr. M. Zoli for careful reading of the manuscript\r\nand helpful suggestions. R.S. is supported by the Laboratory of Cerebral Structure, National Institute for Physiological Sciences, Myodaiji, Okazaki 444-8585, CREST Japan Science and Technology Corporation, Japan.","year":"2001","volume":17,"date_created":"2018-12-11T11:58:38Z","page":"957 - 972","date_updated":"2023-05-24T09:34:13Z","abstract":[{"lang":"eng","text":"Alternative splicing in the mGluR5 gene generates two different receptor isoforms, of which expression is developmentally regulated. However, little is known about the functional significance of mGluR5 splice variants. We have examined the functional coupling, subcellular targeting, and effect on neuronal differentiation of epitope-tagged mGluR5 isoforms by expression in neuroblastoma NG108-15 cells. We found that both mGluR5 splice variants give rise to comparable [Ca2+]i transients and have similar pharmacological profile. Tagged receptors were shown by immunofluorescence to be inserted in the plasma membrane. In undifferentiated cells the subcellular localization of the two mGluR5 isoforms was partially segregated, whereas in differentiated cells the labeling largely redistributed to the newly formed neurites. Interestingly, we demonstrate that mGluR5 splice variants dramatically influence the formation and maturation of neurites; mGluR5a hinders the acquisition of mature neuronal traits and mGluR5b fosters the elaboration and extension of neurites. These effects are partly inhibited by MPEP."}],"month":"06","oa_version":"None","type":"journal_article","language":[{"iso":"eng"}],"issue":"6","doi":"10.1006/mcne.2001.0993","quality_controlled":"1","publication_identifier":{"issn":["1044-7431"]},"publication":"Molecular and Cellular Neuroscience","scopus_import":"1","article_processing_charge":"No","article_type":"original","publisher":"Academic Press","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","pmid":1,"title":"Bidirectional regulation of neurite elaboration by alternatively spliced metabotropic glutamate receptor 5 (mGluR5) isoforms","publist_id":"4291","author":[{"full_name":"Mion, Silvia","first_name":"Silvia","last_name":"Mion"},{"full_name":"Corti, Corrado","last_name":"Corti","first_name":"Corrado"},{"first_name":"Akio","last_name":"Neki","full_name":"Neki, Akio"},{"last_name":"Shigemoto","first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi"},{"first_name":"Mauro","last_name":"Corsi","full_name":"Corsi, Mauro"},{"full_name":"Fumagalli, Guido","first_name":"Guido","last_name":"Fumagalli"},{"last_name":"Ferraguti","first_name":"Francesco","full_name":"Ferraguti, Francesco"}],"day":"01"}]