---
_id: '1956'
abstract:
- lang: eng
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."
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.
article_processing_charge: No
article_type: original
author:
- first_name: Leonid A
full_name: Sazanov, Leonid A
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
- first_name: Paul
full_name: Burrows, Paul
last_name: Burrows
- first_name: Peter
full_name: Nixon, Peter
last_name: Nixon
citation:
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.
PNAS. 1998;95(3):1319-1324. doi:10.1073/pnas.95.3.1319'
apa: 'Sazanov, L. A., 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. National Academy of Sciences. https://doi.org/10.1073/pnas.95.3.1319'
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.” PNAS. National Academy of Sciences, 1998. https://doi.org/10.1073/pnas.95.3.1319.'
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,” PNAS, vol. 95, no. 3. National Academy of Sciences, pp. 1319–1324,
1998.'
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.'
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.”
PNAS, vol. 95, no. 3, National Academy of Sciences, 1998, pp. 1319–24,
doi:10.1073/pnas.95.3.1319.'
short: L.A. Sazanov, P. Burrows, P. Nixon, PNAS 95 (1998) 1319–1324.
date_created: 2018-12-11T11:54:54Z
date_published: 1998-02-03T00:00:00Z
date_updated: 2022-09-01T13:47:05Z
day: '03'
doi: 10.1073/pnas.95.3.1319
extern: '1'
external_id:
pmid:
- '9448329 '
fulldoi: https://doi.org/10.1073/pnas.95.3.1319
intvolume: ' 95'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://europepmc.org/article/pmc/18756
month: '02'
oa: 1
oa_version: None
page: 1319 - 1324
pmid: 1
publication: PNAS
publication_identifier:
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
publist_id: '5130'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of
a complex I analogue from pea thylakoid membranes'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 95
year: '1998'
...
---
_id: '4408'
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).'
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
- first_name: Pierre
full_name: Schobbens, Pierre
last_name: Schobbens
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Raskin J, Schobbens P, Henzinger TA. Axioms for real-time logics. In: Proceedings
of the 9th Interantional Conference on Concurrency Theory. Vol 1466. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 1998:219-236. doi:10.1007/BFb0055625'
apa: 'Raskin, J., Schobbens, P., & Henzinger, T. A. (1998). Axioms for real-time
logics. In Proceedings of the 9th Interantional Conference on Concurrency Theory
(Vol. 1466, pp. 219–236). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.1007/BFb0055625'
chicago: Raskin, Jean, Pierre Schobbens, and Thomas A Henzinger. “Axioms for Real-Time
Logics.” In Proceedings of the 9th Interantional Conference on Concurrency
Theory, 1466:219–36. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998.
https://doi.org/10.1007/BFb0055625.
ieee: J. Raskin, P. Schobbens, and T. A. Henzinger, “Axioms for real-time logics,”
in Proceedings of the 9th Interantional Conference on Concurrency Theory,
Nice, France, 1998, vol. 1466, pp. 219–236.
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.'
mla: Raskin, Jean, et al. “Axioms for Real-Time Logics.” Proceedings of the 9th
Interantional Conference on Concurrency Theory, vol. 1466, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 1998, pp. 219–36, doi:10.1007/BFb0055625.
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.
conference:
end_date: 1998-09-11
location: Nice, France
name: 'CONCUR: Concurrency Theory'
start_date: 1998-09-08
date_created: 2018-12-11T12:08:42Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T12:15:17Z
day: '01'
doi: 10.1007/BFb0055625
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0055625
intvolume: ' 1466'
language:
- iso: eng
month: '01'
oa_version: None
page: 219 - 236
publication: Proceedings of the 9th Interantional Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540648963'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '323'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Axioms for real-time logics
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1466
year: '1998'
...
---
_id: '4410'
abstract:
- lang: eng
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’)."
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jörg
full_name: Preußig, Jörg
last_name: Preußig
- first_name: Stefan
full_name: Kowalewski, Stefan
last_name: Kowalewski
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Preußig J, Kowalewski S, Wong Toi H, Henzinger TA. An algorithm for the approximative
analysis of rectangular automata. In: Proceedings of the 5th International
Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Vol
1486. Springer; 1998:228-240. doi:10.1007/BFb0055350'
apa: 'Preußig, J., Kowalewski, S., Wong Toi, H., & Henzinger, T. A. (1998).
An algorithm for the approximative analysis of rectangular automata. In Proceedings
of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant
Systems (Vol. 1486, pp. 228–240). Lyngby, Denmark: Springer. https://doi.org/10.1007/BFb0055350'
chicago: Preußig, Jörg, Stefan Kowalewski, Howard Wong Toi, and Thomas A Henzinger.
“An Algorithm for the Approximative Analysis of Rectangular Automata.” In Proceedings
of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant
Systems, 1486:228–40. Springer, 1998. https://doi.org/10.1007/BFb0055350.
ieee: J. Preußig, S. Kowalewski, H. Wong Toi, and T. A. Henzinger, “An algorithm
for the approximative analysis of rectangular automata,” in Proceedings of
the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant
Systems, 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.” Proceedings of the 5th International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems, vol. 1486, Springer, 1998, pp. 228–40,
doi:10.1007/BFb0055350.
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.
conference:
end_date: 1998-09-18
location: Lyngby, Denmark
name: 'FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems'
start_date: 1998-09-14
date_created: 2018-12-11T12:08:43Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T12:01:57Z
day: '01'
doi: 10.1007/BFb0055350
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0055350
intvolume: ' 1486'
language:
- iso: eng
month: '01'
oa_version: None
page: 228 - 240
publication: Proceedings of the 5th International Symposium on Formal Techniques in
Real-Time and Fault-Tolerant Systems
publication_identifier:
isbn:
- '9783540650034'
publication_status: published
publisher: Springer
publist_id: '320'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An algorithm for the approximative analysis of rectangular automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1486
year: '1998'
...
---
_id: '4429'
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.
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."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vlad
full_name: Rusu, Vlad
last_name: Rusu
citation:
ama: 'Henzinger TA, Rusu V. Reachability verification for hybrid automata. In: Proceedings
of the 1st International Workshop on Hybrid Systems: Computation and Control.
Vol 1386. Springer; 1998:190-204. doi:10.1007/3-540-64358-3_40'
apa: 'Henzinger, T. A., & Rusu, V. (1998). Reachability verification for hybrid
automata. In Proceedings of the 1st International Workshop on Hybrid Systems:
Computation and Control (Vol. 1386, pp. 190–204). Berkely, CA, United States
of America: Springer. https://doi.org/10.1007/3-540-64358-3_40'
chicago: 'Henzinger, Thomas A, and Vlad Rusu. “Reachability Verification for Hybrid
Automata.” In Proceedings of the 1st International Workshop on Hybrid Systems:
Computation and Control, 1386:190–204. Springer, 1998. https://doi.org/10.1007/3-540-64358-3_40.'
ieee: 'T. A. Henzinger and V. Rusu, “Reachability verification for hybrid automata,”
in Proceedings of the 1st International Workshop on Hybrid Systems: Computation
and Control, 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.'
mla: 'Henzinger, Thomas A., and Vlad Rusu. “Reachability Verification for Hybrid
Automata.” Proceedings of the 1st International Workshop on Hybrid Systems:
Computation and Control, vol. 1386, Springer, 1998, pp. 190–204, doi:10.1007/3-540-64358-3_40.'
short: 'T.A. Henzinger, V. Rusu, in:, Proceedings of the 1st International Workshop
on Hybrid Systems: Computation and Control, Springer, 1998, pp. 190–204.'
conference:
end_date: 1998-04-15
location: Berkely, CA, United States of America
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 1998-04-13
date_created: 2018-12-11T12:08:48Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T11:29:14Z
day: '01'
doi: 10.1007/3-540-64358-3_40
extern: '1'
fulldoi: https://doi.org/10.1007/3-540-64358-3_40
intvolume: ' 1386'
language:
- iso: eng
month: '01'
oa_version: None
page: 190 - 204
publication: 'Proceedings of the 1st International Workshop on Hybrid Systems: Computation
and Control'
publication_identifier:
isbn:
- '9783540643586'
publication_status: published
publisher: Springer
publist_id: '299'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reachability verification for hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1386
year: '1998'
...
---
_id: '4430'
alternative_title:
- LNCS
article_processing_charge: No
citation:
ama: 'Henzinger TA, ed. HSCC: Hybrid Systems—Computation and Control. Vol
1386. Springer; 1998. doi:10.1007/3-540-64358-3'
apa: 'Henzinger, T. A. (Ed.). (1998). HSCC: Hybrid Systems—Computation and Control
(Vol. 1386). Presented at the HSCC: Hybrid Systems: Computation and Control, Berkeley,
CA, United States of America: Springer. https://doi.org/10.1007/3-540-64358-3'
chicago: 'Henzinger, Thomas A, ed. HSCC: Hybrid Systems—Computation and Control.
Vol. 1386. Springer, 1998. https://doi.org/10.1007/3-540-64358-3.'
ieee: 'T. A. Henzinger, Ed., HSCC: Hybrid Systems—Computation and Control,
vol. 1386. Springer, 1998.'
ista: 'Henzinger TA ed. 1998. HSCC: Hybrid Systems—Computation and Control, Springer,p.'
mla: 'Henzinger, Thomas A., editor. HSCC: Hybrid Systems—Computation and Control.
Vol. 1386, Springer, 1998, doi:10.1007/3-540-64358-3.'
short: 'T.A. Henzinger, ed., HSCC: Hybrid Systems—Computation and Control, Springer,
1998.'
conference:
end_date: 1998-04-15
location: Berkeley, CA, United States of America
name: 'HSCC: Hybrid Systems: Computation and Control'
start_date: 1998-04-13
date_created: 2018-12-11T12:08:49Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T11:36:03Z
day: '01'
doi: 10.1007/3-540-64358-3
editor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
extern: '1'
fulldoi: https://doi.org/10.1007/3-540-64358-3
intvolume: ' 1386'
language:
- iso: eng
month: '01'
oa_version: None
publication_identifier:
isbn:
- 978-3-540-64358-6
publication_status: published
publisher: Springer
publist_id: '300'
status: public
title: 'HSCC: Hybrid Systems—Computation and Control'
type: conference_editor
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1386
year: '1998'
...
---
_id: '4486'
abstract:
- lang: eng
text: 'The simulation preorder on state transition systems is widely accepted as
a useful notion of refinement, both in its own right and as an efficiently checkable
sufficient condition for trace containment. For composite systems, due to the
exponential explosion of the state space, there is a need for decomposing a simulation
check of the form P< s Q 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
assumptions on transition systems'
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
- first_name: Serdar
full_name: Tasiran, Serdar
last_name: Tasiran
citation:
ama: 'Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for
checking simulation. In: Proceedings of the 2nd International Conference on
Formal Methods in Computer-Aided Design. Vol 1522. Springer; 1998:421-432.
doi:10.1007/3-540-49519-3_27'
apa: 'Henzinger, T. A., Qadeer, S., Rajamani, S., & Tasiran, S. (1998). An assume-guarantee
rule for checking simulation. In Proceedings of the 2nd International Conference
on Formal Methods in Computer-Aided Design (Vol. 1522, pp. 421–432). Palo
Alto, CA, United States of America: Springer. https://doi.org/10.1007/3-540-49519-3_27'
chicago: Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran.
“An Assume-Guarantee Rule for Checking Simulation.” In Proceedings of the 2nd
International Conference on Formal Methods in Computer-Aided Design, 1522:421–32.
Springer, 1998. https://doi.org/10.1007/3-540-49519-3_27.
ieee: T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee
rule for checking simulation,” in Proceedings of the 2nd International Conference
on Formal Methods in Computer-Aided Design, 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.'
mla: Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.”
Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided
Design, vol. 1522, Springer, 1998, pp. 421–32, doi:10.1007/3-540-49519-3_27.
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.
conference:
end_date: 1998-11-06
location: Palo Alto, CA, United States of America
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 1998-11-04
date_created: 2018-12-11T12:09:06Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T10:00:50Z
day: '01'
doi: 10.1007/3-540-49519-3_27
extern: '1'
fulldoi: https://doi.org/10.1007/3-540-49519-3_27
intvolume: ' 1522'
language:
- iso: eng
month: '01'
oa_version: None
page: 421 - 432
publication: Proceedings of the 2nd International Conference on Formal Methods in
Computer-Aided Design
publication_identifier:
isbn:
- '9783540651918'
publication_status: published
publisher: Springer
publist_id: '242'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An assume-guarantee rule for checking simulation
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1522
year: '1998'
...
---
_id: '4488'
abstract:
- lang: eng
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.
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Henzinger TA, Qadeer S, Rajamani S. You assume, we guarantee: Methodology
and case studies. In: Proceedings of the 10th International Conference on Computer
Aided Verification. Vol 1427. Springer; 1998:440-451. doi:10.1007/BFb0028765'
apa: 'Henzinger, T. A., Qadeer, S., & Rajamani, S. (1998). You assume, we guarantee:
Methodology and case studies. In Proceedings of the 10th International Conference
on Computer Aided Verification (Vol. 1427, pp. 440–451). Vancouver, Canada:
Springer. https://doi.org/10.1007/BFb0028765'
chicago: 'Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “You Assume, We
Guarantee: Methodology and Case Studies.” In Proceedings of the 10th International
Conference on Computer Aided Verification, 1427:440–51. Springer, 1998. https://doi.org/10.1007/BFb0028765.'
ieee: 'T. A. Henzinger, S. Qadeer, and S. Rajamani, “You assume, we guarantee: Methodology
and case studies,” in Proceedings of the 10th International Conference on Computer
Aided Verification, 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.'
mla: 'Henzinger, Thomas A., et al. “You Assume, We Guarantee: Methodology and Case
Studies.” Proceedings of the 10th International Conference on Computer Aided
Verification, vol. 1427, Springer, 1998, pp. 440–51, doi:10.1007/BFb0028765.'
short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 10th International
Conference on Computer Aided Verification, Springer, 1998, pp. 440–451.
conference:
end_date: 1998-07-02
location: Vancouver, Canada
name: 'CAV: Computer Aided Verification'
start_date: 1998-06-28
date_created: 2018-12-11T12:09:06Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-09-05T07:31:52Z
day: '01'
doi: 10.1007/BFb0028765
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0028765
intvolume: ' 1427'
language:
- iso: eng
month: '01'
oa_version: None
page: 440 - 451
publication: Proceedings of the 10th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540646082'
publication_status: published
publisher: Springer
publist_id: '239'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'You assume, we guarantee: Methodology and case studies'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1427
year: '1998'
...
---
_id: '4489'
abstract:
- lang: eng
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."
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: 'Henzinger TA, Kupferman O, Qadeer S. From pre-historic to post-modern symbolic
model checking. In: Proceedings of the 10th International Conference on Computer
Aided Verification. Vol 1427. Springer; 1998:195-206. doi:10.1007/BFb0028745'
apa: 'Henzinger, T. A., Kupferman, O., & Qadeer, S. (1998). From pre-historic
to post-modern symbolic model checking. In Proceedings of the 10th International
Conference on Computer Aided Verification (Vol. 1427, pp. 195–206). Vancouver,
Canada: Springer. https://doi.org/10.1007/BFb0028745'
chicago: Henzinger, Thomas A, Orna Kupferman, and Shaz Qadeer. “From Pre-Historic
to Post-Modern Symbolic Model Checking.” In Proceedings of the 10th International
Conference on Computer Aided Verification, 1427:195–206. Springer, 1998. https://doi.org/10.1007/BFb0028745.
ieee: T. A. Henzinger, O. Kupferman, and S. Qadeer, “From pre-historic to post-modern
symbolic model checking,” in Proceedings of the 10th International Conference
on Computer Aided Verification, Vancouver, Canada, 1998, vol. 1427, pp. 195–206.
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.'
mla: Henzinger, Thomas A., et al. “From Pre-Historic to Post-Modern Symbolic Model
Checking.” Proceedings of the 10th International Conference on Computer Aided
Verification, vol. 1427, Springer, 1998, pp. 195–206, doi:10.1007/BFb0028745.
short: T.A. Henzinger, O. Kupferman, S. Qadeer, in:, Proceedings of the 10th International
Conference on Computer Aided Verification, Springer, 1998, pp. 195–206.
conference:
end_date: 1998-07-02
location: Vancouver, Canada
name: 'CAV: Computer Aided Verification'
start_date: 1998-06-28
date_created: 2018-12-11T12:09:07Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T09:19:53Z
day: '01'
doi: 10.1007/BFb0028745
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0028745
intvolume: ' 1427'
language:
- iso: eng
month: '01'
oa_version: None
page: 195 - 206
publication: Proceedings of the 10th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540646082'
publication_status: published
publisher: Springer
publist_id: '240'
quality_controlled: '1'
scopus_import: '1'
status: public
title: From pre-historic to post-modern symbolic model checking
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1427
year: '1998'
...
---
_id: '4490'
abstract:
- lang: eng
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."
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
- first_name: Pierre
full_name: Schobbens, Pierre
last_name: Schobbens
citation:
ama: 'Henzinger TA, Raskin J, Schobbens P. The regular real-time languages. In:
Proceedings of the 25th International Colloqium on Automata, Languages and
Programming. Vol 1443. Springer; 1998:580-591. doi:10.1007/BFb0055086'
apa: 'Henzinger, T. A., Raskin, J., & Schobbens, P. (1998). The regular real-time
languages. In Proceedings of the 25th International Colloqium on Automata,
Languages and Programming (Vol. 1443, pp. 580–591). Aalborg, Denmark: Springer.
https://doi.org/10.1007/BFb0055086'
chicago: Henzinger, Thomas A, Jean Raskin, and Pierre Schobbens. “The Regular Real-Time
Languages.” In Proceedings of the 25th International Colloqium on Automata,
Languages and Programming, 1443:580–91. Springer, 1998. https://doi.org/10.1007/BFb0055086.
ieee: T. A. Henzinger, J. Raskin, and P. Schobbens, “The regular real-time languages,”
in Proceedings of the 25th International Colloqium on Automata, Languages and
Programming, Aalborg, Denmark, 1998, vol. 1443, pp. 580–591.
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.'
mla: Henzinger, Thomas A., et al. “The Regular Real-Time Languages.” Proceedings
of the 25th International Colloqium on Automata, Languages and Programming,
vol. 1443, Springer, 1998, pp. 580–91, doi:10.1007/BFb0055086.
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.
conference:
end_date: 1998-07-17
location: Aalborg, Denmark
name: 'ICALP: Automata, Languages and Programming'
start_date: 1998-07-13
date_created: 2018-12-11T12:09:07Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T09:30:11Z
day: '01'
doi: 10.1007/BFb0055086
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0055086
intvolume: ' 1443'
language:
- iso: eng
month: '01'
oa_version: None
page: 580 - 591
publication: Proceedings of the 25th International Colloqium on Automata, Languages
and Programming
publication_identifier:
isbn:
- '9783540647812'
publication_status: published
publisher: Springer
publist_id: '241'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The regular real-time languages
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1443
year: '1998'
...
---
_id: '4491'
abstract:
- lang: eng
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
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Pei
full_name: Ho, Pei
last_name: Ho
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: Henzinger TA, Ho P, Wong Toi H. Algorithmic analysis of nonlinear hybrid systems.
IEEE Transactions on Automatic Control. 1998;43(4):540-554. doi:10.1109/9.664156
apa: Henzinger, T. A., Ho, P., & Wong Toi, H. (1998). Algorithmic analysis of
nonlinear hybrid systems. IEEE Transactions on Automatic Control. IEEE.
https://doi.org/10.1109/9.664156
chicago: Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “Algorithmic Analysis
of Nonlinear Hybrid Systems.” IEEE Transactions on Automatic Control. IEEE,
1998. https://doi.org/10.1109/9.664156
.
ieee: T. A. Henzinger, P. Ho, and H. Wong Toi, “Algorithmic analysis of nonlinear
hybrid systems,” IEEE Transactions on Automatic Control, vol. 43, no. 4.
IEEE, pp. 540–554, 1998.
ista: Henzinger TA, Ho P, Wong Toi H. 1998. Algorithmic analysis of nonlinear hybrid
systems. IEEE Transactions on Automatic Control. 43(4), 540–554.
mla: Henzinger, Thomas A., et al. “Algorithmic Analysis of Nonlinear Hybrid Systems.”
IEEE Transactions on Automatic Control, vol. 43, no. 4, IEEE, 1998, pp.
540–54, doi:10.1109/9.664156 .
short: T.A. Henzinger, P. Ho, H. Wong Toi, IEEE Transactions on Automatic Control
43 (1998) 540–554.
date_created: 2018-12-11T12:09:07Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T14:34:35Z
day: '01'
doi: '10.1109/9.664156 '
extern: '1'
fulldoi: 'https://doi.org/10.1109/9.664156 '
intvolume: ' 43'
issue: '4'
language:
- iso: eng
month: '01'
oa_version: None
page: 540 - 554
publication: IEEE Transactions on Automatic Control
publication_identifier:
issn:
- 0018-9162
publication_status: published
publisher: IEEE
publist_id: '238'
quality_controlled: '1'
status: public
title: Algorithmic analysis of nonlinear hybrid systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 43
year: '1998'
...
---
_id: '4492'
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.
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.
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Peter
full_name: Kopke, Peter
last_name: Kopke
- first_name: Anuj
full_name: Puri, Anuj
last_name: Puri
- first_name: P.
full_name: Varaiya, P.
last_name: Varaiya
citation:
ama: Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata?
Journal of Computer and System Sciences. 1998;57(1):94-124. doi:10.1006/jcss.1998.1581
apa: Henzinger, T. A., Kopke, P., Puri, A., & Varaiya, P. (1998). What’s decidable
about hybrid automata? Journal of Computer and System Sciences. Elsevier.
https://doi.org/10.1006/jcss.1998.1581
chicago: Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable
about Hybrid Automata?” Journal of Computer and System Sciences. Elsevier,
1998. https://doi.org/10.1006/jcss.1998.1581.
ieee: T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about
hybrid automata?,” Journal of Computer and System Sciences, vol. 57, no.
1. Elsevier, pp. 94–124, 1998.
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.
mla: Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” Journal
of Computer and System Sciences, vol. 57, no. 1, Elsevier, 1998, pp. 94–124,
doi:10.1006/jcss.1998.1581.
short: T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, Journal of Computer and System
Sciences 57 (1998) 94–124.
date_created: 2018-12-11T12:09:08Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T14:29:15Z
day: '01'
doi: 10.1006/jcss.1998.1581
extern: '1'
fulldoi: https://doi.org/10.1006/jcss.1998.1581
intvolume: ' 57'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0022000098915811
month: '01'
oa: 1
oa_version: Published Version
page: 94 - 124
publication: Journal of Computer and System Sciences
publication_identifier:
isbn:
- 0022-0000
publication_status: published
publisher: Elsevier
publist_id: '237'
quality_controlled: '1'
status: public
title: What's decidable about hybrid automata?
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 57
year: '1998'
...
---
_id: '4515'
abstract:
- lang: eng
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.
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. It’s about time: Real-time logics reviewed. In: Proceedings
of the 9th Interantional Conference on Concurrency Theory. Vol 1466. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 1998:439-454. doi:10.1007/BFb0055640'
apa: 'Henzinger, T. A. (1998). It’s about time: Real-time logics reviewed. In Proceedings
of the 9th Interantional Conference on Concurrency Theory (Vol. 1466, pp.
439–454). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/BFb0055640'
chicago: 'Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” In
Proceedings of the 9th Interantional Conference on Concurrency Theory,
1466:439–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. https://doi.org/10.1007/BFb0055640.'
ieee: 'T. A. Henzinger, “It’s about time: Real-time logics reviewed,” in Proceedings
of the 9th Interantional Conference on Concurrency Theory, Nice, France, 1998,
vol. 1466, pp. 439–454.'
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.'
mla: 'Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” Proceedings
of the 9th Interantional Conference on Concurrency Theory, vol. 1466, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–54, doi:10.1007/BFb0055640.'
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.
conference:
end_date: 1998-09-11
location: Nice, France
name: 'CONCUR: Concurrency Theory'
start_date: 1998-09-08
date_created: 2018-12-11T12:09:15Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T14:24:08Z
day: '01'
doi: 10.1007/BFb0055640
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0055640
intvolume: ' 1466'
language:
- iso: eng
month: '01'
oa_version: None
page: 439 - 454
publication: Proceedings of the 9th Interantional Conference on Concurrency Theory
publication_identifier:
isbn:
- 978-3-540-64896-3
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '214'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'It''s about time: Real-time logics reviewed'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1466
year: '1998'
...
---
_id: '4603'
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.
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: 'Alur R, Henzinger TA, Kupferman O, Vardi M. Alternating refinement relations.
In: Proceedings of the 9th Interantional Conference on Concurrency Theory.
Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:163-178. doi:10.1007/BFb0055622'
apa: 'Alur, R., Henzinger, T. A., Kupferman, O., & Vardi, M. (1998). Alternating
refinement relations. In Proceedings of the 9th Interantional Conference on
Concurrency Theory (Vol. 1466, pp. 163–178). Nice, France: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.1007/BFb0055622'
chicago: Alur, Rajeev, Thomas A Henzinger, Orna Kupferman, and Moshe Vardi. “Alternating
Refinement Relations.” In Proceedings of the 9th Interantional Conference on
Concurrency Theory, 1466:163–78. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
1998. https://doi.org/10.1007/BFb0055622.
ieee: R. Alur, T. A. Henzinger, O. Kupferman, and M. Vardi, “Alternating refinement
relations,” in Proceedings of the 9th Interantional Conference on Concurrency
Theory, Nice, France, 1998, vol. 1466, pp. 163–178.
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.'
mla: Alur, Rajeev, et al. “Alternating Refinement Relations.” Proceedings of
the 9th Interantional Conference on Concurrency Theory, vol. 1466, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–78, doi:10.1007/BFb0055622.
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.
conference:
end_date: 1998-09-11
location: Nice, France
name: 'CONCUR: Concurrency Theory'
start_date: 1998-09-08
date_created: 2018-12-11T12:09:42Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T09:50:34Z
day: '01'
doi: 10.1007/BFb0055622
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0055622
intvolume: ' 1466'
language:
- iso: eng
month: '01'
oa_version: None
page: 163 - 178
publication: Proceedings of the 9th Interantional Conference on Concurrency Theory
publication_identifier:
isbn:
- 978-3-540-64896-3
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '104'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating refinement relations
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1466
year: '1998'
...
---
_id: '4604'
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
- first_name: Serdar
full_name: Tasiran, Serdar
last_name: Tasiran
citation:
ama: 'Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani S, Tasiran S. Mocha: Modularity
in model checking. In: Proceedings of the 10th International Conference on
Computer Aided Verification. Vol 1427. Springer; 1998:521-525. doi:10.1007/BFb0028774'
apa: 'Alur, R., Henzinger, T. A., Mang, F., Qadeer, S., Rajamani, S., & Tasiran,
S. (1998). Mocha: Modularity in model checking. In Proceedings of the 10th
International Conference on Computer Aided Verification (Vol. 1427, pp. 521–525).
Vancouver, Canada: Springer. https://doi.org/10.1007/BFb0028774'
chicago: 'Alur, Rajeev, Thomas A Henzinger, Freddy Mang, Shaz Qadeer, Sriram Rajamani,
and Serdar Tasiran. “Mocha: Modularity in Model Checking.” In Proceedings of
the 10th International Conference on Computer Aided Verification, 1427:521–25.
Springer, 1998. https://doi.org/10.1007/BFb0028774.'
ieee: 'R. Alur, T. A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran,
“Mocha: Modularity in model checking,” in Proceedings of the 10th International
Conference on Computer Aided Verification, Vancouver, Canada, 1998, vol. 1427,
pp. 521–525.'
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.'
mla: 'Alur, Rajeev, et al. “Mocha: Modularity in Model Checking.” Proceedings
of the 10th International Conference on Computer Aided Verification, vol.
1427, Springer, 1998, pp. 521–25, doi:10.1007/BFb0028774.'
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.
conference:
end_date: 1998-07-02
location: Vancouver, Canada
name: 'CAV: Computer Aided Verification'
start_date: 1998-06-28
date_created: 2018-12-11T12:09:42Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T09:06:21Z
day: '01'
doi: 10.1007/BFb0028774
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0028774
intvolume: ' 1427'
language:
- iso: eng
month: '01'
oa_version: None
page: 521 - 525
publication: Proceedings of the 10th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540646082'
publication_status: published
publisher: Springer
publist_id: '103'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Mocha: Modularity in model checking'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1427
year: '1998'
...
---
_id: '4606'
abstract:
- lang: eng
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."
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"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Alur R, Henzinger TA, Rajamani S. Symbolic exploration of transition hierarchies.
In: Proceedings of the 4th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems. Vol 1384. Springer; 1998:330-344.
doi:10.1007/BFb0054181'
apa: 'Alur, R., Henzinger, T. A., & Rajamani, S. (1998). Symbolic exploration
of transition hierarchies. In Proceedings of the 4th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems (Vol.
1384, pp. 330–344). Lisbon, Portugal: Springer. https://doi.org/10.1007/BFb0054181'
chicago: Alur, Rajeev, Thomas A Henzinger, and Sriram Rajamani. “Symbolic Exploration
of Transition Hierarchies.” In Proceedings of the 4th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 1384:330–44.
Springer, 1998. https://doi.org/10.1007/BFb0054181.
ieee: R. Alur, T. A. Henzinger, and S. Rajamani, “Symbolic exploration of transition
hierarchies,” in Proceedings of the 4th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, 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.'
mla: Alur, Rajeev, et al. “Symbolic Exploration of Transition Hierarchies.” Proceedings
of the 4th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 1384, Springer, 1998, pp. 330–44, doi:10.1007/BFb0054181.
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.
conference:
end_date: 1998-04-04
location: Lisbon, Portugal
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 1998-03-28
date_created: 2018-12-11T12:09:43Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T08:44:36Z
day: '01'
doi: 10.1007/BFb0054181
extern: '1'
fulldoi: https://doi.org/10.1007/BFb0054181
intvolume: ' 1384'
language:
- iso: eng
month: '01'
oa_version: None
page: 330 - 344
publication: Proceedings of the 4th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems
publication_identifier:
isbn:
- '9783540643562'
publication_status: published
publisher: Springer
publist_id: '102'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic exploration of transition hierarchies
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1384
year: '1998'
...
---
_id: '4639'
abstract:
- lang: eng
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 ε>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'
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'De Alfaro L, Henzinger TA, Kupferman O. Concurrent reachability games. In:
Proceedings 39th Annual Symposium on Foundations of Computer Science.
IEEE; 1998:564-575. doi:10.1109/SFCS.1998.743507
'
apa: 'De Alfaro, L., Henzinger, T. A., & Kupferman, O. (1998). Concurrent reachability
games. In Proceedings 39th Annual Symposium on Foundations of Computer Science
(pp. 564–575). Palo Alto, CA, United States of America: IEEE. https://doi.org/10.1109/SFCS.1998.743507 '
chicago: De Alfaro, Luca, Thomas A Henzinger, and Orna Kupferman. “Concurrent Reachability
Games.” In Proceedings 39th Annual Symposium on Foundations of Computer Science,
564–75. IEEE, 1998. https://doi.org/10.1109/SFCS.1998.743507
.
ieee: L. De Alfaro, T. A. Henzinger, and O. Kupferman, “Concurrent reachability
games,” in Proceedings 39th Annual Symposium on Foundations of Computer Science,
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.'
mla: De Alfaro, Luca, et al. “Concurrent Reachability Games.” Proceedings 39th
Annual Symposium on Foundations of Computer Science, IEEE, 1998, pp. 564–75,
doi:10.1109/SFCS.1998.743507
.
short: L. De Alfaro, T.A. Henzinger, O. Kupferman, in:, Proceedings 39th Annual
Symposium on Foundations of Computer Science, IEEE, 1998, pp. 564–575.
conference:
end_date: 1998-11-11
location: Palo Alto, CA, United States of America
name: 'FOCS: Foundations of Computer Science'
start_date: 1998-11-08
date_created: 2018-12-11T12:09:53Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-22T14:09:02Z
day: '01'
doi: '10.1109/SFCS.1998.743507 '
extern: '1'
fulldoi: 'https://doi.org/10.1109/SFCS.1998.743507 '
language:
- iso: eng
month: '01'
oa_version: None
page: 564 - 575
publication: ' Proceedings 39th Annual Symposium on Foundations of Computer Science'
publication_identifier:
isbn:
- '0818691727'
publication_status: published
publisher: IEEE
publist_id: '68'
quality_controlled: '1'
status: public
title: Concurrent reachability games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1998'
...
---
_id: '6160'
abstract:
- lang: eng
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.
author:
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
- first_name: Cornelia I
full_name: Bargmann, Cornelia I
last_name: Bargmann
citation:
ama: de Bono M, Bargmann CI. Natural variation in a neuropeptide Y receptor homolog
modifies social behavior and food response in C. elegans. Cell. 1998;94(5):679-689.
doi:10.1016/s0092-8674(00)81609-8
apa: de Bono, M., & Bargmann, C. I. (1998). Natural variation in a neuropeptide
Y receptor homolog modifies social behavior and food response in C. elegans. Cell.
Elsevier. https://doi.org/10.1016/s0092-8674(00)81609-8
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.”
Cell. Elsevier, 1998. https://doi.org/10.1016/s0092-8674(00)81609-8.
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,” Cell,
vol. 94, no. 5. Elsevier, pp. 679–689, 1998.
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.
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.”
Cell, vol. 94, no. 5, Elsevier, 1998, pp. 679–89, doi:10.1016/s0092-8674(00)81609-8.
short: M. de Bono, C.I. Bargmann, Cell 94 (1998) 679–689.
date_created: 2019-03-21T10:32:06Z
date_published: 1998-09-04T00:00:00Z
date_updated: 2021-01-12T08:06:28Z
day: '04'
doi: 10.1016/s0092-8674(00)81609-8
extern: '1'
external_id:
pmid:
- '9741632'
fulldoi: https://doi.org/10.1016/s0092-8674(00)81609-8
intvolume: ' 94'
issue: '5'
language:
- iso: eng
month: '09'
oa_version: None
page: 679-689
pmid: 1
publication: Cell
publication_identifier:
issn:
- 0092-8674
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Natural variation in a neuropeptide Y receptor homolog modifies social behavior
and food response in C. elegans
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 94
year: '1998'
...
---
_id: '3487'
abstract:
- lang: eng
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.
acknowledgement: "See comment by Nicoll RA, Malenka RC (1998) Science 281:360-361\r\n"
article_processing_charge: No
article_type: original
author:
- first_name: Peter M
full_name: Jonas, Peter M
id: 353C1B58-F248-11E8-B48F-1D18A9856A87
last_name: Jonas
orcid: 0000-0001-5001-4804
- first_name: Joseph
full_name: Bischofberger, Joseph
last_name: Bischofberger
- first_name: Jürgen
full_name: Sandkühler, Jürgen
last_name: Sandkühler
citation:
ama: Jonas PM, Bischofberger J, Sandkühler J. Corelease of two fast neurotransmitters
at a central synapse. Science. 1998;281(5375):419-424. doi:10.1126/science.281.5375.419
apa: Jonas, P. M., Bischofberger, J., & Sandkühler, J. (1998). Corelease of
two fast neurotransmitters at a central synapse. Science. American Association
for the Advancement of Science. https://doi.org/10.1126/science.281.5375.419
chicago: Jonas, Peter M, Joseph Bischofberger, and Jürgen Sandkühler. “Corelease
of Two Fast Neurotransmitters at a Central Synapse.” Science. American
Association for the Advancement of Science, 1998. https://doi.org/10.1126/science.281.5375.419.
ieee: P. M. Jonas, J. Bischofberger, and J. Sandkühler, “Corelease of two fast neurotransmitters
at a central synapse,” Science, vol. 281, no. 5375. American Association
for the Advancement of Science, pp. 419–424, 1998.
ista: Jonas PM, Bischofberger J, Sandkühler J. 1998. Corelease of two fast neurotransmitters
at a central synapse. Science. 281(5375), 419–424.
mla: Jonas, Peter M., et al. “Corelease of Two Fast Neurotransmitters at a Central
Synapse.” Science, vol. 281, no. 5375, American Association for the Advancement
of Science, 1998, pp. 419–24, doi:10.1126/science.281.5375.419.
short: P.M. Jonas, J. Bischofberger, J. Sandkühler, Science 281 (1998) 419–424.
date_created: 2018-12-11T12:03:35Z
date_published: 1998-07-17T00:00:00Z
date_updated: 2022-08-29T14:52:38Z
day: '17'
doi: 10.1126/science.281.5375.419
extern: '1'
external_id:
pmid:
- '9665886 '
fulldoi: https://doi.org/10.1126/science.281.5375.419
intvolume: ' 281'
issue: '5375'
language:
- iso: eng
month: '07'
oa_version: None
page: 419 - 424
pmid: 1
publication: Science
publication_identifier:
issn:
- 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '2900'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Corelease of two fast neurotransmitters at a central synapse
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 281
year: '1998'
...
---
_id: '3488'
abstract:
- lang: eng
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 <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.
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.
article_processing_charge: No
article_type: original
author:
- first_name: Marco
full_name: Martina, Marco
last_name: Martina
- first_name: Jobst
full_name: Schultz, Jobst
last_name: Schultz
- first_name: Heimo
full_name: Ehmke, Heimo
last_name: Ehmke
- first_name: Hannah
full_name: Monyer, Hannah
last_name: Monyer
- first_name: Peter M
full_name: Jonas, Peter M
id: 353C1B58-F248-11E8-B48F-1D18A9856A87
last_name: Jonas
orcid: 0000-0001-5001-4804
citation:
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. Journal of Neuroscience. 1998;18(20):8111-8125.
doi:10.1523/JNEUROSCI.18-20-08111.1998
apa: Martina, M., Schultz, J., Ehmke, H., Monyer, H., & Jonas, P. M. (1998).
Functional and molecular differences between voltage-gated K+ channels of fast-spiking
interneurons and pyramidal neurons of rat hippocampus. Journal of Neuroscience.
Society for Neuroscience. https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998
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.” Journal
of Neuroscience. Society for Neuroscience, 1998. https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998.
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,” Journal of Neuroscience, 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.
mla: Martina, Marco, et al. “Functional and Molecular Differences between Voltage-Gated
K+ Channels of Fast-Spiking Interneurons and Pyramidal Neurons of Rat Hippocampus.”
Journal of Neuroscience, vol. 18, no. 20, Society for Neuroscience, 1998,
pp. 8111–25, doi:10.1523/JNEUROSCI.18-20-08111.1998.
short: M. Martina, J. Schultz, H. Ehmke, H. Monyer, P.M. Jonas, Journal of Neuroscience
18 (1998) 8111–8125.
date_created: 2018-12-11T12:03:35Z
date_published: 1998-10-15T00:00:00Z
date_updated: 2022-08-29T14:20:39Z
day: '15'
doi: 10.1523/JNEUROSCI.18-20-08111.1998
extern: '1'
external_id:
pmid:
- '9763458'
fulldoi: https://doi.org/10.1523/JNEUROSCI.18-20-08111.1998
intvolume: ' 18'
issue: '20'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6792860/
month: '10'
oa: 1
oa_version: None
page: 8111 - 8125
pmid: 1
publication: Journal of Neuroscience
publication_identifier:
issn:
- 0270-6474
publication_status: published
publisher: Society for Neuroscience
publist_id: '2899'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Functional and molecular differences between voltage-gated K+ channels of fast-spiking
interneurons and pyramidal neurons of rat hippocampus
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 18
year: '1998'
...
---
_id: '3506'
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.
applicant:
- Raindrop Geomagic, Inc.
article_processing_charge: No
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Ping
full_name: Fu, Ping
last_name: Fu
citation:
ama: Edelsbrunner H, Fu P. Apparatus and method for geometric morphing. 1998.
apa: Edelsbrunner, H., & Fu, P. (1998). Apparatus and method for geometric morphing.
chicago: Edelsbrunner, Herbert, and Ping Fu. “Apparatus and Method for Geometric
Morphing,” 1998.
ieee: H. Edelsbrunner and P. Fu, “Apparatus and method for geometric morphing.”
1998.
ista: Edelsbrunner H, Fu P. 1998. Apparatus and method for geometric morphing.
mla: Edelsbrunner, Herbert, and Ping Fu. Apparatus and Method for Geometric Morphing.
1998.
short: H. Edelsbrunner, P. Fu, (1998).
date_created: 2018-12-11T12:03:41Z
date_published: 1998-12-15T00:00:00Z
date_updated: 2022-01-05T15:16:35Z
day: '15'
extern: '1'
ipc: G06T13/20 ; G06T2210/44
ipn: US5850229A
main_file_link:
- open_access: '1'
url: https://patents.google.com/patent/US5850229A
month: '12'
oa: 1
oa_version: Published Version
publication_date: 1998-12-15
publist_id: '2881'
status: public
title: Apparatus and method for geometric morphing
type: patent
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '1998'
...