---
_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'
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'
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'
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'
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'
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'
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'
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'
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'
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: '8527'
abstract:
- lang: eng
text: We introduce a new potential-theoretic definition of the dimension spectrum of
a probability measure for q > 1 and explain its relation to prior definitions.
We apply this definition to prove that if and is a Borel probability measure
with compact support in , then under almost every linear transformation from to
, the q-dimension of the image of is ; in particular, the q-dimension of is
preserved provided . We also present results on the preservation of information
dimension and pointwise dimension. Finally, for and q > 2 we give examples for
which is not preserved by any linear transformation into . All results for typical
linear transformations are also proved for typical (in the sense of prevalence)
continuously differentiable functions.
article_processing_charge: No
article_type: original
author:
- first_name: Brian R
full_name: Hunt, Brian R
last_name: Hunt
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
citation:
ama: Hunt BR, Kaloshin V. How projections affect the dimension spectrum of fractal
measures. Nonlinearity. 1997;10(5):1031-1046. doi:10.1088/0951-7715/10/5/002
apa: Hunt, B. R., & Kaloshin, V. (1997). How projections affect the dimension
spectrum of fractal measures. Nonlinearity. IOP Publishing. https://doi.org/10.1088/0951-7715/10/5/002
chicago: Hunt, Brian R, and Vadim Kaloshin. “How Projections Affect the Dimension
Spectrum of Fractal Measures.” Nonlinearity. IOP Publishing, 1997. https://doi.org/10.1088/0951-7715/10/5/002.
ieee: B. R. Hunt and V. Kaloshin, “How projections affect the dimension spectrum
of fractal measures,” Nonlinearity, vol. 10, no. 5. IOP Publishing, pp.
1031–1046, 1997.
ista: Hunt BR, Kaloshin V. 1997. How projections affect the dimension spectrum of
fractal measures. Nonlinearity. 10(5), 1031–1046.
mla: Hunt, Brian R., and Vadim Kaloshin. “How Projections Affect the Dimension Spectrum
of Fractal Measures.” Nonlinearity, vol. 10, no. 5, IOP Publishing, 1997,
pp. 1031–46, doi:10.1088/0951-7715/10/5/002.
short: B.R. Hunt, V. Kaloshin, Nonlinearity 10 (1997) 1031–1046.
date_created: 2020-09-18T10:50:41Z
date_published: 1997-06-19T00:00:00Z
date_updated: 2021-01-12T08:19:53Z
day: '19'
doi: 10.1088/0951-7715/10/5/002
extern: '1'
intvolume: ' 10'
issue: '5'
keyword:
- Mathematical Physics
- General Physics and Astronomy
- Applied Mathematics
- Statistical and Nonlinear Physics
language:
- iso: eng
month: '06'
oa_version: None
page: 1031-1046
publication: Nonlinearity
publication_identifier:
issn:
- 0951-7715
- 1361-6544
publication_status: published
publisher: IOP Publishing
quality_controlled: '1'
status: public
title: How projections affect the dimension spectrum of fractal measures
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '1997'
...
---
_id: '8528'
abstract:
- lang: eng
text: "In the present paper, we give a definition of prevalent (\"metrically prevalent\"
) sets in nonlinear function\r\nspaces. A subset of a Euclidean space is said
to be metrically prevalent if its complement has measure zero.\r\nThere is no
natural way to generalize the definition of a set of measure zero in a finite-dimensional
space\r\nto the infinite-dimensional case [6]. Therefore, it is necessary to give
a special definition of a metrically\r\nprevalent set (set of full measure) in
an infinite-dimensional space. There are various ways to do so. We\r\nsuggest
one of the possible ways to define the class of metrically prevalent sets in the
space of smooth maps\r\nof one smooth manifold into another. It is shown in this
paper that the class of metrically prevalent sets\r\nhas natural properties; in
particular, the intersection of finitely many metrically prevalent sets is metrically\r\nprevalent.
The main result of the paper is a prevalent version of Thorn's transversality
theorem.\r\nIt is common practice in singularity theory and the theory of dynamical
systems to say that a property\r\nholds for \"almost every\" map (or flow) if
it holds for a residual set, i.e., a set that contains a countable\r\nintersection
of open dense sets in the corresponding function space. However, even in finite-dimensional\r\nspaces
such a set can have arbitrarily small (say, zero) Lebesgue measure. We prove that
Thorn's transversality theorem holds for an essentially \"thicker\" set than a
residual set. It seems reasonable to revise from\r\nthe prevalent point of view
the classical results of singularity theory and theory of dynamical systems,\r\nincluding
the multijet transversality theorem, Mather's stability theorem, Kupka-Smale's
theorem for dynamical systems, etc. We shall do this elsewhere. The notion of
prevalence in linear Banach spaces was\r\nintroduced and investigated in [8].
One of the possible ways to define a class of prevalent sets in the space\r\nof
smooth maps of manifolds, which essentially differs from that presented in this
paper, is given in [7].\r\nDefinitions of typicalness based on the Lebesgue measure
in a finite-dimensional space were suggested\r\nby Kolmogorov [10] and Arnold
[11]. These definitions were cited and discussed in [9]. Here we only point\r\nout
that the finite-dimensional analog of Arnold's definition allows prevalent sets
to have arbitrarily small\r\nmeasure, whereas the prevalent sets in the sense
of the finite-dimensional analog of the definition given in\r\nthe present paper
are necessarily of full measure. Our definition is a modification of that due
to Arnold.\r\nI wish to thank Yu. S. Illyashenko for constant attention to this
work and useful discussions and\r\nR. I. Bogdanov for help in the preparation
of this paper. "
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. Prevalence in the space of finitely smooth maps. Functional
Analysis and Its Applications. 1997;31(2):95-99. doi:10.1007/bf02466014
apa: Kaloshin, V. (1997). Prevalence in the space of finitely smooth maps. Functional
Analysis and Its Applications. Springer Nature. https://doi.org/10.1007/bf02466014
chicago: Kaloshin, Vadim. “Prevalence in the Space of Finitely Smooth Maps.” Functional
Analysis and Its Applications. Springer Nature, 1997. https://doi.org/10.1007/bf02466014.
ieee: V. Kaloshin, “Prevalence in the space of finitely smooth maps,” Functional
Analysis and Its Applications, vol. 31, no. 2. Springer Nature, pp. 95–99,
1997.
ista: Kaloshin V. 1997. Prevalence in the space of finitely smooth maps. Functional
Analysis and Its Applications. 31(2), 95–99.
mla: Kaloshin, Vadim. “Prevalence in the Space of Finitely Smooth Maps.” Functional
Analysis and Its Applications, vol. 31, no. 2, Springer Nature, 1997, pp.
95–99, doi:10.1007/bf02466014.
short: V. Kaloshin, Functional Analysis and Its Applications 31 (1997) 95–99.
date_created: 2020-09-18T10:50:54Z
date_published: 1997-03-30T00:00:00Z
date_updated: 2021-01-12T08:19:54Z
day: '30'
doi: 10.1007/bf02466014
extern: '1'
intvolume: ' 31'
issue: '2'
keyword:
- Applied Mathematics
- Analysis
language:
- iso: eng
month: '03'
oa_version: None
page: 95-99
publication: Functional Analysis and Its Applications
publication_identifier:
issn:
- 0016-2663
- 1573-8485
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Prevalence in the space of finitely smooth maps
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 31
year: '1997'
...
---
_id: '11666'
abstract:
- lang: eng
text: This article describes the Digital Continuous Profiling Infrastructure, a
sampling-based profiling system designed to run continuously on production systems.
The system supports multiprocessors, works on unmodified executables, and collects
profiles for entire systems, including user programs, shared libraries, and the
operating system kernel. Samples are collected at a high rate (over 5200 samples/sec.
per 333MHz processor), yet with low overhead (1–3% slowdown for most workloads).
Analysis tools supplied with the profiling system use the sample data to produce
a precise and accurate accounting, down to the level of pipeline stalls incurred
by individual instructions, of where time is bring spent. When instructions incur
stalls, the tools identify possible reasons, such as cache misses, branch mispredictions,
and functional unit contention. The fine-grained instruction-level analysis guides
users and automated optimizers to the causes of performance problems and provides
important insights for fixing them.
acknowledgement: We would like to thank Mike Burrows, Allan Heydon, Hal Murray, Sharon
Perl, and Sharon Smith for helpful comments that greatly improved the content and
presentation of this article; the anonymous referees for SOSP and TOCS also provided
numerous helpful comments. We would also like to thank Dawson Engler for initially
suggesting the use of interprocessor interrupts to avoid expensive synchronization
operations in the interrupt handler, Mitch Lichtenberg for his work on the Alpha/NT
version of our system and in general for his help and suggestions on the project,
and the developers of iprobe for supplying us with source code that helped us get
off the ground in building the early versions of our data collection system. Finally,
we would like to thank Gary Carleton and Bob Davies of Intel for answering our questions
about VTune and Marty Itzkowitz of SGI for answering our questions about SpeedShop.
article_processing_charge: No
article_type: original
author:
- first_name: Jennifer M.
full_name: Anderson, Jennifer M.
last_name: Anderson
- first_name: Lance M.
full_name: Berc, Lance M.
last_name: Berc
- first_name: Jeffrey
full_name: Dean, Jeffrey
last_name: Dean
- first_name: Sanjay
full_name: Ghemawat, Sanjay
last_name: Ghemawat
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Shun-Tak A.
full_name: Leung, Shun-Tak A.
last_name: Leung
- first_name: Richard L.
full_name: Sites, Richard L.
last_name: Sites
- first_name: Mark T.
full_name: Vandevoorde, Mark T.
last_name: Vandevoorde
- first_name: Carl A.
full_name: Waldspurger, Carl A.
last_name: Waldspurger
- first_name: William E.
full_name: Weihl, William E.
last_name: Weihl
citation:
ama: 'Anderson JM, Berc LM, Dean J, et al. Continuous profiling: Where have all
the cycles gone? ACM Transactions on Computer Systems. 1997;15(4):357-390.
doi:10.1145/265924.265925'
apa: 'Anderson, J. M., Berc, L. M., Dean, J., Ghemawat, S., Henzinger, M. H., Leung,
S.-T. A., … Weihl, W. E. (1997). Continuous profiling: Where have all the cycles
gone? ACM Transactions on Computer Systems. Association for Computing Machinery.
https://doi.org/10.1145/265924.265925'
chicago: 'Anderson, Jennifer M., Lance M. Berc, Jeffrey Dean, Sanjay Ghemawat, Monika
H Henzinger, Shun-Tak A. Leung, Richard L. Sites, Mark T. Vandevoorde, Carl A.
Waldspurger, and William E. Weihl. “Continuous Profiling: Where Have All the Cycles
Gone?” ACM Transactions on Computer Systems. Association for Computing
Machinery, 1997. https://doi.org/10.1145/265924.265925.'
ieee: 'J. M. Anderson et al., “Continuous profiling: Where have all the cycles
gone?,” ACM Transactions on Computer Systems, vol. 15, no. 4. Association
for Computing Machinery, pp. 357–390, 1997.'
ista: 'Anderson JM, Berc LM, Dean J, Ghemawat S, Henzinger MH, Leung S-TA, Sites
RL, Vandevoorde MT, Waldspurger CA, Weihl WE. 1997. Continuous profiling: Where
have all the cycles gone? ACM Transactions on Computer Systems. 15(4), 357–390.'
mla: 'Anderson, Jennifer M., et al. “Continuous Profiling: Where Have All the Cycles
Gone?” ACM Transactions on Computer Systems, vol. 15, no. 4, Association
for Computing Machinery, 1997, pp. 357–90, doi:10.1145/265924.265925.'
short: J.M. Anderson, L.M. Berc, J. Dean, S. Ghemawat, M.H. Henzinger, S.-T.A. Leung,
R.L. Sites, M.T. Vandevoorde, C.A. Waldspurger, W.E. Weihl, ACM Transactions on
Computer Systems 15 (1997) 357–390.
date_created: 2022-07-27T11:42:25Z
date_published: 1997-11-01T00:00:00Z
date_updated: 2022-09-09T12:00:13Z
day: '01'
doi: 10.1145/265924.265925
extern: '1'
intvolume: ' 15'
issue: '4'
language:
- iso: eng
month: '11'
oa_version: None
page: 357-390
publication: ACM Transactions on Computer Systems
publication_identifier:
eissn:
- 1557-7333
issn:
- 0734-2071
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Continuous profiling: Where have all the cycles gone?'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '1997'
...
---
_id: '11765'
abstract:
- lang: eng
text: This paper presents insertions-only algorithms for maintaining the exact and/or
approximate size of the minimum edge cut and the minimum vertex cut of a graph.
The algorithms output the approximate or exact sizekin timeO(1) and a cut of sizekin
time linear in its size. For the minimum edge cut problem and for any 0 < ε ≤
1, the amortized time per insertion isO(1/ε2) for a (2 + ε)-approximation,O((log
λ)((log n)/ε)2) for a (1 + ε)-approximation, andO(λ log n) for the exact size,
wherenis the number of nodes in the graph and λ is the size of the minimum cut.
The (2 + ε)-approximation algorithm and the exact algorithm are deterministic;
the (1 + ε)-approximation algorithm is randomized. We also present a static 2-approximation
algorithm for the size κ of the minimum vertex cut in a graph, which takes time.
This is a factor of κ faster than the best algorithm for computing the exact size,
which takes time. We give an insertions-only algorithm for maintaining a (2 +
ε)-approximation of the minimum vertex cut with amortized insertion timeO(n/ε).
article_processing_charge: No
article_type: original
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
citation:
ama: Henzinger MH. A static 2-approximation algorithm for vertex connectivity and
incremental approximation algorithms for edge and vertex connectivity. Journal
of Algorithms. 1997;24(1):194-220. doi:10.1006/jagm.1997.0855
apa: Henzinger, M. H. (1997). A static 2-approximation algorithm for vertex connectivity
and incremental approximation algorithms for edge and vertex connectivity. Journal
of Algorithms. Elsevier. https://doi.org/10.1006/jagm.1997.0855
chicago: Henzinger, Monika H. “A Static 2-Approximation Algorithm for Vertex Connectivity
and Incremental Approximation Algorithms for Edge and Vertex Connectivity.” Journal
of Algorithms. Elsevier, 1997. https://doi.org/10.1006/jagm.1997.0855.
ieee: M. H. Henzinger, “A static 2-approximation algorithm for vertex connectivity
and incremental approximation algorithms for edge and vertex connectivity,” Journal
of Algorithms, vol. 24, no. 1. Elsevier, pp. 194–220, 1997.
ista: Henzinger MH. 1997. A static 2-approximation algorithm for vertex connectivity
and incremental approximation algorithms for edge and vertex connectivity. Journal
of Algorithms. 24(1), 194–220.
mla: Henzinger, Monika H. “A Static 2-Approximation Algorithm for Vertex Connectivity
and Incremental Approximation Algorithms for Edge and Vertex Connectivity.” Journal
of Algorithms, vol. 24, no. 1, Elsevier, 1997, pp. 194–220, doi:10.1006/jagm.1997.0855.
short: M.H. Henzinger, Journal of Algorithms 24 (1997) 194–220.
date_created: 2022-08-08T12:18:38Z
date_published: 1997-07-01T00:00:00Z
date_updated: 2022-09-12T09:15:38Z
day: '01'
doi: 10.1006/jagm.1997.0855
extern: '1'
intvolume: ' 24'
issue: '1'
language:
- iso: eng
month: '07'
oa_version: None
page: 194-220
publication: Journal of Algorithms
publication_identifier:
issn:
- 0196-6774
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: A static 2-approximation algorithm for vertex connectivity and incremental
approximation algorithms for edge and vertex connectivity
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 24
year: '1997'
...
---
_id: '11767'
abstract:
- lang: eng
text: We give a linear-time algorithm for single-source shortest paths in planar
graphs with nonnegative edge-lengths. Our algorithm also yields a linear-time
algorithm for maximum flow in a planar graph with the source and sink on the same
face. For the case where negative edge-lengths are allowed, we give an algorithm
requiringO(n4/3 log(nL)) time, whereLis the absolute value of the most negative
length. This algorithm can be used to obtain similar bounds for computing a feasible
flow in a planar network, for finding a perfect matching in a planar bipartite
graph, and for finding a maximum flow in a planar graph when the source and sink
are not on the same face. We also give parallel and dynamic versions of these
algorithms.
article_processing_charge: No
article_type: original
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Philip
full_name: Klein, Philip
last_name: Klein
- first_name: Satish
full_name: Rao, Satish
last_name: Rao
- first_name: Sairam
full_name: Subramanian, Sairam
last_name: Subramanian
citation:
ama: Henzinger MH, Klein P, Rao S, Subramanian S. Faster shortest-path algorithms
for planar graphs. Journal of Computer and System Sciences. 1997;55(1):3-23.
doi:10.1006/jcss.1997.1493
apa: Henzinger, M. H., Klein, P., Rao, S., & Subramanian, S. (1997). Faster
shortest-path algorithms for planar graphs. Journal of Computer and System
Sciences. Elsevier. https://doi.org/10.1006/jcss.1997.1493
chicago: Henzinger, Monika H, Philip Klein, Satish Rao, and Sairam Subramanian.
“Faster Shortest-Path Algorithms for Planar Graphs.” Journal of Computer and
System Sciences. Elsevier, 1997. https://doi.org/10.1006/jcss.1997.1493.
ieee: M. H. Henzinger, P. Klein, S. Rao, and S. Subramanian, “Faster shortest-path
algorithms for planar graphs,” Journal of Computer and System Sciences,
vol. 55, no. 1. Elsevier, pp. 3–23, 1997.
ista: Henzinger MH, Klein P, Rao S, Subramanian S. 1997. Faster shortest-path algorithms
for planar graphs. Journal of Computer and System Sciences. 55(1), 3–23.
mla: Henzinger, Monika H., et al. “Faster Shortest-Path Algorithms for Planar Graphs.”
Journal of Computer and System Sciences, vol. 55, no. 1, Elsevier, 1997,
pp. 3–23, doi:10.1006/jcss.1997.1493.
short: M.H. Henzinger, P. Klein, S. Rao, S. Subramanian, Journal of Computer and
System Sciences 55 (1997) 3–23.
date_created: 2022-08-08T12:28:45Z
date_published: 1997-08-01T00:00:00Z
date_updated: 2022-09-12T10:46:21Z
day: '01'
doi: 10.1006/jcss.1997.1493
extern: '1'
intvolume: ' 55'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1006/jcss.1997.1493
month: '08'
oa: 1
oa_version: Published Version
page: 3-23
publication: Journal of Computer and System Sciences
publication_identifier:
issn:
- 0022-0000
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster shortest-path algorithms for planar graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '1997'
...
---
_id: '11803'
abstract:
- lang: eng
text: We present the first fully dynamic algorithm for maintaining a minimum spanning
tree in time o(√n) per operation. To be precise, the algorithm uses O(n 1/3 log
n) amortized time per update operation. The algorithm is fairly simple and deterministic.
An immediate consequence is the first fully dynamic deterministic algorithm for
maintaining connectivity and, bipartiteness in amortized time O(n 1/3 log n) per
update, with O(1) worst case time per query.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Valerie
full_name: King, Valerie
last_name: King
citation:
ama: 'Henzinger MH, King V. Maintaining minimum spanning trees in dynamic graphs.
In: 24th International Colloquium on Automata, Languages and Programming.
Vol 1256. Springer Nature; 1997:594–604. doi:10.1007/3-540-63165-8_214'
apa: 'Henzinger, M. H., & King, V. (1997). Maintaining minimum spanning trees
in dynamic graphs. In 24th International Colloquium on Automata, Languages
and Programming (Vol. 1256, pp. 594–604). Bologna, Italy: Springer Nature.
https://doi.org/10.1007/3-540-63165-8_214'
chicago: Henzinger, Monika H, and Valerie King. “Maintaining Minimum Spanning Trees
in Dynamic Graphs.” In 24th International Colloquium on Automata, Languages
and Programming, 1256:594–604. Springer Nature, 1997. https://doi.org/10.1007/3-540-63165-8_214.
ieee: M. H. Henzinger and V. King, “Maintaining minimum spanning trees in dynamic
graphs,” in 24th International Colloquium on Automata, Languages and Programming,
Bologna, Italy, 1997, vol. 1256, pp. 594–604.
ista: 'Henzinger MH, King V. 1997. Maintaining minimum spanning trees in dynamic
graphs. 24th International Colloquium on Automata, Languages and Programming.
ICALP: International Colloquium on Automata, Languages, and Programming, LNCS,
vol. 1256, 594–604.'
mla: Henzinger, Monika H., and Valerie King. “Maintaining Minimum Spanning Trees
in Dynamic Graphs.” 24th International Colloquium on Automata, Languages and
Programming, vol. 1256, Springer Nature, 1997, pp. 594–604, doi:10.1007/3-540-63165-8_214.
short: M.H. Henzinger, V. King, in:, 24th International Colloquium on Automata,
Languages and Programming, Springer Nature, 1997, pp. 594–604.
conference:
end_date: 1997-07-11
location: Bologna, Italy
name: 'ICALP: International Colloquium on Automata, Languages, and Programming'
start_date: 1997-07-07
date_created: 2022-08-11T13:35:06Z
date_published: 1997-07-01T00:00:00Z
date_updated: 2023-02-14T07:49:03Z
day: '01'
doi: 10.1007/3-540-63165-8_214
extern: '1'
intvolume: ' 1256'
language:
- iso: eng
month: '07'
oa_version: None
page: 594–604
publication: 24th International Colloquium on Automata, Languages and Programming
publication_identifier:
eisbn:
- '9783540691945'
eissn:
- 1611-3349
isbn:
- '9783540631651'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Maintaining minimum spanning trees in dynamic graphs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 1256
year: '1997'
...
---
_id: '11849'
abstract:
- lang: eng
text: "This paper describes the DIGlTAL Continuous Profiling Infrastmcture, a sampling-based
profiling system designed to run continuously on production systems. The system
supports multiprocessors, works on unmodified executable& and collects profiles
for entire systems, including user programs, shared libraries, and the operating
system kernel. Samples are collected at a high rate (over 5200 samples/secper333-MHz
processor), yet with low overhead (l-3% slowdown for most workloads). Analysis
tools supplied with the profiling system use the sample data to produce an accurate
accounting, down to the level of pipeline stalls incurred by individual instructions,
of where time is being spent. When instructions incur stalls, the tools identify
possible reasons, such as cache misses, branch mispredictions, and functional
unit contention. The fine-grained instruction-level analysis guides users and
automated optimizers to the causes of performance\r\nproblems and provides important
insights for fixing them. "
article_processing_charge: No
article_type: original
author:
- first_name: Jennifer M.
full_name: Anderson, Jennifer M.
last_name: Anderson
- first_name: Lance M.
full_name: Berc, Lance M.
last_name: Berc
- first_name: Jeffrey
full_name: Dean, Jeffrey
last_name: Dean
- first_name: Sanjay
full_name: Ghemawat, Sanjay
last_name: Ghemawat
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Shun-Tak A.
full_name: Leung, Shun-Tak A.
last_name: Leung
- first_name: Richard L.
full_name: Sites, Richard L.
last_name: Sites
- first_name: Mark T.
full_name: Vandevoorde, Mark T.
last_name: Vandevoorde
- first_name: Carl A.
full_name: Waldspurger, Carl A.
last_name: Waldspurger
- first_name: William E.
full_name: Weihl, William E.
last_name: Weihl
citation:
ama: 'Anderson JM, Berc LM, Dean J, et al. Continuous profiling: Where have all
the cycles gone? ACM SIGOPS Operating Systems Review. 1997;31(5):1-14.
doi:10.1145/269005.266637'
apa: 'Anderson, J. M., Berc, L. M., Dean, J., Ghemawat, S., Henzinger, M. H., Leung,
S.-T. A., … Weihl, W. E. (1997). Continuous profiling: Where have all the cycles
gone? ACM SIGOPS Operating Systems Review. Association for Computing Machinery.
https://doi.org/10.1145/269005.266637'
chicago: 'Anderson, Jennifer M., Lance M. Berc, Jeffrey Dean, Sanjay Ghemawat, Monika
H Henzinger, Shun-Tak A. Leung, Richard L. Sites, Mark T. Vandevoorde, Carl A.
Waldspurger, and William E. Weihl. “Continuous Profiling: Where Have All the Cycles
Gone?” ACM SIGOPS Operating Systems Review. Association for Computing Machinery,
1997. https://doi.org/10.1145/269005.266637.'
ieee: 'J. M. Anderson et al., “Continuous profiling: Where have all the cycles
gone?,” ACM SIGOPS Operating Systems Review, vol. 31, no. 5. Association
for Computing Machinery, pp. 1–14, 1997.'
ista: 'Anderson JM, Berc LM, Dean J, Ghemawat S, Henzinger MH, Leung S-TA, Sites
RL, Vandevoorde MT, Waldspurger CA, Weihl WE. 1997. Continuous profiling: Where
have all the cycles gone? ACM SIGOPS Operating Systems Review. 31(5), 1–14.'
mla: 'Anderson, Jennifer M., et al. “Continuous Profiling: Where Have All the Cycles
Gone?” ACM SIGOPS Operating Systems Review, vol. 31, no. 5, Association
for Computing Machinery, 1997, pp. 1–14, doi:10.1145/269005.266637.'
short: J.M. Anderson, L.M. Berc, J. Dean, S. Ghemawat, M.H. Henzinger, S.-T.A. Leung,
R.L. Sites, M.T. Vandevoorde, C.A. Waldspurger, W.E. Weihl, ACM SIGOPS Operating
Systems Review 31 (1997) 1–14.
date_created: 2022-08-16T07:07:03Z
date_published: 1997-12-01T00:00:00Z
date_updated: 2023-02-21T16:30:27Z
day: '01'
doi: 10.1145/269005.266637
extern: '1'
intvolume: ' 31'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/269005.266637
month: '12'
oa: 1
oa_version: Published Version
page: 1-14
publication: ACM SIGOPS Operating Systems Review
publication_identifier:
issn:
- 0163-5980
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '11849'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'Continuous profiling: Where have all the cycles gone?'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 31
year: '1997'
...
---
_id: '11883'
abstract:
- lang: eng
text: 'In dynamic graph algorithms the following provide-or-bound problem has to
be solved quickly: Given a set S containing a subset R and a way of generating
random elements from S testing for membership in R, either (i) provide an element
of R, or (ii) give a (small) upper bound on the size of R that holds with high
probability. We give an optimal algorithm for this problem. This algorithm improves
the time per operation for various dynamic graph algorithms by a factor of O(log n).
For example, it improves the time per update for fully dynamic connectivity from
O(log3n) to O(log2n).'
article_processing_charge: No
article_type: original
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Mikkel
full_name: Thorup, Mikkel
last_name: Thorup
citation:
ama: 'Henzinger MH, Thorup M. Sampling to provide or to bound: With applications
to fully dynamic graph algorithms. Random Structures and Algorithms. 1997;11(4):369-379.
doi:10.1002/(sici)1098-2418(199712)11:4<369::aid-rsa5>3.0.co;2-x'
apa: 'Henzinger, M. H., & Thorup, M. (1997). Sampling to provide or to bound:
With applications to fully dynamic graph algorithms. Random Structures and
Algorithms. Wiley. https://doi.org/10.1002/(sici)1098-2418(199712)11:4<369::aid-rsa5>3.0.co;2-x'
chicago: 'Henzinger, Monika H, and Mikkel Thorup. “Sampling to Provide or to Bound:
With Applications to Fully Dynamic Graph Algorithms.” Random Structures and
Algorithms. Wiley, 1997. https://doi.org/10.1002/(sici)1098-2418(199712)11:4<369::aid-rsa5>3.0.co;2-x.'
ieee: 'M. H. Henzinger and M. Thorup, “Sampling to provide or to bound: With applications
to fully dynamic graph algorithms,” Random Structures and Algorithms, vol.
11, no. 4. Wiley, pp. 369–379, 1997.'
ista: 'Henzinger MH, Thorup M. 1997. Sampling to provide or to bound: With applications
to fully dynamic graph algorithms. Random Structures and Algorithms. 11(4), 369–379.'
mla: 'Henzinger, Monika H., and Mikkel Thorup. “Sampling to Provide or to Bound:
With Applications to Fully Dynamic Graph Algorithms.” Random Structures and
Algorithms, vol. 11, no. 4, Wiley, 1997, pp. 369–79, doi:10.1002/(sici)1098-2418(199712)11:4<369::aid-rsa5>3.0.co;2-x.'
short: M.H. Henzinger, M. Thorup, Random Structures and Algorithms 11 (1997) 369–379.
date_created: 2022-08-17T07:21:55Z
date_published: 1997-12-07T00:00:00Z
date_updated: 2023-02-17T14:05:02Z
day: '07'
doi: 10.1002/(sici)1098-2418(199712)11:4<369::aid-rsa5>3.0.co;2-x
extern: '1'
intvolume: ' 11'
issue: '4'
language:
- iso: eng
month: '12'
oa_version: None
page: 369-379
publication: Random Structures and Algorithms
publication_identifier:
eissn:
- 1098-2418
issn:
- 1042-9832
publication_status: published
publisher: Wiley
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Sampling to provide or to bound: With applications to fully dynamic graph
algorithms'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 11
year: '1997'
...
---
_id: '2493'
abstract:
- lang: eng
text: 'A specific antiserum against substance P receptor (SPR) labels nonprincipal
neurons in the cerebral cortex of the rat (T. Kaneko et al. [1994], Neuroscience
60:199-211; Y. Nakaya et al. [1994], J. Comp. Neurol. 347:249-274). In the present
study, we aimed to identify the types of SPR- immunoreactive neurons in the hippocampus
according to their content of neurochemical markers, which label interneuron populations
with distinct termination patterns. Markers for perisomatic inhibitory cells,
parvalbumin and cholecystokinin (CCK), colocalized with SPR in pyramidallike basket
cells in the dentate gyrus and in large multipolar or bitufted cells within all
hippocampal subfields respectively. A dense meshwork of SPR-immunoreactive spiny
dendrites in the hilus and stratum lucidum of the CA3 region belonged largely
to inhibitory cells terminating in the distal dendritic region of granule cells,
as indicated by the somatostatin and neuropeptide Y (NPY) content. In addition,
SPR and NPY were colocalized in numerous multipolar interneurons with dendrites
branching close to the soma. Twenty-five percent of the SPR-immunoreactive cells
overlapped with calretinin-positive neurons in all hippocampal subfields, showing
that interneurons specialized to contact other gamma-aminobutyric acid-ergic cells
may also contain SPR. On the basis of the known termination pattern of the colocalized
markers, we conclude that SPR-positive interneurons are functionally heterogeneous
and participate in different inhibitory processes: (1) perisomatic inhibition
of principal cells (CCK-containing cells, and parvalbumin-positive cells in the
dentate gyrus), (2) feedback dendritic inhibition in the entorhinal termination
zone (somatostatin and NPY-containing cells), and (3) innervation of other interneurons
(calretinin-containing cells).'
acknowledgement: This sudy was supported by grants from the Human Frontier Science
Program Organisation, the Howard Hughes Medical Institute, and OTKA (T 16942) Hungary.We
are grateful to Dr. K.G. Baimbridge and to Dr. M.R.Celio (calbindin and parvalbumin),
Dr. T. Go ̈rcs (CCK, VIP,NPY, and somatostatin), Dr. J.H. Rogers (calretinin), andDr.
C.G. Beaulieau (GABA) for kind gifts of antisera. The excellent technical assistance
of Mrs. E. Borok, Mrs. A.Z.Szabo, and Mr. G. Terstyanszky is also acknowledged
article_processing_charge: No
article_type: original
author:
- first_name: László
full_name: Acsády, László
last_name: Acsády
- first_name: István
full_name: Katona, István
last_name: Katona
- first_name: Attila
full_name: Gulyás, Attila
last_name: Gulyás
- first_name: Ryuichi
full_name: Shigemoto, Ryuichi
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Tamás
full_name: Freund, Tamás
last_name: Freund
citation:
ama: Acsády L, Katona I, Gulyás A, Shigemoto R, Freund T. Immunostaining for substance
P receptor labels GABAergic cells with distinct termination patterns in the hippocampus.
Journal of Comparative Neurology. 1997;378(3):320-336. doi:10.1002/(SICI)1096-9861(19970217)378:3<320::AID-CNE2>3.0.CO;2-5
apa: Acsády, L., Katona, I., Gulyás, A., Shigemoto, R., & Freund, T. (1997).
Immunostaining for substance P receptor labels GABAergic cells with distinct termination
patterns in the hippocampus. Journal of Comparative Neurology. Wiley-Blackwell.
https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3<320::AID-CNE2>3.0.CO;2-5
chicago: Acsády, László, István Katona, Attila Gulyás, Ryuichi Shigemoto, and Tamás
Freund. “Immunostaining for Substance P Receptor Labels GABAergic Cells with Distinct
Termination Patterns in the Hippocampus.” Journal of Comparative Neurology.
Wiley-Blackwell, 1997. https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3<320::AID-CNE2>3.0.CO;2-5.
ieee: L. Acsády, I. Katona, A. Gulyás, R. Shigemoto, and T. Freund, “Immunostaining
for substance P receptor labels GABAergic cells with distinct termination patterns
in the hippocampus,” Journal of Comparative Neurology, vol. 378, no. 3.
Wiley-Blackwell, pp. 320–336, 1997.
ista: Acsády L, Katona I, Gulyás A, Shigemoto R, Freund T. 1997. Immunostaining
for substance P receptor labels GABAergic cells with distinct termination patterns
in the hippocampus. Journal of Comparative Neurology. 378(3), 320–336.
mla: Acsády, László, et al. “Immunostaining for Substance P Receptor Labels GABAergic
Cells with Distinct Termination Patterns in the Hippocampus.” Journal of Comparative
Neurology, vol. 378, no. 3, Wiley-Blackwell, 1997, pp. 320–36, doi:10.1002/(SICI)1096-9861(19970217)378:3<320::AID-CNE2>3.0.CO;2-5.
short: L. Acsády, I. Katona, A. Gulyás, R. Shigemoto, T. Freund, Journal of Comparative
Neurology 378 (1997) 320–336.
date_created: 2018-12-11T11:57:59Z
date_published: 1997-02-17T00:00:00Z
date_updated: 2022-08-22T13:43:18Z
day: '17'
doi: 10.1002/(SICI)1096-9861(19970217)378:3<320::AID-CNE2>3.0.CO;2-5
extern: '1'
external_id:
pmid:
- '9034894'
intvolume: ' 378'
issue: '3'
language:
- iso: eng
month: '02'
oa_version: None
page: 320 - 336
pmid: 1
publication: Journal of Comparative Neurology
publication_identifier:
issn:
- 0021-9967
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4408'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Immunostaining for substance P receptor labels GABAergic cells with distinct
termination patterns in the hippocampus
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 378
year: '1997'
...
---
_id: '2575'
abstract:
- lang: eng
text: It was examined electron microscopically in the rat if a metabotropic glutamate
receptor, mGluR7, might be localized in axon terminals of nociceptive, primary
afferent fibers in laminae I and II of the spinal dorsal horn. Nociceptive nature
of axon terminals showing mGluR7-like immunoreactivity (mGluR7-LI) was indicated
by binding to the isolectin I-B4 from Griffonia simplicifolia (I-B4), or by substance
P-like immunoreactivity (SP-LI). Axon terminals labeled with immunogold particles
indicating mGluR7-LI were usually filled with round synaptic vesicles and were
in asymmetric synaptic contact with dendritic or somatic profiles; occasionally
they contained pleomorphic vesicles and were in symmetric synaptic contact with
somatic profiles in lamina II. The double-labeling studies revealed that most
of axon terminals with I-B4 labeling as well as a small population of axon terminals
with SP-LI, showed mGluR7-LI. About one-third or much smaller population of axon
terminals with mGluR7-LI in laminae I and II were labeled, respectively, with
I-B4 or SP-LI; these were in asymmetric synaptic contact with dendritic profiles.
acknowledgement: We are grateful for photographic help of Mr. Akira Uesugi. We also
express our gratitude for the support of Drs. Satoru Fukuchi, Ritsu Hayashi, Sohzaburo
Hayashi, Mizuho Katsurada, Hitoshi Kawai, Yutaka Kitani, Toshihiko Kuroda, Keiko
Kumagai, Hiroshi Matsubara, Hiroshi Matsushima, Chisato Minakuchi, Gonpei Niwa,
Hajime Oda, Masahiko Ohbayashi, Sei-ichi Ohbayashi, Hiroyasu Ohtsuka, Shigeo Tamaki,
Eizo Watanabe, Kazuo Yoshino, and Toshiaki Yoshino. This work was supported in part
by Grant-in-Aid from Ministry of Education, Science, Culture and Sports of Japan.
article_processing_charge: No
article_type: original
author:
- first_name: He
full_name: Li, He
last_name: Li
- first_name: Hitoshi
full_name: Ohishi, Hitoshi
last_name: Ohishi
- first_name: Ayae
full_name: Kinoshita, Ayae
last_name: Kinoshita
- first_name: Ryuichi
full_name: Shigemoto, Ryuichi
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Sakashi
full_name: Nomura, Sakashi
last_name: Nomura
- first_name: Noboru
full_name: Mizuno, Noboru
last_name: Mizuno
citation:
ama: 'Li H, Ohishi H, Kinoshita A, Shigemoto R, Nomura S, Mizuno N. Localization
of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive,
primary afferent fibers in the superficial layers of the spinal dorsal horn: An
electron microscope study in the rat. Neuroscience Letters. 1997;223(3):153-156.
doi:10.1016/S0304-3940(97)13429-2'
apa: 'Li, H., Ohishi, H., Kinoshita, A., Shigemoto, R., Nomura, S., & Mizuno,
N. (1997). Localization of a metabotropic glutamate receptor, mGluR7, in axon
terminals of presumed nociceptive, primary afferent fibers in the superficial
layers of the spinal dorsal horn: An electron microscope study in the rat. Neuroscience
Letters. Elsevier. https://doi.org/10.1016/S0304-3940(97)13429-2'
chicago: 'Li, He, Hitoshi Ohishi, Ayae Kinoshita, Ryuichi Shigemoto, Sakashi Nomura,
and Noboru Mizuno. “Localization of a Metabotropic Glutamate Receptor, MGluR7,
in Axon Terminals of Presumed Nociceptive, Primary Afferent Fibers in the Superficial
Layers of the Spinal Dorsal Horn: An Electron Microscope Study in the Rat.” Neuroscience
Letters. Elsevier, 1997. https://doi.org/10.1016/S0304-3940(97)13429-2.'
ieee: 'H. Li, H. Ohishi, A. Kinoshita, R. Shigemoto, S. Nomura, and N. Mizuno, “Localization
of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive,
primary afferent fibers in the superficial layers of the spinal dorsal horn: An
electron microscope study in the rat,” Neuroscience Letters, vol. 223,
no. 3. Elsevier, pp. 153–156, 1997.'
ista: 'Li H, Ohishi H, Kinoshita A, Shigemoto R, Nomura S, Mizuno N. 1997. Localization
of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive,
primary afferent fibers in the superficial layers of the spinal dorsal horn: An
electron microscope study in the rat. Neuroscience Letters. 223(3), 153–156.'
mla: 'Li, He, et al. “Localization of a Metabotropic Glutamate Receptor, MGluR7,
in Axon Terminals of Presumed Nociceptive, Primary Afferent Fibers in the Superficial
Layers of the Spinal Dorsal Horn: An Electron Microscope Study in the Rat.” Neuroscience
Letters, vol. 223, no. 3, Elsevier, 1997, pp. 153–56, doi:10.1016/S0304-3940(97)13429-2.'
short: H. Li, H. Ohishi, A. Kinoshita, R. Shigemoto, S. Nomura, N. Mizuno, Neuroscience
Letters 223 (1997) 153–156.
date_created: 2018-12-11T11:58:28Z
date_published: 1997-02-28T00:00:00Z
date_updated: 2022-08-22T13:06:30Z
day: '28'
doi: 10.1016/S0304-3940(97)13429-2
extern: '1'
external_id:
pmid:
- '9080455'
intvolume: ' 223'
issue: '3'
language:
- iso: eng
month: '02'
oa_version: None
page: 153 - 156
pmid: 1
publication: Neuroscience Letters
publication_identifier:
issn:
- 0304-3940
publication_status: published
publisher: Elsevier
publist_id: '4322'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals
of presumed nociceptive, primary afferent fibers in the superficial layers of the
spinal dorsal horn: An electron microscope study in the rat'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 223
year: '1997'
...
---
_id: '2576'
abstract:
- lang: eng
text: Primary afferent neurons containing substance P (SP) are apparently implicated
in the transmission of noxious information from the periphery to the central nervous
system, and SP released from primary afferent neurons acts on second-order neurons
with the SP receptor (SPR). In the rat, nociceptive information reached the hypothalamus
not only through indirect pathways but also directly through trigeminohypothalamic
and spinohypothalamic pathways. Thus, in the present study, the distribution pattern
of trigeminohypothalamic and spinohypothalamic tract neurons showing SPR-like
immunoreactivity (SPR-LI) was examined in the rat by a retrograde tract-tracing
method combined with immunofluorescence histochemistry for SPR. A substantial
number of trigeminal and spinal neurons with SPR-LI were retrogradely labeled
with Fluore-Gold (FG) injected into the hypothalamic regions. These neurons were
distributed mainly in lamina I of the medullary and spinal dorsal horns, lateral
spinal nucleus, regions around the central canal of the spinal cord, and the lateral
aspect of the deep part of the spinal dorsal horn. A number of SPR-LI neurons
in the spinal parasympathetic nucleus were labeled with FG injected into the area
around the paraventricular hypothalamic nucleus. Some SPR-LI neurons in the lateral
spinal nucleus and the lateral aspect of the deep part of the spinal dorsal horn
were also labeled with FG injected into the septal region. On the basis of the
distribution areas of SPR-LI trigeminal and spinal neurons projecting to the hypothalamic
and septal regions, it is likely that these neurons are involved in the transmission
of somatic and/or visceral noxious information.
acknowledgement: This study was supported by grants 08279106 and 08458245 from the
Ministry of Education, Science, Sportsand Culture of Japan. We are grateful for
the photographic help of Mr. Akira Uesugi and the support of Dr. Kajitaro Morita
in Morita Clinic of Internal Medicine and Pediatrics, Kadoma, Osaka, Japan. We also
express our gratitude for the support of Drs. Satoru Fukuchi, Ritsu Hayashi,Sohzaburo
Hayashi, Mizuho Katsurada, Hitoski Kawai,Yutaka Kitani, Toshihiko Kuroda, Keiko
Kumagai, Hiroshi Matsubara, Hiroshi Matsushima, Chisato Minakuchi,Gonpei Niwa, Hajime
Oda, Mashiko Ohbayashi, Seiichi Ohbayashi, Hiroyasu Ohtsuka, Shigeo Tamaki, EizoWatanabe,
Kazuo Yoshino, and Toshiaki Yoshino.
article_processing_charge: No
article_type: original
author:
- first_name: Jin
full_name: Li, Jin
last_name: Li
- first_name: Takeshi
full_name: Kaneko, Takeshi
last_name: Kaneko
- first_name: Ryuichi
full_name: Shigemoto, Ryuichi
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Noboru
full_name: Mizuno, Noboru
last_name: Mizuno
citation:
ama: Li J, Kaneko T, Shigemoto R, Mizuno N. Distribution of trigeminohypothalamic
and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity
in the rat. Journal of Comparative Neurology. 1997;378(4):508-521. doi:10.1002/(SICI)1096-9861(19970224)378:4<508::AID-CNE6>3.0.CO;2-6
apa: Li, J., Kaneko, T., Shigemoto, R., & Mizuno, N. (1997). Distribution of
trigeminohypothalamic and spinohypothalamic tract neurons displaying substance
P receptor-like immunoreactivity in the rat. Journal of Comparative Neurology.
Wiley-Blackwell. https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4<508::AID-CNE6>3.0.CO;2-6
chicago: Li, Jin, Takeshi Kaneko, Ryuichi Shigemoto, and Noboru Mizuno. “Distribution
of Trigeminohypothalamic and Spinohypothalamic Tract Neurons Displaying Substance
P Receptor-like Immunoreactivity in the Rat.” Journal of Comparative Neurology.
Wiley-Blackwell, 1997. https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4<508::AID-CNE6>3.0.CO;2-6.
ieee: J. Li, T. Kaneko, R. Shigemoto, and N. Mizuno, “Distribution of trigeminohypothalamic
and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity
in the rat,” Journal of Comparative Neurology, vol. 378, no. 4. Wiley-Blackwell,
pp. 508–521, 1997.
ista: Li J, Kaneko T, Shigemoto R, Mizuno N. 1997. Distribution of trigeminohypothalamic
and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity
in the rat. Journal of Comparative Neurology. 378(4), 508–521.
mla: Li, Jin, et al. “Distribution of Trigeminohypothalamic and Spinohypothalamic
Tract Neurons Displaying Substance P Receptor-like Immunoreactivity in the Rat.”
Journal of Comparative Neurology, vol. 378, no. 4, Wiley-Blackwell, 1997,
pp. 508–21, doi:10.1002/(SICI)1096-9861(19970224)378:4<508::AID-CNE6>3.0.CO;2-6.
short: J. Li, T. Kaneko, R. Shigemoto, N. Mizuno, Journal of Comparative Neurology
378 (1997) 508–521.
date_created: 2018-12-11T11:58:28Z
date_published: 1997-02-24T00:00:00Z
date_updated: 2022-08-22T13:34:53Z
day: '24'
doi: 10.1002/(SICI)1096-9861(19970224)378:4<508::AID-CNE6>3.0.CO;2-6
extern: '1'
external_id:
pmid:
- '9034907'
intvolume: ' 378'
issue: '4'
language:
- iso: eng
month: '02'
oa_version: None
page: 508 - 521
pmid: 1
publication: Journal of Comparative Neurology
publication_identifier:
issn:
- 0021-9967
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4323'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying
substance P receptor-like immunoreactivity in the rat
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 378
year: '1997'
...