---
_id: '4432'
abstract:
- lang: eng
text: We add freeze quantifiers to the game logic ATL in order to specify real-time
objectives for games played on timed structures. We define the semantics of the
resulting logic TATL by restricting the players to physically meaningful strategies,
which do not prevent time from diverging. We show that TATL can be model checked
over timed automaton games. We also specify timed optimization problems for physically
meaningful strategies, and we show that for timed automaton games, the optimal
answers can be approximated to within any degree of precision.
acknowledgement: This research was supported in part by the NSF grants CCR-0208875,
CCR-0225610, and CCR-0234690.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vinayak
full_name: Prabhu, Vinayak S
last_name: Prabhu
citation:
ama: 'Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: Vol 4202.
Springer; 2006:1-17. doi:10.1007/11867340_1'
apa: 'Henzinger, T. A., & Prabhu, V. (2006). Timed alternating-time temporal
logic (Vol. 4202, pp. 1–17). Presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, Springer. https://doi.org/10.1007/11867340_1'
chicago: Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal
Logic,” 4202:1–17. Springer, 2006. https://doi.org/10.1007/11867340_1.
ieee: 'T. A. Henzinger and V. Prabhu, “Timed alternating-time temporal logic,” presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, vol. 4202,
pp. 1–17.'
ista: 'Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.'
mla: Henzinger, Thomas A., and Vinayak Prabhu. Timed Alternating-Time Temporal
Logic. Vol. 4202, Springer, 2006, pp. 1–17, doi:10.1007/11867340_1.
short: T.A. Henzinger, V. Prabhu, in:, Springer, 2006, pp. 1–17.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:49Z
date_published: 2006-09-19T00:00:00Z
date_updated: 2021-01-12T07:56:56Z
day: '19'
doi: 10.1007/11867340_1
extern: 1
intvolume: ' 4202'
month: '09'
page: 1 - 17
publication_status: published
publisher: Springer
publist_id: '296'
quality_controlled: 0
status: public
title: Timed alternating-time temporal logic
type: conference
volume: 4202
year: '2006'
...
---
_id: '4436'
abstract:
- lang: eng
text: We present an assume-guarantee interface algebra for real-time components.
In our formalism a component implements a set of task sequences that share a resource.
A component interface consists of an arrival rate function and a latency for each
task sequence, and a capacity function for the shared resource. The interface
specifies that the component guarantees certain task latencies depending on assumptions
about task arrival rates and allocated resource capacities. Our algebra defines
compatibility and refinement relations on interfaces. Interface compatibility
can be checked on partial designs, even when some component interfaces are yet
unknown. In this case interface composition computes as new assumptions the weakest
constraints on the unknown components that are necessary to satisfy the specified
guarantees. Interface refinement is defined in a way that ensures that compatible
interfaces can be refined and implemented independently. Our algebra thus formalizes
an interface-based design methodology that supports both the incremental addition
of new components and the independent stepwise refinement of existing components.
We demonstrate the flexibility and efficiency of the framework through simulation
experiments.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Matic S. An interface algebra for real-time components. In:
IEEE; 2006:253-266. doi:10.1109/RTAS.2006.11'
apa: 'Henzinger, T. A., & Matic, S. (2006). An interface algebra for real-time
components (pp. 253–266). Presented at the RTAS: Real-time and Embedded Technology
and Applications Symposium, IEEE. https://doi.org/10.1109/RTAS.2006.11'
chicago: Henzinger, Thomas A, and Slobodan Matic. “An Interface Algebra for Real-Time
Components,” 253–66. IEEE, 2006. https://doi.org/10.1109/RTAS.2006.11.
ieee: 'T. A. Henzinger and S. Matic, “An interface algebra for real-time components,”
presented at the RTAS: Real-time and Embedded Technology and Applications Symposium,
2006, pp. 253–266.'
ista: 'Henzinger TA, Matic S. 2006. An interface algebra for real-time components.
RTAS: Real-time and Embedded Technology and Applications Symposium, 253–266.'
mla: Henzinger, Thomas A., and Slobodan Matic. An Interface Algebra for Real-Time
Components. IEEE, 2006, pp. 253–66, doi:10.1109/RTAS.2006.11.
short: T.A. Henzinger, S. Matic, in:, IEEE, 2006, pp. 253–266.
conference:
name: 'RTAS: Real-time and Embedded Technology and Applications Symposium'
date_created: 2018-12-11T12:08:50Z
date_published: 2006-04-24T00:00:00Z
date_updated: 2021-01-12T07:56:57Z
day: '24'
doi: 10.1109/RTAS.2006.11
extern: 1
month: '04'
page: 253 - 266
publication_status: published
publisher: IEEE
publist_id: '294'
quality_controlled: 0
status: public
title: An interface algebra for real-time components
type: conference
year: '2006'
...
---
_id: '4437'
abstract:
- lang: eng
text: The synthesis of reactive systems requires the solution of two-player games
on graphs with ω-regular objectives. When the objective is specified by a linear
temporal logic formula or nondeterministic Büchi automaton, then previous algorithms
for solving the game require the construction of an equivalent deterministic automaton.
However, determinization for automata on infinite words is extremely complicated,
and current implementations fail to produce deterministic automata even for relatively
small inputs. We show how to construct, from a given nondeterministic Büchi automaton,
an equivalent nondeterministic parity automaton that is good for solving games
with objective . The main insight is that a nondeterministic automaton is good
for solving games if it fairly simulates the equivalent deterministic automaton.
In this way, we omit the determinization step in game solving and reactive synthesis.
The fact that our automata are nondeterministic makes them surprisingly simple,
amenable to symbolic implementation, and allows an incremental search for winning
strategies.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Henzinger TA, Piterman N. Solving games without determinization. In: Vol 4207.
Springer; 2006:395-410. doi:10.1007/11874683_26'
apa: 'Henzinger, T. A., & Piterman, N. (2006). Solving games without determinization
(Vol. 4207, pp. 395–410). Presented at the CSL: Computer Science Logic, Springer.
https://doi.org/10.1007/11874683_26'
chicago: Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization,”
4207:395–410. Springer, 2006. https://doi.org/10.1007/11874683_26.
ieee: 'T. A. Henzinger and N. Piterman, “Solving games without determinization,”
presented at the CSL: Computer Science Logic, 2006, vol. 4207, pp. 395–410.'
ista: 'Henzinger TA, Piterman N. 2006. Solving games without determinization. CSL:
Computer Science Logic, LNCS, vol. 4207, 395–410.'
mla: Henzinger, Thomas A., and Nir Piterman. Solving Games without Determinization.
Vol. 4207, Springer, 2006, pp. 395–410, doi:10.1007/11874683_26.
short: T.A. Henzinger, N. Piterman, in:, Springer, 2006, pp. 395–410.
conference:
name: 'CSL: Computer Science Logic'
date_created: 2018-12-11T12:08:51Z
date_published: 2006-09-20T00:00:00Z
date_updated: 2021-01-12T07:56:58Z
day: '20'
doi: 10.1007/11874683_26
extern: 1
intvolume: ' 4207'
month: '09'
page: 395 - 410
publication_status: published
publisher: Springer
publist_id: '295'
quality_controlled: 0
status: public
title: Solving games without determinization
type: conference
volume: 4207
year: '2006'
...
---
_id: '4451'
abstract:
- lang: eng
text: One source of complexity in the μ-calculus is its ability to specify an unbounded
number of switches between universal (AX) and existential (EX) branching modes.
We therefore study the problems of satisfiability, validity, model checking, and
implication for the universal and existential fragments of the μ-calculus, in
which only one branching mode is allowed. The universal fragment is rich enough
to express most specifications of interest, and therefore improved algorithms
are of practical importance. We show that while the satisfiability and validity
problems become indeed simpler for the existential and universal fragments, this
is, unfortunately, not the case for model checking and implication. We also show
the corresponding results for the alternation-free fragment of the μ-calculus,
where no alternations between least and greatest fixed points are allowed. Our
results imply that efforts to find a polynomial-time model-checking algorithm
for the μ-calculus can be replaced by efforts to find such an algorithm for the
universal or existential fragment.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments
of the mu-calculus. Theoretical Computer Science. 2006;354(2):173-186.
doi:10.1016/j.tcs.2005.11.015
apa: Henzinger, T. A., Kupferman, O., & Majumdar, R. (2006). On the universal
and existential fragments of the mu-calculus. Theoretical Computer Science.
Elsevier. https://doi.org/10.1016/j.tcs.2005.11.015
chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science.
Elsevier, 2006. https://doi.org/10.1016/j.tcs.2005.11.015.
ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
fragments of the mu-calculus,” Theoretical Computer Science, vol. 354,
no. 2. Elsevier, pp. 173–186, 2006.
ista: Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential
fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186.
mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of
the Mu-Calculus.” Theoretical Computer Science, vol. 354, no. 2, Elsevier,
2006, pp. 173–86, doi:10.1016/j.tcs.2005.11.015.
short: T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354
(2006) 173–186.
date_created: 2018-12-11T12:08:55Z
date_published: 2006-03-28T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '28'
doi: 10.1016/j.tcs.2005.11.015
extern: 1
intvolume: ' 354'
issue: '2'
month: '03'
page: 173 - 186
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '276'
quality_controlled: 0
status: public
title: On the universal and existential fragments of the mu-calculus
type: journal_article
volume: 354
year: '2006'
...
---
_id: '4523'
abstract:
- lang: eng
text: We consider the problem if a given program satisfies a specified safety property.
Interesting programs have infinite state spaces, with inputs ranging over infinite
domains, and for these programs the property checking problem is undecidable.
Two broad approaches to property checking are testing and verification. Testing
tries to find inputs and executions which demonstrate violations of the property.
Verification tries to construct a formal proof which shows that all executions
of the program satisfy the property. Testing works best when errors are easy to
find, but it is often difficult to achieve sufficient coverage for correct programs.
On the other hand, verification methods are most successful when proofs are easy
to find, but they are often inefficient at discovering errors. We propose a new
algorithm, Synergy, which combines testing and verification. Synergy unifies several
ideas from the literature, including counterexample-guided model checking, directed
testing, and partition refinement.This paper presents a description of the Synergy
algorithm, its theoretical properties, a comparison with related algorithms, and
a prototype implementation called Yogi.
author:
- first_name: Bhargav
full_name: Gulavani, Bhargav S
last_name: Gulavani
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Yamini
full_name: Kannan, Yamini
last_name: Kannan
- first_name: Aditya
full_name: Nori, Aditya V
last_name: Nori
- first_name: Sriram
full_name: Rajamani, Sriram K
last_name: Rajamani
citation:
ama: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm
for property checking. In: ACM; 2006:117-127. doi:10.1145/1181775.1181790'
apa: 'Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., & Rajamani, S. (2006).
Synergy: A new algorithm for property checking (pp. 117–127). Presented at the
FSE: Foundations of Software Engineering, ACM. https://doi.org/10.1145/1181775.1181790'
chicago: 'Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and
Sriram Rajamani. “Synergy: A New Algorithm for Property Checking,” 117–27. ACM,
2006. https://doi.org/10.1145/1181775.1181790.'
ieee: 'B. Gulavani, T. A. Henzinger, Y. Kannan, A. Nori, and S. Rajamani, “Synergy:
A new algorithm for property checking,” presented at the FSE: Foundations of Software
Engineering, 2006, pp. 117–127.'
ista: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. 2006. Synergy: A
new algorithm for property checking. FSE: Foundations of Software Engineering,
117–127.'
mla: 'Gulavani, Bhargav, et al. Synergy: A New Algorithm for Property Checking.
ACM, 2006, pp. 117–27, doi:10.1145/1181775.1181790.'
short: B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, ACM, 2006,
pp. 117–127.
conference:
name: 'FSE: Foundations of Software Engineering'
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '01'
doi: 10.1145/1181775.1181790
extern: 1
month: '01'
page: 117 - 127
publication_status: published
publisher: ACM
publist_id: '206'
quality_controlled: 0
status: public
title: 'Synergy: A new algorithm for property checking'
type: conference
year: '2006'
...
---
_id: '4526'
abstract:
- lang: eng
text: 'We designed and implemented a new programming language called Hierarchical
Timing Language (HTL) for hard realtime systems. Critical timing constraints are
specified within the language,and ensured by the compiler. Programs in HTL are
extensible in two dimensions without changing their timing behavior: new program
modules can be added, and individual program tasks can be refined. The mechanism
supporting time invariance under parallel composition is that different program
modules communicate at specified instances of time. Time invariance under refinement
is achieved by conservative scheduling of the top level. HTL is a coordination
language, in that individual tasks can be implemented in "foreign" languages.
As a case study, we present a distributed HTL implementation of an automotive
steer-by-wire controller.'
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Daniel
full_name: Iercan, Daniel
last_name: Iercan
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Alberto
full_name: Sangiovanni-Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. A hierarchical
coordination language for interacting real-time tasks. In: ACM; 2006:132-141.
doi:10.1145/1176887.1176907'
apa: 'Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., & Sangiovanni Vincentelli,
A. (2006). A hierarchical coordination language for interacting real-time tasks
(pp. 132–141). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1176887.1176907'
chicago: Ghosal, Arkadeb, Thomas A Henzinger, Daniel Iercan, Christoph Kirsch, and
Alberto Sangiovanni Vincentelli. “A Hierarchical Coordination Language for Interacting
Real-Time Tasks,” 132–41. ACM, 2006. https://doi.org/10.1145/1176887.1176907.
ieee: 'A. Ghosal, T. A. Henzinger, D. Iercan, C. Kirsch, and A. Sangiovanni Vincentelli,
“A hierarchical coordination language for interacting real-time tasks,” presented
at the EMSOFT: Embedded Software , 2006, pp. 132–141.'
ista: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. 2006.
A hierarchical coordination language for interacting real-time tasks. EMSOFT:
Embedded Software , 132–141.'
mla: Ghosal, Arkadeb, et al. A Hierarchical Coordination Language for Interacting
Real-Time Tasks. ACM, 2006, pp. 132–41, doi:10.1145/1176887.1176907.
short: A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, A. Sangiovanni Vincentelli,
in:, ACM, 2006, pp. 132–141.
conference:
name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '01'
doi: 10.1145/1176887.1176907
extern: 1
month: '01'
page: 132 - 141
publication_status: published
publisher: ACM
publist_id: '201'
quality_controlled: 0
status: public
title: A hierarchical coordination language for interacting real-time tasks
type: conference
year: '2006'
...
---
_id: '4528'
abstract:
- lang: eng
text: Computational modeling of biological systems is becoming increasingly common
as scientists attempt to understand biological phenomena in their full complexity.
Here we distinguish between two types of biological models mathematical and computational
- according to their different representations of biological phenomena and their
diverse potential. We call the approach of constructing computational models of
biological systems executable biology, as it focuses on the design of executable
computer algorithms that mimic biological phenomena. We give an overview of the
main modeling efforts in this direction, and discuss some of the new challenges
that executable biology poses for computer science and biology. We argue that
for executable biology to reach its full potential as a mainstream biological
technique, formal and algorithmic approaches must be integrated into biological
research, driving biology towards a more precise engineering discipline.
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Fisher J, Henzinger TA. Executable biology. In: IEEE; 2006:1675-1682. doi:10.1109/WSC.2006.322942'
apa: 'Fisher, J., & Henzinger, T. A. (2006). Executable biology (pp. 1675–1682).
Presented at the WSC: Winter Simulation Conference, IEEE. https://doi.org/10.1109/WSC.2006.322942'
chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Biology,” 1675–82.
IEEE, 2006. https://doi.org/10.1109/WSC.2006.322942.
ieee: 'J. Fisher and T. A. Henzinger, “Executable biology,” presented at the WSC:
Winter Simulation Conference, 2006, pp. 1675–1682.'
ista: 'Fisher J, Henzinger TA. 2006. Executable biology. WSC: Winter Simulation
Conference, 1675–1682.'
mla: Fisher, Jasmin, and Thomas A. Henzinger. Executable Biology. IEEE, 2006,
pp. 1675–82, doi:10.1109/WSC.2006.322942.
short: J. Fisher, T.A. Henzinger, in:, IEEE, 2006, pp. 1675–1682.
conference:
name: 'WSC: Winter Simulation Conference'
date_created: 2018-12-11T12:09:19Z
date_published: 2006-12-03T00:00:00Z
date_updated: 2021-01-12T07:59:28Z
day: '03'
doi: 10.1109/WSC.2006.322942
extern: 1
month: '12'
page: 1675 - 1682
publication_status: published
publisher: IEEE
publist_id: '197'
quality_controlled: 0
status: public
title: Executable biology
type: conference
year: '2006'
...
---
_id: '4538'
abstract:
- lang: eng
text: A stochastic graph game is played by two players on a game graph with probabilistic
transitions. We consider stochastic graph games with ω-regular winning conditions
specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy
improvement algorithm for stochastic parity games; this is the first non-brute-force
algorithm for solving these games. From the strategy improvement algorithm we
obtain a randomized subexponential-time algorithm to solve such games.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Strategy improvement and randomized subexponential
algorithms for stochastic parity games. In: Vol 3884. Springer; 2006:512-523.
doi:10.1007/11672142_42'
apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Strategy improvement and randomized
subexponential algorithms for stochastic parity games (Vol. 3884, pp. 512–523).
Presented at the STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_42'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games,” 3884:512–23.
Springer, 2006. https://doi.org/10.1007/11672142_42.
ieee: 'K. Chatterjee and T. A. Henzinger, “Strategy improvement and randomized subexponential
algorithms for stochastic parity games,” presented at the STACS: Theoretical Aspects
of Computer Science, 2006, vol. 3884, pp. 512–523.'
ista: 'Chatterjee K, Henzinger TA. 2006. Strategy improvement and randomized subexponential
algorithms for stochastic parity games. STACS: Theoretical Aspects of Computer
Science, LNCS, vol. 3884, 512–523.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games. Vol. 3884,
Springer, 2006, pp. 512–23, doi:10.1007/11672142_42.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 512–523.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '14'
doi: 10.1007/11672142_42
extern: 1
intvolume: ' 3884'
month: '02'
page: 512 - 523
publication_status: published
publisher: Springer
publist_id: '184'
quality_controlled: 0
status: public
title: Strategy improvement and randomized subexponential algorithms for stochastic
parity games
type: conference
volume: 3884
year: '2006'
...
---
_id: '4539'
abstract:
- lang: eng
text: Games on graphs with ω-regular objectives provide a model for the control
and synthesis of reactive systems. Every ω-regular objective can be decomposed
into a safety part and a liveness part. The liveness part ensures that something
good happens “eventually.” Two main strengths of the classical, infinite-limit
formulation of liveness are robustness (independence from the granularity of transitions)
and simplicity (abstraction of complicated time bounds). However, the classical
liveness formulation suffers from the drawback that the time until something good
happens may be unbounded. A stronger formulation of liveness, so-called finitary
liveness, overcomes this drawback, while still retaining robustness and simplicity.
Finitary liveness requires that there exists an unknown, fixed bound b such that
something good happens within b transitions. While for one-shot liveness (reachability)
objectives, classical and finitary liveness coincide, for repeated liveness (Büchi)
objectives, the finitary formulation is strictly stronger. In this work we study
games with finitary parity and Streett (fairness) objectives. We prove the determinacy
of these games, present algorithms for solving these games, and characterize the
memory requirements of winning strategies. Our algorithms can be used, for example,
for synthesizing controllers that do not let the response time of a system increase
without bound.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
and the NSF ITR grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Finitary winning in omega-regular games. In: Vol
3920. Springer; 2006:257-271. doi:10.1007/11691372_17'
apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Finitary winning in omega-regular
games (Vol. 3920, pp. 257–271). Presented at the TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, Springer. https://doi.org/10.1007/11691372_17'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Finitary Winning in Omega-Regular
Games,” 3920:257–71. Springer, 2006. https://doi.org/10.1007/11691372_17.
ieee: 'K. Chatterjee and T. A. Henzinger, “Finitary winning in omega-regular games,”
presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, 2006, vol. 3920, pp. 257–271.'
ista: 'Chatterjee K, Henzinger TA. 2006. Finitary winning in omega-regular games.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 3920, 257–271.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Finitary Winning in Omega-Regular
Games. Vol. 3920, Springer, 2006, pp. 257–71, doi:10.1007/11691372_17.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 257–271.
conference:
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-03-15T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '15'
doi: 10.1007/11691372_17
extern: 1
intvolume: ' 3920'
month: '03'
page: 257 - 271
publication_status: published
publisher: Springer
publist_id: '183'
quality_controlled: 0
status: public
title: Finitary winning in omega-regular games
type: conference
volume: 3920
year: '2006'
...
---
_id: '4549'
abstract:
- lang: eng
text: We present a compositional theory of system verification, where specifications
assign real-numbered costs to systems. These costs can express a wide variety
of quantitative system properties, such as resource consumption, price, or a measure
of how well a system satisfies its specification. The theory supports the composition
of systems and specifications, and the hiding of variables. Boolean refinement
relations are replaced by real-numbered distances between descriptions of a system
at different levels of detail. We show that the classical Boolean rules for compositional
reasoning have quantitative counterparts in our setting. While our general theory
allows costs to be specified by arbitrary cost functions, we also consider a class
of linear cost functions, which give rise to an instance of our framework where
all operations are computable in polynomial time.
acknowledgement: Supported in part by the NSF grants CCR-0234690, CCR-0208875, and
CCR-0225610; by the NSF grant CCR-0132780 and ARP grant SC20051123.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Marco
full_name: Faella, Marco
last_name: Faella
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: 'Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M.
Compositional quantitative reasoning. In: IEEE; 2006:179-188. doi:10.1109/QEST.2006.11'
apa: 'Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R.,
& Stoelinga, M. (2006). Compositional quantitative reasoning (pp. 179–188).
Presented at the QEST: Quantitative Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.11'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Thomas A Henzinger,
Ritankar Majumdar, and Mariëlle Stoelinga. “Compositional Quantitative Reasoning,”
179–88. IEEE, 2006. https://doi.org/10.1109/QEST.2006.11.
ieee: 'K. Chatterjee, L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and
M. Stoelinga, “Compositional quantitative reasoning,” presented at the QEST: Quantitative
Evaluation of Systems, 2006, pp. 179–188.'
ista: 'Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga
M. 2006. Compositional quantitative reasoning. QEST: Quantitative Evaluation of
Systems, 179–188.'
mla: Chatterjee, Krishnendu, et al. Compositional Quantitative Reasoning.
IEEE, 2006, pp. 179–88, doi:10.1109/QEST.2006.11.
short: K. Chatterjee, L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga,
in:, IEEE, 2006, pp. 179–188.
conference:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-09-01T00:00:00Z
date_updated: 2021-01-12T07:59:37Z
day: '01'
doi: 10.1109/QEST.2006.11
extern: 1
month: '09'
page: 179 - 188
publication_status: published
publisher: IEEE
publist_id: '163'
quality_controlled: 0
status: public
title: Compositional quantitative reasoning
type: conference
year: '2006'
...
---
_id: '4550'
abstract:
- lang: eng
text: 'In 2-player non-zero-sum games, Nash equilibria capture the options for rational
behavior if each player attempts to maximize her payoff. In contrast to classical
game theory, we consider lexicographic objectives: first, each player tries to
maximize her own payoff, and then, the player tries to minimize the opponent''s
payoff. Such objectives arise naturally in the verification of systems with multiple
components. There, instead of proving that each component satisfies its specification
no matter how the other components behave, it sometimes suffices to prove that
each component satisfies its specification provided that the other components
satisfy their specifications. We say that a Nash equilibrium is secure if it is
an equilibrium with respect to the lexicographic objectives of both players. We
prove that in graph games with Borel winning conditions, which include the games
that arise in verification, there may be several Nash equilibria, but there is
always a unique maximal payoff profile of a secure equilibrium. We show how this
equilibrium can be computed in the case of ω-regular winning conditions, and we
characterize the memory requirements of strategies that achieve the equilibrium.'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
citation:
ama: Chatterjee K, Henzinger TA, Jurdziński M. Games with secure equilibria. Theoretical
Computer Science. 2006;365(1-2):67-82. doi:10.1016/j.tcs.2006.07.032
apa: Chatterjee, K., Henzinger, T. A., & Jurdziński, M. (2006). Games with secure
equilibria. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2006.07.032
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Games
with Secure Equilibria.” Theoretical Computer Science. Elsevier, 2006.
https://doi.org/10.1016/j.tcs.2006.07.032.
ieee: K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Games with secure equilibria,”
Theoretical Computer Science, vol. 365, no. 1–2. Elsevier, pp. 67–82, 2006.
ista: Chatterjee K, Henzinger TA, Jurdziński M. 2006. Games with secure equilibria.
Theoretical Computer Science. 365(1–2), 67–82.
mla: Chatterjee, Krishnendu, et al. “Games with Secure Equilibria.” Theoretical
Computer Science, vol. 365, no. 1–2, Elsevier, 2006, pp. 67–82, doi:10.1016/j.tcs.2006.07.032.
short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science
365 (2006) 67–82.
date_created: 2018-12-11T12:09:26Z
date_published: 2006-08-07T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '07'
doi: 10.1016/j.tcs.2006.07.032
extern: 1
intvolume: ' 365'
issue: 1-2
month: '08'
page: 67 - 82
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '164'
quality_controlled: 0
status: public
title: Games with secure equilibria
type: journal_article
volume: 365
year: '2006'
...
---
_id: '4551'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple discounted reward
objectives. Such MDPs occur in design problems where one wishes to simultaneously
optimize several criteria, for example, latency and power. The possible trade-offs
between the different objectives are characterized by the Pareto curve. We show
that every Pareto-optimal point can be achieved by a memoryless strategy; however,
unlike in the single-objective case, the memoryless strategy may require randomization.
Moreover, we show that the Pareto curve can be approximated in polynomial time
in the size of the MDP. Additionally, we study the problem if a given value vector
is realizable by any strategy, and show that it can be decided in polynomial time;
but the question whether it is realizable by a deterministic memoryless strategy
is NP-complete. These results provide efficient algorithms for design exploration
in MDP models with multiple objectives.\nThis research was supported in part by
the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690,
and CCR-0427202. "
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Majumdar R, Henzinger TA. Markov decision processes with multiple
objectives. In: Vol 3884. Springer; 2006:325-336. doi:10.1007/11672142_26'
apa: 'Chatterjee, K., Majumdar, R., & Henzinger, T. A. (2006). Markov decision
processes with multiple objectives (Vol. 3884, pp. 325–336). Presented at the
STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_26'
chicago: Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov
Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. https://doi.org/10.1007/11672142_26.
ieee: 'K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Markov decision processes
with multiple objectives,” presented at the STACS: Theoretical Aspects of Computer
Science, 2006, vol. 3884, pp. 325–336.'
ista: 'Chatterjee K, Majumdar R, Henzinger TA. 2006. Markov decision processes with
multiple objectives. STACS: Theoretical Aspects of Computer Science, LNCS, vol.
3884, 325–336.'
mla: Chatterjee, Krishnendu, et al. Markov Decision Processes with Multiple Objectives.
Vol. 3884, Springer, 2006, pp. 325–36, doi:10.1007/11672142_26.
short: K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '14'
doi: 10.1007/11672142_26
extern: 1
intvolume: ' 3884'
month: '02'
page: 325 - 336
publication_status: published
publisher: Springer
publist_id: '161'
quality_controlled: 0
status: public
title: Markov decision processes with multiple objectives
type: conference
volume: 3884
year: '2006'
...
---
_id: '4552'
abstract:
- lang: eng
text: 'A concurrent reachability game is a two-player game played on a graph: at
each state, the players simultaneously and independently select moves; the two
moves determine jointly a probability distribution over the successor states.
The objective for player 1 consists in reaching a set of target states; the objective
for player 2 is to prevent this, so that the game is zero-sum. Our contributions
are two-fold. First, we present a simple proof of the fact that in concurrent
reachability games, for all epsilon > 0, memoryless epsilon-optimal strategies
exist. A memoryless strategy is independent of the history of plays, and an epsilon-optimal
strategy achieves the objective with probability within epsilon of the value of
the game. In contrast to previous proofs of this fact, which rely on the limit
behavior of discounted games using advanced Puisieux series analysis, our proof
is elementary and combinatorial. Second, we present a strategy-improvement (a.k.a.
policy-iteration) algorithm for concurrent games with reachability objectives.'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent
reachability games. In: IEEE; 2006:291-300. doi:10.1109/QEST.2006.48'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2006). Strategy improvement
for concurrent reachability games (pp. 291–300). Presented at the QEST: Quantitative
Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.48'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy
Improvement for Concurrent Reachability Games,” 291–300. IEEE, 2006. https://doi.org/10.1109/QEST.2006.48.
ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for
concurrent reachability games,” presented at the QEST: Quantitative Evaluation
of Systems, 2006, pp. 291–300.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2006. Strategy improvement for concurrent
reachability games. QEST: Quantitative Evaluation of Systems, 291–300.'
mla: Chatterjee, Krishnendu, et al. Strategy Improvement for Concurrent Reachability
Games. IEEE, 2006, pp. 291–300, doi:10.1109/QEST.2006.48.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2006, pp. 291–300.
conference:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '01'
doi: 10.1109/QEST.2006.48
extern: 1
month: '01'
page: 291 - 300
publication_status: published
publisher: IEEE
publist_id: '162'
quality_controlled: 0
status: public
title: Strategy improvement for concurrent reachability games
type: conference
year: '2006'
...
---
_id: '2455'
abstract:
- lang: eng
text: Local accumulation of the plant growth regulator auxin mediates pattern formation
in Arabidopsis roots and influences outgrowth and development of lateral root-
and shoot-derived primordia. However, it has remained unclear how auxin can simultaneously
regulate patterning and organ outgrowth and how its distribution is stabilized
in a primordium-specif ic manner. Here we show that five PIN genes collectively
control auxin distribution to regulate cell division and cell expansion in the
primary root. Furthermore, the joint action of these genes has an important role
in pattern formation by focusing the auxin maximum and restricting the expression
domain of PLETHORA (PLT) genes, major determinants for root stem cell specification.
In turn, PLT genes are required for PIN gene transcription to stabilize the auxin
maximum at the distal root tip. Our data reveal an interaction network of auxin
transport facilitators and root fate determinants that control patterning and
growth of the root primordium.
author:
- first_name: Ikram
full_name: Billou, Ikram
last_name: Billou
- first_name: Jian
full_name: Xu, Jian
last_name: Xu
- first_name: Marjolein
full_name: Wildwater, Marjolein
last_name: Wildwater
- first_name: Viola
full_name: Willemsen, Viola
last_name: Willemsen
- first_name: Ivan
full_name: Paponov, Ivan A
last_name: Paponov
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
- first_name: Renze
full_name: Heldstra, Renze
last_name: Heldstra
- first_name: Mitsuhiro
full_name: Aida, Mitsuhiro
last_name: Aida
- first_name: Klaus
full_name: Palme, Klaus J
last_name: Palme
- first_name: Ben
full_name: Scheres, Ben
last_name: Scheres
citation:
ama: Billou I, Xu J, Wildwater M, et al. The PIN auxin efflux facilitator network
controls growth and patterning in Arabidopsis roots. Nature. 2005;433(7021):39-44.
doi:10.1038/nature03184
apa: Billou, I., Xu, J., Wildwater, M., Willemsen, V., Paponov, I., Friml, J., …
Scheres, B. (2005). The PIN auxin efflux facilitator network controls growth and
patterning in Arabidopsis roots. Nature. Nature Publishing Group. https://doi.org/10.1038/nature03184
chicago: Billou, Ikram, Jian Xu, Marjolein Wildwater, Viola Willemsen, Ivan Paponov,
Jiří Friml, Renze Heldstra, Mitsuhiro Aida, Klaus Palme, and Ben Scheres. “The
PIN Auxin Efflux Facilitator Network Controls Growth and Patterning in Arabidopsis
Roots.” Nature. Nature Publishing Group, 2005. https://doi.org/10.1038/nature03184.
ieee: I. Billou et al., “The PIN auxin efflux facilitator network controls
growth and patterning in Arabidopsis roots,” Nature, vol. 433, no. 7021.
Nature Publishing Group, pp. 39–44, 2005.
ista: Billou I, Xu J, Wildwater M, Willemsen V, Paponov I, Friml J, Heldstra R,
Aida M, Palme K, Scheres B. 2005. The PIN auxin efflux facilitator network controls
growth and patterning in Arabidopsis roots. Nature. 433(7021), 39–44.
mla: Billou, Ikram, et al. “The PIN Auxin Efflux Facilitator Network Controls Growth
and Patterning in Arabidopsis Roots.” Nature, vol. 433, no. 7021, Nature
Publishing Group, 2005, pp. 39–44, doi:10.1038/nature03184.
short: I. Billou, J. Xu, M. Wildwater, V. Willemsen, I. Paponov, J. Friml, R. Heldstra,
M. Aida, K. Palme, B. Scheres, Nature 433 (2005) 39–44.
date_created: 2018-12-11T11:57:46Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T06:57:35Z
day: '01'
doi: 10.1038/nature03184
extern: 1
intvolume: ' 433'
issue: '7021'
month: '01'
page: 39 - 44
publication: Nature
publication_status: published
publisher: Nature Publishing Group
publist_id: '4448'
quality_controlled: 0
status: public
title: The PIN auxin efflux facilitator network controls growth and patterning in
Arabidopsis roots
type: journal_article
volume: 433
year: '2005'
...
---
_id: '2463'
author:
- first_name: J
full_name: Dubová, J
last_name: Dubová
- first_name: Jan
full_name: Hejátko, Jan
last_name: Hejátko
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
citation:
ama: 'Dubová J, Hejátko J, Friml J. Reproduction, plants. In: Meyers R, ed. Encyclopedia
of Molecular Cell Biology and Molecular Medicine. Vol 12. Wiley-Blackwell;
2005:249-295. doi:10.1002/3527600906'
apa: Dubová, J., Hejátko, J., & Friml, J. (2005). Reproduction, plants. In R.
Meyers (Ed.), Encyclopedia of Molecular Cell Biology and Molecular Medicine
(Vol. 12, pp. 249–295). Wiley-Blackwell. https://doi.org/10.1002/3527600906
chicago: Dubová, J, Jan Hejátko, and Jiří Friml. “Reproduction, Plants.” In Encyclopedia
of Molecular Cell Biology and Molecular Medicine, edited by Robert Meyers,
12:249–95. Wiley-Blackwell, 2005. https://doi.org/10.1002/3527600906.
ieee: J. Dubová, J. Hejátko, and J. Friml, “Reproduction, plants,” in Encyclopedia
of Molecular Cell Biology and Molecular Medicine, vol. 12, R. Meyers, Ed.
Wiley-Blackwell, 2005, pp. 249–295.
ista: 'Dubová J, Hejátko J, Friml J. 2005.Reproduction, plants. In: Encyclopedia
of Molecular Cell Biology and Molecular Medicine. vol. 12, 249–295.'
mla: Dubová, J., et al. “Reproduction, Plants.” Encyclopedia of Molecular Cell
Biology and Molecular Medicine, edited by Robert Meyers, vol. 12, Wiley-Blackwell,
2005, pp. 249–95, doi:10.1002/3527600906.
short: J. Dubová, J. Hejátko, J. Friml, in:, R. Meyers (Ed.), Encyclopedia of Molecular
Cell Biology and Molecular Medicine, Wiley-Blackwell, 2005, pp. 249–295.
date_created: 2018-12-11T11:57:48Z
date_published: 2005-10-28T00:00:00Z
date_updated: 2021-01-12T06:57:38Z
day: '28'
doi: 10.1002/3527600906
editor:
- first_name: Robert
full_name: Meyers, Robert A
last_name: Meyers
extern: 1
intvolume: ' 12'
month: '10'
page: 249 - 295
publication: Encyclopedia of Molecular Cell Biology and Molecular Medicine
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4440'
quality_controlled: 0
status: public
title: Reproduction, plants
type: book_chapter
volume: 12
year: '2005'
...
---
_id: '2464'
alternative_title:
- Annual Plant Reviews
author:
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
- first_name: Justyna
full_name: Wiśniewska, Justyna
last_name: Wiśniewska
citation:
ama: 'Friml J, Wiśniewska J. Auxin as an intercellular signal. In: Fleming A, ed.
Intercellular Communication in Plants. Vol 16. Wiley-Blackwell; 2005.'
apa: Friml, J., & Wiśniewska, J. (2005). Auxin as an intercellular signal. In
A. Fleming (Ed.), Intercellular Communication in Plants (Vol. 16). Wiley-Blackwell.
chicago: Friml, Jiří, and Justyna Wiśniewska. “Auxin as an Intercellular Signal.”
In Intercellular Communication in Plants, edited by Andrew Fleming, Vol.
16. Wiley-Blackwell, 2005.
ieee: J. Friml and J. Wiśniewska, “Auxin as an intercellular signal,” in Intercellular
Communication in Plants, vol. 16, A. Fleming, Ed. Wiley-Blackwell, 2005.
ista: 'Friml J, Wiśniewska J. 2005.Auxin as an intercellular signal. In: Intercellular
Communication in Plants. Annual Plant Reviews, vol. 16.'
mla: Friml, Jiří, and Justyna Wiśniewska. “Auxin as an Intercellular Signal.” Intercellular
Communication in Plants, edited by Andrew Fleming, vol. 16, Wiley-Blackwell,
2005.
short: J. Friml, J. Wiśniewska, in:, A. Fleming (Ed.), Intercellular Communication
in Plants, Wiley-Blackwell, 2005.
date_created: 2018-12-11T11:57:49Z
date_published: 2005-01-13T00:00:00Z
date_updated: 2021-01-12T06:57:38Z
day: '13'
editor:
- first_name: Andrew
full_name: Fleming, Andrew J.
last_name: Fleming
extern: 1
intvolume: ' 16'
month: '01'
publication: Intercellular Communication in Plants
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4439'
quality_controlled: 0
status: public
title: Auxin as an intercellular signal
type: book_chapter
volume: 16
year: '2005'
...
---
_id: '2647'
abstract:
- lang: eng
text: 'Our understanding of the role played by neurotransmitter receptors in the
developing brain has advanced in recent years. The major excitatory and inhibitory
neurotransmitters in the brain, glutamate and GABA, activate both ionotropic (ligand-gated
ion channels) and metabotropic (G protein-coupled) receptors, and are generally
associated with neuronal communication in the mature brain. However, before the
emergence of their role in neurotransmission in adulthood, they also act to influence
earlier developmental events, some of which occur prior to synapse formation:
such as proliferation, migration, differentiation or survival processes during
neural development. To fulfill these actions in the constructing of the nervous
system, different types of glutamate and GABA receptors need to be expressed both
at the right time and at the right place. The identification by molecular cloning
of 16 ionotropic glutamate receptor subunits, eight metabotropic glutamate receptor
subtypes, 21 ionotropic and two metabotropic GABA receptor subunits, some of which
exist in alternatively splice variants, has enriched our appreciation of how molecular
diversity leads to functional diversity in the brain. It now appears that many
different types of glutamate and GABA receptor subunits have prominent expression
in the embryonic and/or postnatal brain, whereas others are mainly present in
the adult brain. Although the significance of this differential expression of
subunits is not fully understood, it appears that the change in subunit composition
is essential for normal development in particular brain regions. This review focuses
on emerging information relating to the expression and role of glutamatergic and
GABAergic neurotransmitter receptors during prenatal and postnatal development.'
author:
- first_name: Rafael
full_name: Luján, Rafael
last_name: Luján
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Guillermina
full_name: López-Bendito, Guillermina
last_name: López Bendito
citation:
ama: Luján R, Shigemoto R, López Bendito G. Glutamate and GABA receptor signalling
in the developing brain. Neuroscience. 2005;130(3):567-580. doi:10.1016/j.neuroscience.2004.09.042
apa: Luján, R., Shigemoto, R., & López Bendito, G. (2005). Glutamate and GABA
receptor signalling in the developing brain. Neuroscience. Elsevier. https://doi.org/10.1016/j.neuroscience.2004.09.042
chicago: Luján, Rafael, Ryuichi Shigemoto, and Guillermina López Bendito. “Glutamate
and GABA Receptor Signalling in the Developing Brain.” Neuroscience. Elsevier,
2005. https://doi.org/10.1016/j.neuroscience.2004.09.042.
ieee: R. Luján, R. Shigemoto, and G. López Bendito, “Glutamate and GABA receptor
signalling in the developing brain,” Neuroscience, vol. 130, no. 3. Elsevier,
pp. 567–580, 2005.
ista: Luján R, Shigemoto R, López Bendito G. 2005. Glutamate and GABA receptor signalling
in the developing brain. Neuroscience. 130(3), 567–580.
mla: Luján, Rafael, et al. “Glutamate and GABA Receptor Signalling in the Developing
Brain.” Neuroscience, vol. 130, no. 3, Elsevier, 2005, pp. 567–80, doi:10.1016/j.neuroscience.2004.09.042.
short: R. Luján, R. Shigemoto, G. López Bendito, Neuroscience 130 (2005) 567–580.
date_created: 2018-12-11T11:58:51Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2020-07-14T12:45:44Z
day: '01'
doi: 10.1016/j.neuroscience.2004.09.042
extern: 1
intvolume: ' 130'
issue: '3'
month: '01'
page: 567 - 580
publication: Neuroscience
publication_status: published
publisher: Elsevier
publist_id: '4250'
quality_controlled: 0
status: public
title: Glutamate and GABA receptor signalling in the developing brain
type: review
volume: 130
year: '2005'
...
---
_id: '2648'
abstract:
- lang: eng
text: Hyperpolarization-activated and cyclic nucleotide-gated (HCN) channels are
involved in the control of neuronal excitability and plasticity. In this study,
we used immunoblotting and immunohistochemical techniques to reveal the developmental
expression and subcellular distribution of the HCN1 subunit in the cerebellar
cortex. During postnatal development, the spatio-temporal expression of HCN1 correlated
well with the morphological events occurring during the ontogenesis of cerebellar
interneurons. Using immunoblotting techniques, HCN1 was weakly detected during
the first postnatal week and continued to increase throughout postnatal development,
peaking at postnatal day (P)15. At the light-microscopic level, HCN1 immunoreactivity
was very weak until P7 whereas from P10-12 to adulthood it was strongly detected
in the lower third of the molecular layer and in the Purkinje cell layer. HCN1
was present in axons running through the molecular layer and in the pericellular
basket around Purkinje cells at P12, but in the periaxonal plexus (the pinceau)
surrounding their initial segment only after P15. Using immunofluorescence, HCN1
colocalized with GAD65 and synaptophysin, demonstrating that the subunit was present
in inhibitory axons and axon terminals. At the electron-microscopic level, in
adulthood, HCN1 immunoparticles were detected at postsynaptic sites in basket
and Purkinje cells but most immunoparticles were found at presynaptic sites in
basket cell axons and in terminals. In the axon terminals, the distribution of
HCN1 was relatively uniform along the extrasynaptic plasma membrane; this was
confirmed using quantitative techniques. The present findings suggest that HCN1
channels may provide a significant route for modulating co-ordinated cerebellar
synaptic transmission through basket cells.
author:
- first_name: Rafael
full_name: Luján, Rafael
last_name: Luján
- first_name: José
full_name: Albasanz, José L
last_name: Albasanz
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: José
full_name: Juíz, José M
last_name: Juíz
citation:
ama: Luján R, Albasanz J, Shigemoto R, Juíz J. Preferential localization of the
hyperpolarization-activated cyclic nucleotide-gated cation channel subunit HCN1
in basket cell terminals of the rat cerebellum. European Journal of Neuroscience.
2005;21(8):2073-2082. doi:10.1111/j.1460-9568.2005.04043.x
apa: Luján, R., Albasanz, J., Shigemoto, R., & Juíz, J. (2005). Preferential
localization of the hyperpolarization-activated cyclic nucleotide-gated cation
channel subunit HCN1 in basket cell terminals of the rat cerebellum. European
Journal of Neuroscience. Wiley-Blackwell. https://doi.org/10.1111/j.1460-9568.2005.04043.x
chicago: Luján, Rafael, José Albasanz, Ryuichi Shigemoto, and José Juíz. “Preferential
Localization of the Hyperpolarization-Activated Cyclic Nucleotide-Gated Cation
Channel Subunit HCN1 in Basket Cell Terminals of the Rat Cerebellum.” European
Journal of Neuroscience. Wiley-Blackwell, 2005. https://doi.org/10.1111/j.1460-9568.2005.04043.x.
ieee: R. Luján, J. Albasanz, R. Shigemoto, and J. Juíz, “Preferential localization
of the hyperpolarization-activated cyclic nucleotide-gated cation channel subunit
HCN1 in basket cell terminals of the rat cerebellum,” European Journal of Neuroscience,
vol. 21, no. 8. Wiley-Blackwell, pp. 2073–2082, 2005.
ista: Luján R, Albasanz J, Shigemoto R, Juíz J. 2005. Preferential localization
of the hyperpolarization-activated cyclic nucleotide-gated cation channel subunit
HCN1 in basket cell terminals of the rat cerebellum. European Journal of Neuroscience.
21(8), 2073–2082.
mla: Luján, Rafael, et al. “Preferential Localization of the Hyperpolarization-Activated
Cyclic Nucleotide-Gated Cation Channel Subunit HCN1 in Basket Cell Terminals of
the Rat Cerebellum.” European Journal of Neuroscience, vol. 21, no. 8,
Wiley-Blackwell, 2005, pp. 2073–82, doi:10.1111/j.1460-9568.2005.04043.x.
short: R. Luján, J. Albasanz, R. Shigemoto, J. Juíz, European Journal of Neuroscience
21 (2005) 2073–2082.
date_created: 2018-12-11T11:58:52Z
date_published: 2005-04-01T00:00:00Z
date_updated: 2021-01-12T06:58:48Z
day: '01'
doi: 10.1111/j.1460-9568.2005.04043.x
extern: 1
intvolume: ' 21'
issue: '8'
month: '04'
page: 2073 - 2082
publication: European Journal of Neuroscience
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4248'
quality_controlled: 0
status: public
title: Preferential localization of the hyperpolarization-activated cyclic nucleotide-gated
cation channel subunit HCN1 in basket cell terminals of the rat cerebellum
type: journal_article
volume: 21
year: '2005'
...
---
_id: '2649'
abstract:
- lang: eng
text: The number of ionotropic receptors in synapses is an essential factor for
determining the efficacy of fast transmission. We estimated the number of functional
AMPA receptors at single postsynaptic sites by a combination of two-photon uncaging
of glutamate and the nonstationary fluctuation analysis in immature rat Purkinje
cells (PCs), which receive a single type of excitatory input from climbing fibers.
Areas of postsynaptic membrane specialization at the recorded synapses were measured
by reconstruction of serial ultrathin sections. The number of functional AMPA
receptors was proportional to the synaptic area with a density of ∼ 1280 receptors/μm
2. Moreover, highly sensitive freeze-fracture replica labeling revealed a homogeneous
density of immunogold particles for AMPA receptors in synaptic sites (910 ± 36
particles/μm 2) and much lower density in extrasynaptic sites (19 ± 2 particles/μm
2) in the immature PCs. Our results indicate that in this developing synapse,
the efficacy of transmission is determined by the synaptic area.
author:
- first_name: Junichi
full_name: Tanaka, Junichi
last_name: Tanaka
- first_name: Masanori
full_name: Matsuzaki, Masanori
last_name: Matsuzaki
- first_name: Etsuko
full_name: Tarusawa, Etsuko
last_name: Tarusawa
- first_name: Akiko
full_name: Momiyama, Akiko
last_name: Momiyama
- first_name: Elek
full_name: Molnár, Elek
last_name: Molnár
- first_name: Haruo
full_name: Kasai, Haruo
last_name: Kasai
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
citation:
ama: Tanaka J, Matsuzaki M, Tarusawa E, et al. Number and density of AMPA receptors
in single synapses in immature cerebellum. Journal of Neuroscience. 2005;25(4):799-807.
doi:10.1523/JNEUROSCI.4256-04.2005
apa: Tanaka, J., Matsuzaki, M., Tarusawa, E., Momiyama, A., Molnár, E., Kasai, H.,
& Shigemoto, R. (2005). Number and density of AMPA receptors in single synapses
in immature cerebellum. Journal of Neuroscience. Society for Neuroscience.
https://doi.org/10.1523/JNEUROSCI.4256-04.2005
chicago: Tanaka, Junichi, Masanori Matsuzaki, Etsuko Tarusawa, Akiko Momiyama, Elek
Molnár, Haruo Kasai, and Ryuichi Shigemoto. “Number and Density of AMPA Receptors
in Single Synapses in Immature Cerebellum.” Journal of Neuroscience. Society
for Neuroscience, 2005. https://doi.org/10.1523/JNEUROSCI.4256-04.2005.
ieee: J. Tanaka et al., “Number and density of AMPA receptors in single synapses
in immature cerebellum,” Journal of Neuroscience, vol. 25, no. 4. Society
for Neuroscience, pp. 799–807, 2005.
ista: Tanaka J, Matsuzaki M, Tarusawa E, Momiyama A, Molnár E, Kasai H, Shigemoto
R. 2005. Number and density of AMPA receptors in single synapses in immature cerebellum.
Journal of Neuroscience. 25(4), 799–807.
mla: Tanaka, Junichi, et al. “Number and Density of AMPA Receptors in Single Synapses
in Immature Cerebellum.” Journal of Neuroscience, vol. 25, no. 4, Society
for Neuroscience, 2005, pp. 799–807, doi:10.1523/JNEUROSCI.4256-04.2005.
short: J. Tanaka, M. Matsuzaki, E. Tarusawa, A. Momiyama, E. Molnár, H. Kasai, R.
Shigemoto, Journal of Neuroscience 25 (2005) 799–807.
date_created: 2018-12-11T11:58:52Z
date_published: 2005-01-26T00:00:00Z
date_updated: 2021-01-12T06:58:48Z
day: '26'
doi: 10.1523/JNEUROSCI.4256-04.2005
extern: 1
intvolume: ' 25'
issue: '4'
month: '01'
page: 799 - 807
publication: Journal of Neuroscience
publication_status: published
publisher: Society for Neuroscience
publist_id: '4249'
quality_controlled: 0
status: public
title: Number and density of AMPA receptors in single synapses in immature cerebellum
type: journal_article
volume: 25
year: '2005'
...
---
_id: '2650'
abstract:
- lang: eng
text: 'Septohippocampal cholinergic neurons play key roles in learning and memory
processes, and in the generation of hippocampal theta rhythm. The range of receptors
for endogenous modulators expressed on these neurons is unclear. Here we describe
GABAB 1a/b receptor (GABABR) and type 1 cannabinoid receptor (CB1R) expression
in rat septal cholinergic [i.e. choline acetyltransferase (ChAT)-positive] cells.
Using double immunofluorescent staining, we found that almost two-thirds of the
cholinergic cells in the rat medial septum were GABABR positive, and that these
cells had significantly larger somata than did GABABR-negative cholinergic neurons.
We detected CB1R labelling in somata after axonal protein transport was blocked
by colchicine. In these animals about one-third of the cholinergic cells were
CB1R positive. These cells again had larger somata than CB1R-negative cholinergic
neurons. The analyses confirmed that the size of GABABR-positive and CB 1R-positive
cholinergic cells were alike, and all CB 1R-positive cholinergic cells were GABABR
positive as well. CB1R-positive cells were invariably ChAT positive. All retrogradely
labelled septohippocampal cholinergic cells were positive for GABABR and at least
half of them also for CB1R. These data shed light on the existence of at least
two cholinergic cell types in the medial septum: one expresses GABABR and CB1R,
has large somata and projects to the hippocampus, whereas the other is negative
for GABABR and CB1R and has smaller somata. The results also suggest that cholinergic
transmission in the hippocampus is fine-tuned by endocannabinoid signalling.'
author:
- first_name: Gábor
full_name: Nyíri, Gábor
last_name: Nyíri
- first_name: Eszter
full_name: Szabadits, Eszter
last_name: Szabadits
- first_name: Csaba
full_name: Cserép, Csaba
last_name: Cserép
- first_name: Ken
full_name: Mackie, Ken P
last_name: Mackie
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Tamás
full_name: Freund, Tamás F
last_name: Freund
citation:
ama: Nyíri G, Szabadits E, Cserép C, Mackie K, Shigemoto R, Freund T. GABAB and
CB1 cannabinoid receptor expression identifies two types of septal cholinergic
neurons. European Journal of Neuroscience. 2005;21(11):3034-3042. doi:10.1111/j.1460-9568.2005.04146.x
apa: Nyíri, G., Szabadits, E., Cserép, C., Mackie, K., Shigemoto, R., & Freund,
T. (2005). GABAB and CB1 cannabinoid receptor expression identifies two types
of septal cholinergic neurons. European Journal of Neuroscience. Wiley-Blackwell.
https://doi.org/10.1111/j.1460-9568.2005.04146.x
chicago: Nyíri, Gábor, Eszter Szabadits, Csaba Cserép, Ken Mackie, Ryuichi Shigemoto,
and Tamás Freund. “GABAB and CB1 Cannabinoid Receptor Expression Identifies Two
Types of Septal Cholinergic Neurons.” European Journal of Neuroscience.
Wiley-Blackwell, 2005. https://doi.org/10.1111/j.1460-9568.2005.04146.x.
ieee: G. Nyíri, E. Szabadits, C. Cserép, K. Mackie, R. Shigemoto, and T. Freund,
“GABAB and CB1 cannabinoid receptor expression identifies two types of septal
cholinergic neurons,” European Journal of Neuroscience, vol. 21, no. 11.
Wiley-Blackwell, pp. 3034–3042, 2005.
ista: Nyíri G, Szabadits E, Cserép C, Mackie K, Shigemoto R, Freund T. 2005. GABAB
and CB1 cannabinoid receptor expression identifies two types of septal cholinergic
neurons. European Journal of Neuroscience. 21(11), 3034–3042.
mla: Nyíri, Gábor, et al. “GABAB and CB1 Cannabinoid Receptor Expression Identifies
Two Types of Septal Cholinergic Neurons.” European Journal of Neuroscience,
vol. 21, no. 11, Wiley-Blackwell, 2005, pp. 3034–42, doi:10.1111/j.1460-9568.2005.04146.x.
short: G. Nyíri, E. Szabadits, C. Cserép, K. Mackie, R. Shigemoto, T. Freund, European
Journal of Neuroscience 21 (2005) 3034–3042.
date_created: 2018-12-11T11:58:52Z
date_published: 2005-06-01T00:00:00Z
date_updated: 2021-01-12T06:58:49Z
day: '01'
doi: 10.1111/j.1460-9568.2005.04146.x
extern: 1
intvolume: ' 21'
issue: '11'
month: '06'
page: 3034 - 3042
publication: European Journal of Neuroscience
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4247'
quality_controlled: 0
status: public
title: GABAB and CB1 cannabinoid receptor expression identifies two types of septal
cholinergic neurons
type: journal_article
volume: 21
year: '2005'
...