---
_id: '4278'
abstract:
- lang: eng
text: 'The ability of species to migrate that has interested ecologists for many
years. Now that so many species and ecosystems face major environmental change,
the ability of species to adapt to these changes by dispersing, migrating, or
moving between different patches of habitat can be crucial to ensuring their survivial.
This book provides a timely and wide-ranging overview of the study of dispersal
and incorporates much of the latest research. The causes, mechanisms, and consequences
of dispersal at the individual, population, species and community levels are considered.
The potential of new techniques and models for studying dispersal, drawn from
molecular biology and demography, is also explored. Perspectives and insights
are offered from the fields of evolution, conservation biology and genetics. Throughout
the book, theoretical approaches are combined with empirical data, and care has
been taken to include examples from as wide a range of species as possible. '
article_processing_charge: No
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: 'Barton NH. The evolutionary consequences of gene flow and local adaptation:
Future approaches. In: Dispersal. Oxford University Press; 2001.'
apa: 'Barton, N. H. (2001). The evolutionary consequences of gene flow and local
adaptation: Future approaches. In Dispersal. Oxford University Press.'
chicago: 'Barton, Nicholas H. “The Evolutionary Consequences of Gene Flow and Local
Adaptation: Future Approaches.” In Dispersal. Oxford University Press,
2001.'
ieee: 'N. H. Barton, “The evolutionary consequences of gene flow and local adaptation:
Future approaches,” in Dispersal, Oxford University Press, 2001.'
ista: 'Barton NH. 2001.The evolutionary consequences of gene flow and local adaptation:
Future approaches. In: Dispersal. .'
mla: 'Barton, Nicholas H. “The Evolutionary Consequences of Gene Flow and Local
Adaptation: Future Approaches.” Dispersal, Oxford University Press, 2001.'
short: N.H. Barton, in:, Dispersal, Oxford University Press, 2001.
date_created: 2018-12-11T12:08:00Z
date_published: 2001-04-01T00:00:00Z
date_updated: 2023-05-10T09:57:10Z
day: '01'
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://www.nhbs.com/dispersal-book
month: '04'
oa_version: None
publication: Dispersal
publication_identifier:
isbn:
- '9780198506591'
publication_status: published
publisher: Oxford University Press
publist_id: '1812'
quality_controlled: '1'
status: public
title: 'The evolutionary consequences of gene flow and local adaptation: Future approaches'
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4449'
abstract:
- lang: eng
text: Embedded software is software that interacts with physical processes. As em-
bedded systems increasingly permeate our daily lives on all levels, from micros-
copic devices to international networks, the cost-efficient development of reliable
embedded software is one of the grand challenges in computer science today. The
purpose of the workshop is to bring together researchers in all areas of computer
science that are traditionally distinct but relevant to embedded software develop-
ment, and to incubate a research community in this way. The workshop aims to cover
all aspects of the design and implementation of embedded software, inclu- ding
operating systems and middleware, programming languages and compilers, modeling
and validation, software engineering and programming methodologies, scheduling
and execution time analysis, networking and fault tolerance, as well as application
areas, such as embedded control, real-time signal processing, and telecommunications.
alternative_title:
- LNCS
article_processing_charge: No
citation:
ama: 'Henzinger TA, ed. EMSOFT: Embedded Software. Vol 2211. ACM; 2001. doi:10.1007/3-540-45449-7'
apa: 'Henzinger, T. A. (Ed.). (2001). EMSOFT: Embedded Software (Vol. 2211).
Presented at the EMSOFT 2001: Embedded Software, Tahoe City, CA, USA: ACM. https://doi.org/10.1007/3-540-45449-7'
chicago: 'Henzinger, Thomas A, ed. EMSOFT: Embedded Software. Vol. 2211.
ACM, 2001. https://doi.org/10.1007/3-540-45449-7.'
ieee: 'T. A. Henzinger, Ed., EMSOFT: Embedded Software, vol. 2211. ACM, 2001.'
ista: 'Henzinger TA ed. 2001. EMSOFT: Embedded Software, ACM,p.'
mla: 'Henzinger, Thomas A., editor. EMSOFT: Embedded Software. Vol. 2211,
ACM, 2001, doi:10.1007/3-540-45449-7.'
short: 'T.A. Henzinger, ed., EMSOFT: Embedded Software, ACM, 2001.'
conference:
end_date: 2001-10-10
location: Tahoe City, CA, USA
name: 'EMSOFT 2001: Embedded Software'
start_date: 2001-10-08
date_created: 2018-12-11T12:08:54Z
date_published: 2001-09-26T00:00:00Z
date_updated: 2023-05-10T09:53:17Z
day: '26'
doi: 10.1007/3-540-45449-7
editor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
extern: '1'
intvolume: ' 2211'
language:
- iso: eng
month: '09'
oa_version: None
publication_identifier:
isbn:
- '9783540426738'
publication_status: published
publisher: ACM
publist_id: '283'
quality_controlled: '1'
status: public
title: 'EMSOFT: Embedded Software'
type: conference_editor
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2211
year: '2001'
...
---
_id: '4475'
abstract:
- lang: eng
text: We provide an overview of the current status of HYTECH, and reflect on some
of the lessons learned from our experiences with the tool. HYTECH is a symbolic
model checker for mixed discrete-continuous systems that are modeled as automata
with piecewise-constant polyhedral differential inclusions. The use of a formal
input language and automated procedures for state-space traversal lay the foundation
for formally verifying properties of hybrid dynamical systems. We describe some
recent experiences analyzing three hybrid systems. We point out the successes
and limitations of the tool. The analysis procedure has been extended in a number
of ways to address some of the tool's shortcomings. We evaluate these extensions,
and conclude with some desiderata for verification tools for hybrid systems.
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: Joerg
full_name: Preussig, Joerg
last_name: Preussig
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Henzinger TA, Preussig J, Wong Toi H. Some lessons from the HYTECH experience.
In: Proceedings of the 40th IEEE Conference on Decision and Control. Vol
3. IEEE; 2001:2887-2892. doi:10.1109/.2001.980714'
apa: 'Henzinger, T. A., Preussig, J., & Wong Toi, H. (2001). Some lessons from
the HYTECH experience. In Proceedings of the 40th IEEE Conference on Decision
and Control (Vol. 3, pp. 2887–2892). Orlando, FL, USA: IEEE. https://doi.org/10.1109/.2001.980714'
chicago: Henzinger, Thomas A, Joerg Preussig, and Howard Wong Toi. “Some Lessons
from the HYTECH Experience.” In Proceedings of the 40th IEEE Conference on
Decision and Control, 3:2887–92. IEEE, 2001. https://doi.org/10.1109/.2001.980714.
ieee: T. A. Henzinger, J. Preussig, and H. Wong Toi, “Some lessons from the HYTECH
experience,” in Proceedings of the 40th IEEE Conference on Decision and Control,
Orlando, FL, USA, 2001, vol. 3, pp. 2887–2892.
ista: 'Henzinger TA, Preussig J, Wong Toi H. 2001. Some lessons from the HYTECH
experience. Proceedings of the 40th IEEE Conference on Decision and Control. CDC:
Decision and Control vol. 3, 2887–2892.'
mla: Henzinger, Thomas A., et al. “Some Lessons from the HYTECH Experience.” Proceedings
of the 40th IEEE Conference on Decision and Control, vol. 3, IEEE, 2001, pp.
2887–92, doi:10.1109/.2001.980714.
short: T.A. Henzinger, J. Preussig, H. Wong Toi, in:, Proceedings of the 40th IEEE
Conference on Decision and Control, IEEE, 2001, pp. 2887–2892.
conference:
end_date: 2001-12-07
location: Orlando, FL, USA
name: 'CDC: Decision and Control'
start_date: 2001-12-04
date_created: 2018-12-11T12:09:02Z
date_published: 2001-05-01T00:00:00Z
date_updated: 2023-05-10T09:47:20Z
day: '01'
doi: 10.1109/.2001.980714
extern: '1'
intvolume: ' 3'
language:
- iso: eng
month: '05'
oa_version: None
page: 2887 - 2892
publication: Proceedings of the 40th IEEE Conference on Decision and Control
publication_identifier:
isbn:
- '0780370619'
publication_status: published
publisher: IEEE
publist_id: '253'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Some lessons from the HYTECH experience
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 3
year: '2001'
...
---
_id: '4477'
abstract:
- lang: eng
text: The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for
decomposing a verification task about a system into subtasks about the individual
components of the system. The key to assume-guarantee reasoning is to consider
each component not in isolation, but in conjunction with assumptions about the
context of the component. Assume-guarantee principles are known for purely concurrent
contexts, which constrain the input data of a component, as well as for purely
sequential contexts, which constrain the entry configurations of a component.
We present a model for hierarchical system design which permits the arbitrary
nesting of parallel as well as serial composition, and which supports an assume-guarantee
principle for mixed parallel-serial contexts. Our model also supports both discrete
and continuous processes, and is therefore well-suited for the modeling and analysis
of embedded software systems which interact with real-world environments. Using
an example of two cooperating robots, we show refinement between a high-level
model which specifies continuous timing constraints and an implementation which
relies on discrete sampling.
acknowledgement: Support for this research was provided in part by the AFOSR MURI
grant F49620- 00-1-0327, and the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC
grant 98-DT-660, the NSF ITR grant CCR-0085949.
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: Marius
full_name: Minea, Marius
last_name: Minea
- first_name: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: 'Henzinger TA, Minea M, Prabhu V. Assume-guarantee reasoning for hierarchical
hybrid systems. In: Proceedings of the 4th International Workshop on Hybrid
Systems. Vol 2034. Springer; 2001:275-290. doi:10.1007/3-540-45351-2_24'
apa: 'Henzinger, T. A., Minea, M., & Prabhu, V. (2001). Assume-guarantee reasoning
for hierarchical hybrid systems. In Proceedings of the 4th International Workshop
on Hybrid Systems (Vol. 2034, pp. 275–290). Rome, Italy: Springer. https://doi.org/10.1007/3-540-45351-2_24'
chicago: Henzinger, Thomas A, Marius Minea, and Vinayak Prabhu. “Assume-Guarantee
Reasoning for Hierarchical Hybrid Systems.” In Proceedings of the 4th International
Workshop on Hybrid Systems, 2034:275–90. Springer, 2001. https://doi.org/10.1007/3-540-45351-2_24.
ieee: T. A. Henzinger, M. Minea, and V. Prabhu, “Assume-guarantee reasoning for
hierarchical hybrid systems,” in Proceedings of the 4th International Workshop
on Hybrid Systems, Rome, Italy, 2001, vol. 2034, pp. 275–290.
ista: 'Henzinger TA, Minea M, Prabhu V. 2001. Assume-guarantee reasoning for hierarchical
hybrid systems. Proceedings of the 4th International Workshop on Hybrid Systems.
HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 2034, 275–290.'
mla: Henzinger, Thomas A., et al. “Assume-Guarantee Reasoning for Hierarchical Hybrid
Systems.” Proceedings of the 4th International Workshop on Hybrid Systems,
vol. 2034, Springer, 2001, pp. 275–90, doi:10.1007/3-540-45351-2_24.
short: T.A. Henzinger, M. Minea, V. Prabhu, in:, Proceedings of the 4th International
Workshop on Hybrid Systems, Springer, 2001, pp. 275–290.
conference:
end_date: 2001-03-30
location: Rome, Italy
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2001-03-28
date_created: 2018-12-11T12:09:03Z
date_published: 2001-03-14T00:00:00Z
date_updated: 2023-05-09T14:47:37Z
day: '14'
doi: 10.1007/3-540-45351-2_24
extern: '1'
intvolume: ' 2034'
language:
- iso: eng
month: '03'
oa_version: None
page: 275 - 290
publication: Proceedings of the 4th International Workshop on Hybrid Systems
publication_identifier:
isbn:
- '9783540418665'
publication_status: published
publisher: Springer
publist_id: '250'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Assume-guarantee reasoning for hierarchical hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2034
year: '2001'
...
---
_id: '4478'
abstract:
- lang: eng
text: Giotto is a principled, tool-supported design methodology for implementing
embedded control systems on platforms of possibly distributed sensors, actuators,
CPUs, and networks. Giotto is based on the principle that time-triggered task
invocations plus time-triggered mode switches can form the abstract essence of
programming real-time control systems. Giotto consists of a programming language
with a formal semantics, and a retargetable compiler and runtime library. Giotto
supports the automation of control system design by strictly separating platform-independent
functionality and timing concerns from platform-dependent scheduling and communication
issues. The time-triggered predictability of Giotto makes it particularly suitable
for safety-critical applications with hard real-time constraints. We illustrate
the platform-independence and time-triggered execution of Giotto by coordinating
a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots.
acknowledgement: We thank Rupak Majumdar for implementing a prototype Giotto compiler
for Lego Mindstorms robots. We thank Dmitry Derevyanko and Winthrop Williams for
building our Intel x86 robots. We thank Edward Lee and Xiaojun Liu for help with
a Ptolemy II [4] implementation of Giotto. This research was supported in part by
the DARPA SEC grant F33615-C-98-3614, the DARPA MoBIES grant F33615- 00-C-1703,
the MARCO GSRC grant 98-DT-660, the AFOSR MURI grant F49620-00-1-0327, and the NSF
ITR grant CCR-0085949.
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: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
citation:
ama: 'Henzinger TA, Horowitz B, Kirsch C. Embedded control systems development with
Giotto. In: Proceedings of the 2nd ACM SIGPLAN Workshop on Languages, Compilers
and Tools for Embedded Systems. ACM; 2001:64-72. doi:10.1145/384197.384208'
apa: 'Henzinger, T. A., Horowitz, B., & Kirsch, C. (2001). Embedded control
systems development with Giotto. In Proceedings of the 2nd ACM SIGPLAN workshop
on Languages, compilers and tools for embedded systems (pp. 64–72). New York,
NY, United States: ACM. https://doi.org/10.1145/384197.384208'
chicago: Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Embedded
Control Systems Development with Giotto.” In Proceedings of the 2nd ACM SIGPLAN
Workshop on Languages, Compilers and Tools for Embedded Systems, 64–72. ACM,
2001. https://doi.org/10.1145/384197.384208.
ieee: T. A. Henzinger, B. Horowitz, and C. Kirsch, “Embedded control systems development
with Giotto,” in Proceedings of the 2nd ACM SIGPLAN workshop on Languages,
compilers and tools for embedded systems, New York, NY, United States, 2001,
pp. 64–72.
ista: 'Henzinger TA, Horowitz B, Kirsch C. 2001. Embedded control systems development
with Giotto. Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers
and tools for embedded systems. LCTES: Languages, Compilers, and Tools for Embedded
Systems, 64–72.'
mla: Henzinger, Thomas A., et al. “Embedded Control Systems Development with Giotto.”
Proceedings of the 2nd ACM SIGPLAN Workshop on Languages, Compilers and Tools
for Embedded Systems, ACM, 2001, pp. 64–72, doi:10.1145/384197.384208.
short: T.A. Henzinger, B. Horowitz, C. Kirsch, in:, Proceedings of the 2nd ACM SIGPLAN
Workshop on Languages, Compilers and Tools for Embedded Systems, ACM, 2001, pp.
64–72.
conference:
location: New York, NY, United States
name: 'LCTES: Languages, Compilers, and Tools for Embedded Systems'
date_created: 2018-12-11T12:09:03Z
date_published: 2001-06-01T00:00:00Z
date_updated: 2023-05-10T09:37:20Z
day: '01'
doi: 10.1145/384197.384208
extern: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: 64 - 72
publication: Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and
tools for embedded systems
publication_identifier:
isbn:
- '9781581134254'
publication_status: published
publisher: ACM
publist_id: '251'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Embedded control systems development with Giotto
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4479'
abstract:
- lang: eng
text: Giotto provides an abstract programmer’s model for the implementation of embedded
control systems with hard real-time constraints. A typical control application
consists of periodic software tasks together with a mode switching logic for enabling
and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations,
and mode switches independent of any implementation platform. Giotto can be annotated
with platform constraints such as task-to-host mappings, and task and communication
schedules. The annotations are directives for the Giotto compiler, but they do
not alter the functionality and timing of a Giotto program. By separating the
platform-independent from the platform-dependent concerns, Giotto enables a great
deal of flexibility in choosing control platforms as well as a great deal of automation
in the validation and synthesis of control software. The time-triggered nature
of Giotto achieves timing predictability, which makes Giotto particularly suitable
for safety-critical applications.
acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614
and by the MARCO GSRC grant 98-DT-660.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
citation:
ama: 'Henzinger TA, Horowitz B, Kirsch C. Giotto: A time-triggered language for
embedded programming. In: Proceedings of the 1st International Workshop on
Embedded Software. Vol 2211. ACM; 2001:166-184. doi:10.1007/3-540-45449-7_12'
apa: 'Henzinger, T. A., Horowitz, B., & Kirsch, C. (2001). Giotto: A time-triggered
language for embedded programming. In Proceedings of the 1st International
Workshop on Embedded Software (Vol. 2211, pp. 166–184). Tahoe City, CA, USA:
ACM. https://doi.org/10.1007/3-540-45449-7_12'
chicago: 'Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Giotto:
A Time-Triggered Language for Embedded Programming.” In Proceedings of the
1st International Workshop on Embedded Software, 2211:166–84. ACM, 2001. https://doi.org/10.1007/3-540-45449-7_12.'
ieee: 'T. A. Henzinger, B. Horowitz, and C. Kirsch, “Giotto: A time-triggered language
for embedded programming,” in Proceedings of the 1st International Workshop
on Embedded Software, Tahoe City, CA, USA, 2001, vol. 2211, pp. 166–184.'
ista: 'Henzinger TA, Horowitz B, Kirsch C. 2001. Giotto: A time-triggered language
for embedded programming. Proceedings of the 1st International Workshop on Embedded
Software. EMSOFT: Embedded Software , LNCS, vol. 2211, 166–184.'
mla: 'Henzinger, Thomas A., et al. “Giotto: A Time-Triggered Language for Embedded
Programming.” Proceedings of the 1st International Workshop on Embedded Software,
vol. 2211, ACM, 2001, pp. 166–84, doi:10.1007/3-540-45449-7_12.'
short: T.A. Henzinger, B. Horowitz, C. Kirsch, in:, Proceedings of the 1st International
Workshop on Embedded Software, ACM, 2001, pp. 166–184.
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:04Z
date_published: 2001-09-26T00:00:00Z
date_updated: 2023-05-10T09:42:10Z
day: '26'
doi: 10.1007/3-540-45449-7_12
extern: '1'
intvolume: ' 2211'
language:
- iso: eng
month: '09'
oa_version: None
page: 166 - 184
publication: Proceedings of the 1st International Workshop on Embedded Software
publication_identifier:
isbn:
- '9783540426738'
publication_status: published
publisher: ACM
publist_id: '252'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Giotto: A time-triggered language for embedded programming'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2211
year: '2001'
...
---
_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: '12925'
abstract:
- lang: eng
text: Normal function of organs and cells is tightly linked to the cytoarchitecture.
Control of the cell volume is therefore vital for the organism. A widely established
strategy of cells to counteract swelling is the activation of chloride and potassium
channels, which leads to a net efflux of salt followed by water - a process termed
regulatory volume decrease. Since there is evidence for swelling-dependent chloride
channels (IClswell) being activated also during pathological processes, the identification
of the molecular entity underlying IClswell is of utmost importance. Several proteins
are discussed as the channel forming IClswell, i.e. phospholemman, p-glycoprotein,
CLC-3 and ICln. In this review we would like to focus on the properties of ICln,
a protein cloned from a Madin Darby canine kidney (MDCK) cell library whose expression
in Xenopus laevis oocytes resulted in a nucleotide sensitive outwardly rectifying
chloride current closely resembling the biophysical properties of IClswell.
article_processing_charge: No
article_type: original
author:
- first_name: Johannes
full_name: Fürst, Johannes
last_name: Fürst
- first_name: Martin
full_name: Jakab, Martin
last_name: Jakab
- first_name: Matthias
full_name: König, Matthias
last_name: König
- first_name: Markus
full_name: Ritter, Markus
last_name: Ritter
- first_name: Martin
full_name: Gschwentner, Martin
last_name: Gschwentner
- first_name: Jakob
full_name: Rudzki, Jakob
last_name: Rudzki
- first_name: Johann G
full_name: Danzl, Johann G
id: 42EFD3B6-F248-11E8-B48F-1D18A9856A87
last_name: Danzl
orcid: 0000-0001-8559-3973
- first_name: Michael
full_name: Mayer, Michael
last_name: Mayer
- first_name: Carmen M.
full_name: Burtscher, Carmen M.
last_name: Burtscher
- first_name: Julia
full_name: Schirmer, Julia
last_name: Schirmer
- first_name: Brigitte
full_name: Maier, Brigitte
last_name: Maier
- first_name: Manfred
full_name: Nairz, Manfred
last_name: Nairz
- first_name: Sabine
full_name: Chwatal, Sabine
last_name: Chwatal
- first_name: Markus
full_name: Paulmichl, Markus
last_name: Paulmichl
citation:
ama: Fürst J, Jakab M, König M, et al. Structure and Function of the Ion Channel
ICln. Cellular Physiology and Biochemistry. 2000;10(5-6):329-334. doi:10.1159/000016374
apa: Fürst, J., Jakab, M., König, M., Ritter, M., Gschwentner, M., Rudzki, J., …
Paulmichl, M. (2000). Structure and Function of the Ion Channel ICln. Cellular
Physiology and Biochemistry. S. Karger AG. https://doi.org/10.1159/000016374
chicago: Fürst, Johannes, Martin Jakab, Matthias König, Markus Ritter, Martin Gschwentner,
Jakob Rudzki, Johann G Danzl, et al. “Structure and Function of the Ion Channel
ICln.” Cellular Physiology and Biochemistry. S. Karger AG, 2000. https://doi.org/10.1159/000016374.
ieee: J. Fürst et al., “Structure and Function of the Ion Channel ICln,”
Cellular Physiology and Biochemistry, vol. 10, no. 5–6. S. Karger AG, pp.
329–334, 2000.
ista: Fürst J, Jakab M, König M, Ritter M, Gschwentner M, Rudzki J, Danzl JG, Mayer
M, Burtscher CM, Schirmer J, Maier B, Nairz M, Chwatal S, Paulmichl M. 2000. Structure
and Function of the Ion Channel ICln. Cellular Physiology and Biochemistry. 10(5–6),
329–334.
mla: Fürst, Johannes, et al. “Structure and Function of the Ion Channel ICln.” Cellular
Physiology and Biochemistry, vol. 10, no. 5–6, S. Karger AG, 2000, pp. 329–34,
doi:10.1159/000016374.
short: J. Fürst, M. Jakab, M. König, M. Ritter, M. Gschwentner, J. Rudzki, J.G.
Danzl, M. Mayer, C.M. Burtscher, J. Schirmer, B. Maier, M. Nairz, S. Chwatal,
M. Paulmichl, Cellular Physiology and Biochemistry 10 (2000) 329–334.
date_created: 2023-05-08T09:04:58Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-05-08T10:07:10Z
doi: 10.1159/000016374
extern: '1'
external_id:
pmid:
- '11125213'
intvolume: ' 10'
issue: 5-6
keyword:
- Physiology
language:
- iso: eng
oa_version: None
page: 329-334
pmid: 1
publication: Cellular Physiology and Biochemistry
publication_identifier:
issn:
- 1015-8987
- 1421-9778
publication_status: published
publisher: S. Karger AG
quality_controlled: '1'
scopus_import: '1'
status: public
title: Structure and Function of the Ion Channel ICln
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2000'
...
---
_id: '842'
article_processing_charge: No
article_type: original
author:
- first_name: Yuri
full_name: Wolf, Yuri
last_name: Wolf
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Eugene
full_name: Koonin, Eugene
last_name: Koonin
citation:
ama: Wolf Y, Kondrashov F, Koonin E. No footprints of primordial introns in a eukaryotic
genome. Trends in Genetics. 2000;16(8):333-334. doi:10.1016/S0168-9525(00)02059-X
apa: Wolf, Y., Kondrashov, F., & Koonin, E. (2000). No footprints of primordial
introns in a eukaryotic genome. Trends in Genetics. Elsevier. https://doi.org/10.1016/S0168-9525(00)02059-X
chicago: Wolf, Yuri, Fyodor Kondrashov, and Eugene Koonin. “No Footprints of Primordial
Introns in a Eukaryotic Genome.” Trends in Genetics. Elsevier, 2000. https://doi.org/10.1016/S0168-9525(00)02059-X.
ieee: Y. Wolf, F. Kondrashov, and E. Koonin, “No footprints of primordial introns
in a eukaryotic genome,” Trends in Genetics, vol. 16, no. 8. Elsevier,
pp. 333–334, 2000.
ista: Wolf Y, Kondrashov F, Koonin E. 2000. No footprints of primordial introns
in a eukaryotic genome. Trends in Genetics. 16(8), 333–334.
mla: Wolf, Yuri, et al. “No Footprints of Primordial Introns in a Eukaryotic Genome.”
Trends in Genetics, vol. 16, no. 8, Elsevier, 2000, pp. 333–34, doi:10.1016/S0168-9525(00)02059-X.
short: Y. Wolf, F. Kondrashov, E. Koonin, Trends in Genetics 16 (2000) 333–334.
date_created: 2018-12-11T11:48:48Z
date_published: 2000-08-01T00:00:00Z
date_updated: 2023-05-08T09:22:03Z
day: '01'
doi: 10.1016/S0168-9525(00)02059-X
extern: '1'
external_id:
pmid:
- '10904260 '
intvolume: ' 16'
issue: '8'
language:
- iso: eng
month: '08'
oa_version: None
page: 333 - 334
pmid: 1
publication: Trends in Genetics
publication_identifier:
issn:
- 0168-9479
publication_status: published
publisher: Elsevier
publist_id: '6806'
quality_controlled: '1'
scopus_import: '1'
status: public
title: No footprints of primordial introns in a eukaryotic genome
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 16
year: '2000'
...
---
_id: '8525'
abstract:
- lang: eng
text: Let M be a smooth compact manifold of dimension at least 2 and Diffr(M) be
the space of C r smooth diffeomorphisms of M. Associate to each diffeomorphism
f;isin; Diffr(M) the sequence P n (f) of the number of isolated periodic points
for f of period n. In this paper we exhibit an open set N in the space of diffeomorphisms
Diffr(M) such for a Baire generic diffeomorphism f∈N the number of periodic points
P n f grows with a period n faster than any following sequence of numbers {a n
} n ∈ Z + along a subsequence, i.e. P n (f)>a ni for some n i →∞ with i→∞. In
the cases of surface diffeomorphisms, i.e. dim M≡2, an open set N with a supergrowth
of the number of periodic points is a Newhouse domain. A proof of the man result
is based on the Gontchenko–Shilnikov–Turaev Theorem [GST]. A complete proof of
that theorem is also presented.
article_processing_charge: No
article_type: original
author:
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
citation:
ama: Kaloshin V. Generic diffeomorphisms with superexponential growth of number
of periodic orbits. Communications in Mathematical Physics. 2000;211:253-271.
doi:10.1007/s002200050811
apa: Kaloshin, V. (2000). Generic diffeomorphisms with superexponential growth of
number of periodic orbits. Communications in Mathematical Physics. Springer
Nature. https://doi.org/10.1007/s002200050811
chicago: Kaloshin, Vadim. “Generic Diffeomorphisms with Superexponential Growth
of Number of Periodic Orbits.” Communications in Mathematical Physics.
Springer Nature, 2000. https://doi.org/10.1007/s002200050811.
ieee: V. Kaloshin, “Generic diffeomorphisms with superexponential growth of number
of periodic orbits,” Communications in Mathematical Physics, vol. 211.
Springer Nature, pp. 253–271, 2000.
ista: Kaloshin V. 2000. Generic diffeomorphisms with superexponential growth of
number of periodic orbits. Communications in Mathematical Physics. 211, 253–271.
mla: Kaloshin, Vadim. “Generic Diffeomorphisms with Superexponential Growth of Number
of Periodic Orbits.” Communications in Mathematical Physics, vol. 211,
Springer Nature, 2000, pp. 253–71, doi:10.1007/s002200050811.
short: V. Kaloshin, Communications in Mathematical Physics 211 (2000) 253–271.
date_created: 2020-09-18T10:50:20Z
date_published: 2000-04-01T00:00:00Z
date_updated: 2021-01-12T08:19:52Z
day: '01'
doi: 10.1007/s002200050811
extern: '1'
intvolume: ' 211'
keyword:
- Mathematical Physics
- Statistical and Nonlinear Physics
language:
- iso: eng
month: '04'
oa_version: None
page: 253-271
publication: Communications in Mathematical Physics
publication_identifier:
issn:
- 0010-3616
- 1432-0916
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Generic diffeomorphisms with superexponential growth of number of periodic
orbits
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 211
year: '2000'
...
---
_id: '1736'
abstract:
- lang: eng
text: A coding scheme called diode is compared with duobinary signalling and with
normal binary transmission. It is shown that the diode coding suppresses the FWM
products of a three channel DWDM system and this reduction against that achieved
with duobinary coding is presented. The results presented show how the average
level of the FWM products relative to the average levels of the three optical
carriers vary over the channel spacing range. The suppression observed is about
/ dB more than that achieved with duobinary modulation and is greater for narrow
channel spacing.
alternative_title:
- LEOS
article_processing_charge: No
author:
- first_name: Georgios
full_name: Katsaros, Georgios
id: 38DB5788-F248-11E8-B48F-1D18A9856A87
last_name: Katsaros
- first_name: Phil
full_name: Lane, Phil
last_name: Lane
- first_name: Michelle
full_name: Murphy, Michelle
last_name: Murphy
citation:
ama: 'Katsaros G, Lane P, Murphy M. Comparison of the impact of FWM on binary, duobinary
and dicode modulation in DWDM systems. In: Proceedings of the 2000 IEEE Annual
Meeting Conference . Vol 1. IEEE; 2000:27-28. doi:10.1109/LEOS.2000.890656'
apa: 'Katsaros, G., Lane, P., & Murphy, M. (2000). Comparison of the impact
of FWM on binary, duobinary and dicode modulation in DWDM systems. In Proceedings
of the 2000 IEEE Annual Meeting Conference (Vol. 1, pp. 27–28). Rio Grande,
PR, USA: IEEE. https://doi.org/10.1109/LEOS.2000.890656'
chicago: Katsaros, Georgios, Phil Lane, and Michelle Murphy. “Comparison of the
Impact of FWM on Binary, Duobinary and Dicode Modulation in DWDM Systems.” In
Proceedings of the 2000 IEEE Annual Meeting Conference , 1:27–28. IEEE,
2000. https://doi.org/10.1109/LEOS.2000.890656.
ieee: G. Katsaros, P. Lane, and M. Murphy, “Comparison of the impact of FWM on binary,
duobinary and dicode modulation in DWDM systems,” in Proceedings of the 2000
IEEE Annual Meeting Conference , Rio Grande, PR, USA, 2000, vol. 1, pp. 27–28.
ista: Katsaros G, Lane P, Murphy M. 2000. Comparison of the impact of FWM on binary,
duobinary and dicode modulation in DWDM systems. Proceedings of the 2000 IEEE
Annual Meeting Conference . Lasers and Electro Optics Society Annual Meeting,
LEOS, vol. 1, 27–28.
mla: Katsaros, Georgios, et al. “Comparison of the Impact of FWM on Binary, Duobinary
and Dicode Modulation in DWDM Systems.” Proceedings of the 2000 IEEE Annual
Meeting Conference , vol. 1, IEEE, 2000, pp. 27–28, doi:10.1109/LEOS.2000.890656.
short: G. Katsaros, P. Lane, M. Murphy, in:, Proceedings of the 2000 IEEE Annual
Meeting Conference , IEEE, 2000, pp. 27–28.
conference:
end_date: 2000-11-16
location: Rio Grande, PR, USA
name: Lasers and Electro Optics Society Annual Meeting
start_date: 2000-11-13
date_created: 2018-12-11T11:53:44Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-05-04T14:46:21Z
day: '01'
doi: 10.1109/LEOS.2000.890656
extern: '1'
intvolume: ' 1'
language:
- iso: eng
month: '01'
oa_version: None
page: 27 - 28
publication: 'Proceedings of the 2000 IEEE Annual Meeting Conference '
publication_identifier:
isbn:
- 078035947X
publication_status: published
publisher: IEEE
publist_id: '5388'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Comparison of the impact of FWM on binary, duobinary and dicode modulation
in DWDM systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1
year: '2000'
...