---
_id: '4483'
abstract:
- lang: eng
text: 'Model-checking algorithms can be used to verify, formally and automatically,
if a low-level description of a design conforms with a high-level description.
However, for designs with very large state spaces, prior to the application of
an algorithm, the refinement-checking task needs to be decomposed into subtasks
of manageable complexity. It is natural to decompose the task following the component
structure of the design. However, an individual component often does not satisfy
its requirements unless the component is put into the right context, which constrains
the inputs to the component. Thus, in order to verify each component individually,
we need to make assumptions about its inputs, which are provided by the other
components of the design. This reasoning is circular: component A is verified
under the assumption that context B behaves correctly, and symmetrically, B is
verified assuming the correctness of A. The assume-guarantee paradigm provides
a systematic theory and methodology for ensuring the soundness of the circular
style of postulating and discharging assumptions in component-based reasoning.We
give a tutorial introduction to the assume-guarantee paradigm for decomposing
refinement-checking tasks. To illustrate the method, we step in detail through
the formal verification of a processor pipeline against an instruction set architecture.
In this example, the verification of a three-stage pipeline is broken up into
three subtasks, one for each stage of the pipeline.'
acknowledgement: 'Supported in part by DARPA Information Technology Office, by the
MARC0 Gigascale Silicon Research Center, and by the National Science Foundation. '
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. Decomposing refinement proofs using assume-guarantee
reasoning. In: Proceedings of the 2000 International Conference on Computer-Aided
Design. IEEE; 2000:245-252. doi:10.1109/ICCAD.2000.896481'
apa: 'Henzinger, T. A., Qadeer, S., & Rajamani, S. (2000). Decomposing refinement
proofs using assume-guarantee reasoning. In Proceedings of the 2000 International
Conference on Computer-Aided Design (pp. 245–252). San Jose, CA, USA: IEEE.
https://doi.org/10.1109/ICCAD.2000.896481'
chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Decomposing Refinement
Proofs Using Assume-Guarantee Reasoning.” In Proceedings of the 2000 International
Conference on Computer-Aided Design, 245–52. IEEE, 2000. https://doi.org/10.1109/ICCAD.2000.896481.
ieee: T. A. Henzinger, S. Qadeer, and S. Rajamani, “Decomposing refinement proofs
using assume-guarantee reasoning,” in Proceedings of the 2000 International
Conference on Computer-Aided Design, San Jose, CA, USA, 2000, pp. 245–252.
ista: 'Henzinger TA, Qadeer S, Rajamani S. 2000. Decomposing refinement proofs using
assume-guarantee reasoning. Proceedings of the 2000 International Conference on
Computer-Aided Design. ICCAD: Computer-Aided Design, 245–252.'
mla: Henzinger, Thomas A., et al. “Decomposing Refinement Proofs Using Assume-Guarantee
Reasoning.” Proceedings of the 2000 International Conference on Computer-Aided
Design, IEEE, 2000, pp. 245–52, doi:10.1109/ICCAD.2000.896481.
short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 2000 International
Conference on Computer-Aided Design, IEEE, 2000, pp. 245–252.
conference:
end_date: 2000-11-09
location: San Jose, CA, USA
name: 'ICCAD: Computer-Aided Design'
start_date: 2000-11-05
date_created: 2018-12-11T12:09:05Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T12:57:52Z
day: '01'
doi: 10.1109/ICCAD.2000.896481
extern: '1'
fulldoi: https://doi.org/10.1109/ICCAD.2000.896481
language:
- iso: eng
month: '01'
oa_version: None
page: 245 - 252
publication: Proceedings of the 2000 International Conference on Computer-Aided Design
publication_identifier:
isbn:
- '0780364457'
publication_status: published
publisher: IEEE
publist_id: '249'
quality_controlled: '1'
status: public
title: Decomposing refinement proofs using assume-guarantee reasoning
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...
---
_id: '4512'
abstract:
- lang: eng
text: "Masaccio is a formal model for hybrid dynamical systems which are built from
atomic discrete components (difference equations) and atomic continuous components
(differential equations) by parallel and serial composition, arbitrarily nested.
Each system component consists of an interface, which determines the possible
ways of using the component, and a set of executions, which define the possible
behaviors of the component in real time.\r\nVersion 1.0 (May 2000).\r\n"
acknowledgement: This research was supported in part by the DARPA grants NAG2-1214
and F33615-C-98-3614, and by the MARCO grant 98-DT-660.
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. Masaccio: A formal model for embedded components. In: Proceedings
of the 1st International Conference on Theoretical Computer Science . Vol
1872. Springer; 2000:549-563. doi:10.1007/3-540-44929-9_38'
apa: 'Henzinger, T. A. (2000). Masaccio: A formal model for embedded components.
In Proceedings of the 1st International Conference on Theoretical Computer
Science (Vol. 1872, pp. 549–563). Sendai, Japan: Springer. https://doi.org/10.1007/3-540-44929-9_38'
chicago: 'Henzinger, Thomas A. “Masaccio: A Formal Model for Embedded Components.”
In Proceedings of the 1st International Conference on Theoretical Computer
Science , 1872:549–63. Springer, 2000. https://doi.org/10.1007/3-540-44929-9_38.'
ieee: 'T. A. Henzinger, “Masaccio: A formal model for embedded components,” in Proceedings
of the 1st International Conference on Theoretical Computer Science , Sendai,
Japan, 2000, vol. 1872, pp. 549–563.'
ista: 'Henzinger TA. 2000. Masaccio: A formal model for embedded components. Proceedings
of the 1st International Conference on Theoretical Computer Science . TCS: Theoretical
Computer Science, LNCS, vol. 1872, 549–563.'
mla: 'Henzinger, Thomas A. “Masaccio: A Formal Model for Embedded Components.” Proceedings
of the 1st International Conference on Theoretical Computer Science , vol.
1872, Springer, 2000, pp. 549–63, doi:10.1007/3-540-44929-9_38.'
short: T.A. Henzinger, in:, Proceedings of the 1st International Conference on Theoretical
Computer Science , Springer, 2000, pp. 549–563.
conference:
end_date: 2000-08-19
location: Sendai, Japan
name: 'TCS: Theoretical Computer Science'
start_date: 2000-08-17
date_created: 2018-12-11T12:09:14Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T13:48:08Z
day: '01'
doi: 10.1007/3-540-44929-9_38
extern: '1'
fulldoi: https://doi.org/10.1007/3-540-44929-9_38
intvolume: ' 1872'
language:
- iso: eng
month: '01'
oa_version: None
page: 549 - 563
publication: 'Proceedings of the 1st International Conference on Theoretical Computer
Science '
publication_identifier:
isbn:
- '9783540678236'
publication_status: published
publisher: Springer
publist_id: '215'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Masaccio: A formal model for embedded components'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1872
year: '2000'
...
---
_id: '4513'
abstract:
- lang: eng
text: 'A hybrid automaton is a formal model for a mixed discrete-continuous system.
We classify hybrid automata according to what questions about their behavior can
be answered algorithmically. The classification reveals structure on mixed discrete-continuous
state spaces that was previously studied on purely discrete state spaces only.
In particular, various classes of hybrid automata induce finitary trace equivalence
(or similarity, or bisimilarity) relations on an uncountable state space, thus
permitting the application of various model-checking techniques that were originally
developed for finitestate 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 CR9504469, 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 96-DC-324.036. '
alternative_title:
- 'NATO ASI Series F: Computer and Systems Sciences'
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. The theory of hybrid automata. In: Inan M, Kurshan R, eds. Verification
of Digital and Hybrid Systems. Vol 170. Springer; 2000:265-292. doi:10.1007/978-3-642-59615-5'
apa: Henzinger, T. A. (2000). The theory of hybrid automata. In M. Inan & R.
Kurshan (Eds.), Verification of Digital and Hybrid Systems (Vol. 170, pp.
265–292). Springer. https://doi.org/10.1007/978-3-642-59615-5
chicago: Henzinger, Thomas A. “The Theory of Hybrid Automata.” In Verification
of Digital and Hybrid Systems, edited by M. Inan and Robert Kurshan, 170:265–92.
Springer, 2000. https://doi.org/10.1007/978-3-642-59615-5.
ieee: T. A. Henzinger, “The theory of hybrid automata,” in Verification of Digital
and Hybrid Systems, vol. 170, M. Inan and R. Kurshan, Eds. Springer, 2000,
pp. 265–292.
ista: 'Henzinger TA. 2000.The theory of hybrid automata. In: Verification of Digital
and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol. 170,
265–292.'
mla: Henzinger, Thomas A. “The Theory of Hybrid Automata.” Verification of Digital
and Hybrid Systems, edited by M. Inan and Robert Kurshan, vol. 170, Springer,
2000, pp. 265–92, doi:10.1007/978-3-642-59615-5.
short: T.A. Henzinger, in:, M. Inan, R. Kurshan (Eds.), Verification of Digital
and Hybrid Systems, Springer, 2000, pp. 265–292.
date_created: 2018-12-11T12:09:14Z
date_published: 2000-04-28T00:00:00Z
date_updated: 2023-04-18T12:37:17Z
day: '28'
doi: 10.1007/978-3-642-59615-5
editor:
- first_name: M.
full_name: Inan, M.
last_name: Inan
- first_name: Robert
full_name: Kurshan, Robert
last_name: Kurshan
extern: '1'
fulldoi: https://doi.org/10.1007/978-3-642-59615-5
intvolume: ' 170'
language:
- iso: eng
month: '04'
oa_version: None
page: 265 - 292
publication: Verification of Digital and Hybrid Systems
publication_identifier:
isbn:
- '9783642596155'
publication_status: published
publisher: Springer
publist_id: '216'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The theory of hybrid automata
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 170
year: '2000'
...
---
_id: '4598'
abstract:
- lang: eng
text: A hybrid system is a dynamical system with both discrete and continuous state
changes. For analysis purposes, it is often useful to abstract a system in a way
that preserves the properties being analyzed while hiding the details that are
of no interest. We show that interesting classes of hybrid systems can be abstracted
to purely discrete systems while preserving all properties that are definable
in temporal logic. The classes that permit discrete abstractions fall into two
categories. Either the continuous dynamics must be restricted, as is the case
for timed and rectangular hybrid systems, or the discrete dynamics must be restricted,
as is the case for o-minimal hybrid systems. In this paper, we survey and unify
results from both areas.
acknowledgement: The authors would like to thank the reviewers for their detailed
comments.
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Gerardo
full_name: Lafferriere, Gerardo
last_name: Lafferriere
- first_name: George
full_name: Pappas, George
last_name: Pappas
citation:
ama: Alur R, Henzinger TA, Lafferriere G, Pappas G. Discrete abstractions of hybrid
systems. Proceedings of the IEEE. 2000;88(7):971-984. doi:10.1109/5.871304
apa: Alur, R., Henzinger, T. A., Lafferriere, G., & Pappas, G. (2000). Discrete
abstractions of hybrid systems. Proceedings of the IEEE. IEEE. https://doi.org/10.1109/5.871304
chicago: Alur, Rajeev, Thomas A Henzinger, Gerardo Lafferriere, and George Pappas.
“Discrete Abstractions of Hybrid Systems.” Proceedings of the IEEE. IEEE,
2000. https://doi.org/10.1109/5.871304
.
ieee: R. Alur, T. A. Henzinger, G. Lafferriere, and G. Pappas, “Discrete abstractions
of hybrid systems,” Proceedings of the IEEE, vol. 88, no. 7. IEEE, pp.
971–984, 2000.
ista: Alur R, Henzinger TA, Lafferriere G, Pappas G. 2000. Discrete abstractions
of hybrid systems. Proceedings of the IEEE. 88(7), 971–984.
mla: Alur, Rajeev, et al. “Discrete Abstractions of Hybrid Systems.” Proceedings
of the IEEE, vol. 88, no. 7, IEEE, 2000, pp. 971–84, doi:10.1109/5.871304 .
short: R. Alur, T.A. Henzinger, G. Lafferriere, G. Pappas, Proceedings of the IEEE
88 (2000) 971–984.
date_created: 2018-12-11T12:09:41Z
date_published: 2000-07-01T00:00:00Z
date_updated: 2023-04-13T13:32:11Z
day: '01'
doi: '10.1109/5.871304 '
extern: '1'
fulldoi: 'https://doi.org/10.1109/5.871304 '
intvolume: ' 88'
issue: '7'
language:
- iso: eng
month: '07'
oa_version: None
page: 971 - 984
publication: Proceedings of the IEEE
publication_identifier:
issn:
- 0018-9219
publication_status: published
publisher: IEEE
publist_id: '107'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discrete abstractions of hybrid systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 88
year: '2000'
...
---
_id: '4627'
abstract:
- lang: eng
text: 'We consider two-player games, which are played on a finite state space for
an infinite number of rounds. The games are concurrent, that is, in each round,
the two players choose their moves independently and simultaneously; the current
state and the two moves determine a successor state. We consider omega-regular
winning conditions on the resulting infinite state sequence. To model the independent
choice of moves, both players are allowed to use randomization for selecting their
moves. This gives rise to the following qualitative modes of winning, which can
be studied without numerical considerations concerning probabilities: sure-win
(player 1 can ensure winning with certainty), almost-sure-win (player 1 can ensure
winning with probability 1), limit-win (player 1 can ensure winning with probability
arbitrarily close to 1), bounded-win (player 1 can ensure winning with probability
bounded away from 0), positive-win (player 1 can ensure winning with positive
probability), and exist-win (player 1 can ensure that at least one possible outcome
of the game satisfies the winning condition).We provide algorithms for computing
the sets of winning states for each of these winning modes. In particular, we
solve concurrent Rabin-chain games in n0 (m) time, where n is the size of the
game structure and m is the number of pairs in the Rabin-chain condition. While
this complexity is in line with traditional turn-based games, where in each state
only one of the two players has a choice of moves, our algorithms are considerably
more involved than those for turn-based games are. This is because concurrent
games violate two of the most fundamental properties of turn-based games. First,
concurrent games are not determined, but rather exhibit a more general duality
property, which involves multiple modes of winning. Second, winning strategies
for concurrent games may require infinite memory.'
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
citation:
ama: 'De Alfaro L, Henzinger TA. Concurrent omega-regular games. In: Proceedings
of the 15th Annual IEEE Symposium on Logic in Computer Science. IEEE; 2000:141-154.
doi:10.1109/LICS.2000.855763'
apa: 'De Alfaro, L., & Henzinger, T. A. (2000). Concurrent omega-regular games.
In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science
(pp. 141–154). Santa Barbara, CA, USA: IEEE. https://doi.org/10.1109/LICS.2000.855763'
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Concurrent Omega-Regular Games.”
In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science,
141–54. IEEE, 2000. https://doi.org/10.1109/LICS.2000.855763.
ieee: L. De Alfaro and T. A. Henzinger, “Concurrent omega-regular games,” in Proceedings
of the 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara,
CA, USA, 2000, pp. 141–154.
ista: 'De Alfaro L, Henzinger TA. 2000. Concurrent omega-regular games. Proceedings
of the 15th Annual IEEE Symposium on Logic in Computer Science. LICS: Logic in
Computer Science, 141–154.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. “Concurrent Omega-Regular Games.”
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science,
IEEE, 2000, pp. 141–54, doi:10.1109/LICS.2000.855763.
short: L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 15th Annual IEEE Symposium
on Logic in Computer Science, IEEE, 2000, pp. 141–154.
conference:
end_date: 2000-06-28
location: Santa Barbara, CA, USA
name: 'LICS: Logic in Computer Science'
start_date: 2000-06-26
date_created: 2018-12-11T12:09:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T13:24:29Z
day: '01'
doi: 10.1109/LICS.2000.855763
extern: '1'
fulldoi: https://doi.org/10.1109/LICS.2000.855763
language:
- iso: eng
month: '01'
oa_version: None
page: 141 - 154
publication: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
isbn:
- '0769507255'
publication_status: published
publisher: IEEE
publist_id: '82'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Concurrent omega-regular games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...
---
_id: '4637'
abstract:
- lang: eng
text: "In the synchronous composition of processes, one process may prevent another
process from proceeding unless compositions without a well-defined product behavior
are ruled out. They can be ruled out semantically, by insisting on the existence
of certain fixed points, or syntactically, by equipping processes with types,
which make the dependencies between input and output signals transparent. We classify
various typing mechanisms and study their effects on the control problem.\r\nA
static type enforces fixed, acyclic dependencies between input and output ports.
For example, synchronous hardware without combinational loops can be typed statically.
A dynamic type may vary the dependencies from state to state, while maintaining
acyclicity, as in level-sensitive latches. Then, two dynamically typed processes
can be syntactically compatible, if all pairs of possible dependencies are compatible,
or semantically compatible, if in each state the combined dependencies remain
acyclic. For a given plant process and control objective, there may be a controller
of a static type, or only a controller of a syntactically compatible dynamic type,
or only a controller of a semantically compatible dynamic type. We show this to
be a strict hierarchy of possibilities, and we present algorithms and determine
the complexity of the corresponding control problems.\r\nFurthermore, we consider
versions of the control problem in which the type of the controller (static or
dynamic) is given. We show that the solution of these fixed-type control problems
requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas,
and is therefore harder (nondeterministic exponential time) than more traditional
control questions"
acknowledgement: This research was supported in part by the DARPA grants NAG2-1214
and F33615-C-98-3614, the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660,
and the NSF CAREER award CCR-9501708.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems. In:
Proceedings of the 11th International Conference on Concurrency Theory.
Vol 1877. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2000:458-473. doi:10.1007/3-540-44618-4_33'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). The control of synchronous
systems. In Proceedings of the 11th International Conference on Concurrency
Theory (Vol. 1877, pp. 458–473). University Park, PA, USA: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44618-4_33'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous
Systems.” In Proceedings of the 11th International Conference on Concurrency
Theory, 1877:458–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2000.
https://doi.org/10.1007/3-540-44618-4_33.
ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems,”
in Proceedings of the 11th International Conference on Concurrency Theory,
University Park, PA, USA, 2000, vol. 1877, pp. 458–473.
ista: 'De Alfaro L, Henzinger TA, Mang F. 2000. The control of synchronous systems.
Proceedings of the 11th International Conference on Concurrency Theory. CONCUR:
Concurrency Theory, LNCS, vol. 1877, 458–473.'
mla: De Alfaro, Luca, et al. “The Control of Synchronous Systems.” Proceedings
of the 11th International Conference on Concurrency Theory, vol. 1877, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2000, pp. 458–73, doi:10.1007/3-540-44618-4_33.
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 11th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2000, pp. 458–473.
conference:
end_date: 2000-08-25
location: University Park, PA, USA
name: 'CONCUR: Concurrency Theory'
start_date: 2000-08-22
date_created: 2018-12-11T12:09:53Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T11:00:46Z
day: '01'
doi: 10.1007/3-540-44618-4_33
extern: '1'
fulldoi: https://doi.org/10.1007/3-540-44618-4_33
intvolume: ' 1877'
language:
- iso: eng
month: '01'
oa_version: None
page: 458 - 473
publication: Proceedings of the 11th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540678977'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '69'
quality_controlled: '1'
status: public
title: The control of synchronous systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1877
year: '2000'
...
---
_id: '4638'
abstract:
- lang: eng
text: "Any formal method or tool is almost certainly more often applied in situations
where the outcome is failure (a counterexample) rather than success (a correctness
proof). We present a method for symbolic model checking that can lead to significant
time and memory savings for model-checking runs that fail, while occurring only
a small overhead for model-checking runs that succeed. Our method discovers an
error as soon as it cannot be prevented, which can be long before it actually
occurs; for example, the violation of an invariant may become unpreventable many
transitions before the invariant is violated.\r\nThe key observation is that “unpreventability”
is a local property of a single module: an error is unpreventable in a module
state if no environment can prevent it. Therefore, unpreventability is inexpensive
to compute for each module, yet can save much work in the state exploration of
the global, compound system. Based on different degrees of information available
about the environment, we define and implement several notions of “unpreventability,”
including the standard notion of uncontrollability from discrete-event control.
We present experimental results for two examples, a distributed database protocol
and a wireless communication protocol."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, the DARPA (MARCO) grant
MDA972-99-1-0001, and the NSF CAREER award CCR-9501708.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'De Alfaro L, Henzinger TA, Mang F. Detecting errors before reaching them.
In: Proceedings of the 12th International Conference on Computer Aided Verification.
Vol 1855. Springer; 2000:186-201. doi:10.1007/10722167_17'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). Detecting errors before
reaching them. In Proceedings of the 12th International Conference on Computer
Aided Verification (Vol. 1855, pp. 186–201). Chicago, IL, USA: Springer. https://doi.org/10.1007/10722167_17'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “Detecting Errors
before Reaching Them.” In Proceedings of the 12th International Conference
on Computer Aided Verification, 1855:186–201. Springer, 2000. https://doi.org/10.1007/10722167_17.
ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “Detecting errors before reaching
them,” in Proceedings of the 12th International Conference on Computer Aided
Verification, Chicago, IL, USA, 2000, vol. 1855, pp. 186–201.
ista: 'De Alfaro L, Henzinger TA, Mang F. 2000. Detecting errors before reaching
them. Proceedings of the 12th International Conference on Computer Aided Verification.
CAV: Computer-Aided Verification, LNCS, vol. 1855, 186–201.'
mla: De Alfaro, Luca, et al. “Detecting Errors before Reaching Them.” Proceedings
of the 12th International Conference on Computer Aided Verification, vol.
1855, Springer, 2000, pp. 186–201, doi:10.1007/10722167_17.
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International
Conference on Computer Aided Verification, Springer, 2000, pp. 186–201.
conference:
end_date: 2000-07-19
location: Chicago, IL, USA
name: 'CAV: Computer-Aided Verification'
start_date: 2000-07-15
date_created: 2018-12-11T12:09:53Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T13:18:06Z
day: '01'
doi: 10.1007/10722167_17
extern: '1'
fulldoi: https://doi.org/10.1007/10722167_17
intvolume: ' 1855'
language:
- iso: eng
month: '01'
oa_version: None
page: 186 - 201
publication: Proceedings of the 12th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540677703'
publication_status: published
publisher: Springer
publist_id: '70'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Detecting errors before reaching them
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1855
year: '2000'
...
---
_id: '842'
article_processing_charge: No
article_type: original
author:
- first_name: Yuri
full_name: Wolf, Yuri
last_name: Wolf
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Eugene
full_name: Koonin, Eugene
last_name: Koonin
citation:
ama: Wolf Y, Kondrashov F, Koonin E. No footprints of primordial introns in a eukaryotic
genome. Trends in Genetics. 2000;16(8):333-334. doi:10.1016/S0168-9525(00)02059-X
apa: Wolf, Y., Kondrashov, F., & Koonin, E. (2000). No footprints of primordial
introns in a eukaryotic genome. Trends in Genetics. Elsevier. https://doi.org/10.1016/S0168-9525(00)02059-X
chicago: Wolf, Yuri, Fyodor Kondrashov, and Eugene Koonin. “No Footprints of Primordial
Introns in a Eukaryotic Genome.” Trends in Genetics. Elsevier, 2000. https://doi.org/10.1016/S0168-9525(00)02059-X.
ieee: Y. Wolf, F. Kondrashov, and E. Koonin, “No footprints of primordial introns
in a eukaryotic genome,” Trends in Genetics, vol. 16, no. 8. Elsevier,
pp. 333–334, 2000.
ista: Wolf Y, Kondrashov F, Koonin E. 2000. No footprints of primordial introns
in a eukaryotic genome. Trends in Genetics. 16(8), 333–334.
mla: Wolf, Yuri, et al. “No Footprints of Primordial Introns in a Eukaryotic Genome.”
Trends in Genetics, vol. 16, no. 8, Elsevier, 2000, pp. 333–34, doi:10.1016/S0168-9525(00)02059-X.
short: Y. Wolf, F. Kondrashov, E. Koonin, Trends in Genetics 16 (2000) 333–334.
date_created: 2018-12-11T11:48:48Z
date_published: 2000-08-01T00:00:00Z
date_updated: 2023-05-08T09:22:03Z
day: '01'
doi: 10.1016/S0168-9525(00)02059-X
extern: '1'
external_id:
pmid:
- '10904260 '
fulldoi: https://doi.org/10.1016/S0168-9525(00)02059-X
intvolume: ' 16'
issue: '8'
language:
- iso: eng
month: '08'
oa_version: None
page: 333 - 334
pmid: 1
publication: Trends in Genetics
publication_identifier:
issn:
- 0168-9479
publication_status: published
publisher: Elsevier
publist_id: '6806'
quality_controlled: '1'
scopus_import: '1'
status: public
title: No footprints of primordial introns in a eukaryotic genome
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 16
year: '2000'
...
---
_id: '8525'
abstract:
- lang: eng
text: Let M be a smooth compact manifold of dimension at least 2 and Diffr(M) be
the space of C r smooth diffeomorphisms of M. Associate to each diffeomorphism
f;isin; Diffr(M) the sequence P n (f) of the number of isolated periodic points
for f of period n. In this paper we exhibit an open set N in the space of diffeomorphisms
Diffr(M) such for a Baire generic diffeomorphism f∈N the number of periodic points
P n f grows with a period n faster than any following sequence of numbers {a n
} n ∈ Z + along a subsequence, i.e. P n (f)>a ni for some n i →∞ with i→∞. In
the cases of surface diffeomorphisms, i.e. dim M≡2, an open set N with a supergrowth
of the number of periodic points is a Newhouse domain. A proof of the man result
is based on the Gontchenko–Shilnikov–Turaev Theorem [GST]. A complete proof of
that theorem is also presented.
article_processing_charge: No
article_type: original
author:
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
citation:
ama: Kaloshin V. Generic diffeomorphisms with superexponential growth of number
of periodic orbits. Communications in Mathematical Physics. 2000;211:253-271.
doi:10.1007/s002200050811
apa: Kaloshin, V. (2000). Generic diffeomorphisms with superexponential growth of
number of periodic orbits. Communications in Mathematical Physics. Springer
Nature. https://doi.org/10.1007/s002200050811
chicago: Kaloshin, Vadim. “Generic Diffeomorphisms with Superexponential Growth
of Number of Periodic Orbits.” Communications in Mathematical Physics.
Springer Nature, 2000. https://doi.org/10.1007/s002200050811.
ieee: V. Kaloshin, “Generic diffeomorphisms with superexponential growth of number
of periodic orbits,” Communications in Mathematical Physics, vol. 211.
Springer Nature, pp. 253–271, 2000.
ista: Kaloshin V. 2000. Generic diffeomorphisms with superexponential growth of
number of periodic orbits. Communications in Mathematical Physics. 211, 253–271.
mla: Kaloshin, Vadim. “Generic Diffeomorphisms with Superexponential Growth of Number
of Periodic Orbits.” Communications in Mathematical Physics, vol. 211,
Springer Nature, 2000, pp. 253–71, doi:10.1007/s002200050811.
short: V. Kaloshin, Communications in Mathematical Physics 211 (2000) 253–271.
date_created: 2020-09-18T10:50:20Z
date_published: 2000-04-01T00:00:00Z
date_updated: 2021-01-12T08:19:52Z
day: '01'
doi: 10.1007/s002200050811
extern: '1'
fulldoi: https://doi.org/10.1007/s002200050811
intvolume: ' 211'
keyword:
- Mathematical Physics
- Statistical and Nonlinear Physics
language:
- iso: eng
month: '04'
oa_version: None
page: 253-271
publication: Communications in Mathematical Physics
publication_identifier:
issn:
- 0010-3616
- 1432-0916
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Generic diffeomorphisms with superexponential growth of number of periodic
orbits
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 211
year: '2000'
...
---
_id: '3149'
abstract:
- lang: eng
text: The prohormone convertases (PCs) are an evolutionarily ancient group of proteases
required for the maturation of neuropeptide and peptide hormone precursors. In
Drosophila melanogaster, the homolog of prohormone convertase 2, dPC2 (amontillado),
is required for normal hatching behavior, and immunoblotting data indicate that
flies express 80- and 75-kDa forms of this protein. Because mouse PC2 (mPC2) requires
7B2, a helper protein for productive maturation, we searched the fly data base
for the 7B2 signature motif PPNPCP and identified an expressed sequence tag clone
encoding the entire open reading frame for this protein. dPC2 and d7B2 cDNAs were
subcloned into expression vectors for transfection into HEK-293 cells; mPC2 and
rat 7B2 were used as controls. Although active mPC2 was detected in medium in
the presence of either d7B2 or r7B2, dPC2 showed no proteolytic activity upon
coexpression of either d7B2 or r7B2. Labeling experiments showed that dPC2 was
synthesized but not secreted from HEK-293 cells. However, when dPC2 and either
d7B2 or r7B2 were coexpressed in Drosophila S2 cells, abundant immunoreactive
dPC2 was secreted into the medium, coincident with the appearance of PC2 activity.
Expression and secretion of dPC2 enzyme activity thus appears to require insect
cell-specific posttranslational processing events. The significant differences
in the cell biology of the insect and mammalian enzymes, with 7B2 absolutely required
for secretion of dPC2 and zymogen conversion occurring intracellularly in the
case of dPC2 but not mPC2, support the idea that the Drosophila enzyme has specific
requirements for maturation and secretion that can be met only in insect cells.
acknowledgement: This work was supported by National Institutes of Health Grants DK49703
(to I. L.), NS21749 (to P. H. T.), and GM39697 (to R. S. F.). The costs of publication
of this article were defrayed in part by the payment of page charges. This article
must therefore be hereby marked “advertisement” in accordance with 18 U.S.C. Section
1734 solely to indicate this fact. 10749852. We thank members of the Lindberg laboratory
and Laurent Muller for helpful comments, Bin Tu for construction of the C. elegans
PC2 expression vector, and Joelle Finley for assistance with cell culture.
article_processing_charge: No
article_type: original
author:
- first_name: Jae
full_name: Hwang, Jae
last_name: Hwang
- first_name: Daria E
full_name: Siekhaus, Daria E
id: 3D224B9E-F248-11E8-B48F-1D18A9856A87
last_name: Siekhaus
orcid: 0000-0001-8323-8353
- first_name: Robert
full_name: Fuller, Robert
last_name: Fuller
- first_name: Paul
full_name: Taghert, Paul
last_name: Taghert
- first_name: Iris
full_name: Lindberg, Iris
last_name: Lindberg
citation:
ama: 'Hwang J, Siekhaus DE, Fuller R, Taghert P, Lindberg I. Interaction of Drosophila
melanogaster prohormone convertase 2 and 7B2: Insect cell specific processing
and secretion. Journal of Biological Chemistry. 2000;275(23):17886-17893.
doi:10.1074/jbc.M000032200 '
apa: 'Hwang, J., Siekhaus, D. E., Fuller, R., Taghert, P., & Lindberg, I. (2000).
Interaction of Drosophila melanogaster prohormone convertase 2 and 7B2: Insect
cell specific processing and secretion. Journal of Biological Chemistry.
American Society for Biochemistry and Molecular Biology. https://doi.org/10.1074/jbc.M000032200 '
chicago: 'Hwang, Jae, Daria E Siekhaus, Robert Fuller, Paul Taghert, and Iris Lindberg.
“Interaction of Drosophila Melanogaster Prohormone Convertase 2 and 7B2: Insect
Cell Specific Processing and Secretion.” Journal of Biological Chemistry.
American Society for Biochemistry and Molecular Biology, 2000. https://doi.org/10.1074/jbc.M000032200 .'
ieee: 'J. Hwang, D. E. Siekhaus, R. Fuller, P. Taghert, and I. Lindberg, “Interaction
of Drosophila melanogaster prohormone convertase 2 and 7B2: Insect cell specific
processing and secretion,” Journal of Biological Chemistry, vol. 275, no.
23. American Society for Biochemistry and Molecular Biology, pp. 17886–17893,
2000.'
ista: 'Hwang J, Siekhaus DE, Fuller R, Taghert P, Lindberg I. 2000. Interaction
of Drosophila melanogaster prohormone convertase 2 and 7B2: Insect cell specific
processing and secretion. Journal of Biological Chemistry. 275(23), 17886–17893.'
mla: 'Hwang, Jae, et al. “Interaction of Drosophila Melanogaster Prohormone Convertase
2 and 7B2: Insect Cell Specific Processing and Secretion.” Journal of Biological
Chemistry, vol. 275, no. 23, American Society for Biochemistry and Molecular
Biology, 2000, pp. 17886–93, doi:10.1074/jbc.M000032200 .'
short: J. Hwang, D.E. Siekhaus, R. Fuller, P. Taghert, I. Lindberg, Journal of Biological
Chemistry 275 (2000) 17886–17893.
date_created: 2018-12-11T12:01:40Z
date_published: 2000-06-09T00:00:00Z
date_updated: 2023-05-03T08:47:13Z
day: '09'
doi: '10.1074/jbc.M000032200 '
extern: '1'
external_id:
pmid:
- '10749852'
fulldoi: 'https://doi.org/10.1074/jbc.M000032200 '
intvolume: ' 275'
issue: '23'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0021925819833215?via%3Dihub
month: '06'
oa: 1
oa_version: Published Version
page: 17886 - 17893
pmid: 1
publication: Journal of Biological Chemistry
publication_identifier:
issn:
- 0021-9258
publication_status: published
publisher: American Society for Biochemistry and Molecular Biology
publist_id: '3546'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Interaction of Drosophila melanogaster prohormone convertase 2 and 7B2: Insect
cell specific processing and secretion'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 275
year: '2000'
...
---
_id: '3489'
abstract:
- lang: eng
text: We have examined factors that determine the strength and dynamics of GABAergic
synapses between interneurons [dentate gyrus basket cells (BCs)] and principal
neurons [dentate gyrus granule cells (GCs)] using paired recordings in rat hippocampal
slices at 34°C. Unitary IPSCs recorded from BC–GC pairs in high intracellular
Cl− concentration showed a fast rise and a biexponential decay, with mean time
constants of 2 and 9 msec. The mean quantal conductance change, determined directly
at reduced extracellular Ca2+/Mg2+concentration ratios, was 1.7 nS. Quantal release
at the BC–GC synapse occurred with short delay and was highly synchronized. Analysis
of IPSC peak amplitudes and numbers of failures by multiple probability compound
binomial analysis indicated that synaptic transmission at the BC–GC synapse involves
three to seven release sites, each of which releases transmitter with high probability
(∼0.5 in 2 mMCa2+/1 mM Mg2+). Unitary BC–GC IPSCs showed paired-pulse depression
(PPD); maximal depression, measured for 10 msec intervals, was 37%, and recovery
from depression occurred with a time constant of 2 sec. Paired-pulse depression
was mainly presynaptic in origin but appeared to be independent of previous release.
Synaptic transmission at the BC–GC synapse showed frequency-dependent depression,
with half-maximal decrease at 5 Hz after a series of 1000 presynaptic action potentials.
The relative stability of transmission at the BC–GC synapse is consistent with
a model in which an activity-dependent gating mechanism reduces release probability
and thereby prevents depletion of the releasable pool of synaptic vesicles. Thus
several mechanisms converge on the generation of powerful and sustained transmission
at interneuron–principal neuron synapses in hippocampal circuits.
acknowledgement: This work was supported by grants from the Deutsche Forschungsgemeinschaft
(SFB 505/C5) and the Human Frontiers Science Program Organization (RG0017/1998-B)
to P.J. Novartis generously provided CGP55845A. We thank Drs. J. Bischofberger,
F. A. Edwards, J. R. P. Geiger, M. V. Jones, M. Martina, and A. Roth for critically
reading this manuscript. We also thank A. Blomenkamp for technical assistance.
article_processing_charge: No
article_type: original
author:
- first_name: Udo
full_name: Kraushaar, Udo
last_name: Kraushaar
- 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: Kraushaar U, Jonas PM. Efficacy and stability of quantal GABA release at a
hippocampal interneuron-principal neuron synapse. Journal of Neuroscience.
2000;20(15):5594-5607. doi:10.1523/JNEUROSCI.20-15-05594.2000
apa: Kraushaar, U., & Jonas, P. M. (2000). Efficacy and stability of quantal
GABA release at a hippocampal interneuron-principal neuron synapse. Journal
of Neuroscience. Society for Neuroscience. https://doi.org/10.1523/JNEUROSCI.20-15-05594.2000
chicago: Kraushaar, Udo, and Peter M Jonas. “Efficacy and Stability of Quantal GABA
Release at a Hippocampal Interneuron-Principal Neuron Synapse.” Journal of
Neuroscience. Society for Neuroscience, 2000. https://doi.org/10.1523/JNEUROSCI.20-15-05594.2000.
ieee: U. Kraushaar and P. M. Jonas, “Efficacy and stability of quantal GABA release
at a hippocampal interneuron-principal neuron synapse,” Journal of Neuroscience,
vol. 20, no. 15. Society for Neuroscience, pp. 5594–5607, 2000.
ista: Kraushaar U, Jonas PM. 2000. Efficacy and stability of quantal GABA release
at a hippocampal interneuron-principal neuron synapse. Journal of Neuroscience.
20(15), 5594–5607.
mla: Kraushaar, Udo, and Peter M. Jonas. “Efficacy and Stability of Quantal GABA
Release at a Hippocampal Interneuron-Principal Neuron Synapse.” Journal of
Neuroscience, vol. 20, no. 15, Society for Neuroscience, 2000, pp. 5594–607,
doi:10.1523/JNEUROSCI.20-15-05594.2000.
short: U. Kraushaar, P.M. Jonas, Journal of Neuroscience 20 (2000) 5594–5607.
date_created: 2018-12-11T12:03:36Z
date_published: 2000-08-01T00:00:00Z
date_updated: 2023-05-03T08:18:39Z
day: '01'
doi: 10.1523/JNEUROSCI.20-15-05594.2000
extern: '1'
external_id:
pmid:
- '10908596'
fulldoi: https://doi.org/10.1523/JNEUROSCI.20-15-05594.2000
intvolume: ' 20'
issue: '15'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6772523/
month: '08'
oa: 1
oa_version: Published Version
page: 5594 - 5607
pmid: 1
publication: Journal of Neuroscience
publication_identifier:
issn:
- 0270-6474
publication_status: published
publisher: Society for Neuroscience
publist_id: '2898'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficacy and stability of quantal GABA release at a hippocampal interneuron-principal
neuron synapse
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 20
year: '2000'
...
---
_id: '3490'
abstract:
- lang: eng
text: Long-term depression (LTD) is a form of synaptic plasticity that can be induced
either by low-frequency stimulation of presynaptic fibers or in an associative
manner by asynchronous pairing of presynaptic and postsynaptic activity. We investigated
the induction mechanisms of associative LTD in CA1 pyramidal neurons of the hippocampus
using whole-cell patch-clamp recordings and Ca2+ imaging in acute brain slices.
Asynchronous pairing of postsynaptic action potentials with EPSPs evoked with
a delay of 20 msec induced a robust, long-lasting depression of the EPSP amplitude
to 43%. Unlike LTD induced by low-frequency stimulation, associative LTD was resistant
to the application of D-AP-5, indicating that it is independent of NMDA receptors.
In contrast, associative LTD was inhibited by (S)-α-methyl-4-carboxyphenyl-glycine,
indicating the involvement of metabotropic glutamate receptors. Furthermore, associative
LTD is dependent on the activation of voltage-gated Ca2+ channels by postsynaptic
action potentials. Both nifedipine, an L-type Ca2+ channel antagonist, and ω-conotoxin
GVIA, a selective N-type channel blocker, abolished the induction of associative
LTD. 8-hydroxy-2-dipropylaminotetralin (OH-DPAT), a 5-HT(1A) receptor agonist,
inhibited postsynaptic Ca2+ influx through N-type Ca2+ channels, without affecting
presynaptic transmitter release. OH-DPAT also inhibited the induction of associative
LTD, suggesting that the involvement of N-type channels makes synaptic plasticity
accessible to modulation by neurotransmitters. Thus, the modulation of N-type
Ca2+ channels provides a gain control for synaptic depression in hippocampal pyramidal
neurons.
acknowledgement: This work was supported by a grant from the Deutsche Forschungsgemeinschaft
Bi 642/1–2 and University funds (J.B.) and by the Vada and Theodore Stanley Foundation
(J.W.). We thank Drs. M. Bartos, J. R. P. Geiger, and M. Martina for critically
reading this manuscript and A. Blomenkamp for technical assistance.
article_processing_charge: No
article_type: original
author:
- first_name: Claus
full_name: Normann, Claus
last_name: Normann
- first_name: Diana
full_name: Peckys, Diana
last_name: Peckys
- first_name: Christian
full_name: Schulze, Christian
last_name: Schulze
- first_name: Jörg
full_name: Walden, Jörg
last_name: Walden
- 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
citation:
ama: Normann C, Peckys D, Schulze C, Walden J, Jonas PM, Bischofberger J. Associative
long-term depression in the hippocampus is dependent on postsynaptic N-type Ca(2+)
channels. Journal of Neuroscience. 2000;20(22):8290-8297. doi:10.1523/JNEUROSCI.20-22-08290.2000
apa: Normann, C., Peckys, D., Schulze, C., Walden, J., Jonas, P. M., & Bischofberger,
J. (2000). Associative long-term depression in the hippocampus is dependent on
postsynaptic N-type Ca(2+) channels. Journal of Neuroscience. Society for
Neuroscience. https://doi.org/10.1523/JNEUROSCI.20-22-08290.2000
chicago: Normann, Claus, Diana Peckys, Christian Schulze, Jörg Walden, Peter M Jonas,
and Joseph Bischofberger. “Associative Long-Term Depression in the Hippocampus
Is Dependent on Postsynaptic N-Type Ca(2+) Channels.” Journal of Neuroscience.
Society for Neuroscience, 2000. https://doi.org/10.1523/JNEUROSCI.20-22-08290.2000.
ieee: C. Normann, D. Peckys, C. Schulze, J. Walden, P. M. Jonas, and J. Bischofberger,
“Associative long-term depression in the hippocampus is dependent on postsynaptic
N-type Ca(2+) channels,” Journal of Neuroscience, vol. 20, no. 22. Society
for Neuroscience, pp. 8290–8297, 2000.
ista: Normann C, Peckys D, Schulze C, Walden J, Jonas PM, Bischofberger J. 2000.
Associative long-term depression in the hippocampus is dependent on postsynaptic
N-type Ca(2+) channels. Journal of Neuroscience. 20(22), 8290–8297.
mla: Normann, Claus, et al. “Associative Long-Term Depression in the Hippocampus
Is Dependent on Postsynaptic N-Type Ca(2+) Channels.” Journal of Neuroscience,
vol. 20, no. 22, Society for Neuroscience, 2000, pp. 8290–97, doi:10.1523/JNEUROSCI.20-22-08290.2000.
short: C. Normann, D. Peckys, C. Schulze, J. Walden, P.M. Jonas, J. Bischofberger,
Journal of Neuroscience 20 (2000) 8290–8297.
date_created: 2018-12-11T12:03:36Z
date_published: 2000-11-15T00:00:00Z
date_updated: 2023-05-03T08:02:52Z
day: '15'
doi: 10.1523/JNEUROSCI.20-22-08290.2000
extern: '1'
external_id:
pmid:
- '11069935'
fulldoi: https://doi.org/10.1523/JNEUROSCI.20-22-08290.2000
intvolume: ' 20'
issue: '22'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6773198/
month: '11'
oa: 1
oa_version: Published Version
page: 8290 - 8297
pmid: 1
publication: Journal of Neuroscience
publication_identifier:
issn:
- 0270-6474
publication_status: published
publisher: Society for Neuroscience
publist_id: '2897'
quality_controlled: '1'
status: public
title: Associative long-term depression in the hippocampus is dependent on postsynaptic
N-type Ca(2+) channels
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 20
year: '2000'
...
---
_id: '3491'
abstract:
- lang: eng
text: Fast and reliable activation of inhibitory interneurons is critical for the
stability of cortical neuronal networks. Active conductances in dendrites may
facilitate interneuron activation, but direct experimental evidence was unavailable.
Patch-clamp recordings from dendrites of hippocampal oriens- alveus interneurons
revealed high densities of voltage-gated sodium and potassium ion channels. Simultaneous
recordings from dendrites and somata suggested that action potential initiation
occurs preferentially in the axon with long threshold stimuli, but can be shifted
to somatodendritic sites when brief stimuli are applied. After initiation, action
potentials propagate over the somatodendritic domain with constant amplitude,
high velocity, and reliability, even during high-frequency trains.
article_processing_charge: No
article_type: original
author:
- first_name: Marco
full_name: Martina, Marco
last_name: Martina
- first_name: Imre
full_name: Vida, Imre
last_name: Vida
- 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, Vida I, Jonas PM. Distal initiation and active propagation of action
potentials in interneuron dendrites. Science. 2000;287(5451):295-300. doi:10.1126/science.287.5451.295
apa: Martina, M., Vida, I., & Jonas, P. M. (2000). Distal initiation and active
propagation of action potentials in interneuron dendrites. Science. American
Association for the Advancement of Science. https://doi.org/10.1126/science.287.5451.295
chicago: Martina, Marco, Imre Vida, and Peter M Jonas. “Distal Initiation and Active
Propagation of Action Potentials in Interneuron Dendrites.” Science. American
Association for the Advancement of Science, 2000. https://doi.org/10.1126/science.287.5451.295.
ieee: M. Martina, I. Vida, and P. M. Jonas, “Distal initiation and active propagation
of action potentials in interneuron dendrites,” Science, vol. 287, no.
5451. American Association for the Advancement of Science, pp. 295–300, 2000.
ista: Martina M, Vida I, Jonas PM. 2000. Distal initiation and active propagation
of action potentials in interneuron dendrites. Science. 287(5451), 295–300.
mla: Martina, Marco, et al. “Distal Initiation and Active Propagation of Action
Potentials in Interneuron Dendrites.” Science, vol. 287, no. 5451, American
Association for the Advancement of Science, 2000, pp. 295–300, doi:10.1126/science.287.5451.295.
short: M. Martina, I. Vida, P.M. Jonas, Science 287 (2000) 295–300.
date_created: 2018-12-11T12:03:36Z
date_published: 2000-01-14T00:00:00Z
date_updated: 2023-05-03T07:55:32Z
day: '14'
doi: 10.1126/science.287.5451.295
extern: '1'
external_id:
pmid:
- '10634782'
fulldoi: https://doi.org/10.1126/science.287.5451.295
intvolume: ' 287'
issue: '5451'
language:
- iso: eng
month: '01'
oa_version: None
page: 295 - 300
pmid: 1
publication: Science
publication_identifier:
issn:
- 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '2896'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Distal initiation and active propagation of action potentials in interneuron
dendrites
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 287
year: '2000'
...
---
_id: '3492'
abstract:
- lang: eng
text: Analysis of presynaptic determinants of synaptic strength has been difficult
at cortical synapses, mainly due to the lack of direct access to presynaptic elements.
Here we report patch-clamp recordings from mossy fiber boutons (MFBs) in rat hippocampal
slices. The presynaptic action potential is very short during low-frequency stimulation
but is prolonged up to 3-fold during high-frequency stimulation. Voltage-gated
K+ channels in MFBs inactivate rapidly but recover from inactivation very slowly,
suggesting that cumulative K+ channel inactivation mediates activity-dependent
spike broadening. Prolongation of the presynaptic voltage waveform leads to an
increase in the number of Ca2+ ions entering the terminal per action potential
and to a consecutive potentiation of evoked excitatory postsynaptic currents at
MFB-CA3 pyramidal cell synapses. Thus, inactivation of presynaptic K+ channels
contributes to the control of efficacy of a glutamatergic synapse in the cortex.
article_processing_charge: No
article_type: original
author:
- first_name: Jörg
full_name: Geiger, Jörg
last_name: Geiger
- 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: Geiger J, Jonas PM. Dynamic control of presynaptic Ca(2+) inflow by fast-inactivating
K+ channels in hippocampal mossy fiber boutons. Neuron. 2000;28(3):927-939.
doi:10.1016/S0896-6273(00)00164-1
apa: Geiger, J., & Jonas, P. M. (2000). Dynamic control of presynaptic Ca(2+)
inflow by fast-inactivating K+ channels in hippocampal mossy fiber boutons. Neuron.
Elsevier. https://doi.org/10.1016/S0896-6273(00)00164-1
chicago: Geiger, Jörg, and Peter M Jonas. “Dynamic Control of Presynaptic Ca(2+)
Inflow by Fast-Inactivating K+ Channels in Hippocampal Mossy Fiber Boutons.” Neuron.
Elsevier, 2000. https://doi.org/10.1016/S0896-6273(00)00164-1.
ieee: J. Geiger and P. M. Jonas, “Dynamic control of presynaptic Ca(2+) inflow by
fast-inactivating K+ channels in hippocampal mossy fiber boutons,” Neuron,
vol. 28, no. 3. Elsevier, pp. 927–939, 2000.
ista: Geiger J, Jonas PM. 2000. Dynamic control of presynaptic Ca(2+) inflow by
fast-inactivating K+ channels in hippocampal mossy fiber boutons. Neuron. 28(3),
927–939.
mla: Geiger, Jörg, and Peter M. Jonas. “Dynamic Control of Presynaptic Ca(2+) Inflow
by Fast-Inactivating K+ Channels in Hippocampal Mossy Fiber Boutons.” Neuron,
vol. 28, no. 3, Elsevier, 2000, pp. 927–39, doi:10.1016/S0896-6273(00)00164-1.
short: J. Geiger, P.M. Jonas, Neuron 28 (2000) 927–939.
date_created: 2018-12-11T12:03:37Z
date_published: 2000-12-01T00:00:00Z
date_updated: 2023-05-02T14:34:37Z
day: '01'
doi: 10.1016/S0896-6273(00)00164-1
extern: '1'
external_id:
pmid:
- '11163277'
fulldoi: https://doi.org/10.1016/S0896-6273(00)00164-1
intvolume: ' 28'
issue: '3'
language:
- iso: eng
month: '12'
oa_version: None
page: 927 - 939
pmid: 1
publication: Neuron
publication_identifier:
issn:
- 0896-6273
publication_status: published
publisher: Elsevier
publist_id: '2895'
quality_controlled: '1'
status: public
title: Dynamic control of presynaptic Ca(2+) inflow by fast-inactivating K+ channels
in hippocampal mossy fiber boutons
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 28
year: '2000'
...
---
_id: '3532'
abstract:
- lang: eng
text: Multichannel tetrode array recording in awake behaving animals provides a
powerful method to record the activity of large numbers of neurons. The power
of this method could be extended if further information concerning the intracellular
state of the neurons could be extracted from the extracellularly recorded signals.
Toward this end, we have simultaneously recorded intracellular and extracellular
signals from hippocampal CA1 pyramidal cells and interneurons in the anesthetized
rat. We found that several intracellular parameters can be deduced from extracellular
spike waveforms. The width of the intracellular action potential is defined precisely
by distinct points on the extracellular spike. Amplitude changes of the intracellular
action potential are reflected by changes in the amplitude of the initial negative
phase of the extracellular spike, and these amplitude changes are dependent on
the state of the network. In addition, intracellular recordings from dendrites
with simultaneous extracellular recordings from the soma indicate that, on average,
action potentials are initiated in the perisomatic region and propagate to the
dendrites at 1.68 m/s. Finally we determined that a tetrode in hippocampal area
CA1 theoretically should be able to record electrical signals from similar to
1,000 neurons. Of these, 60-100 neurons should generate spikes of sufficient amplitude
to be detectable from the noise and to allow for their separation using current
spatial clustering methods. This theoretical maximum is in contrast to the approximately
six units that are usually detected per tetrode. From this, we conclude that a
large percentage of hippocampal CA1 pyramidal cells are silent in any given behavioral
condition.
acknowledgement: We thank M. Recce for comments on the manuscript and J. Hetke and
K.Wise for supplying us with the silicon probes (1P41RR09754).This work was supported
by National Institutes of Health Grants NS-34994,MH-54671, and MH-12403 (to D.
A. Henze), the Epilepsy Foundation of American (D. A.Henze), and an Eotvos fellowship
(Z. Borhegyi).
article_processing_charge: No
article_type: original
author:
- first_name: Darrell
full_name: Henze, Darrell
last_name: Henze
- first_name: Zsolt
full_name: Borhegyi, Zsolt
last_name: Borhegyi
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: Akira
full_name: Mamiya, Akira
last_name: Mamiya
- first_name: Kenneth
full_name: Harris, Kenneth
last_name: Harris
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Henze D, Borhegyi Z, Csicsvari JL, Mamiya A, Harris K, Buzsáki G. Intracellular
features predicted by extracellular recordings in the hippocampus in vivo. Journal
of Neurophysiology. 2000;84(1):390-400. doi:10.1152/jn.2000.84.1.390
apa: Henze, D., Borhegyi, Z., Csicsvari, J. L., Mamiya, A., Harris, K., & Buzsáki,
G. (2000). Intracellular features predicted by extracellular recordings in the
hippocampus in vivo. Journal of Neurophysiology. American Physiological
Society. https://doi.org/10.1152/jn.2000.84.1.390
chicago: Henze, Darrell, Zsolt Borhegyi, Jozsef L Csicsvari, Akira Mamiya, Kenneth
Harris, and György Buzsáki. “Intracellular Features Predicted by Extracellular
Recordings in the Hippocampus in Vivo.” Journal of Neurophysiology. American
Physiological Society, 2000. https://doi.org/10.1152/jn.2000.84.1.390.
ieee: D. Henze, Z. Borhegyi, J. L. Csicsvari, A. Mamiya, K. Harris, and G. Buzsáki,
“Intracellular features predicted by extracellular recordings in the hippocampus
in vivo,” Journal of Neurophysiology, vol. 84, no. 1. American Physiological
Society, pp. 390–400, 2000.
ista: Henze D, Borhegyi Z, Csicsvari JL, Mamiya A, Harris K, Buzsáki G. 2000. Intracellular
features predicted by extracellular recordings in the hippocampus in vivo. Journal
of Neurophysiology. 84(1), 390–400.
mla: Henze, Darrell, et al. “Intracellular Features Predicted by Extracellular Recordings
in the Hippocampus in Vivo.” Journal of Neurophysiology, vol. 84, no. 1,
American Physiological Society, 2000, pp. 390–400, doi:10.1152/jn.2000.84.1.390.
short: D. Henze, Z. Borhegyi, J.L. Csicsvari, A. Mamiya, K. Harris, G. Buzsáki,
Journal of Neurophysiology 84 (2000) 390–400.
date_created: 2018-12-11T12:03:49Z
date_published: 2000-07-01T00:00:00Z
date_updated: 2023-05-02T14:31:13Z
day: '01'
doi: 10.1152/jn.2000.84.1.390
extern: '1'
external_id:
pmid:
- '10899213'
fulldoi: https://doi.org/10.1152/jn.2000.84.1.390
intvolume: ' 84'
issue: '1'
language:
- iso: eng
month: '07'
oa_version: None
page: 390 - 400
pmid: 1
publication: Journal of Neurophysiology
publication_identifier:
issn:
- 0022-3077
publication_status: published
publisher: American Physiological Society
publist_id: '2854'
quality_controlled: '1'
status: public
title: Intracellular features predicted by extracellular recordings in the hippocampus
in vivo
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 84
year: '2000'
...
---
_id: '3542'
abstract:
- lang: eng
text: Transfer of neuronal patterns from the CA3 to CA1 region was studied by simultaneous
recording of neuronal ensembles in the behaving rat. A nonlinear interaction among
pyramidal neurons was observed during sharp wave (SPW)-related population bursts,
with stronger synchrony associated with more widespread spatial coherence. SPW
bursts emerged in the CA3a-b subregions and spread to CA3c before invading the
CA1 area. Synchronous discharge of >10% of the CA3 within a 100 ms window was
required to exert a detectable influence on CA1 pyramidal cells. Activity of some
CA3 pyramidal neurons differentially predicted the ripple-related discharge of
circumscribed groups of CA1 pyramidal cells. We suggest that, in SPW behavioral
state, the coherent discharge of a small group of CA3 cells is the primary cause
of spiking activity in CA1 pyramidal neurons.
article_processing_charge: No
article_type: original
author:
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: Hajima
full_name: Hirase, Hajima
last_name: Hirase
- first_name: Akira
full_name: Mamiya, Akira
last_name: Mamiya
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Csicsvari JL, Hirase H, Mamiya A, Buzsáki G. Ensemble patterns of hippocampal
CA3-CA1 neurons during sharp wave-associated population events. Neuron.
2000;28(2):585-594. doi:10.1016/S0896-6273(00)00135-5
apa: Csicsvari, J. L., Hirase, H., Mamiya, A., & Buzsáki, G. (2000). Ensemble
patterns of hippocampal CA3-CA1 neurons during sharp wave-associated population
events. Neuron. Elsevier. https://doi.org/10.1016/S0896-6273(00)00135-5
chicago: Csicsvari, Jozsef L, Hajima Hirase, Akira Mamiya, and György Buzsáki. “Ensemble
Patterns of Hippocampal CA3-CA1 Neurons during Sharp Wave-Associated Population
Events.” Neuron. Elsevier, 2000. https://doi.org/10.1016/S0896-6273(00)00135-5.
ieee: J. L. Csicsvari, H. Hirase, A. Mamiya, and G. Buzsáki, “Ensemble patterns
of hippocampal CA3-CA1 neurons during sharp wave-associated population events,”
Neuron, vol. 28, no. 2. Elsevier, pp. 585–594, 2000.
ista: Csicsvari JL, Hirase H, Mamiya A, Buzsáki G. 2000. Ensemble patterns of hippocampal
CA3-CA1 neurons during sharp wave-associated population events. Neuron. 28(2),
585–594.
mla: Csicsvari, Jozsef L., et al. “Ensemble Patterns of Hippocampal CA3-CA1 Neurons
during Sharp Wave-Associated Population Events.” Neuron, vol. 28, no. 2,
Elsevier, 2000, pp. 585–94, doi:10.1016/S0896-6273(00)00135-5.
short: J.L. Csicsvari, H. Hirase, A. Mamiya, G. Buzsáki, Neuron 28 (2000) 585–594.
date_created: 2018-12-11T12:03:52Z
date_published: 2000-11-01T00:00:00Z
date_updated: 2023-05-02T14:26:07Z
day: '01'
doi: 10.1016/S0896-6273(00)00135-5
extern: '1'
fulldoi: https://doi.org/10.1016/S0896-6273(00)00135-5
intvolume: ' 28'
issue: '2'
language:
- iso: eng
month: '11'
oa_version: None
page: 585 - 594
publication: Neuron
publication_identifier:
issn:
- 0896-6273
publication_status: published
publisher: Elsevier
publist_id: '2843'
quality_controlled: '1'
status: public
title: Ensemble patterns of hippocampal CA3-CA1 neurons during sharp wave-associated
population events
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 28
year: '2000'
...
---
_id: '3548'
abstract:
- lang: eng
text: Simultaneous recording from large numbers of neurons is a prerequisite for
understanding their cooperative behavior. Various recording techniques and spike
separation methods are being used toward this goal. However, the error rates involved
in spike separation have not yet been quantified. We studied the separation reliability
of “tetrode” (4-wire electrode) recorded spikes by monitoring simultaneously from
the same cell intracellularly with a glass pipette and extracellularly with a
tetrode. With manual spike sorting, we found a trade-off between Type I and Type
II errors, with errors typically ranging from 0 to 30% depending on the amplitude
and firing pattern of the cell, the similarity of the waveshapes of neighboring
neurons, and the experience of the operator. Performance using only a single wire
was markedly lower, indicating the advantages of multiple-site monitoring techniques
over single-wire recordings. For tetrode recordings, error rates were increased
by burst activity and during periods of cellular synchrony. The lowest possible
separation error rates were estimated by a search for the best ellipsoidal cluster
shape. Human operator performance was significantly below the estimated optimum.
Investigation of error distributions indicated that suboptimal performance was
caused by inability of the operators to mark cluster boundaries accurately in
a high-dimensional feature space. We therefore hypothesized that automatic spike-sorting
algorithms have the potential to significantly lower error rates. Implementation
of a semi-automatic classification system confirms this suggestion, reducing errors
close to the estimated optimum, in the range 0-8%.
acknowledgement: The costs of publication of this article were defrayed in part by
the payment of page charges. The article must therefore be hereby marked ‘‘advertisement’
’in accordance with 18 U.S.C. Section 1734 solely to indicate this fact. We thank
R. Bruno for performing cluster analysis and drawing our attention to the AutoClass
program, M. Recce and P. Mitra for suggestions withdata analysis and comments on
the manuscript, C. King, G. Dragoi, and X.Leinekugel for performing cluster analysis,
and J. Hetke and K. Wise for supplying silicon probes. The data used in this paper
are available on request by e-mail to G. Buzsaki. This work was supported by National
Institutes of Health Grants NS-34994,413 MH-54671, and MH-12403 (to D. A. Henze)
and by the Epilepsy Foundationof America (to D. A. Henze).
article_processing_charge: No
article_type: original
author:
- first_name: Kenneth
full_name: Harris, Kenneth
last_name: Harris
- first_name: Darrell
full_name: Henze, Darrell
last_name: Henze
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: Hajima
full_name: Hirase, Hajima
last_name: Hirase
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Harris K, Henze D, Csicsvari JL, Hirase H, Buzsáki G. Accuracy of tetrode spike
separation as determined by simultaneous intracellular and extracellular measurements.
Journal of Neurophysiology. 2000;84(1):401-414. doi:10.1152/jn.2000.84.1.401
apa: Harris, K., Henze, D., Csicsvari, J. L., Hirase, H., & Buzsáki, G. (2000).
Accuracy of tetrode spike separation as determined by simultaneous intracellular
and extracellular measurements. Journal of Neurophysiology. American Physiological
Society. https://doi.org/10.1152/jn.2000.84.1.401
chicago: Harris, Kenneth, Darrell Henze, Jozsef L Csicsvari, Hajima Hirase, and
György Buzsáki. “Accuracy of Tetrode Spike Separation as Determined by Simultaneous
Intracellular and Extracellular Measurements.” Journal of Neurophysiology.
American Physiological Society, 2000. https://doi.org/10.1152/jn.2000.84.1.401.
ieee: K. Harris, D. Henze, J. L. Csicsvari, H. Hirase, and G. Buzsáki, “Accuracy
of tetrode spike separation as determined by simultaneous intracellular and extracellular
measurements,” Journal of Neurophysiology, vol. 84, no. 1. American Physiological
Society, pp. 401–414, 2000.
ista: Harris K, Henze D, Csicsvari JL, Hirase H, Buzsáki G. 2000. Accuracy of tetrode
spike separation as determined by simultaneous intracellular and extracellular
measurements. Journal of Neurophysiology. 84(1), 401–414.
mla: Harris, Kenneth, et al. “Accuracy of Tetrode Spike Separation as Determined
by Simultaneous Intracellular and Extracellular Measurements.” Journal of Neurophysiology,
vol. 84, no. 1, American Physiological Society, 2000, pp. 401–14, doi:10.1152/jn.2000.84.1.401.
short: K. Harris, D. Henze, J.L. Csicsvari, H. Hirase, G. Buzsáki, Journal of Neurophysiology
84 (2000) 401–414.
date_created: 2018-12-11T12:03:54Z
date_published: 2000-07-01T00:00:00Z
date_updated: 2023-05-02T14:16:45Z
day: '01'
doi: 10.1152/jn.2000.84.1.401
extern: '1'
external_id:
pmid:
- '10899214 '
fulldoi: https://doi.org/10.1152/jn.2000.84.1.401
intvolume: ' 84'
issue: '1'
language:
- iso: eng
month: '07'
oa_version: None
page: 401 - 414
pmid: 1
publication: Journal of Neurophysiology
publication_identifier:
issn:
- 0022-3077
publication_status: published
publisher: American Physiological Society
publist_id: '2837'
quality_controlled: '1'
status: public
title: Accuracy of tetrode spike separation as determined by simultaneous intracellular
and extracellular measurements
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 84
year: '2000'
...
---
_id: '3555'
abstract:
- lang: eng
text: A sliver is a tetrahedron whose four vertices lie close to a plane and whose
perpendicular projection to that plane is a convex quadrilateral with no short
edge. Slivers are both undesirable and ubiquitous in 3-dimensional Delaunay triangulations.
Even when the point-set is well-spaced, slivers may result. This paper shows that
such a point set permits a small perturbation whose Delaunay triangulation contains
no slivers. It also gives deterministic algorithms that compute the perturbation
of n points in time O(n log n) with one processor and in time O(log n) with O(n)
processors.
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: Xiang
full_name: Li, Xiang
id: 4B7E523C-F248-11E8-B48F-1D18A9856A87
last_name: Li
- first_name: Gary
full_name: Miller, Gary
last_name: Miller
- first_name: Andreas
full_name: Stathopoulos, Andreas
last_name: Stathopoulos
- first_name: Dafna
full_name: Talmor, Dafna
last_name: Talmor
- first_name: Shang
full_name: Teng, Shang
last_name: Teng
- first_name: Alper
full_name: Üngör, Alper
last_name: Üngör
- first_name: Noel
full_name: Walkington, Noel
last_name: Walkington
citation:
ama: 'Edelsbrunner H, Li X, Miller G, et al. Smoothing and cleaning up slivers.
In: Proceedings of the 32nd Annual ACM Symposium on Theory of Computing.
ACM; 2000:273-277. doi:10.1145/335305.335338'
apa: 'Edelsbrunner, H., Li, X., Miller, G., Stathopoulos, A., Talmor, D., Teng,
S., … Walkington, N. (2000). Smoothing and cleaning up slivers. In Proceedings
of the 32nd annual ACM symposium on Theory of computing (pp. 273–277). Portland,
OR, USA: ACM. https://doi.org/10.1145/335305.335338'
chicago: Edelsbrunner, Herbert, Xiang Li, Gary Miller, Andreas Stathopoulos, Dafna
Talmor, Shang Teng, Alper Üngör, and Noel Walkington. “Smoothing and Cleaning
up Slivers.” In Proceedings of the 32nd Annual ACM Symposium on Theory of Computing,
273–77. ACM, 2000. https://doi.org/10.1145/335305.335338.
ieee: H. Edelsbrunner et al., “Smoothing and cleaning up slivers,” in Proceedings
of the 32nd annual ACM symposium on Theory of computing, Portland, OR, USA,
2000, pp. 273–277.
ista: 'Edelsbrunner H, Li X, Miller G, Stathopoulos A, Talmor D, Teng S, Üngör A,
Walkington N. 2000. Smoothing and cleaning up slivers. Proceedings of the 32nd
annual ACM symposium on Theory of computing. STOC: Symposium on the Theory of
Computing, 273–277.'
mla: Edelsbrunner, Herbert, et al. “Smoothing and Cleaning up Slivers.” Proceedings
of the 32nd Annual ACM Symposium on Theory of Computing, ACM, 2000, pp. 273–77,
doi:10.1145/335305.335338.
short: H. Edelsbrunner, X. Li, G. Miller, A. Stathopoulos, D. Talmor, S. Teng, A.
Üngör, N. Walkington, in:, Proceedings of the 32nd Annual ACM Symposium on Theory
of Computing, ACM, 2000, pp. 273–277.
conference:
end_date: 2000-05-23
location: Portland, OR, USA
name: 'STOC: Symposium on the Theory of Computing'
start_date: 2000-05-21
date_created: 2018-12-11T12:03:56Z
date_published: 2000-06-01T00:00:00Z
date_updated: 2023-05-02T14:07:00Z
day: '01'
doi: 10.1145/335305.335338
extern: '1'
fulldoi: https://doi.org/10.1145/335305.335338
language:
- iso: eng
month: '06'
oa_version: None
page: 273 - 277
publication: Proceedings of the 32nd annual ACM symposium on Theory of computing
publication_identifier:
isbn:
- '9781581131840'
publication_status: published
publisher: ACM
publist_id: '2830'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Smoothing and cleaning up slivers
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...
---
_id: '3572'
abstract:
- lang: eng
text: "Allzulange wurde die spielhafte Beschäftigung als Gegensatz zu ernsthafter
Arbeit gesehen. Dieser Artikel propagiert die spielerische Untersuchung von Kreis-
und Kugelmengen. Gleichzeitig belegt er die nutzbare Anwendung\r\nvon elementaren
Einsichten in der Molekularbiologie und allgemeiner\r\nin der Beschreibung von
Form und Verformung."
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
citation:
ama: 'Edelsbrunner H. Spielereien mit Kreisen und Kugeln. Zum Thema Form und Verformung.
In: Zur Kunst Des Formalen Denkens. Passagen Verlag; 2000:153-171.'
apa: Edelsbrunner, H. (2000). Spielereien mit Kreisen und Kugeln. Zum Thema Form
und Verformung. In Zur Kunst des formalen Denkens (pp. 153–171). Passagen
Verlag.
chicago: Edelsbrunner, Herbert. “Spielereien Mit Kreisen Und Kugeln. Zum Thema Form
Und Verformung.” In Zur Kunst Des Formalen Denkens, 153–71. Passagen Verlag,
2000.
ieee: H. Edelsbrunner, “Spielereien mit Kreisen und Kugeln. Zum Thema Form und Verformung,”
in Zur Kunst des formalen Denkens, Passagen Verlag, 2000, pp. 153–171.
ista: 'Edelsbrunner H. 2000.Spielereien mit Kreisen und Kugeln. Zum Thema Form und
Verformung. In: Zur Kunst des formalen Denkens. , 153–171.'
mla: Edelsbrunner, Herbert. “Spielereien Mit Kreisen Und Kugeln. Zum Thema Form
Und Verformung.” Zur Kunst Des Formalen Denkens, Passagen Verlag, 2000,
pp. 153–71.
short: H. Edelsbrunner, in:, Zur Kunst Des Formalen Denkens, Passagen Verlag, 2000,
pp. 153–171.
date_created: 2018-12-11T12:04:01Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-05-02T13:07:14Z
day: '01'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 153 - 171
publication: Zur Kunst des formalen Denkens
publication_identifier:
isbn:
- '3851653580'
publication_status: published
publisher: Passagen Verlag
publist_id: '2813'
quality_controlled: '1'
status: public
title: Spielereien mit Kreisen und Kugeln. Zum Thema Form und Verformung
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...
---
_id: '3583'
abstract:
- lang: eng
text: The Delaunay triangulation of a finite point set is a central theme in computational
geometry. It finds its major application in the generation of meshes used in the
simulation of physical processes. This paper connects the predominantly combinatorial
work in classical computational geometry with the numerical interest in mesh generation.
It focuses on the two- and three-dimensional case and covers results obtained
during the twentieth century.
acknowledgement: Research is partially supported by the Army Research Office under
grant DAAG55-98-1-0177 and by the National Science Foundation under grants CCR-96-19542
and CCR-97-12088.
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
citation:
ama: Edelsbrunner H. Triangulations and meshes in computational geometry. Acta
Numerica. 2000;9:133-213. doi:10.1017/S0962492900001331
apa: Edelsbrunner, H. (2000). Triangulations and meshes in computational geometry.
Acta Numerica. Cambridge University Press. https://doi.org/10.1017/S0962492900001331
chicago: Edelsbrunner, Herbert. “Triangulations and Meshes in Computational Geometry.”
Acta Numerica. Cambridge University Press, 2000. https://doi.org/10.1017/S0962492900001331.
ieee: H. Edelsbrunner, “Triangulations and meshes in computational geometry,” Acta
Numerica, vol. 9. Cambridge University Press, pp. 133–213, 2000.
ista: Edelsbrunner H. 2000. Triangulations and meshes in computational geometry.
Acta Numerica. 9, 133–213.
mla: Edelsbrunner, Herbert. “Triangulations and Meshes in Computational Geometry.”
Acta Numerica, vol. 9, Cambridge University Press, 2000, pp. 133–213, doi:10.1017/S0962492900001331.
short: H. Edelsbrunner, Acta Numerica 9 (2000) 133–213.
date_created: 2018-12-11T12:04:05Z
date_published: 2000-03-21T00:00:00Z
date_updated: 2023-05-02T12:20:27Z
day: '21'
doi: 10.1017/S0962492900001331
extern: '1'
fulldoi: https://doi.org/10.1017/S0962492900001331
intvolume: ' 9'
language:
- iso: eng
month: '03'
oa_version: None
page: 133 - 213
publication: Acta Numerica
publication_status: published
publisher: Cambridge University Press
publist_id: '2802'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Triangulations and meshes in computational geometry
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 9
year: '2000'
...