[{"status":"public","type":"journal_article","acknowledgement":"We gratefully acknowledge Dr. A.Carne (Institute of Cancer Research, London, U.K.) for help with N-terminal sequencing. We thank Prof. C. J. Leaver (University of Oxford, U.K.), Prof. K.-H. Süss (Institute of Plant Genetics and Crop Plant Research, Gatersleben, Germany), and Prof. L. J. Rogers (University of Aberystwyth, U.K.) for gifts of antiserum against maize mitochondrial cytochrome oxidase subunit 1 and cytochrome bc1 complex, spinach FNR, and spinach ferredoxin, respectively. This work was supported by grants from The Royal Society and the Biotechnology and Biological Sciences Research Council.","date_published":"1998-02-03T00:00:00Z","main_file_link":[{"url":"https://europepmc.org/article/pmc/18756","open_access":"1"}],"year":"1998","_id":"1956","title":"The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes","scopus_import":"1","publist_id":"5130","abstract":[{"text":"\r\nThe plastid genomes of several plants contain ndh genes-homologues of genes encoding subunits of the proton-pumping NADH:ubiquinone oxidoreductase, or complex I, involved in respiration in mitochondria and eubacteria. From sequence similarities with these genes, the ndh gene products have been suggested to form a large protein complex (Ndh complex); however, the structure and function of this complex remains to be established. Herein we report the isolation of the Ndh complex from the chloroplasts of the higher plant Pisum sativum. The purification procedure involved selective solubilization of the thylakoid membrane with dodecyl maltoside, followed by two anion-exchange chromatography steps and one size-exclusion chromatography step. The isolated Ndh complex has an apparent total molecular mass of approximately 550 kDa and according to SDS/PAGE consists of at least 16 subunits including NdhA, NdhI, NdhJ, NdhK, and NdhH, which were identified by N-terminal sequencing and immunoblotting. The Ndh complex showed an NADH- and deamino-NADH-specific dehydrogenase activity, characteristic of complex I, when either ferricyanide or the quinones menadione and duroquinone were used as electron acceptors. This study describes the isolation of the chloroplast analogue of the respiratory complex I and provides direct evidence for the function of the plastid Ndh complex as an NADH:plastoquinone oxidoreductase. Our results are compatible with a dual role for the Ndh complex in the chloro-respiratory and cyclic photophosphorylation pathways.","lang":"eng"}],"oa_version":"None","day":"03","doi":"10.1073/pnas.95.3.1319","volume":95,"publication":"PNAS","issue":"3","quality_controlled":"1","month":"02","publication_identifier":{"issn":["0027-8424"]},"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","publication_status":"published","pmid":1,"date_updated":"2022-09-01T13:47:05Z","language":[{"iso":"eng"}],"author":[{"id":"338D39FE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0977-7989","first_name":"Leonid A","full_name":"Sazanov, Leonid A","last_name":"Sazanov"},{"last_name":"Burrows","full_name":"Burrows, Paul","first_name":"Paul"},{"first_name":"Peter","full_name":"Nixon, Peter","last_name":"Nixon"}],"oa":1,"external_id":{"pmid":["9448329 "]},"page":"1319 - 1324","fulldoi":"https://doi.org/10.1073/pnas.95.3.1319","citation":{"short":"L.A. Sazanov, P. Burrows, P. Nixon, PNAS 95 (1998) 1319–1324.","chicago":"Sazanov, Leonid A, Paul Burrows, and Peter Nixon. “The Plastid Ndh Genes Code for an NADH-Specific Dehydrogenase: Isolation of a Complex I Analogue from Pea Thylakoid Membranes.” <i>PNAS</i>. National Academy of Sciences, 1998. <a href=\"https://doi.org/10.1073/pnas.95.3.1319\">https://doi.org/10.1073/pnas.95.3.1319</a>.","mla":"Sazanov, Leonid A., et al. “The Plastid Ndh Genes Code for an NADH-Specific Dehydrogenase: Isolation of a Complex I Analogue from Pea Thylakoid Membranes.” <i>PNAS</i>, vol. 95, no. 3, National Academy of Sciences, 1998, pp. 1319–24, doi:<a href=\"https://doi.org/10.1073/pnas.95.3.1319\">10.1073/pnas.95.3.1319</a>.","ista":"Sazanov LA, Burrows P, Nixon P. 1998. The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes. PNAS. 95(3), 1319–1324.","ieee":"L. A. Sazanov, P. Burrows, and P. Nixon, “The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes,” <i>PNAS</i>, vol. 95, no. 3. National Academy of Sciences, pp. 1319–1324, 1998.","apa":"Sazanov, L. A., Burrows, P., &#38; Nixon, P. (1998). The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.95.3.1319\">https://doi.org/10.1073/pnas.95.3.1319</a>","ama":"Sazanov LA, Burrows P, Nixon P. The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes. <i>PNAS</i>. 1998;95(3):1319-1324. doi:<a href=\"https://doi.org/10.1073/pnas.95.3.1319\">10.1073/pnas.95.3.1319</a>"},"article_type":"original","intvolume":"        95","date_created":"2018-12-11T11:54:54Z","publisher":"National Academy of Sciences"},{"page":"219 - 236","citation":{"chicago":"Raskin, Jean, Pierre Schobbens, and Thomas A Henzinger. “Axioms for Real-Time Logics.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:219–36. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055625\">https://doi.org/10.1007/BFb0055625</a>.","short":"J. Raskin, P. Schobbens, T.A. Henzinger, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 219–236.","mla":"Raskin, Jean, et al. “Axioms for Real-Time Logics.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 219–36, doi:<a href=\"https://doi.org/10.1007/BFb0055625\">10.1007/BFb0055625</a>.","ista":"Raskin J, Schobbens P, Henzinger TA. 1998. Axioms for real-time logics. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 219–236.","ieee":"J. Raskin, P. Schobbens, and T. A. Henzinger, “Axioms for real-time logics,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 219–236.","apa":"Raskin, J., Schobbens, P., &#38; Henzinger, T. A. (1998). Axioms for real-time logics. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 219–236). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055625\">https://doi.org/10.1007/BFb0055625</a>","ama":"Raskin J, Schobbens P, Henzinger TA. Axioms for real-time logics. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:219-236. doi:<a href=\"https://doi.org/10.1007/BFb0055625\">10.1007/BFb0055625</a>"},"fulldoi":"https://doi.org/10.1007/BFb0055625","intvolume":"      1466","alternative_title":["LNCS"],"date_created":"2018-12-11T12:08:42Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2022-08-24T12:15:17Z","language":[{"iso":"eng"}],"author":[{"first_name":"Jean","full_name":"Raskin, Jean","last_name":"Raskin"},{"last_name":"Schobbens","full_name":"Schobbens, Pierre","first_name":"Pierre"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"publist_id":"323","abstract":[{"lang":"eng","text":"This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic (ECL) and the Metric Interval Temporal Logic with past (MITL). The completeness proof consists of an effective proof building procedure for ECL. From this result we obtain a complete axiomatization of MITL by providing axioms translating MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of these logics, such as the linear temporal logic of the real numbers (LTR)."}],"oa_version":"None","doi":"10.1007/BFb0055625","day":"01","volume":1466,"publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","month":"01","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"isbn":["9783540648963"]},"extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","type":"conference","status":"public","date_published":"1998-01-01T00:00:00Z","acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, by the SRC contract 97-DC-324.041, the Belgian National Fund for Scientific Research (FNRS), the European Commission under WGs Aspire and Fireworks, the Portuguese FCT, and by Belgacom.","conference":{"name":"CONCUR: Concurrency Theory","location":"Nice, France","end_date":"1998-09-11","start_date":"1998-09-08"},"_id":"4408","year":"1998","title":"Axioms for real-time logics","scopus_import":"1"},{"scopus_import":"1","title":"An algorithm for the approximative analysis of rectangular automata","_id":"4410","year":"1998","date_published":"1998-01-01T00:00:00Z","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","conference":{"start_date":"1998-09-14","end_date":"1998-09-18","location":"Lyngby, Denmark","name":"FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems"},"type":"conference","status":"public","publication_status":"published","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","publication_identifier":{"isbn":["9783540650034"]},"month":"01","quality_controlled":"1","volume":1486,"publication":"Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","day":"01","doi":"10.1007/BFb0055350","oa_version":"None","abstract":[{"text":"Rectangular automata are well suited for approximate modeling of continuous-discrete systems. The exact analysis of these automata is feasible for small examples but can encounter severe numerical problems for even medium-sized systems. This paper presents an analysis algorithm that uses conservative overapproximation to avoid these numerical problems. The algorithm is demonstrated on a simple benchmark system consisting of two connected tanks.\r\nSupported by the German Research Council (DFG) under grant Ko1430/3 in the special program KONDISK (‘Continuous-discrete dynamics of technical systems’).","lang":"eng"}],"publist_id":"320","author":[{"last_name":"Preußig","full_name":"Preußig, Jörg","first_name":"Jörg"},{"last_name":"Kowalewski","first_name":"Stefan","full_name":"Kowalewski, Stefan"},{"first_name":"Howard","full_name":"Wong Toi, Howard","last_name":"Wong Toi"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"date_updated":"2022-08-24T12:01:57Z","publisher":"Springer","date_created":"2018-12-11T12:08:43Z","alternative_title":["LNCS"],"intvolume":"      1486","citation":{"ama":"Preußig J, Kowalewski S, Wong Toi H, Henzinger TA. An algorithm for the approximative analysis of rectangular automata. In: <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>. Vol 1486. Springer; 1998:228-240. doi:<a href=\"https://doi.org/10.1007/BFb0055350\">10.1007/BFb0055350</a>","apa":"Preußig, J., Kowalewski, S., Wong Toi, H., &#38; Henzinger, T. A. (1998). An algorithm for the approximative analysis of rectangular automata. In <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i> (Vol. 1486, pp. 228–240). Lyngby, Denmark: Springer. <a href=\"https://doi.org/10.1007/BFb0055350\">https://doi.org/10.1007/BFb0055350</a>","ieee":"J. Preußig, S. Kowalewski, H. Wong Toi, and T. A. Henzinger, “An algorithm for the approximative analysis of rectangular automata,” in <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, Lyngby, Denmark, 1998, vol. 1486, pp. 228–240.","ista":"Preußig J, Kowalewski S, Wong Toi H, Henzinger TA. 1998. An algorithm for the approximative analysis of rectangular automata. Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, vol. 1486, 228–240.","mla":"Preußig, Jörg, et al. “An Algorithm for the Approximative Analysis of Rectangular Automata.” <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, vol. 1486, Springer, 1998, pp. 228–40, doi:<a href=\"https://doi.org/10.1007/BFb0055350\">10.1007/BFb0055350</a>.","short":"J. Preußig, S. Kowalewski, H. Wong Toi, T.A. Henzinger, in:, Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, 1998, pp. 228–240.","chicago":"Preußig, Jörg, Stefan Kowalewski, Howard Wong Toi, and Thomas A Henzinger. “An Algorithm for the Approximative Analysis of Rectangular Automata.” In <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, 1486:228–40. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0055350\">https://doi.org/10.1007/BFb0055350</a>."},"fulldoi":"https://doi.org/10.1007/BFb0055350","page":"228 - 240"},{"author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Rusu","first_name":"Vlad","full_name":"Rusu, Vlad"}],"language":[{"iso":"eng"}],"date_updated":"2022-08-24T11:29:14Z","alternative_title":["LNCS"],"date_created":"2018-12-11T12:08:48Z","publisher":"Springer","page":"190 - 204","citation":{"ieee":"T. A. Henzinger and V. Rusu, “Reachability verification for hybrid automata,” in <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>, Berkely, CA, United States of America, 1998, vol. 1386, pp. 190–204.","ista":"Henzinger TA, Rusu V. 1998. Reachability verification for hybrid automata. Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 1386, 190–204.","apa":"Henzinger, T. A., &#38; Rusu, V. (1998). Reachability verification for hybrid automata. In <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i> (Vol. 1386, pp. 190–204). Berkely, CA, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-64358-3_40\">https://doi.org/10.1007/3-540-64358-3_40</a>","ama":"Henzinger TA, Rusu V. Reachability verification for hybrid automata. In: <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>. Vol 1386. Springer; 1998:190-204. doi:<a href=\"https://doi.org/10.1007/3-540-64358-3_40\">10.1007/3-540-64358-3_40</a>","chicago":"Henzinger, Thomas A, and Vlad Rusu. “Reachability Verification for Hybrid Automata.” In <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>, 1386:190–204. Springer, 1998. <a href=\"https://doi.org/10.1007/3-540-64358-3_40\">https://doi.org/10.1007/3-540-64358-3_40</a>.","short":"T.A. Henzinger, V. Rusu, in:, Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control, Springer, 1998, pp. 190–204.","mla":"Henzinger, Thomas A., and Vlad Rusu. “Reachability Verification for Hybrid Automata.” <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>, vol. 1386, Springer, 1998, pp. 190–204, doi:<a href=\"https://doi.org/10.1007/3-540-64358-3_40\">10.1007/3-540-64358-3_40</a>."},"fulldoi":"https://doi.org/10.1007/3-540-64358-3_40","intvolume":"      1386","title":"Reachability verification for hybrid automata","scopus_import":"1","type":"conference","status":"public","date_published":"1998-01-01T00:00:00Z","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.\r\nSupported by Lavoisier grant of the French Foreign Affairs Ministry and by SRI.","conference":{"start_date":"1998-04-13","end_date":"1998-04-15","name":"HSCC: Hybrid Systems - Computation and Control","location":"Berkely, CA, United States of America"},"_id":"4429","year":"1998","month":"01","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"isbn":["9783540643586"]},"extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","publist_id":"299","abstract":[{"lang":"eng","text":"We study the reachability problem for hybrid automata. Automatic approaches, which attempt to construct the reachable region by symbolic execution, often do not terminate. In these cases, we require the user to guess the reachable region, and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata according to the theory in which their reachable region can be defined finitely. This is the theory in which the prover needs to operate in order to verify the guess. The approach is interesting, because an appropriate guess can often be deduced by extrapolating from the first few steps of symbolic execution."}],"oa_version":"None","doi":"10.1007/3-540-64358-3_40","day":"01","volume":1386,"publication":"Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control"},{"editor":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"title":"HSCC: Hybrid Systems—Computation and Control","_id":"4430","year":"1998","language":[{"iso":"eng"}],"date_updated":"2022-08-24T11:36:03Z","date_published":"1998-01-01T00:00:00Z","conference":{"location":"Berkeley, CA, United States of America","name":"HSCC: Hybrid Systems: Computation and Control","end_date":"1998-04-15","start_date":"1998-04-13"},"type":"conference_editor","status":"public","publisher":"Springer","publication_status":"published","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_created":"2018-12-11T12:08:49Z","alternative_title":["LNCS"],"article_processing_charge":"No","publication_identifier":{"isbn":["978-3-540-64358-6"]},"month":"01","intvolume":"      1386","volume":1386,"day":"01","doi":"10.1007/3-540-64358-3","citation":{"ieee":"T. A. Henzinger, Ed., <i>HSCC: Hybrid Systems—Computation and Control</i>, vol. 1386. Springer, 1998.","ista":"Henzinger TA ed. 1998. HSCC: Hybrid Systems—Computation and Control, Springer,p.","ama":"Henzinger TA, ed. <i>HSCC: Hybrid Systems—Computation and Control</i>. Vol 1386. Springer; 1998. doi:<a href=\"https://doi.org/10.1007/3-540-64358-3\">10.1007/3-540-64358-3</a>","apa":"Henzinger, T. A. (Ed.). (1998). <i>HSCC: Hybrid Systems—Computation and Control</i> (Vol. 1386). Presented at the HSCC: Hybrid Systems: Computation and Control, Berkeley, CA, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-64358-3\">https://doi.org/10.1007/3-540-64358-3</a>","chicago":"Henzinger, Thomas A, ed. <i>HSCC: Hybrid Systems—Computation and Control</i>. Vol. 1386. Springer, 1998. <a href=\"https://doi.org/10.1007/3-540-64358-3\">https://doi.org/10.1007/3-540-64358-3</a>.","short":"T.A. Henzinger, ed., HSCC: Hybrid Systems—Computation and Control, Springer, 1998.","mla":"Henzinger, Thomas A., editor. <i>HSCC: Hybrid Systems—Computation and Control</i>. Vol. 1386, Springer, 1998, doi:<a href=\"https://doi.org/10.1007/3-540-64358-3\">10.1007/3-540-64358-3</a>."},"fulldoi":"https://doi.org/10.1007/3-540-64358-3","oa_version":"None","publist_id":"300"},{"intvolume":"      1522","page":"421 - 432","citation":{"chicago":"Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “An Assume-Guarantee Rule for Checking Simulation.” In <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>, 1522:421–32. Springer, 1998. <a href=\"https://doi.org/10.1007/3-540-49519-3_27\">https://doi.org/10.1007/3-540-49519-3_27</a>.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, in:, Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design, Springer, 1998, pp. 421–432.","mla":"Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.” <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>, vol. 1522, Springer, 1998, pp. 421–32, doi:<a href=\"https://doi.org/10.1007/3-540-49519-3_27\">10.1007/3-540-49519-3_27</a>.","ieee":"T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee rule for checking simulation,” in <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>, Palo Alto, CA, United States of America, 1998, vol. 1522, pp. 421–432.","ista":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 1998. An assume-guarantee rule for checking simulation. Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, LNCS, vol. 1522, 421–432.","apa":"Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (1998). An assume-guarantee rule for checking simulation. In <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i> (Vol. 1522, pp. 421–432). Palo Alto, CA, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-49519-3_27\">https://doi.org/10.1007/3-540-49519-3_27</a>","ama":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for checking simulation. In: <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>. Vol 1522. Springer; 1998:421-432. doi:<a href=\"https://doi.org/10.1007/3-540-49519-3_27\">10.1007/3-540-49519-3_27</a>"},"fulldoi":"https://doi.org/10.1007/3-540-49519-3_27","date_created":"2018-12-11T12:09:06Z","publisher":"Springer","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"date_updated":"2022-08-24T10:00:50Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"},{"full_name":"Tasiran, Serdar","first_name":"Serdar","last_name":"Tasiran"}],"day":"01","doi":"10.1007/3-540-49519-3_27","volume":1522,"publication":"Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design","publist_id":"242","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&lt; s Q into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P&lt; s Q. We also extend our assume-guarantee rule to account for fairness assumptions on transition systems","lang":"eng"}],"oa_version":"None","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","month":"01","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"isbn":["9783540651918"]},"_id":"4486","year":"1998","type":"conference","status":"public","date_published":"1998-01-01T00:00:00Z","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.","conference":{"start_date":"1998-11-04","name":"FMCAD: Formal Methods in Computer-Aided Design","location":"Palo Alto, CA, United States of America","end_date":"1998-11-06"},"title":"An assume-guarantee rule for checking simulation","scopus_import":"1"},{"publisher":"Springer","date_created":"2018-12-11T12:09:06Z","alternative_title":["LNCS"],"intvolume":"      1427","citation":{"mla":"Henzinger, Thomas A., et al. “You Assume, We Guarantee: Methodology and Case Studies.” <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, vol. 1427, Springer, 1998, pp. 440–51, doi:<a href=\"https://doi.org/10.1007/BFb0028765\">10.1007/BFb0028765</a>.","chicago":"Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “You Assume, We Guarantee: Methodology and Case Studies.” In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, 1427:440–51. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0028765\">https://doi.org/10.1007/BFb0028765</a>.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 440–451.","ama":"Henzinger TA, Qadeer S, Rajamani S. You assume, we guarantee: Methodology and case studies. In: <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>. Vol 1427. Springer; 1998:440-451. doi:<a href=\"https://doi.org/10.1007/BFb0028765\">10.1007/BFb0028765</a>","apa":"Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1998). You assume, we guarantee: Methodology and case studies. In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 440–451). Vancouver, Canada: Springer. <a href=\"https://doi.org/10.1007/BFb0028765\">https://doi.org/10.1007/BFb0028765</a>","ieee":"T. A. Henzinger, S. Qadeer, and S. Rajamani, “You assume, we guarantee: Methodology and case studies,” in <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 440–451.","ista":"Henzinger TA, Qadeer S, Rajamani S. 1998. You assume, we guarantee: Methodology and case studies. Proceedings of the 10th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 440–451."},"fulldoi":"https://doi.org/10.1007/BFb0028765","page":"440 - 451","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"},{"first_name":"Sriram","full_name":"Rajamani, Sriram","last_name":"Rajamani"}],"language":[{"iso":"eng"}],"date_updated":"2022-09-05T07:31:52Z","publication_status":"published","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","publication_identifier":{"isbn":["9783540646082"]},"month":"01","quality_controlled":"1","publication":"Proceedings of the 10th International Conference on Computer Aided Verification","volume":1427,"day":"01","doi":"10.1007/BFb0028765","oa_version":"None","abstract":[{"text":"Assume-guarantee reasoning has long been advertised as an important method for decomposing proof obligations in system verification. Refinement mappings (homomorphisms) have long been advertised as an important method for solving the language-inclusion problem in practice. When confronted with large verification problems, we therefore attempted to make use of both techniques. We soon found that rather than offering instant solutions, the success of assume-guarantee reasoning depends critically on the construction of suitable abstraction modules, and the success of refinement checking depends critically on the construction of suitable witness modules. Moreover, as abstractions need to be witnessed, and witnesses abstracted, the process must be iterated. We present here the main lessons we learned from our experiments, in limn of a systematic and structured discipline for the compositional verification of reactive modules. An infrastructure to support this discipline, and automate parts of the verification, has been implemented in the tool Mocha.","lang":"eng"}],"publist_id":"239","scopus_import":"1","title":"You assume, we guarantee: Methodology and case studies","_id":"4488","year":"1998","date_published":"1998-01-01T00:00:00Z","acknowledgement":"This work is supported in part by ONR YIP award N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","conference":{"location":"Vancouver, Canada","name":"CAV: Computer Aided Verification","end_date":"1998-07-02","start_date":"1998-06-28"},"type":"conference","status":"public"},{"author":[{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"}],"date_updated":"2022-08-24T09:19:53Z","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"publisher":"Springer","date_created":"2018-12-11T12:09:07Z","fulldoi":"https://doi.org/10.1007/BFb0028745","citation":{"apa":"Henzinger, T. A., Kupferman, O., &#38; Qadeer, S. (1998). From pre-historic to post-modern symbolic model checking. In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 195–206). Vancouver, Canada: Springer. <a href=\"https://doi.org/10.1007/BFb0028745\">https://doi.org/10.1007/BFb0028745</a>","ama":"Henzinger TA, Kupferman O, Qadeer S. From pre-historic to post-modern symbolic model checking. In: <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>. Vol 1427. Springer; 1998:195-206. doi:<a href=\"https://doi.org/10.1007/BFb0028745\">10.1007/BFb0028745</a>","ista":"Henzinger TA, Kupferman O, Qadeer S. 1998. From pre-historic to post-modern symbolic model checking. Proceedings of the 10th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 195–206.","ieee":"T. A. Henzinger, O. Kupferman, and S. Qadeer, “From pre-historic to post-modern symbolic model checking,” in <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 195–206.","mla":"Henzinger, Thomas A., et al. “From Pre-Historic to Post-Modern Symbolic Model Checking.” <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, vol. 1427, Springer, 1998, pp. 195–206, doi:<a href=\"https://doi.org/10.1007/BFb0028745\">10.1007/BFb0028745</a>.","short":"T.A. Henzinger, O. Kupferman, S. Qadeer, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 195–206.","chicago":"Henzinger, Thomas A, Orna Kupferman, and Shaz Qadeer. “From Pre-Historic to Post-Modern Symbolic Model Checking.” In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, 1427:195–206. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0028745\">https://doi.org/10.1007/BFb0028745</a>."},"page":"195 - 206","intvolume":"      1427","scopus_import":"1","title":"From pre-historic to post-modern symbolic model checking","conference":{"start_date":"1998-06-28","end_date":"1998-07-02","location":"Vancouver, Canada","name":"CAV: Computer Aided Verification"},"date_published":"1998-01-01T00:00:00Z","acknowledgement":"This work is supported in part by ONR YIP award N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","status":"public","type":"conference","year":"1998","_id":"4489","publication_identifier":{"isbn":["9783540646082"]},"article_processing_charge":"No","quality_controlled":"1","month":"01","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","oa_version":"None","publist_id":"240","abstract":[{"text":"Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating with expressions that represent state sets. Traditionally, symbolic model-checking tools arc based on backward state traversal; their basic operation is the function pre, which given a set of states, returns the set of all predecessor states. This is because specifiers usally employ formalisms with future-time modalities. which are naturally evaluated by iterating applications of pre. It has been recently shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only those parts of the state space are explored which are reachable from an initial state and relevant for satisfaction or violation of the specification; that is, errors can be detected as soon as possible.\r\nIn this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation; the post- calculus, on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.","lang":"eng"}],"volume":1427,"publication":"Proceedings of the 10th International Conference on Computer Aided Verification","day":"01","doi":"10.1007/BFb0028745"},{"year":"1998","_id":"4490","status":"public","type":"conference","conference":{"start_date":"1998-07-13","location":"Aalborg, Denmark","name":"ICALP: Automata, Languages and Programming","end_date":"1998-07-17"},"date_published":"1998-01-01T00:00:00Z","acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, the NSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the ARO MURI grant DAAH-04-96-1-0341, the SRC contract 97-DC-324.041, the Belgian National Fund for Scientific Research (FNRS), the European Commission under WGs Aspire and Fireworks, the Portuguese FCT, and by Belgacom.","title":"The regular real-time languages","scopus_import":"1","doi":"10.1007/BFb0055086","day":"01","publication":"Proceedings of the 25th International Colloqium on Automata, Languages and Programming","volume":1443,"abstract":[{"text":"A specification formalism for reactive systems defines a class of Ω-languages. We call a specification formalism fully decidable if it is constructively closed under boolean operations and has a decidable satisfiability (nonemptiness) problem. There are two important, robust classes of Ω-languages that are definable by fully decidable formalisms. The Ω -reqular languages are definable by finite automata, or equivalcntly, by the Sequential Calculus. The counter-free Ω-regular languages are definable by temporal logic, or equivalcntly, by the first-order fragment of the Sequential Calculus. The gap between both classes can be closed by finite counting (using automata connectives), or equivalently, by projection (existential second-order quantification over letters).\r\nA specification formalism for real-time systems defines a class of timed Ω-langnages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed Ω-languages are robust, and we explain their relationship.\r\nFirst, we show that temporal logic with event clocks defines the same class of timed Ω-languages as temporal logic with nonsingular time bounds, and we identify a first-order monadic theory that also defines this class. Second, we show that if the ability of finite counting is added to these formalisms, we obtain the class of timed Ω-languages that are definable by finite automata with event clocks, or equivalently, by a restricted second-order extension of the monadic theory. Third, we show that if projection is added, we obtain the class of timed Ω-languages that are definable by timed automata, or equivalently, by a richer second-order extension of the monadic theory. These results identify three robust classes of timed Ω-languages, of which the third, while popular, is not definable by a, fully decidable formalism. By contrast, the first two classes are definable by fully decidable formalisms from temporal logic, from automata theory, and from monadic logic. Since the gap between these two classes can be closed by finite counting, we dub them the timed Ω-regular languages and the timed counter-free Ω-rcgular languages, respectively.","lang":"eng"}],"publist_id":"241","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","publication_status":"published","quality_controlled":"1","month":"01","publication_identifier":{"isbn":["9783540647812"]},"article_processing_charge":"No","language":[{"iso":"eng"}],"date_updated":"2022-08-24T09:30:11Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"},{"last_name":"Schobbens","full_name":"Schobbens, Pierre","first_name":"Pierre"}],"intvolume":"      1443","page":"580 - 591","fulldoi":"https://doi.org/10.1007/BFb0055086","citation":{"mla":"Henzinger, Thomas A., et al. “The Regular Real-Time Languages.” <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, vol. 1443, Springer, 1998, pp. 580–91, doi:<a href=\"https://doi.org/10.1007/BFb0055086\">10.1007/BFb0055086</a>.","short":"T.A. Henzinger, J. Raskin, P. Schobbens, in:, Proceedings of the 25th International Colloqium on Automata, Languages and Programming, Springer, 1998, pp. 580–591.","chicago":"Henzinger, Thomas A, Jean Raskin, and Pierre Schobbens. “The Regular Real-Time Languages.” In <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, 1443:580–91. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0055086\">https://doi.org/10.1007/BFb0055086</a>.","apa":"Henzinger, T. A., Raskin, J., &#38; Schobbens, P. (1998). The regular real-time languages. In <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i> (Vol. 1443, pp. 580–591). Aalborg, Denmark: Springer. <a href=\"https://doi.org/10.1007/BFb0055086\">https://doi.org/10.1007/BFb0055086</a>","ama":"Henzinger TA, Raskin J, Schobbens P. The regular real-time languages. In: <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>. Vol 1443. Springer; 1998:580-591. doi:<a href=\"https://doi.org/10.1007/BFb0055086\">10.1007/BFb0055086</a>","ista":"Henzinger TA, Raskin J, Schobbens P. 1998. The regular real-time languages. Proceedings of the 25th International Colloqium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 1443, 580–591.","ieee":"T. A. Henzinger, J. Raskin, and P. Schobbens, “The regular real-time languages,” in <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, Aalborg, Denmark, 1998, vol. 1443, pp. 580–591."},"date_created":"2018-12-11T12:09:07Z","publisher":"Springer","alternative_title":["LNCS"]},{"abstract":[{"text":"We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology","lang":"eng"}],"publist_id":"238","oa_version":"None","doi":"10.1109/9.664156 ","day":"01","issue":"4","volume":43,"publication":"IEEE Transactions on Automatic Control","month":"01","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"issn":["0018-9162"]},"extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","type":"journal_article","status":"public","date_published":"1998-01-01T00:00:00Z","_id":"4491","year":"1998","title":"Algorithmic analysis of nonlinear hybrid systems","page":"540 - 554","citation":{"chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “Algorithmic Analysis of Nonlinear Hybrid Systems.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 1998. <a href=\"https://doi.org/10.1109/9.664156 \">https://doi.org/10.1109/9.664156 </a>.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, IEEE Transactions on Automatic Control 43 (1998) 540–554.","mla":"Henzinger, Thomas A., et al. “Algorithmic Analysis of Nonlinear Hybrid Systems.” <i>IEEE Transactions on Automatic Control</i>, vol. 43, no. 4, IEEE, 1998, pp. 540–54, doi:<a href=\"https://doi.org/10.1109/9.664156 \">10.1109/9.664156 </a>.","ista":"Henzinger TA, Ho P, Wong Toi H. 1998. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control. 43(4), 540–554.","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “Algorithmic analysis of nonlinear hybrid systems,” <i>IEEE Transactions on Automatic Control</i>, vol. 43, no. 4. IEEE, pp. 540–554, 1998.","ama":"Henzinger TA, Ho P, Wong Toi H. Algorithmic analysis of nonlinear hybrid systems. <i>IEEE Transactions on Automatic Control</i>. 1998;43(4):540-554. doi:<a href=\"https://doi.org/10.1109/9.664156 \">10.1109/9.664156 </a>","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1998). Algorithmic analysis of nonlinear hybrid systems. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/9.664156 \">https://doi.org/10.1109/9.664156 </a>"},"fulldoi":"https://doi.org/10.1109/9.664156 ","article_type":"original","intvolume":"        43","date_created":"2018-12-11T12:09:07Z","publisher":"IEEE","language":[{"iso":"eng"}],"date_updated":"2022-08-23T14:34:35Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Ho","full_name":"Ho, Pei","first_name":"Pei"},{"last_name":"Wong Toi","full_name":"Wong Toi, Howard","first_name":"Howard"}]},{"title":"What's decidable about hybrid automata?","status":"public","type":"journal_article","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator Award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation Grant CCR-9504469, by the Air Force Office of Scientific Research Contract F49620-93-1-0056, by the Army Research Office MURI Grant DAAH-04-96-1-0341, by the Army Research Office Contract DAAH-04-94-G-0026, by the Defense Advanced Research Projects Agency Grant NAG2-892, and by the California PATH program.","date_published":"1998-01-01T00:00:00Z","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0022000098915811","open_access":"1"}],"year":"1998","_id":"4492","quality_controlled":"1","month":"01","publication_identifier":{"isbn":["0022-0000"]},"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","publication_status":"published","publist_id":"237","abstract":[{"lang":"eng","text":"Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves theω-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch."}],"oa_version":"Published Version","doi":"10.1006/jcss.1998.1581","day":"01","volume":57,"publication":"Journal of Computer and System Sciences","issue":"1","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"full_name":"Kopke, Peter","first_name":"Peter","last_name":"Kopke"},{"last_name":"Puri","full_name":"Puri, Anuj","first_name":"Anuj"},{"first_name":"P.","full_name":"Varaiya, P.","last_name":"Varaiya"}],"oa":1,"date_updated":"2022-08-23T14:29:15Z","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:08Z","publisher":"Elsevier","page":"94 - 124","fulldoi":"https://doi.org/10.1006/jcss.1998.1581","citation":{"short":"T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, Journal of Computer and System Sciences 57 (1998) 94–124.","chicago":"Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” <i>Journal of Computer and System Sciences</i>. Elsevier, 1998. <a href=\"https://doi.org/10.1006/jcss.1998.1581\">https://doi.org/10.1006/jcss.1998.1581</a>.","mla":"Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” <i>Journal of Computer and System Sciences</i>, vol. 57, no. 1, Elsevier, 1998, pp. 94–124, doi:<a href=\"https://doi.org/10.1006/jcss.1998.1581\">10.1006/jcss.1998.1581</a>.","ista":"Henzinger TA, Kopke P, Puri A, Varaiya P. 1998. What’s decidable about hybrid automata? Journal of Computer and System Sciences. 57(1), 94–124.","ieee":"T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” <i>Journal of Computer and System Sciences</i>, vol. 57, no. 1. Elsevier, pp. 94–124, 1998.","apa":"Henzinger, T. A., Kopke, P., Puri, A., &#38; Varaiya, P. (1998). What’s decidable about hybrid automata? <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1006/jcss.1998.1581\">https://doi.org/10.1006/jcss.1998.1581</a>","ama":"Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? <i>Journal of Computer and System Sciences</i>. 1998;57(1):94-124. doi:<a href=\"https://doi.org/10.1006/jcss.1998.1581\">10.1006/jcss.1998.1581</a>"},"article_type":"original","intvolume":"        57"},{"citation":{"chicago":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:439–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>.","short":"T.A. Henzinger, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–454.","mla":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–54, doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>.","ista":"Henzinger TA. 1998. It’s about time: Real-time logics reviewed. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 439–454.","ieee":"T. A. Henzinger, “It’s about time: Real-time logics reviewed,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 439–454.","ama":"Henzinger TA. It’s about time: Real-time logics reviewed. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:439-454. doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>","apa":"Henzinger, T. A. (1998). It’s about time: Real-time logics reviewed. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 439–454). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>"},"fulldoi":"https://doi.org/10.1007/BFb0055640","page":"439 - 454","intvolume":"      1466","alternative_title":["LNCS"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2018-12-11T12:09:15Z","date_updated":"2022-08-23T14:24:08Z","language":[{"iso":"eng"}],"author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"None","abstract":[{"text":"We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.","lang":"eng"}],"publist_id":"214","volume":1466,"publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","day":"01","doi":"10.1007/BFb0055640","article_processing_charge":"No","publication_identifier":{"isbn":["978-3-540-64896-3"]},"month":"01","quality_controlled":"1","publication_status":"published","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.","date_published":"1998-01-01T00:00:00Z","conference":{"location":"Nice, France","name":"CONCUR: Concurrency Theory","end_date":"1998-09-11","start_date":"1998-09-08"},"type":"conference","status":"public","_id":"4515","year":"1998","scopus_import":"1","title":"It's about time: Real-time logics reviewed"},{"alternative_title":["LNCS"],"date_created":"2018-12-11T12:09:42Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","page":"163 - 178","citation":{"chicago":"Alur, Rajeev, Thomas A Henzinger, Orna Kupferman, and Moshe Vardi. “Alternating Refinement Relations.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:163–78. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055622\">https://doi.org/10.1007/BFb0055622</a>.","short":"R. Alur, T.A. Henzinger, O. Kupferman, M. Vardi, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–178.","mla":"Alur, Rajeev, et al. “Alternating Refinement Relations.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–78, doi:<a href=\"https://doi.org/10.1007/BFb0055622\">10.1007/BFb0055622</a>.","ista":"Alur R, Henzinger TA, Kupferman O, Vardi M. 1998. Alternating refinement relations. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 163–178.","ieee":"R. Alur, T. A. Henzinger, O. Kupferman, and M. Vardi, “Alternating refinement relations,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 163–178.","ama":"Alur R, Henzinger TA, Kupferman O, Vardi M. Alternating refinement relations. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:163-178. doi:<a href=\"https://doi.org/10.1007/BFb0055622\">10.1007/BFb0055622</a>","apa":"Alur, R., Henzinger, T. A., Kupferman, O., &#38; Vardi, M. (1998). Alternating refinement relations. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 163–178). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055622\">https://doi.org/10.1007/BFb0055622</a>"},"fulldoi":"https://doi.org/10.1007/BFb0055622","intvolume":"      1466","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"},{"full_name":"Vardi, Moshe","first_name":"Moshe","last_name":"Vardi"}],"date_updated":"2022-08-23T09:50:34Z","language":[{"iso":"eng"}],"month":"01","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"isbn":["978-3-540-64896-3"]},"extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","abstract":[{"lang":"eng","text":"Alternating transition systems are a general model for composite systems which allow the study of collaborative as well as adversarial relationships between individual system components. Unlike in labeled transition systems, where each transition corresponds to a possible step of the system (which may involve some or all components), in alternating transition systems, each transition corresponds to a possible move in a game between the components. In this paper, we study refinement relations between alternating transition systems, such as “Does the implementation refine the set A of specification components without constraining the components not in A?” In particular, we generalize the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems. The generalizations are called alternating simulation and alternating trace containment. Unlike existing refinement relations, they allow the refinement of individual components within the context of a composite system description. We show that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. While ordinary trace containment is PSPACE-complete, we establish alternating trace containment to be EXPTIME-complete. Finally, we present logical characterizations for the two preorders in terms of ATL, a temporal logic capable of referring to games between system components."}],"publist_id":"104","oa_version":"None","doi":"10.1007/BFb0055622","day":"01","publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","volume":1466,"title":"Alternating refinement relations","scopus_import":"1","type":"conference","status":"public","acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9504469, CCR-9628400, and CCR-9700061, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, by the SRC contract 97-DC-324.041, and by a grant from the Intel Corporation.","date_published":"1998-01-01T00:00:00Z","conference":{"start_date":"1998-09-08","location":"Nice, France","name":"CONCUR: Concurrency Theory","end_date":"1998-09-11"},"_id":"4603","year":"1998"},{"publist_id":"103","oa_version":"None","doi":"10.1007/BFb0028774","day":"01","volume":1427,"publication":"Proceedings of the 10th International Conference on Computer Aided Verification","quality_controlled":"1","month":"01","publication_identifier":{"isbn":["9783540646082"]},"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","publication_status":"published","status":"public","type":"conference","conference":{"start_date":"1998-06-28","end_date":"1998-07-02","location":"Vancouver, Canada","name":"CAV: Computer Aided Verification"},"date_published":"1998-01-01T00:00:00Z","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","year":"1998","_id":"4604","title":"Mocha: Modularity in model checking","scopus_import":"1","page":"521 - 525","fulldoi":"https://doi.org/10.1007/BFb0028774","citation":{"chicago":"Alur, Rajeev, Thomas A Henzinger, Freddy Mang, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “Mocha: Modularity in Model Checking.” In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, 1427:521–25. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0028774\">https://doi.org/10.1007/BFb0028774</a>.","short":"R. Alur, T.A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, S. Tasiran, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 521–525.","mla":"Alur, Rajeev, et al. “Mocha: Modularity in Model Checking.” <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, vol. 1427, Springer, 1998, pp. 521–25, doi:<a href=\"https://doi.org/10.1007/BFb0028774\">10.1007/BFb0028774</a>.","ista":"Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani S, Tasiran S. 1998. Mocha: Modularity in model checking. Proceedings of the 10th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 521–525.","ieee":"R. Alur, T. A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran, “Mocha: Modularity in model checking,” in <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 521–525.","apa":"Alur, R., Henzinger, T. A., Mang, F., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (1998). Mocha: Modularity in model checking. In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 521–525). Vancouver, Canada: Springer. <a href=\"https://doi.org/10.1007/BFb0028774\">https://doi.org/10.1007/BFb0028774</a>","ama":"Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani S, Tasiran S. Mocha: Modularity in model checking. In: <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>. Vol 1427. Springer; 1998:521-525. doi:<a href=\"https://doi.org/10.1007/BFb0028774\">10.1007/BFb0028774</a>"},"intvolume":"      1427","alternative_title":["LNCS"],"date_created":"2018-12-11T12:09:42Z","publisher":"Springer","date_updated":"2022-08-23T09:06:21Z","language":[{"iso":"eng"}],"author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Mang","first_name":"Freddy","full_name":"Mang, Freddy"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"},{"last_name":"Rajamani","full_name":"Rajamani, Sriram","first_name":"Sriram"},{"first_name":"Serdar","full_name":"Tasiran, Serdar","last_name":"Tasiran"}]},{"author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"}],"language":[{"iso":"eng"}],"date_updated":"2022-08-23T08:44:36Z","alternative_title":["LNCS"],"date_created":"2018-12-11T12:09:43Z","publisher":"Springer","page":"330 - 344","citation":{"mla":"Alur, Rajeev, et al. “Symbolic Exploration of Transition Hierarchies.” <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 1384, Springer, 1998, pp. 330–44, doi:<a href=\"https://doi.org/10.1007/BFb0054181\">10.1007/BFb0054181</a>.","chicago":"Alur, Rajeev, Thomas A Henzinger, and Sriram Rajamani. “Symbolic Exploration of Transition Hierarchies.” In <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 1384:330–44. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0054181\">https://doi.org/10.1007/BFb0054181</a>.","short":"R. Alur, T.A. Henzinger, S. Rajamani, in:, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 1998, pp. 330–344.","apa":"Alur, R., Henzinger, T. A., &#38; Rajamani, S. (1998). Symbolic exploration of transition hierarchies. In <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 1384, pp. 330–344). Lisbon, Portugal: Springer. <a href=\"https://doi.org/10.1007/BFb0054181\">https://doi.org/10.1007/BFb0054181</a>","ama":"Alur R, Henzinger TA, Rajamani S. Symbolic exploration of transition hierarchies. In: <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 1384. Springer; 1998:330-344. doi:<a href=\"https://doi.org/10.1007/BFb0054181\">10.1007/BFb0054181</a>","ieee":"R. Alur, T. A. Henzinger, and S. Rajamani, “Symbolic exploration of transition hierarchies,” in <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Lisbon, Portugal, 1998, vol. 1384, pp. 330–344.","ista":"Alur R, Henzinger TA, Rajamani S. 1998. Symbolic exploration of transition hierarchies. Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1384, 330–344."},"fulldoi":"https://doi.org/10.1007/BFb0054181","intvolume":"      1384","title":"Symbolic exploration of transition hierarchies","scopus_import":"1","type":"conference","status":"public","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Air Force Office of Scientific Research contract F49620-93-1-0056, by the Army Research Office MURI grant DAAH-04-96-1-0341, by the Advanced Research Projects Agency grant NAG2-892, and by the Semiconductor Research Corporation contract 95-DC-324.036.\r\n","date_published":"1998-01-01T00:00:00Z","conference":{"location":"Lisbon, Portugal","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"1998-04-04","start_date":"1998-03-28"},"_id":"4606","year":"1998","month":"01","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"isbn":["9783540643562"]},"extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","abstract":[{"text":"In formal design verification, successful model checking is typically preceded by a laborious manual process of constructing design abstractions. We present a methodology for partially—and in some cases, fully—bypassing the abstraction process. For this purpose, we provide to the designer abstraction operators which, if used judiciously in the description of a design, structure the corresponding state space hierarchically. This structure can then be exploited by verification tools, and makes possible the automatic and exhaustive exploration of state spaces that would otherwise be out of scope for existing model checkers.\r\nSpecifically, we present the following contributions:\r\n- \t A temporal abstraction operator that aggregates transitions and hides intermediate steps. Mathematically, our abstraction operator is a function that maps a flat transition system into a two-level hierarchy where each atomic upper-level transition expands into an entire lower-level transition system. For example, an arithmetic operation may expand into a sequence of bit operations.\r\n- \t A BDD-based algorithm for the symbolic exploration of multi-level hierarchies of transition systems. The algorithm traverses a level-n transition by expanding the corresponding level-(n − 1) transition system on-the-fly. The level-n successors of a state are determined by computing a level-(n − 1) reach set, which is then immediately released from memory. In this fashion, we can exhaustively explore hierarchically structured state spaces whose flat counterparts cause memory overflows.\r\n- \t We experimentally demonstrate the efficiency of our method with three examples—a multiplier, a cache coherence protocol, and a multiprocessor system. In the first two examples, we obtain significant improvements in run times and peak BDD sizes over traditional state-space search. The third example cannot be model checked at all using conventional methods (without manual abstractions), but can be analyzed fully automatically using transition hierarchies.","lang":"eng"}],"publist_id":"102","oa_version":"None","day":"01","doi":"10.1007/BFb0054181","volume":1384,"publication":"Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"month":"01","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"isbn":["0818691727"]},"extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_created":"2018-12-11T12:09:53Z","publication_status":"published","publisher":"IEEE","abstract":[{"text":"An open system can be modeled as a two-player game between the system and its environment. At each round of the game, player 1 (the system) and player 2 (the environment) independently and simultaneously choose moves, and the two choices determine the next state of the game. Properties of open systems can be modeled as objectives of these two-player games. For the basic objective of reachability-can player 1 force the game to a given set of target states?-there are three types of winning states, according to the degree of certainty with which player 1 can reach the target. From type-1 states, player 1 has a deterministic strategy to always reach the target. From type-2 states, player 1 has a randomized strategy to reach the target with probability 1. From type-3 states, player 1 has for every real ε&gt;0 a randomized strategy to reach the target with probability greater than 1-ε. We show that for finite state spaces, all three sets of winning states can be computed in polynomial time: type-1 states in linear time, and type-2 and type-3 states in quadratic time. The algorithms to compute the three sets of winning states also enable the construction of the winning and spoiling strategies. Finally, we apply our results by introducing a temporal logic in which all three kinds of winning conditions can be specified, and which can be model checked in polynomial time. This logic, called Randomized ATL, is suitable for reasoning about randomized behavior in open (two-agent) as well as multi-agent systems","lang":"eng"}],"publist_id":"68","page":"564 - 575","citation":{"mla":"De Alfaro, Luca, et al. “Concurrent Reachability Games.” <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, IEEE, 1998, pp. 564–75, doi:<a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">10.1109/SFCS.1998.743507  </a>.","short":"L. De Alfaro, T.A. Henzinger, O. Kupferman, in:,  Proceedings 39th Annual Symposium on Foundations of Computer Science, IEEE, 1998, pp. 564–575.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Orna Kupferman. “Concurrent Reachability Games.” In <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, 564–75. IEEE, 1998. <a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">https://doi.org/10.1109/SFCS.1998.743507  </a>.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Kupferman, O. (1998). Concurrent reachability games. In <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i> (pp. 564–575). Palo Alto, CA, United States of America: IEEE. <a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">https://doi.org/10.1109/SFCS.1998.743507  </a>","ama":"De Alfaro L, Henzinger TA, Kupferman O. Concurrent reachability games. In: <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>. IEEE; 1998:564-575. doi:<a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">10.1109/SFCS.1998.743507  </a>","ieee":"L. De Alfaro, T. A. Henzinger, and O. Kupferman, “Concurrent reachability games,” in <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, Palo Alto, CA, United States of America, 1998, pp. 564–575.","ista":"De Alfaro L, Henzinger TA, Kupferman O. 1998. Concurrent reachability games.  Proceedings 39th Annual Symposium on Foundations of Computer Science. FOCS: Foundations of Computer Science, 564–575."},"fulldoi":"https://doi.org/10.1109/SFCS.1998.743507  ","oa_version":"None","day":"01","doi":"10.1109/SFCS.1998.743507  ","publication":" Proceedings 39th Annual Symposium on Foundations of Computer Science","title":"Concurrent reachability games","author":[{"last_name":"De Alfaro","full_name":"De Alfaro, Luca","first_name":"Luca"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"type":"conference","status":"public","date_published":"1998-01-01T00:00:00Z","conference":{"start_date":"1998-11-08","end_date":"1998-11-11","name":"FOCS: Foundations of Computer Science","location":"Palo Alto, CA, United States of America"},"language":[{"iso":"eng"}],"date_updated":"2022-08-22T14:09:02Z","_id":"4639","year":"1998"},{"year":"1998","_id":"6160","language":[{"iso":"eng"}],"date_updated":"2021-01-12T08:06:28Z","date_published":"1998-09-04T00:00:00Z","status":"public","type":"journal_article","author":[{"last_name":"de Bono","id":"4E3FF80E-F248-11E8-B48F-1D18A9856A87","first_name":"Mario","full_name":"de Bono, Mario","orcid":"0000-0001-8347-0443"},{"last_name":"Bargmann","first_name":"Cornelia I","full_name":"Bargmann, Cornelia I"}],"title":"Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans","volume":94,"publication":"Cell","intvolume":"        94","issue":"5","day":"04","doi":"10.1016/s0092-8674(00)81609-8","fulldoi":"https://doi.org/10.1016/s0092-8674(00)81609-8","oa_version":"None","citation":{"ista":"de Bono M, Bargmann CI. 1998. Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans. Cell. 94(5), 679–689.","ieee":"M. de Bono and C. I. Bargmann, “Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans,” <i>Cell</i>, vol. 94, no. 5. Elsevier, pp. 679–689, 1998.","ama":"de Bono M, Bargmann CI. Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans. <i>Cell</i>. 1998;94(5):679-689. doi:<a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">10.1016/s0092-8674(00)81609-8</a>","apa":"de Bono, M., &#38; Bargmann, C. I. (1998). Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans. <i>Cell</i>. Elsevier. <a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">https://doi.org/10.1016/s0092-8674(00)81609-8</a>","chicago":"Bono, Mario de, and Cornelia I Bargmann. “Natural Variation in a Neuropeptide Y Receptor Homolog Modifies Social Behavior and Food Response in C. Elegans.” <i>Cell</i>. Elsevier, 1998. <a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">https://doi.org/10.1016/s0092-8674(00)81609-8</a>.","short":"M. de Bono, C.I. Bargmann, Cell 94 (1998) 679–689.","mla":"de Bono, Mario, and Cornelia I. Bargmann. “Natural Variation in a Neuropeptide Y Receptor Homolog Modifies Social Behavior and Food Response in C. Elegans.” <i>Cell</i>, vol. 94, no. 5, Elsevier, 1998, pp. 679–89, doi:<a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">10.1016/s0092-8674(00)81609-8</a>."},"page":"679-689","external_id":{"pmid":["9741632"]},"abstract":[{"text":"Natural isolates of C. elegans exhibit either solitary or social feeding behavior. Solitary foragers move slowly on a bacterial lawn and disperse across it, while social foragers move rapidly on bacteria and aggregate together. A loss-of-function mutation in the npr-1 gene, which encodes a predicted G protein–coupled receptor similar to neuropeptide Y receptors, causes a solitary strain to take on social behavior. Two isoforms of NPR-1 that differ at a single residue occur in the wild. One isoform, NPR-1 215F, is found exclusively in social strains, while the other isoform, NPR-1 215V, is found exclusively in solitary strains. An NPR-1 215V transgene can induce solitary feeding behavior in a wild social strain. Thus, isoforms of a putative neuropeptide receptor generate natural variation in C. elegans feeding behavior.","lang":"eng"}],"publication_status":"published","publisher":"Elsevier","pmid":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_created":"2019-03-21T10:32:06Z","extern":"1","publication_identifier":{"issn":["0092-8674"]},"quality_controlled":"1","month":"09"},{"author":[{"first_name":"Peter M","full_name":"Jonas, Peter M","orcid":"0000-0001-5001-4804","id":"353C1B58-F248-11E8-B48F-1D18A9856A87","last_name":"Jonas"},{"last_name":"Bischofberger","full_name":"Bischofberger, Joseph","first_name":"Joseph"},{"last_name":"Sandkühler","first_name":"Jürgen","full_name":"Sandkühler, Jürgen"}],"date_updated":"2022-08-29T14:52:38Z","language":[{"iso":"eng"}],"publisher":"American Association for the Advancement of Science","date_created":"2018-12-11T12:03:35Z","fulldoi":"https://doi.org/10.1126/science.281.5375.419","citation":{"ama":"Jonas PM, Bischofberger J, Sandkühler J. Corelease of two fast neurotransmitters at a central synapse. <i>Science</i>. 1998;281(5375):419-424. doi:<a href=\"https://doi.org/10.1126/science.281.5375.419\">10.1126/science.281.5375.419</a>","apa":"Jonas, P. M., Bischofberger, J., &#38; Sandkühler, J. (1998). Corelease of two fast neurotransmitters at a central synapse. <i>Science</i>. American Association for the Advancement of Science. <a href=\"https://doi.org/10.1126/science.281.5375.419\">https://doi.org/10.1126/science.281.5375.419</a>","ista":"Jonas PM, Bischofberger J, Sandkühler J. 1998. Corelease of two fast neurotransmitters at a central synapse. Science. 281(5375), 419–424.","ieee":"P. M. Jonas, J. Bischofberger, and J. Sandkühler, “Corelease of two fast neurotransmitters at a central synapse,” <i>Science</i>, vol. 281, no. 5375. American Association for the Advancement of Science, pp. 419–424, 1998.","mla":"Jonas, Peter M., et al. “Corelease of Two Fast Neurotransmitters at a Central Synapse.” <i>Science</i>, vol. 281, no. 5375, American Association for the Advancement of Science, 1998, pp. 419–24, doi:<a href=\"https://doi.org/10.1126/science.281.5375.419\">10.1126/science.281.5375.419</a>.","short":"P.M. Jonas, J. Bischofberger, J. Sandkühler, Science 281 (1998) 419–424.","chicago":"Jonas, Peter M, Joseph Bischofberger, and Jürgen Sandkühler. “Corelease of Two Fast Neurotransmitters at a Central Synapse.” <i>Science</i>. American Association for the Advancement of Science, 1998. <a href=\"https://doi.org/10.1126/science.281.5375.419\">https://doi.org/10.1126/science.281.5375.419</a>."},"external_id":{"pmid":["9665886 "]},"page":"419 - 424","intvolume":"       281","article_type":"original","scopus_import":"1","title":"Corelease of two fast neurotransmitters at a central synapse","acknowledgement":"See comment by Nicoll RA, Malenka RC (1998) Science 281:360-361\r\n","date_published":"1998-07-17T00:00:00Z","status":"public","type":"journal_article","year":"1998","_id":"3487","publication_identifier":{"issn":["0036-8075"]},"article_processing_charge":"No","quality_controlled":"1","month":"07","publication_status":"published","pmid":1,"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","oa_version":"None","abstract":[{"text":"It is widely accepted that individual neurons in the central nervous system release only a single fast transmitter. The possibility of corelease of fast neurotransmitters was examined by making paired recordings from synaptically connected neurons in spinal cord slices. Unitary inhibitory postsynaptic currents generated at interneuron-motoneuron synapses consisted of a strychnine-sensitive, glycine receptor-mediated component and a bicuculline-sensitive, γ-aminobutyric acid (GABA)(A) receptor-mediated component. These results indicate that spinal interneurons release both glycine and GABA to activate functionally distinct receptors in their postsynaptic target cells. A subset of miniature synaptic currents also showed both components, consistent with corelease from individual synaptic vesicles.","lang":"eng"}],"publist_id":"2900","volume":281,"publication":"Science","issue":"5375","doi":"10.1126/science.281.5375.419","day":"17"},{"acknowledgement":"Supported by German Israeli Foundation Grant I 0352–073.01/94 to P.J. and Deutsche Forschungsgemeinschaft Grant Mo 432/3–1 to H.M. We thank Drs. L. Y. Jan, D. McKinnon, O. Pongs, L. Salkoff, S. H. Snyder, and J. S. Trimmer for providing plasmids, Dr. D. J. Surmeier for sharing unpublished data, and Drs. J. Bischofberger and J. R. P. Geiger for critically reading this manuscript. M.M. and J.H.S. contributed equally to this work.","date_published":"1998-10-15T00:00:00Z","type":"journal_article","status":"public","_id":"3488","year":"1998","main_file_link":[{"url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6792860/","open_access":"1"}],"scopus_import":"1","title":"Functional and molecular differences between voltage-gated K+ channels of fast-spiking interneurons and pyramidal neurons of rat hippocampus","oa_version":"None","publist_id":"2899","abstract":[{"text":"We have examined gating and pharmacological characteristics of somatic K+ channels in fast-spiking interneurons and regularly spiking principal neurons of hippocampal slices. In nucleated patches isolated from basket cells of the dentate gyrus, a fast delayed rectifier K+ current component that was highly sensitive to tetraethylammonium (TEA) and 4-aminopyridine (4- AP) (half-maximal inhibitory concentrations &lt;0.1 mM) predominated, contributing an average of 58% to the total K+ current in these cells. By contrast, in pyramidal neurons of the CA1 region a rapidly inactivating A- type K+ current component that was TEA-resistant prevailed, contributing 61% to the total K+ current. Both types of neurons also showed small amounts of the K+ current component mainly found in the other type of neuron and, in addition, a slow delayed rectifier K+ current component with intermediate properties (sow inactivation, intermediate sensitivity to TEA). Single-cell RT-PCR analysis of mRNA revealed that Kv3 (Kv3.1, Kv3.2) subunit transcripts were expressed in almost all (89%) of the interneurons but only in 17% of the pyramidal neurons. In contrast, Kv4 (Kv4.2, Kv4.3) subunit mRNAs were present in 87% of pyramidal neurons but only in 55% of interneurons. Selective block of fast delayed rectifier K+ channels, presumably assembled from Kv3 subunits, by 4-AP reduced substantially the action potential frequency in interneurons. These results indicate that the differential expression of Kv3 and Kv4 subunits shapes the action potential phenotypes of principal neurons and interneurons in the cortex.","lang":"eng"}],"issue":"20","publication":"Journal of Neuroscience","volume":18,"day":"15","doi":"10.1523/JNEUROSCI.18-20-08111.1998","article_processing_charge":"No","publication_identifier":{"issn":["0270-6474"]},"month":"10","quality_controlled":"1","pmid":1,"publication_status":"published","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","language":[{"iso":"eng"}],"date_updated":"2022-08-29T14:20:39Z","author":[{"full_name":"Martina, Marco","first_name":"Marco","last_name":"Martina"},{"last_name":"Schultz","first_name":"Jobst","full_name":"Schultz, Jobst"},{"first_name":"Heimo","full_name":"Ehmke, Heimo","last_name":"Ehmke"},{"full_name":"Monyer, Hannah","first_name":"Hannah","last_name":"Monyer"},{"id":"353C1B58-F248-11E8-B48F-1D18A9856A87","full_name":"Jonas, Peter M","first_name":"Peter M","orcid":"0000-0001-5001-4804","last_name":"Jonas"}],"oa":1,"citation":{"ieee":"M. Martina, J. Schultz, H. Ehmke, H. Monyer, and P. M. Jonas, “Functional and molecular differences between voltage-gated K+ channels of fast-spiking interneurons and pyramidal neurons of rat hippocampus,” <i>Journal of Neuroscience</i>, vol. 18, no. 20. Society for Neuroscience, pp. 8111–8125, 1998.","ista":"Martina M, Schultz J, Ehmke H, Monyer H, Jonas PM. 1998. Functional and molecular differences between voltage-gated K+ channels of fast-spiking interneurons and pyramidal neurons of rat hippocampus. Journal of Neuroscience. 18(20), 8111–8125.","ama":"Martina M, Schultz J, Ehmke H, Monyer H, Jonas PM. Functional and molecular differences between voltage-gated K+ channels of fast-spiking interneurons and pyramidal neurons of rat hippocampus. <i>Journal of Neuroscience</i>. 1998;18(20):8111-8125. doi:<a href=\"https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998\">10.1523/JNEUROSCI.18-20-08111.1998</a>","apa":"Martina, M., Schultz, J., Ehmke, H., Monyer, H., &#38; Jonas, P. M. (1998). Functional and molecular differences between voltage-gated K+ channels of fast-spiking interneurons and pyramidal neurons of rat hippocampus. <i>Journal of Neuroscience</i>. Society for Neuroscience. <a href=\"https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998\">https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998</a>","chicago":"Martina, Marco, Jobst Schultz, Heimo Ehmke, Hannah Monyer, and Peter M Jonas. “Functional and Molecular Differences between Voltage-Gated K+ Channels of Fast-Spiking Interneurons and Pyramidal Neurons of Rat Hippocampus.” <i>Journal of Neuroscience</i>. Society for Neuroscience, 1998. <a href=\"https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998\">https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998</a>.","short":"M. Martina, J. Schultz, H. Ehmke, H. Monyer, P.M. Jonas, Journal of Neuroscience 18 (1998) 8111–8125.","mla":"Martina, Marco, et al. “Functional and Molecular Differences between Voltage-Gated K+ Channels of Fast-Spiking Interneurons and Pyramidal Neurons of Rat Hippocampus.” <i>Journal of Neuroscience</i>, vol. 18, no. 20, Society for Neuroscience, 1998, pp. 8111–25, doi:<a href=\"https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998\">10.1523/JNEUROSCI.18-20-08111.1998</a>."},"fulldoi":"https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998","external_id":{"pmid":["9763458"]},"page":"8111 - 8125","intvolume":"        18","article_type":"original","publisher":"Society for Neuroscience","date_created":"2018-12-11T12:03:35Z"},{"oa":1,"ipn":"US5850229A","title":"Apparatus and method for geometric morphing","author":[{"last_name":"Edelsbrunner","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","first_name":"Herbert","full_name":"Edelsbrunner, Herbert","orcid":"0000-0002-9823-6833"},{"first_name":"Ping","full_name":"Fu, Ping","last_name":"Fu"}],"_id":"3506","applicant":["Raindrop Geomagic, Inc."],"year":"1998","date_updated":"2022-01-05T15:16:35Z","main_file_link":[{"open_access":"1","url":"https://patents.google.com/patent/US5850229A"}],"date_published":"1998-12-15T00:00:00Z","type":"patent","status":"public","publication_date":"1998-12-15","extern":"1","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_created":"2018-12-11T12:03:41Z","article_processing_charge":"No","month":"12","ipc":"G06T13/20 ; G06T2210/44","day":"15","citation":{"ama":"Edelsbrunner H, Fu P. Apparatus and method for geometric morphing. 1998.","apa":"Edelsbrunner, H., &#38; Fu, P. (1998). Apparatus and method for geometric morphing.","ista":"Edelsbrunner H, Fu P. 1998. Apparatus and method for geometric morphing.","ieee":"H. Edelsbrunner and P. Fu, “Apparatus and method for geometric morphing.” 1998.","mla":"Edelsbrunner, Herbert, and Ping Fu. <i>Apparatus and Method for Geometric Morphing</i>. 1998.","chicago":"Edelsbrunner, Herbert, and Ping Fu. “Apparatus and Method for Geometric Morphing,” 1998.","short":"H. Edelsbrunner, P. Fu, (1998)."},"oa_version":"Published Version","abstract":[{"lang":"eng","text":"A method of geometric morphing between a first object having a first shape and a second object having a second shape. The method includes the steps of generating a first Delaunay complex corresponding to the first shape and a second Delaunay complex corresponding to the second shape and generating a plurality of intermediary Delaunay complexes defined by a continuous family of mixed shapes corresponding to a mixing of the first shape and the second shape. The method further includes the steps of constructing a first skin corresponding to the first Delaunay complex and a second skin corresponding to the second Delaunay complex and constructing a plurality of intermediary skins corresponding to the plurality of intermediary Delaunay complexes. The first skin, second skin and plurality of intermediary skins may be visually displayed on an output device."}],"publist_id":"2881"}]