---
_id: '4564'
abstract:
- lang: eng
text: This paper presents a concept for integrating the embedded programming methodology
Giotto and the object-oriented AOCS Framework to create an environment for the
rapid development of distributed software for safety-critical embedded control
systems with hard real-time requirements of the kind typically found in aerospace
applications.
acknowledgement: 'This research was supported in part by DARPA under grants F336 15-C-98-36
14, F33615-00-(2-1693, and F33615-00-C-1703, and by MARC0 under grant 98-DT-660. '
article_processing_charge: No
author:
- first_name: Timothy
full_name: Brown, Timothy
last_name: Brown
- first_name: Alessandro
full_name: Pasetti, Alessandro
last_name: Pasetti
- first_name: Wolfgang
full_name: Pree, Wolfgang
last_name: Pree
- 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: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
citation:
ama: 'Brown T, Pasetti A, Pree W, Henzinger TA, Kirsch C. A reusable and platform-independent
framework for distributed control systems. In: Proceedings of the 20th Digital
Avionics Systems Conference. IEEE; 2001:1-11. doi:10.1109/DASC.2001.964169'
apa: 'Brown, T., Pasetti, A., Pree, W., Henzinger, T. A., & Kirsch, C. (2001).
A reusable and platform-independent framework for distributed control systems.
In Proceedings of the 20th Digital Avionics Systems Conference (pp. 1–11).
Daytona Beach, FL, USA: IEEE. https://doi.org/10.1109/DASC.2001.964169'
chicago: Brown, Timothy, Alessandro Pasetti, Wolfgang Pree, Thomas A Henzinger,
and Christoph Kirsch. “A Reusable and Platform-Independent Framework for Distributed
Control Systems.” In Proceedings of the 20th Digital Avionics Systems Conference,
1–11. IEEE, 2001. https://doi.org/10.1109/DASC.2001.964169.
ieee: T. Brown, A. Pasetti, W. Pree, T. A. Henzinger, and C. Kirsch, “A reusable
and platform-independent framework for distributed control systems,” in Proceedings
of the 20th Digital Avionics Systems Conference, Daytona Beach, FL, USA, 2001,
pp. 1–11.
ista: 'Brown T, Pasetti A, Pree W, Henzinger TA, Kirsch C. 2001. A reusable and
platform-independent framework for distributed control systems. Proceedings of
the 20th Digital Avionics Systems Conference. DASC: Digital Avionics Systems Conference,
1–11.'
mla: Brown, Timothy, et al. “A Reusable and Platform-Independent Framework for Distributed
Control Systems.” Proceedings of the 20th Digital Avionics Systems Conference,
IEEE, 2001, pp. 1–11, doi:10.1109/DASC.2001.964169.
short: T. Brown, A. Pasetti, W. Pree, T.A. Henzinger, C. Kirsch, in:, Proceedings
of the 20th Digital Avionics Systems Conference, IEEE, 2001, pp. 1–11.
conference:
end_date: 2001-10-18
location: Daytona Beach, FL, USA
name: 'DASC: Digital Avionics Systems Conference'
start_date: 2001-10-14
date_created: 2018-12-11T12:09:30Z
date_published: 2001-08-06T00:00:00Z
date_updated: 2023-05-09T12:23:16Z
day: '06'
doi: 10.1109/DASC.2001.964169
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 1 - 11
publication: Proceedings of the 20th Digital Avionics Systems Conference
publication_identifier:
isbn:
- '0780370341'
publication_status: published
publisher: IEEE
publist_id: '143'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A reusable and platform-independent framework for distributed control systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4599'
abstract:
- lang: eng
text: 'State-space explosion is a fundamental obstacle in the formal verification
of designs and protocols. Several techniques for combating this problem have emerged
in the past few years, among which two are significant: partial-order reduction
and symbolic state-space search. In asynchronous systems, interleavings of independent
concurrent events are equivalent, and only a representative interleaving needs
to be explored to verify local properties. Partial-order methods exploit this
redundancy and visit only a subset of the reachable states. Symbolic techniques,
on the other hand, capture the transition relation of a system and the set of
reachable states as boolean functions. In many cases, these functions can be represented
compactly using binary decision diagrams (BDDs). Traditionally, the two techniques
have been practiced by two different schools—partial-order methods with enumerative
depth-first search for the analysis of asynchronous network protocols, and symbolic
breadth-first search for the analysis of synchronous hardware designs. We combine
both approaches and develop a method for using partial-order reduction techniques
in symbolic BDD-based invariant checking. We present theoretical results to prove
the correctness of the method, and experimental results to demonstrate its efficacy.'
acknowledgement: Gerard Holzmann provided us with information on SPIN. Ken McMillan
and Doron Peled contributed through discussions. The VIS group at UC Berkeley and
Rajeev Ranjan in particular helped with the experiments.
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Robert
full_name: Brayton, Robert
last_name: Brayton
- 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: Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction
in symbolic state-space exploration. Formal Methods in System Design. 2001;18(2):97-116.
doi:10.1023/A:1008767206905
apa: Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., & Rajamani, S. (2001).
Partial-order reduction in symbolic state-space exploration. Formal Methods
in System Design. Springer. https://doi.org/10.1023/A:1008767206905
chicago: Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram
Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” Formal
Methods in System Design. Springer, 2001. https://doi.org/10.1023/A:1008767206905.
ieee: R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order
reduction in symbolic state-space exploration,” Formal Methods in System Design,
vol. 18, no. 2. Springer, pp. 97–116, 2001.
ista: Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 2001. Partial-order
reduction in symbolic state-space exploration. Formal Methods in System Design.
18(2), 97–116.
mla: Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.”
Formal Methods in System Design, vol. 18, no. 2, Springer, 2001, pp. 97–116,
doi:10.1023/A:1008767206905.
short: R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, Formal Methods
in System Design 18 (2001) 97–116.
date_created: 2018-12-11T12:09:41Z
date_published: 2001-03-01T00:00:00Z
date_updated: 2023-05-08T12:22:38Z
day: '01'
doi: 10.1023/A:1008767206905
extern: '1'
intvolume: ' 18'
issue: '2'
language:
- iso: eng
month: '03'
oa_version: None
page: 97 - 116
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '108'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Partial-order reduction in symbolic state-space exploration
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 18
year: '2001'
...
---
_id: '4600'
abstract:
- lang: eng
text: 'Model checking is a practical tool for automated debugging of embedded software.
In model checking, a high-level description of a system is compared against a
logical correctness requirement to discover inconsistencies. Since model checking
is based on exhaustive state-space exploration and the size of the state space
of a design grows exponentially with the size of the description, scalability
remains a challenge. We have thus developed techniques for exploiting modular
design structure during model checking, and the model checker jMocha (Java MOdel-CHecking
Algorithm) is based on this theme. Instead of manipulating unstructured state-transition
graphs, it supports the hierarchical modeling framework of reactive modules. jMocha
is a growing interactive software environment for specification, simulation and
verification, and is intended as a vehicle for the development of new verification
algorithms and approaches. It is written in Java and uses native C-code BDD libraries
from VIS. jMocha offers: (1) a GUI that looks familiar to Windows/Java users;
(2) a simulator that displays traces in a message sequence chart fashion; (3)
requirements verification both by symbolic and enumerative model checking; (4)
implementation verification by checking trace containment; (5) a proof manager
that aids compositional and assume-guarantee reasoning; and (6) SLANG (Scripting
LANGuage) for the rapid and structured development of new verification algorithms.
jMocha is available publicly at ; it is a successor and extension of the original
Mocha tool that was entirely written in C.'
acknowledgement: 'We thank Himyanshu Anand, Ben Horowitz, Franjo Ivancic, Michael
McDougall, Marius Minea, Oliver Moeller. Shaz Qadeer, Sriram Rajamani, and Jean-Francois
Raskin for their assistance in the development of JMOCHA. The MOCHA project is funded
in part by the DARPA grant NAG2-1214, the NSF CAREER awards CCR95-01708 and CCR97-34115,
the NSF grant CCR99-70925, the NSF ITR grant CCR0085949, the MARC0 grant 98-DT-660,
and the SRC contracts 99-TJ-683.003 and 99-TJ-688. '
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- 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: Myong
full_name: Kang, Myong
last_name: Kang
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
- first_name: Bow
full_name: Wang, Bow
last_name: Wang
citation:
ama: 'Alur R, De Alfaro L, Grosu R, et al. jMocha: A model-checking tool that exploits
design structure. In: Proceedings of the 23rd International Conference on Software
Engineering. IEEE; 2001:835-836. doi:10.1109/ICSE.2001.919196'
apa: 'Alur, R., De Alfaro, L., Grosu, R., Henzinger, T. A., Kang, M., Kirsch, C.,
… Wang, B. (2001). jMocha: A model-checking tool that exploits design structure.
In Proceedings of the 23rd International Conference on Software Engineering
(pp. 835–836). IEEE. https://doi.org/10.1109/ICSE.2001.919196'
chicago: 'Alur, Rajeev, Luca De Alfaro, Radu Grosu, Thomas A Henzinger, Myong Kang,
Christoph Kirsch, Ritankar Majumdar, Freddy Mang, and Bow Wang. “JMocha: A Model-Checking
Tool That Exploits Design Structure.” In Proceedings of the 23rd International
Conference on Software Engineering, 835–36. IEEE, 2001. https://doi.org/10.1109/ICSE.2001.919196.'
ieee: 'R. Alur et al., “jMocha: A model-checking tool that exploits design
structure,” in Proceedings of the 23rd International Conference on Software
Engineering, 2001, pp. 835–836.'
ista: 'Alur R, De Alfaro L, Grosu R, Henzinger TA, Kang M, Kirsch C, Majumdar R,
Mang F, Wang B. 2001. jMocha: A model-checking tool that exploits design structure.
Proceedings of the 23rd International Conference on Software Engineering. ICSE:
Software Engineering, 835–836.'
mla: 'Alur, Rajeev, et al. “JMocha: A Model-Checking Tool That Exploits Design Structure.”
Proceedings of the 23rd International Conference on Software Engineering,
IEEE, 2001, pp. 835–36, doi:10.1109/ICSE.2001.919196.'
short: R. Alur, L. De Alfaro, R. Grosu, T.A. Henzinger, M. Kang, C. Kirsch, R. Majumdar,
F. Mang, B. Wang, in:, Proceedings of the 23rd International Conference on Software
Engineering, IEEE, 2001, pp. 835–836.
conference:
name: 'ICSE: Software Engineering'
date_created: 2018-12-11T12:09:41Z
date_published: 2001-08-07T00:00:00Z
date_updated: 2023-05-08T14:06:55Z
day: '07'
doi: 10.1109/ICSE.2001.919196
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 835 - 836
publication: Proceedings of the 23rd International Conference on Software Engineering
publication_identifier:
isbn:
- '0769510507'
publication_status: published
publisher: IEEE
publist_id: '109'
quality_controlled: '1'
status: public
title: 'jMocha: A model-checking tool that exploits design structure'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4622'
abstract:
- lang: eng
text: Conventional type systems specify interfaces in terms of values and domains.
We present a light-weight formalism that captures the temporal aspects of software
component interfaces. Specifically, we use an automata-based language to capture
both input assumptions about the order in which the methods of a component are
called, and output guarantees about the order in which the component calls external
methods. The formalism supports automatic compatability checks between interface
models, and thus constitutes a type system for component interaction. Unlike traditional
uses of automata, our formalism is based on an optimistic approach to composition,
and on an alternating approach to design refinement. According to the optimistic
approach, two components are compatible if there is some environment that can
make them work together. According to the alternating approach, one interface
refines another if it has weaker input assumptions, and stronger output guarantees.
We show that these notions have game-theoretic foundations that lead to efficient
algorithms for checking compatibility and refinement.
acknowledgement: We thank Edward A. Lee, Xiaojun Liu, Freddy Mang, and Yuhong Xiong
for fruitful discussions. This research was supported in part by the AFOSR MURI
grant F49620-00-1-0327, the DARPA MoBIES grant F33615-00-C-1703, the MARCO GSRC
grant 98-DT-660, the NSF Theory grant CCR-9988172, and the NSF ITR grant CCR-0085949.
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. Interface automata. In: Proceedings of the 8th
European Software Engineering Conference. ACM; 2001:109-120. doi:10.1145/503209.503226'
apa: 'De Alfaro, L., & Henzinger, T. A. (2001). Interface automata. In Proceedings
of the 8th European software engineering conference (pp. 109–120). Vienna,
Austria: ACM. https://doi.org/10.1145/503209.503226'
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Interface Automata.” In Proceedings
of the 8th European Software Engineering Conference, 109–20. ACM, 2001. https://doi.org/10.1145/503209.503226.
ieee: L. De Alfaro and T. A. Henzinger, “Interface automata,” in Proceedings
of the 8th European software engineering conference, Vienna, Austria, 2001,
pp. 109–120.
ista: 'De Alfaro L, Henzinger TA. 2001. Interface automata. Proceedings of the 8th
European software engineering conference. FSE: Foundations of Software Engineering,
109–120.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. “Interface Automata.” Proceedings
of the 8th European Software Engineering Conference, ACM, 2001, pp. 109–20,
doi:10.1145/503209.503226.
short: L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 8th European Software
Engineering Conference, ACM, 2001, pp. 109–120.
conference:
end_date: 2001-09-14
location: Vienna, Austria
name: 'FSE: Foundations of Software Engineering'
start_date: 2001-09-10
date_created: 2018-12-11T12:09:48Z
date_published: 2001-06-01T00:00:00Z
date_updated: 2023-05-08T12:01:02Z
day: '01'
doi: 10.1145/503209.503226
extern: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: 109 - 120
publication: Proceedings of the 8th European software engineering conference
publication_identifier:
isbn:
- '9781581133905'
publication_status: published
publisher: ACM
publist_id: '83'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interface automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4623'
abstract:
- lang: eng
text: We classify component-based models of computation into component models and
interface models. A component model specifies for each component howthe component
behaves in an arbitrary environment; an interface model specifies for each component
what the component expects from the environment. Component models support compositional
abstraction, and therefore component-based verification. Interface models support
compositional refinement, and therefore componentbased design. Many aspects of
interface models, such as compatibility and refinement checking between interfaces,
are properly viewed in a gametheoretic setting, where the input and output values
of an interface are chosen by different players.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
the DARPA ITO grant F33615-00-C-1693, the MARCO grant 98-DT-660, and the NSF ITR
grant CCR-0085949.
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
citation:
ama: 'De Alfaro L, Henzinger TA. Interface theories for component-based design.
In: Proceedings of the 1st International Workshop on Embedded Software.
Vol 2211. ACM; 2001:148-165. doi:10.1007/3-540-45449-7_11'
apa: 'De Alfaro, L., & Henzinger, T. A. (2001). Interface theories for component-based
design. In Proceedings of the 1st International Workshop on Embedded Software
(Vol. 2211, pp. 148–165). Tahoe City, CA, USA: ACM. https://doi.org/10.1007/3-540-45449-7_11'
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Interface Theories for Component-Based
Design.” In Proceedings of the 1st International Workshop on Embedded Software,
2211:148–65. ACM, 2001. https://doi.org/10.1007/3-540-45449-7_11.
ieee: L. De Alfaro and T. A. Henzinger, “Interface theories for component-based
design,” in Proceedings of the 1st International Workshop on Embedded Software,
Tahoe City, CA, USA, 2001, vol. 2211, pp. 148–165.
ista: 'De Alfaro L, Henzinger TA. 2001. Interface theories for component-based design.
Proceedings of the 1st International Workshop on Embedded Software. EMSOFT: Embedded
Software , LNCS, vol. 2211, 148–165.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. “Interface Theories for Component-Based
Design.” Proceedings of the 1st International Workshop on Embedded Software,
vol. 2211, ACM, 2001, pp. 148–65, doi:10.1007/3-540-45449-7_11.
short: L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 1st International Workshop
on Embedded Software, ACM, 2001, pp. 148–165.
conference:
end_date: 2001-10-10
location: Tahoe City, CA, USA
name: 'EMSOFT: Embedded Software '
start_date: 2001-10-08
date_created: 2018-12-11T12:09:48Z
date_published: 2001-09-26T00:00:00Z
date_updated: 2023-05-08T12:11:20Z
day: '26'
doi: 10.1007/3-540-45449-7_11
extern: '1'
intvolume: ' 2211'
language:
- iso: eng
month: '09'
oa_version: None
page: 148 - 165
publication: Proceedings of the 1st International Workshop on Embedded Software
publication_identifier:
isbn:
- '9783540426738'
publication_status: published
publisher: ACM
publist_id: '84'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interface theories for component-based design
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2211
year: '2001'
...
---
_id: '4632'
abstract:
- lang: eng
text: We present a compositional trace-based model for probabilistic systems. The
behavior of a system with probabilistic choice is a stochastic process, namely,
a probability distribution on traces, or “bundle.” Consequently, the semantics
of a system with both nondeterministic and probabilistic choice is a set of bundles.
The bundles of a composite system can be obtained by combining the bundles of
the components in a simple mathematical way. Refinement between systems is bundle
containment. We achieve assume-guarantee compositionality for bundle semantics
by introducing two scoping mechanisms. The first mechanism, which is standard
in compositional modeling, distinguishes inputs from outputs and hidden state.
The second mechanism, which arises in probabilistic systems, partitions the state
into probabilistically independent regions.
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
the AFOSR MURI grant F49620-00-1-0327, the MARCO GSRC grant 98-DT-660, the NSF Theory
grant CCR-9988172, and the DARPA SEC grant F33615-C-98-3614.
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: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
citation:
ama: 'De Alfaro L, Henzinger TA, Jhala R. Compositional methods for probabilistic
systems. In: Proceedings of the 12th International Conference on on Concurrency
Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:351-365.
doi:10.1007/3-540-44685-0_24'
apa: 'De Alfaro, L., Henzinger, T. A., & Jhala, R. (2001). Compositional methods
for probabilistic systems. In Proceedings of the 12th International Conference
on on Concurrency Theory (Vol. 2154, pp. 351–365). Aalborg, Denmark: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_24'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Ranjit Jhala. “Compositional Methods
for Probabilistic Systems.” In Proceedings of the 12th International Conference
on on Concurrency Theory, 2154:351–65. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2001. https://doi.org/10.1007/3-540-44685-0_24.
ieee: L. De Alfaro, T. A. Henzinger, and R. Jhala, “Compositional methods for probabilistic
systems,” in Proceedings of the 12th International Conference on on Concurrency
Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 351–365.
ista: 'De Alfaro L, Henzinger TA, Jhala R. 2001. Compositional methods for probabilistic
systems. Proceedings of the 12th International Conference on on Concurrency Theory.
CONCUR: Concurrency Theory, LNCS, vol. 2154, 351–365.'
mla: De Alfaro, Luca, et al. “Compositional Methods for Probabilistic Systems.”
Proceedings of the 12th International Conference on on Concurrency Theory,
vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–65,
doi:10.1007/3-540-44685-0_24.
short: L. De Alfaro, T.A. Henzinger, R. Jhala, in:, Proceedings of the 12th International
Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001, pp. 351–365.
conference:
end_date: 2001-08-25
location: Aalborg, Denmark
name: 'CONCUR: Concurrency Theory'
start_date: 2001-08-20
date_created: 2018-12-11T12:09:51Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T10:24:59Z
day: '13'
doi: 10.1007/3-540-44685-0_24
extern: '1'
intvolume: ' 2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 351 - 365
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
isbn:
- '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '75'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Compositional methods for probabilistic systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4633'
abstract:
- lang: eng
text: "A procedure for the analysis of state spaces is called symbolic if it manipulates
not individual states, but sets of states that are represented by constraints.
Such a procedure can be used for the analysis of infinite state spaces, provided
termination is guaranteed. We present symbolic procedures, and corresponding termination
criteria, for the solution of infinite-state games, which occur in the control
and modular verification of infinite-state systems. To characterize the termination
of symbolic procedures for solving infinite-state games, we classify these game
structures into four increasingly restrictive categories:\r\n1 \tClass 1 consists
of infinite-state structures for which all safety and reachability games can be
solved.\r\n2 \tClass 2 consists of infinite-state structures for which all ω-regular
games can be solved.\r\n3 \tClass 3 consists of infinite-state structures for
which all nested positive boolean combinations of ω-regular games can be solved.\r\n4
\ \tClass 4 consists of infinite-state structures for which all nested boolean
combinations of ω-regular games can be solved.\r\nWe give a structural characterization
for each class, using equivalence relations on the state spaces of games which
range from game versions of trace equivalence to a game version of bisimilarity.
We provide infinite-state examples for all four classes of games from control
problems for hybrid systems. We conclude by presenting symbolic algorithms for
the synthesis of winning strategies (“controller synthesis”) for infinitestate
games with arbitrary ω-regular objectives, and prove termination over all class-2
structures. This settles, in particular, the symbolic controller synthesis problem
for rectangular hybrid systems."
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF Theory
grant CCR-9988172, and the NSF ITR grant CCR-0085949.
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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'De Alfaro L, Henzinger TA, Majumdar R. Symbolic algorithms for infinite-state
games. In: Proceedings of the 12th International Conference on on Concurrency
Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:536-550.
doi:10.1007/3-540-44685-0_36'
apa: 'De Alfaro, L., Henzinger, T. A., & Majumdar, R. (2001). Symbolic algorithms
for infinite-state games. In Proceedings of the 12th International Conference
on on Concurrency Theory (Vol. 2154, pp. 536–550). Aalborg, Denmark: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_36'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Symbolic Algorithms
for Infinite-State Games.” In Proceedings of the 12th International Conference
on on Concurrency Theory, 2154:536–50. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2001. https://doi.org/10.1007/3-540-44685-0_36.
ieee: L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Symbolic algorithms for infinite-state
games,” in Proceedings of the 12th International Conference on on Concurrency
Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 536–550.
ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2001. Symbolic algorithms for infinite-state
games. Proceedings of the 12th International Conference on on Concurrency Theory.
CONCUR: Concurrency Theory, LNCS, vol. 2154, 536–550.'
mla: De Alfaro, Luca, et al. “Symbolic Algorithms for Infinite-State Games.” Proceedings
of the 12th International Conference on on Concurrency Theory, vol. 2154,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–50, doi:10.1007/3-540-44685-0_36.
short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 12th International
Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001, pp. 536–550.
conference:
end_date: 2001-08-25
location: Aalborg, Denmark
name: 'CONCUR: Concurrency Theory'
start_date: 2001-08-20
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T09:57:31Z
day: '13'
doi: 10.1007/3-540-44685-0_36
extern: '1'
intvolume: ' 2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 536 - 550
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
isbn:
- '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '73'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic algorithms for infinite-state games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4634'
abstract:
- lang: eng
text: "A controller is an environment for a system that achieves a particular control
objective by providing inputs to the system without constraining the choices of
the system. For synchronous systems, where system and controller make simultaneous
and interdependent choices, the notion that a controller must not constrain the
choices of the system can be formalized by type systems for composability. In
a previous paper, we solved the control problem for static and dynamic types:
a static type is a dependency relation between inputs and outputs, and composition
is well-typed if it does not introduce cyclic dependencies; a dynamic type is
a set of static types, one for each state. Static and dynamic types, however,
cannot capture many important digital circuits, such as gated clocks, bidirectional
buses, and random-access memory. We therefore introduce more general type systems,
so-called dependent and bidirectional types, for modeling these situations, and
we solve the corresponding control problems.\r\nIn a system with a dependent type,
the dependencies between inputs and outputs are determined gradually through a
game of the system against the controller. In a system with a bidirectional type,
also the distinction between inputs and outputs is resolved dynamically by such
a game. The game proceeds in several rounds. In each round the system and the
controller choose to update some variables dependent on variables that have already
been updated. The solution of the control problem for dependent and bidirectional
types is based on algorithms for solving these games."
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the AFOSR
MURI grant F49620-00-1-0327, and the NSF Theory grant CCR-9988172.
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, Part
II. In: Proceedings of the 12th International Conference on on Concurrency
Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:566-581.
doi:10.1007/3-540-44685-0_38'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2001). The control of synchronous
systems, Part II. In Proceedings of the 12th International Conference on on
Concurrency Theory (Vol. 2154, pp. 566–581). Aalborg, Denmark: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_38'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous
Systems, Part II.” In Proceedings of the 12th International Conference on on
Concurrency Theory, 2154:566–81. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001. https://doi.org/10.1007/3-540-44685-0_38.
ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems,
Part II,” in Proceedings of the 12th International Conference on on Concurrency
Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 566–581.
ista: 'De Alfaro L, Henzinger TA, Mang F. 2001. The control of synchronous systems,
Part II. Proceedings of the 12th International Conference on on Concurrency Theory.
CONCUR: Concurrency Theory, LNCS, vol. 2154, 566–581.'
mla: De Alfaro, Luca, et al. “The Control of Synchronous Systems, Part II.” Proceedings
of the 12th International Conference on on Concurrency Theory, vol. 2154,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–81, doi:10.1007/3-540-44685-0_38.
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International
Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001, pp. 566–581.
conference:
end_date: 2001-08-25
location: Aalborg, Denmark
name: 'CONCUR: Concurrency Theory'
start_date: 2001-08-20
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T10:20:19Z
day: '13'
doi: 10.1007/3-540-44685-0_38
extern: '1'
intvolume: ' 2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 566 - 581
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
isbn:
- '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '74'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The control of synchronous systems, Part II
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4635'
abstract:
- lang: eng
text: We show how model checking techniques can be applied to the analysis of connectivity
and cost-of-traversal properties of Web sites.
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. MCWEB: A model-checking tool for web-site
debugging. In: Proceedings of the 10th International Conference on World Wide
Web. ACM; 2001:86-87.'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2001). MCWEB: A model-checking
tool for web-site debugging. In Proceedings of the 10th international conference
on World Wide Web (pp. 86–87). Hong Kong, Hong Kong: ACM.'
chicago: 'De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “MCWEB: A Model-Checking
Tool for Web-Site Debugging.” In Proceedings of the 10th International Conference
on World Wide Web, 86–87. ACM, 2001.'
ieee: 'L. De Alfaro, T. A. Henzinger, and F. Mang, “MCWEB: A model-checking tool
for web-site debugging,” in Proceedings of the 10th international conference
on World Wide Web, Hong Kong, Hong Kong, 2001, pp. 86–87.'
ista: 'De Alfaro L, Henzinger TA, Mang F. 2001. MCWEB: A model-checking tool for
web-site debugging. Proceedings of the 10th international conference on World
Wide Web. WWW: World Wide Web Conference, 86–87.'
mla: 'De Alfaro, Luca, et al. “MCWEB: A Model-Checking Tool for Web-Site Debugging.”
Proceedings of the 10th International Conference on World Wide Web, ACM,
2001, pp. 86–87.'
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 10th International
Conference on World Wide Web, ACM, 2001, pp. 86–87.
conference:
end_date: 2000-05-05
location: Hong Kong, Hong Kong
name: 'WWW: World Wide Web Conference'
start_date: 2001-05-01
date_created: 2018-12-11T12:09:52Z
date_published: 2001-05-01T00:00:00Z
date_updated: 2023-05-08T09:39:02Z
day: '01'
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ir.webis.de/anthology/2001.wwwconf_conference-2001p.57/
month: '05'
oa_version: None
page: 86 - 87
publication: Proceedings of the 10th international conference on World Wide Web
publication_identifier:
isbn:
- '9781581133486'
publication_status: published
publisher: ACM
publist_id: '71'
quality_controlled: '1'
status: public
title: 'MCWEB: A model-checking tool for web-site debugging'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4636'
abstract:
- lang: eng
text: 'Abstract. Dynamic programs, or fixpoint iteration schemes, are useful for
solving many problems on state spaces, including model checking on Kripke structures
(“verification”), computing shortest paths on weighted graphs (“optimization”),
computing the value of games played on game graphs (“control”). For Kripke structures,
a rich fixpoint theory is available in the form of the µ-calculus. Yet few connections
have been made between different interpretations of fixpoint algorithms. We study
the question of when a particular fixpoint iteration scheme ϕ for verifying an
ω-regular property Ψ on a Kripke structure can be used also for solving a two-player
game on a game graph with winning objective Ψ. We provide a sufficient and necessary
criterion for the answer to be affirmative in the form of an extremal-model theorem
for games: under a game interpretation, the dynamic program ϕ solves the game
with objective Ψ if and only if both (1) under an existential interpretation on
Kripke structures, ϕ is equivalent to ∃Ψ, and (2) under a universal interpretation
on Kripke structures, ϕ is equivalent to ∀Ψ. In other words, ϕ is correct on all
two-player game graphs iff it is correct on all extremal game graphs, where one
or the other player has no choice of moves. The theorem generalizes to quantitative
interpretations, where it connects two-player games with costs to weighted graphs.
While the standard translations from ω-regular properties to the µ-calculus violate
(1) or (2), we give a translation that satisfies both conditions. Our construction,
therefore, yields fixpoint iteration schemes that can be uniformly applied on
Kripke structures, weighted graphs, game graphs, and game graphs with costs, in
order to meet or optimize a given ω-regular objective.'
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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'De Alfaro L, Henzinger TA, Majumdar R. From verification to control: dynamic
programs for omega-regular objectives. In: Proceedings of the 16th Annual IEEE
Symposium on Logic in Computer Science. IEEE; 2001:279-290. doi:10.1109/LICS.2001.932504'
apa: 'De Alfaro, L., Henzinger, T. A., & Majumdar, R. (2001). From verification
to control: dynamic programs for omega-regular objectives. In Proceedings of
the 16th Annual IEEE Symposium on Logic in Computer Science (pp. 279–290).
Boston, MA, USA: IEEE. https://doi.org/10.1109/LICS.2001.932504'
chicago: 'De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “From Verification
to Control: Dynamic Programs for Omega-Regular Objectives.” In Proceedings
of the 16th Annual IEEE Symposium on Logic in Computer Science, 279–90. IEEE,
2001. https://doi.org/10.1109/LICS.2001.932504.'
ieee: 'L. De Alfaro, T. A. Henzinger, and R. Majumdar, “From verification to control:
dynamic programs for omega-regular objectives,” in Proceedings of the 16th
Annual IEEE Symposium on Logic in Computer Science, Boston, MA, USA, 2001,
pp. 279–290.'
ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2001. From verification to control:
dynamic programs for omega-regular objectives. Proceedings of the 16th Annual
IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science,
279–290.'
mla: 'De Alfaro, Luca, et al. “From Verification to Control: Dynamic Programs for
Omega-Regular Objectives.” Proceedings of the 16th Annual IEEE Symposium on
Logic in Computer Science, IEEE, 2001, pp. 279–90, doi:10.1109/LICS.2001.932504.'
short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 16th Annual
IEEE Symposium on Logic in Computer Science, IEEE, 2001, pp. 279–290.
conference:
end_date: 2001-06-19
location: Boston, MA, USA
name: 'LICS: Logic in Computer Science'
start_date: 2001-06-16
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-07T00:00:00Z
date_updated: 2023-05-08T09:48:06Z
day: '07'
doi: 10.1109/LICS.2001.932504
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 279 - 290
publication: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
isbn:
- 076951281X
publication_status: published
publisher: IEEE
publist_id: '72'
quality_controlled: '1'
status: public
title: 'From verification to control: dynamic programs for omega-regular objectives'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '1452'
abstract:
- lang: eng
text: 'In this Note we present pairs of hyperkähler orbifolds which satisfy two
different versions of mirror symmetry. On the one hand, we show that their Hodge
numbers (or more precisely, stringy E-polynomials) are equal. On the other hand,
we show that they satisfy the prescription of Strominger, Yau, and Zaslow (which
in the present case goes back to Bershadsky, Johansen, Sadov and Vafa): that a
Calabi-Yau and its mirror should fiber over the same real manifold, with special
Lagrangian fibers which are tori dual to each other. Our examples arise as moduli
spaces of local systems on a curve with structure group SL(n); the mirror is the
corresponding space with structure group PGL(n). The special Lagrangian tori come
from an algebraically completely integrable Hamiltonian system: the Hitchin system.'
acknowledgement: The authors are grateful for Nigel Hitchin for suggesting the similarity
between [4] and [12] in 1996 and for Pierre Deligne for numerous useful comments
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Tamas
full_name: Hausel, Tamas
id: 4A0666D8-F248-11E8-B48F-1D18A9856A87
last_name: Hausel
- first_name: Michael
full_name: Thaddeus, Michael
last_name: Thaddeus
citation:
ama: 'Hausel T, Thaddeus M. Examples of mirror partners arising from integrable
systems. Comptes Rendus de l’Academie des Sciences - Series I: Mathematics.
2001;333(4):313-318. doi:10.1016/S0764-4442(01)02057-2'
apa: 'Hausel, T., & Thaddeus, M. (2001). Examples of mirror partners arising
from integrable systems. Comptes Rendus de l’Academie Des Sciences - Series
I: Mathematics. Elsevier. https://doi.org/10.1016/S0764-4442(01)02057-2'
chicago: 'Hausel, Tamás, and Michael Thaddeus. “Examples of Mirror Partners Arising
from Integrable Systems.” Comptes Rendus de l’Academie Des Sciences - Series
I: Mathematics. Elsevier, 2001. https://doi.org/10.1016/S0764-4442(01)02057-2.'
ieee: 'T. Hausel and M. Thaddeus, “Examples of mirror partners arising from integrable
systems,” Comptes Rendus de l’Academie des Sciences - Series I: Mathematics,
vol. 333, no. 4. Elsevier, pp. 313–318, 2001.'
ista: 'Hausel T, Thaddeus M. 2001. Examples of mirror partners arising from integrable
systems. Comptes Rendus de l’Academie des Sciences - Series I: Mathematics. 333(4),
313–318.'
mla: 'Hausel, Tamás, and Michael Thaddeus. “Examples of Mirror Partners Arising
from Integrable Systems.” Comptes Rendus de l’Academie Des Sciences - Series
I: Mathematics, vol. 333, no. 4, Elsevier, 2001, pp. 313–18, doi:10.1016/S0764-4442(01)02057-2.'
short: 'T. Hausel, M. Thaddeus, Comptes Rendus de l’Academie Des Sciences - Series
I: Mathematics 333 (2001) 313–318.'
date_created: 2018-12-11T11:52:06Z
date_published: 2001-08-15T00:00:00Z
date_updated: 2023-05-31T09:57:48Z
day: '15'
doi: 10.1016/S0764-4442(01)02057-2
extern: '1'
external_id:
arxiv:
- math/0106140
intvolume: ' 333'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/math/0106140
month: '08'
oa: 1
oa_version: Preprint
page: 313 - 318
publication: 'Comptes Rendus de l''Academie des Sciences - Series I: Mathematics'
publication_identifier:
issn:
- 0764-4442
publication_status: published
publisher: Elsevier
publist_id: '5742'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Examples of mirror partners arising from integrable systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 333
year: '2001'
...
---
_id: '1453'
abstract:
- lang: eng
text: In this Letter we exhibit a one-parameter family of new Taub-NUT instantons
parameterized by a half-line. The endpoint of the half-line will be the reducible
Yang-Mills instanton corresponding to the Eguchi-Hanson-Gibbons L2 harmonic 2-form,
while at an inner point we recover the Pope-Yuille instanton constructed as a
projection of the Levi-Civitá connection onto the positive su(2)+ ⊂ so(4) subalgebra.
Our method imitates the Jackiw-Nohl-Rebbi construction originally designed for
flat R4. That is we find a one-parameter family of harmonic functions on the Taub-NUT
space with a point singularity, rescale the metric and project the obtained Levi-Civitá
connection onto the other negative su(2)- ⊂ so(4) part. Our solutions will possess
the full U(2) symmetry, and thus provide more solutions to the recently proposed
U(2) symmetric ansatz of Kim and Yoon.
acknowledgement: We would like to acknowledge the financial support provided by the
Miller Institute of Basic Research in Science, the Japan Society for the Promotion
of Science, grant No. P99736 and the partial support by OTKA grant No. T032478.
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Gábor
full_name: Etesi, Gábor
last_name: Etesi
- first_name: Tamas
full_name: Hausel, Tamas
id: 4A0666D8-F248-11E8-B48F-1D18A9856A87
last_name: Hausel
citation:
ama: 'Etesi G, Hausel T. Geometric construction of new Yang-Mills instantons over
Taub-NUT space. Physics Letters, Section B: Nuclear, Elementary Particle and
High-Energy Physics. 2001;514(1-2):189-199. doi:10.1016/S0370-2693(01)00821-8'
apa: 'Etesi, G., & Hausel, T. (2001). Geometric construction of new Yang-Mills
instantons over Taub-NUT space. Physics Letters, Section B: Nuclear, Elementary
Particle and High-Energy Physics. Elsevier. https://doi.org/10.1016/S0370-2693(01)00821-8'
chicago: 'Etesi, Gábor, and Tamás Hausel. “Geometric Construction of New Yang-Mills
Instantons over Taub-NUT Space.” Physics Letters, Section B: Nuclear, Elementary
Particle and High-Energy Physics. Elsevier, 2001. https://doi.org/10.1016/S0370-2693(01)00821-8.'
ieee: 'G. Etesi and T. Hausel, “Geometric construction of new Yang-Mills instantons
over Taub-NUT space,” Physics Letters, Section B: Nuclear, Elementary Particle
and High-Energy Physics, vol. 514, no. 1–2. Elsevier, pp. 189–199, 2001.'
ista: 'Etesi G, Hausel T. 2001. Geometric construction of new Yang-Mills instantons
over Taub-NUT space. Physics Letters, Section B: Nuclear, Elementary Particle
and High-Energy Physics. 514(1–2), 189–199.'
mla: 'Etesi, Gábor, and Tamás Hausel. “Geometric Construction of New Yang-Mills
Instantons over Taub-NUT Space.” Physics Letters, Section B: Nuclear, Elementary
Particle and High-Energy Physics, vol. 514, no. 1–2, Elsevier, 2001, pp. 189–99,
doi:10.1016/S0370-2693(01)00821-8.'
short: 'G. Etesi, T. Hausel, Physics Letters, Section B: Nuclear, Elementary Particle
and High-Energy Physics 514 (2001) 189–199.'
date_created: 2018-12-11T11:52:07Z
date_published: 2001-08-09T00:00:00Z
date_updated: 2023-05-31T11:51:37Z
day: '09'
doi: 10.1016/S0370-2693(01)00821-8
extern: '1'
external_id:
arxiv:
- hep-th/0105118
intvolume: ' 514'
issue: 1-2
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/hep-th/0105118
month: '08'
oa: 1
oa_version: Preprint
page: 189 - 199
publication: 'Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy
Physics'
publication_identifier:
issn:
- 0370-2693
publication_status: published
publisher: Elsevier
publist_id: '5743'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Geometric construction of new Yang-Mills instantons over Taub-NUT space
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 514
year: '2001'
...
---
_id: '1454'
abstract:
- lang: eng
text: We address the problem of finding Abelian instantons of finite energy on the
Euclidean Schwarzschild manifold. This amounts to construct self-dual L2 harmonic
2-forms on the space. Gibbons found a non-topological L2 harmonic form in the
Taub-NUT metric, leading to Abelian instantons with continuous energy. We imitate
his construction in the case of the Euclidean Schwarzschild manifold and find
a non-topological self-dual L2 harmonic 2-form on it. We show how this gives rise
to Abelian instantons and identify them with SU(2)-instantons of Pontryagin number
2n2 found by Charap and Duff in 1977. Using results of Dodziuk and Hitchin we
also calculate the full L2 harmonic space for the Euclidean Schwarzschild manifold.
acknowledgement: The work in this paper was done when Tamás Hausel visited the Yukawa
Institute of Kyoto University in February 2000. We are grateful for Prof. G.W. Gibbons
for insightful discussions and Prof. H. Kodama and the Yukawa Institute for the
invitation and hospitality.
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Gábor
full_name: Etesi, Gábor
last_name: Etesi
- first_name: Tamas
full_name: Hausel, Tamas
id: 4A0666D8-F248-11E8-B48F-1D18A9856A87
last_name: Hausel
citation:
ama: Etesi G, Hausel T. Geometric interpretation of Schwarzschild instantons. Journal
of Geometry and Physics. 2001;37(1-2):126-136. doi:10.1016/S0393-0440(00)00040-1
apa: Etesi, G., & Hausel, T. (2001). Geometric interpretation of Schwarzschild
instantons. Journal of Geometry and Physics. Elsevier. https://doi.org/10.1016/S0393-0440(00)00040-1
chicago: Etesi, Gábor, and Tamás Hausel. “Geometric Interpretation of Schwarzschild
Instantons.” Journal of Geometry and Physics. Elsevier, 2001. https://doi.org/10.1016/S0393-0440(00)00040-1.
ieee: G. Etesi and T. Hausel, “Geometric interpretation of Schwarzschild instantons,”
Journal of Geometry and Physics, vol. 37, no. 1–2. Elsevier, pp. 126–136,
2001.
ista: Etesi G, Hausel T. 2001. Geometric interpretation of Schwarzschild instantons.
Journal of Geometry and Physics. 37(1–2), 126–136.
mla: Etesi, Gábor, and Tamás Hausel. “Geometric Interpretation of Schwarzschild
Instantons.” Journal of Geometry and Physics, vol. 37, no. 1–2, Elsevier,
2001, pp. 126–36, doi:10.1016/S0393-0440(00)00040-1.
short: G. Etesi, T. Hausel, Journal of Geometry and Physics 37 (2001) 126–136.
date_created: 2018-12-11T11:52:07Z
date_published: 2001-01-01T00:00:00Z
date_updated: 2023-05-31T12:08:45Z
day: '01'
doi: 10.1016/S0393-0440(00)00040-1
extern: '1'
external_id:
arxiv:
- hep-th/0003239
intvolume: ' 37'
issue: 1-2
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/hep-th/0003239
month: '01'
oa: 1
oa_version: Preprint
page: 126 - 136
publication: Journal of Geometry and Physics
publication_identifier:
issn:
- 0393-0440
publication_status: published
publisher: Elsevier
publist_id: '5744'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Geometric interpretation of Schwarzschild instantons
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 37
year: '2001'
...
---
_id: '9444'
abstract:
- lang: eng
text: Epigenetic silenced alleles of the Arabidopsis SUPERMANlocus (the clark kent
alleles) are associated with dense hypermethylation at noncanonical cytosines
(CpXpG and asymmetric sites, where X = A, T, C, or G). A genetic screen for suppressors
of a hypermethylated clark kent mutant identified nine loss-of-function alleles
of CHROMOMETHYLASE3(CMT3), a novel cytosine methyltransferase homolog. These cmt3
mutants display a wild-type morphology but exhibit decreased CpXpG methylation
of the SUP gene and of other sequences throughout the genome. They also show reactivated
expression of endogenous retrotransposon sequences. These results show that a
non-CpG DNA methyltransferase is responsible for maintaining epigenetic gene silencing.
article_processing_charge: No
article_type: original
author:
- first_name: A. M.
full_name: Lindroth, A. M.
last_name: Lindroth
- first_name: Xiaofeng
full_name: Cao, Xiaofeng
last_name: Cao
- first_name: James P.
full_name: Jackson, James P.
last_name: Jackson
- first_name: Daniel
full_name: Zilberman, Daniel
id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
last_name: Zilberman
orcid: 0000-0002-0123-8649
- first_name: Claire M.
full_name: McCallum, Claire M.
last_name: McCallum
- first_name: Steven
full_name: Henikoff, Steven
last_name: Henikoff
- first_name: Steven E.
full_name: Jacobsen, Steven E.
last_name: Jacobsen
citation:
ama: Lindroth AM, Cao X, Jackson JP, et al. Requirement of CHROMOMETHYLASE3 for
maintenance of CpXpG methylation. Science. 2001;292(5524):2077-2080. doi:10.1126/science.1059745
apa: Lindroth, A. M., Cao, X., Jackson, J. P., Zilberman, D., McCallum, C. M., Henikoff,
S., & Jacobsen, S. E. (2001). Requirement of CHROMOMETHYLASE3 for maintenance
of CpXpG methylation. Science. American Association for the Advancement
of Science. https://doi.org/10.1126/science.1059745
chicago: Lindroth, A. M., Xiaofeng Cao, James P. Jackson, Daniel Zilberman, Claire
M. McCallum, Steven Henikoff, and Steven E. Jacobsen. “Requirement of CHROMOMETHYLASE3
for Maintenance of CpXpG Methylation.” Science. American Association for
the Advancement of Science, 2001. https://doi.org/10.1126/science.1059745.
ieee: A. M. Lindroth et al., “Requirement of CHROMOMETHYLASE3 for maintenance
of CpXpG methylation,” Science, vol. 292, no. 5524. American Association
for the Advancement of Science, pp. 2077–2080, 2001.
ista: Lindroth AM, Cao X, Jackson JP, Zilberman D, McCallum CM, Henikoff S, Jacobsen
SE. 2001. Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation.
Science. 292(5524), 2077–2080.
mla: Lindroth, A. M., et al. “Requirement of CHROMOMETHYLASE3 for Maintenance of
CpXpG Methylation.” Science, vol. 292, no. 5524, American Association for
the Advancement of Science, 2001, pp. 2077–80, doi:10.1126/science.1059745.
short: A.M. Lindroth, X. Cao, J.P. Jackson, D. Zilberman, C.M. McCallum, S. Henikoff,
S.E. Jacobsen, Science 292 (2001) 2077–2080.
date_created: 2021-06-02T13:35:16Z
date_published: 2001-06-15T00:00:00Z
date_updated: 2021-12-14T08:40:32Z
day: '15'
department:
- _id: DaZi
doi: 10.1126/science.1059745
extern: '1'
external_id:
pmid:
- '11349138'
intvolume: ' 292'
issue: '5524'
keyword:
- Multidisciplinary
language:
- iso: eng
month: '06'
oa_version: None
page: 2077-2080
pmid: 1
publication: Science
publication_identifier:
eissn:
- 1095-9203
issn:
- 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 292
year: '2001'
...
---
_id: '11892'
abstract:
- lang: eng
text: "We present the first fully dynamic algorithm for maintaining a minimum spanning
forest in time \U0001D45C(\U0001D45B√) per operation. To be precise, the algorithm
uses O(n1/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(n1/3 log n) per update, with O(1) worst case time per query."
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: Valerie
full_name: King, Valerie
last_name: King
citation:
ama: Henzinger MH, King V. Maintaining minimum spanning forests in dynamic graphs.
SIAM Journal on Computing. 2001;31(2):364-374. doi:10.1137/s0097539797327209
apa: Henzinger, M. H., & King, V. (2001). Maintaining minimum spanning forests
in dynamic graphs. SIAM Journal on Computing. Society for Industrial &
Applied Mathematics. https://doi.org/10.1137/s0097539797327209
chicago: Henzinger, Monika H, and Valerie King. “Maintaining Minimum Spanning Forests
in Dynamic Graphs.” SIAM Journal on Computing. Society for Industrial &
Applied Mathematics, 2001. https://doi.org/10.1137/s0097539797327209.
ieee: M. H. Henzinger and V. King, “Maintaining minimum spanning forests in dynamic
graphs,” SIAM Journal on Computing, vol. 31, no. 2. Society for Industrial
& Applied Mathematics, pp. 364–374, 2001.
ista: Henzinger MH, King V. 2001. Maintaining minimum spanning forests in dynamic
graphs. SIAM Journal on Computing. 31(2), 364–374.
mla: Henzinger, Monika H., and Valerie King. “Maintaining Minimum Spanning Forests
in Dynamic Graphs.” SIAM Journal on Computing, vol. 31, no. 2, Society
for Industrial & Applied Mathematics, 2001, pp. 364–74, doi:10.1137/s0097539797327209.
short: M.H. Henzinger, V. King, SIAM Journal on Computing 31 (2001) 364–374.
date_created: 2022-08-17T08:43:43Z
date_published: 2001-03-01T00:00:00Z
date_updated: 2023-02-17T14:24:55Z
day: '01'
doi: 10.1137/s0097539797327209
extern: '1'
intvolume: ' 31'
issue: '2'
language:
- iso: eng
month: '03'
oa_version: None
page: 364-374
publication: SIAM Journal on Computing
publication_identifier:
eissn:
- 1095-7111
issn:
- 0097-5397
publication_status: published
publisher: Society for Industrial & Applied Mathematics
quality_controlled: '1'
scopus_import: '1'
status: public
title: Maintaining minimum spanning forests in dynamic graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 31
year: '2001'
...
---
_id: '11914'
abstract:
- lang: eng
text: 'Previous studies of the Web graph structure have focused on the graph structure
at the level of individual pages. In actuality the Web is a hierarchically nested
graph, with domains, hosts and Web sites introducing intermediate levels of affiliation
and administrative control. To better understand the growth of the Web we need
to understand its macro-structure, in terms of the linkage between Web sites.
We approximate this by studying the graph of the linkage between hosts on the
Web. This was done based on snapshots of the Web taken by Google in Oct 1999,
Aug 2000 and Jun 2001. The connectivity between hosts is represented by a directed
graph, with hosts as nodes and weighted edges representing the count of hyperlinks
between pages on the corresponding hosts. We demonstrate how such a "hostgraph"
can be used to study connectivity properties of hosts and domains over time, and
discuss a modified "copy model" to explain observed link weight distributions
as a function of subgraph size. We discuss changes in the Web over time in the
size and connectivity of Web sites and country domains. We also describe a data
mining application of the hostgraph: a related host finding algorithm which achieves
a precision of 0.65 at rank 3.'
article_processing_charge: No
author:
- first_name: K.
full_name: Bharat, K.
last_name: Bharat
- first_name: Bay-Wei
full_name: Chang, Bay-Wei
last_name: Chang
- 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: M.
full_name: Ruhl, M.
last_name: Ruhl
citation:
ama: 'Bharat K, Chang B-W, Henzinger MH, Ruhl M. Who links to whom: Mining linkage
between Web sites. In: 1st IEEE International Conference on Data Mining.
Institute of Electrical and Electronics Engineers; 2001:51-58. doi:10.1109/ICDM.2001.989500'
apa: 'Bharat, K., Chang, B.-W., Henzinger, M. H., & Ruhl, M. (2001). Who links
to whom: Mining linkage between Web sites. In 1st IEEE International Conference
on Data Mining (pp. 51–58). San Jose, CA, United States: Institute of Electrical
and Electronics Engineers. https://doi.org/10.1109/ICDM.2001.989500'
chicago: 'Bharat, K., Bay-Wei Chang, Monika H Henzinger, and M. Ruhl. “Who Links
to Whom: Mining Linkage between Web Sites.” In 1st IEEE International Conference
on Data Mining, 51–58. Institute of Electrical and Electronics Engineers,
2001. https://doi.org/10.1109/ICDM.2001.989500.'
ieee: 'K. Bharat, B.-W. Chang, M. H. Henzinger, and M. Ruhl, “Who links to whom:
Mining linkage between Web sites,” in 1st IEEE International Conference on
Data Mining, San Jose, CA, United States, 2001, pp. 51–58.'
ista: 'Bharat K, Chang B-W, Henzinger MH, Ruhl M. 2001. Who links to whom: Mining
linkage between Web sites. 1st IEEE International Conference on Data Mining. ICMD:
International Conference on Data Mining, 51–58.'
mla: 'Bharat, K., et al. “Who Links to Whom: Mining Linkage between Web Sites.”
1st IEEE International Conference on Data Mining, Institute of Electrical
and Electronics Engineers, 2001, pp. 51–58, doi:10.1109/ICDM.2001.989500.'
short: K. Bharat, B.-W. Chang, M.H. Henzinger, M. Ruhl, in:, 1st IEEE International
Conference on Data Mining, Institute of Electrical and Electronics Engineers,
2001, pp. 51–58.
conference:
end_date: 2001-12-02
location: San Jose, CA, United States
name: 'ICMD: International Conference on Data Mining'
start_date: 2001-11-29
date_created: 2022-08-18T07:12:46Z
date_published: 2001-12-01T00:00:00Z
date_updated: 2023-02-17T09:59:47Z
day: '01'
doi: 10.1109/ICDM.2001.989500
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 51-58
publication: 1st IEEE International Conference on Data Mining
publication_identifier:
isbn:
- 0-7695-1119-8
issn:
- '15504786'
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Who links to whom: Mining linkage between Web sites'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2001'
...
---
_id: '3434'
abstract:
- lang: eng
text: "This chapter contains sections titled:\r\n\r\nIntroduction\r\n\r\n- History\r\n\r\n-
Developing an Intuition of Likelihood\r\n\r\n- Method of Maximum Likelihood\r\n\r\n-
Bayesian Inference\r\n\r\n- Markov Chain Monte Carlo\r\n\r\n- Assessing Uncertainty
of Phylogenies\r\n\r\n- Hypothesis Testing and Model Choice\r\n\r\n- Comparative
Analysis\r\n\r\n- Conclusions\r\n\r\n- References"
article_processing_charge: No
author:
- first_name: John
full_name: Huelsenbeck, John
last_name: Huelsenbeck
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: 'Huelsenbeck J, Bollback JP. Application of the likelihood function in phylogenetic
analysis. In: Balding D, Bishop M, Cannings C, eds. Handbook of Statistical
Genetics. Wiley-Blackwell; 2001:415-439. doi:10.1002/9780470061619.ch15'
apa: Huelsenbeck, J., & Bollback, J. P. (2001). Application of the likelihood
function in phylogenetic analysis. In D. Balding, M. Bishop, & C. Cannings
(Eds.), Handbook of Statistical Genetics (pp. 415–439). Wiley-Blackwell.
https://doi.org/10.1002/9780470061619.ch15
chicago: Huelsenbeck, John, and Jonathan P Bollback. “Application of the Likelihood
Function in Phylogenetic Analysis.” In Handbook of Statistical Genetics,
edited by David Balding, Martin Bishop, and Chriss Cannings, 415–39. Wiley-Blackwell,
2001. https://doi.org/10.1002/9780470061619.ch15.
ieee: J. Huelsenbeck and J. P. Bollback, “Application of the likelihood function
in phylogenetic analysis,” in Handbook of Statistical Genetics, D. Balding,
M. Bishop, and C. Cannings, Eds. Wiley-Blackwell, 2001, pp. 415–439.
ista: 'Huelsenbeck J, Bollback JP. 2001.Application of the likelihood function in
phylogenetic analysis. In: Handbook of Statistical Genetics. , 415–439.'
mla: Huelsenbeck, John, and Jonathan P. Bollback. “Application of the Likelihood
Function in Phylogenetic Analysis.” Handbook of Statistical Genetics, edited
by David Balding et al., Wiley-Blackwell, 2001, pp. 415–39, doi:10.1002/9780470061619.ch15.
short: J. Huelsenbeck, J.P. Bollback, in:, D. Balding, M. Bishop, C. Cannings (Eds.),
Handbook of Statistical Genetics, Wiley-Blackwell, 2001, pp. 415–439.
date_created: 2018-12-11T12:03:19Z
date_published: 2001-01-01T00:00:00Z
date_updated: 2023-05-15T14:43:39Z
day: '01'
doi: 10.1002/9780470061619.ch15
editor:
- first_name: David
full_name: Balding, David
last_name: Balding
- first_name: Martin
full_name: Bishop, Martin
last_name: Bishop
- first_name: Chriss
full_name: Cannings, Chriss
last_name: Cannings
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 415 - 439
publication: Handbook of Statistical Genetics
publication_identifier:
isbn:
- '9781119429142 '
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2966'
quality_controlled: '1'
status: public
title: Application of the likelihood function in phylogenetic analysis
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '3438'
abstract:
- lang: eng
text: As a discipline, phylogenetics is becoming transformed by a flood of molecular
data. These data allow broad questions to be asked about the history of life,
but also present difficult statistical and computational problems. Bayesian inference
of phylogeny brings a new perspective to a number of outstanding issues in evolutionary
biology, including the analysis of large phylogenetic trees and complex evolutionary
models and the detection of the footprint of natural selection in DNA sequences.
article_processing_charge: No
author:
- first_name: John
full_name: Huelsenbeck, John
last_name: Huelsenbeck
- first_name: Fredrik
full_name: Ronquist, Fredrik
last_name: Ronquist
- first_name: Rasmus
full_name: Nielsen, Rasmus
last_name: Nielsen
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: Huelsenbeck J, Ronquist F, Nielsen R, Bollback JP. Bayesian inference of phylogeny
and its impact on evolutionary biology. Science. 2001;294(5550):2310-2314.
doi:10.1126/science.1065889
apa: Huelsenbeck, J., Ronquist, F., Nielsen, R., & Bollback, J. P. (2001). Bayesian
inference of phylogeny and its impact on evolutionary biology. Science.
American Association for the Advancement of Science. https://doi.org/10.1126/science.1065889
chicago: Huelsenbeck, John, Fredrik Ronquist, Rasmus Nielsen, and Jonathan P Bollback.
“Bayesian Inference of Phylogeny and Its Impact on Evolutionary Biology.” Science.
American Association for the Advancement of Science, 2001. https://doi.org/10.1126/science.1065889.
ieee: J. Huelsenbeck, F. Ronquist, R. Nielsen, and J. P. Bollback, “Bayesian inference
of phylogeny and its impact on evolutionary biology,” Science, vol. 294,
no. 5550. American Association for the Advancement of Science, pp. 2310–2314,
2001.
ista: Huelsenbeck J, Ronquist F, Nielsen R, Bollback JP. 2001. Bayesian inference
of phylogeny and its impact on evolutionary biology. Science. 294(5550), 2310–2314.
mla: Huelsenbeck, John, et al. “Bayesian Inference of Phylogeny and Its Impact on
Evolutionary Biology.” Science, vol. 294, no. 5550, American Association
for the Advancement of Science, 2001, pp. 2310–14, doi:10.1126/science.1065889.
short: J. Huelsenbeck, F. Ronquist, R. Nielsen, J.P. Bollback, Science 294 (2001)
2310–2314.
date_created: 2018-12-11T12:03:20Z
date_published: 2001-12-14T00:00:00Z
date_updated: 2023-05-15T14:10:13Z
day: '14'
doi: 10.1126/science.1065889
extern: '1'
external_id:
pmid:
- '11743192 '
intvolume: ' 294'
issue: '5550'
language:
- iso: eng
month: '12'
oa_version: None
page: 2310 - 2314
pmid: 1
publication: Science
publication_identifier:
issn:
- 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '2962'
quality_controlled: '1'
status: public
title: Bayesian inference of phylogeny and its impact on evolutionary biology
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 294
year: '2001'
...
---
_id: '3439'
abstract:
- lang: eng
text: High molecular weight DNA was extracted from the primary Neotropical malaria
vector, Anopheles darlingi from Capanema, Pará, Brazil, to create a small insert
genomic library, and then a phagemid library. Enriched sublibraries were constructed
from the phagemid library using a microsatellite oligo primed second strand synthesis
protocol. The resulting 242 760 individual clones were screened. The mean clone
size of the positive clones was 302 bp. Flanking primers were designed for each
suitable microsatellite sequence. Eight polymorphic loci were optimized and characterized.
The allele size ranges are based on 253 samples of A. darlingi from eastern Amazonian
and central Brazil.
acknowledgement: For support in Brazil we thank D. Galiza, R.N.L. Lacerda,E.P.
Santa Rosa, M.N.O. Segura, and R.T.L. de Souza. We also thankM.J. Braun for allowing work on the library construction at theLaboratory
of Molecular Systematics, Washington. Supported byNIH AI 40116 to JEC and Instituto
Evandro Chagas, Belém, Brazil.
article_processing_charge: No
article_type: original
author:
- first_name: Jan
full_name: Conn, Jan
last_name: Conn
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: David
full_name: Onyabe, David
last_name: Onyabe
- first_name: Tessa
full_name: Robinson, Tessa
last_name: Robinson
- first_name: Richard
full_name: Wilkerson, Richard
last_name: Wilkerson
- first_name: Marinete
full_name: Povoa, Marinete
last_name: Povoa
citation:
ama: Conn J, Bollback JP, Onyabe D, Robinson T, Wilkerson R, Povoa M. Isolation
of polymorphic microsatellite markers from the malaria vector Anopheles darlingi.
Molecular Ecology Notes. 2001;1(4):223-225. doi: 10.1046/j.1471-8278.2001.00078.x
apa: Conn, J., Bollback, J. P., Onyabe, D., Robinson, T., Wilkerson, R., & Povoa,
M. (2001). Isolation of polymorphic microsatellite markers from the malaria vector
Anopheles darlingi. Molecular Ecology Notes. Wiley-Blackwell. https://doi.org/ 10.1046/j.1471-8278.2001.00078.x
chicago: Conn, Jan, Jonathan P Bollback, David Onyabe, Tessa Robinson, Richard Wilkerson,
and Marinete Povoa. “Isolation of Polymorphic Microsatellite Markers from the
Malaria Vector Anopheles Darlingi.” Molecular Ecology Notes. Wiley-Blackwell,
2001. https://doi.org/
10.1046/j.1471-8278.2001.00078.x.
ieee: J. Conn, J. P. Bollback, D. Onyabe, T. Robinson, R. Wilkerson, and M. Povoa,
“Isolation of polymorphic microsatellite markers from the malaria vector Anopheles
darlingi,” Molecular Ecology Notes, vol. 1, no. 4. Wiley-Blackwell, pp.
223–225, 2001.
ista: Conn J, Bollback JP, Onyabe D, Robinson T, Wilkerson R, Povoa M. 2001. Isolation
of polymorphic microsatellite markers from the malaria vector Anopheles darlingi.
Molecular Ecology Notes. 1(4), 223–225.
mla: Conn, Jan, et al. “Isolation of Polymorphic Microsatellite Markers from the
Malaria Vector Anopheles Darlingi.” Molecular Ecology Notes, vol. 1, no.
4, Wiley-Blackwell, 2001, pp. 223–25, doi:
10.1046/j.1471-8278.2001.00078.x.
short: J. Conn, J.P. Bollback, D. Onyabe, T. Robinson, R. Wilkerson, M. Povoa, Molecular
Ecology Notes 1 (2001) 223–225.
date_created: 2018-12-11T12:03:20Z
date_published: 2001-12-01T00:00:00Z
date_updated: 2023-05-15T13:58:49Z
day: '01'
doi: ' 10.1046/j.1471-8278.2001.00078.x'
extern: '1'
intvolume: ' 1'
issue: '4'
language:
- iso: eng
month: '12'
oa_version: None
page: 223 - 225
publication: Molecular Ecology Notes
publication_identifier:
issn:
- 1471-8278
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2961'
quality_controlled: '1'
status: public
title: Isolation of polymorphic microsatellite markers from the malaria vector Anopheles
darlingi
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1
year: '2001'
...
---
_id: '3440'
abstract:
- lang: eng
text: "Several methods have been proposed to infer the states at the ancestral nodes
on a phylogeny. These methods assume a specific tree and set of branch lengths
when estimating the ancestral character state. Inferences of the ancestral states,
then, are conditioned on the tree and branch lengths being true. We develop a
hierarchical Bayes method for inferring the ancestral states on a tree. The method
integrates over uncertainty in the tree, branch lengths, and substitution model
parameters by using Markov chain Monte Carlo. We compare the hierarchical Bayes
inferences of ancestral states with inferences of ancestral states made under
the assumption that a specific tree is correct. We find that the methods are correlated,
but that accommodating uncertainty in parameters of the phylogenetic model can
make inferences of ancestral states even more uncertain than they would be in
an empirical Bayes analysis.\r\n"
article_processing_charge: No
article_type: original
author:
- first_name: John
full_name: Huelsenbeck, John
last_name: Huelsenbeck
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: Huelsenbeck J, Bollback JP. Empirical and hierarchical Bayesian estimation
of ancestral states. Systematic Biology. 2001;50(3):351-366. doi:10.1080/10635150119871
apa: Huelsenbeck, J., & Bollback, J. P. (2001). Empirical and hierarchical Bayesian
estimation of ancestral states. Systematic Biology. Oxford University Press.
https://doi.org/10.1080/10635150119871
chicago: Huelsenbeck, John, and Jonathan P Bollback. “Empirical and Hierarchical
Bayesian Estimation of Ancestral States.” Systematic Biology. Oxford University
Press, 2001. https://doi.org/10.1080/10635150119871.
ieee: J. Huelsenbeck and J. P. Bollback, “Empirical and hierarchical Bayesian estimation
of ancestral states,” Systematic Biology, vol. 50, no. 3. Oxford University
Press, pp. 351–366, 2001.
ista: Huelsenbeck J, Bollback JP. 2001. Empirical and hierarchical Bayesian estimation
of ancestral states. Systematic Biology. 50(3), 351–366.
mla: Huelsenbeck, John, and Jonathan P. Bollback. “Empirical and Hierarchical Bayesian
Estimation of Ancestral States.” Systematic Biology, vol. 50, no. 3, Oxford
University Press, 2001, pp. 351–66, doi:10.1080/10635150119871.
short: J. Huelsenbeck, J.P. Bollback, Systematic Biology 50 (2001) 351–366.
date_created: 2018-12-11T12:03:20Z
date_published: 2001-05-01T00:00:00Z
date_updated: 2023-05-15T13:54:01Z
day: '01'
doi: 10.1080/10635150119871
extern: '1'
external_id:
pmid:
- '12116580'
intvolume: ' 50'
issue: '3'
language:
- iso: eng
month: '05'
oa_version: None
page: 351 - 366
pmid: 1
publication: Systematic Biology
publication_identifier:
issn:
- 0039-7989
publication_status: published
publisher: Oxford University Press
publist_id: '2960'
quality_controlled: '1'
status: public
title: Empirical and hierarchical Bayesian estimation of ancestral states
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 50
year: '2001'
...