---
_id: '4452'
abstract:
- lang: eng
text: We describe Valigator, a software tool for imperative program verification
that efficiently combines symbolic computation and automated reasoning in a uniform
framework. The system offers support for automatically generating and proving
verification conditions and, most importantly, for automatically inferring loop
invariants and bound assertions by means of symbolic summation, Gröbner basis
computation, and quantifier elimination. We present general principles of the
implementation and illustrate them on examples.
acknowledgement: This research was supported by the Swiss NSF.
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: Thibaud
full_name: Hottelier, Thibaud
last_name: Hottelier
- first_name: Laura
full_name: Kovács, Laura
last_name: Kovács
citation:
ama: 'Henzinger TA, Hottelier T, Kovács L. Valigator: A verification tool with bound
and invariant generation. In: Vol 5330. Springer; 2008:333-342. doi:10.1007/978-3-540-89439-1_24'
apa: 'Henzinger, T. A., Hottelier, T., & Kovács, L. (2008). Valigator: A verification
tool with bound and invariant generation (Vol. 5330, pp. 333–342). Presented at
the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Springer.
https://doi.org/10.1007/978-3-540-89439-1_24'
chicago: 'Henzinger, Thomas A, Thibaud Hottelier, and Laura Kovács. “Valigator:
A Verification Tool with Bound and Invariant Generation,” 5330:333–42. Springer,
2008. https://doi.org/10.1007/978-3-540-89439-1_24.'
ieee: 'T. A. Henzinger, T. Hottelier, and L. Kovács, “Valigator: A verification
tool with bound and invariant generation,” presented at the LPAR: Logic for Programming,
Artificial Intelligence, and Reasoning, 2008, vol. 5330, pp. 333–342.'
ista: 'Henzinger TA, Hottelier T, Kovács L. 2008. Valigator: A verification tool
with bound and invariant generation. LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, LNCS, vol. 5330, 333–342.'
mla: 'Henzinger, Thomas A., et al. Valigator: A Verification Tool with Bound
and Invariant Generation. Vol. 5330, Springer, 2008, pp. 333–42, doi:10.1007/978-3-540-89439-1_24.'
short: T.A. Henzinger, T. Hottelier, L. Kovács, in:, Springer, 2008, pp. 333–342.
conference:
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
date_created: 2018-12-11T12:08:55Z
date_published: 2008-11-13T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '13'
doi: 10.1007/978-3-540-89439-1_24
extern: 1
intvolume: ' 5330'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/valigator.pdf
month: '11'
page: 333 - 342
publication_status: published
publisher: Springer
publist_id: '277'
quality_controlled: 0
status: public
title: 'Valigator: A verification tool with bound and invariant generation'
type: conference
volume: 5330
year: '2008'
...
---
_id: '4509'
abstract:
- lang: eng
text: 'I discuss two main challenges in embedded systems design: the challenge to
build predictable systems, and that to build robust systems. I suggest how predictability
can be formalized as a form of determinism, and robustness as a form of continuity.'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. Two challenges in embedded systems design: Predictability and
robustness. Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. 2008;366(1881):3727-3736. doi:10.1098/rsta.2008.0141'
apa: 'Henzinger, T. A. (2008). Two challenges in embedded systems design: Predictability
and robustness. Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. Royal Society of London. https://doi.org/10.1098/rsta.2008.0141'
chicago: 'Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability
and Robustness.” Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. Royal Society of London, 2008. https://doi.org/10.1098/rsta.2008.0141.'
ieee: 'T. A. Henzinger, “Two challenges in embedded systems design: Predictability
and robustness,” Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences, vol. 366, no. 1881. Royal Society of London,
pp. 3727–3736, 2008.'
ista: 'Henzinger TA. 2008. Two challenges in embedded systems design: Predictability
and robustness. Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. 366(1881), 3727–3736.'
mla: 'Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability
and Robustness.” Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences, vol. 366, no. 1881, Royal Society of London,
2008, pp. 3727–36, doi:10.1098/rsta.2008.0141.'
short: T.A. Henzinger, Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences 366 (2008) 3727–3736.
date_created: 2018-12-11T12:09:13Z
date_published: 2008-07-31T00:00:00Z
date_updated: 2021-01-12T07:59:19Z
day: '31'
doi: 10.1098/rsta.2008.0141
extern: 1
intvolume: ' 366'
issue: '1881'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/two_challenges_in_embedded_systems_design.pdf
month: '07'
page: 3727 - 3736
publication: Philosophical Transactions of the Royal Society A Mathematical Physical
and Engineering Sciences
publication_status: published
publisher: Royal Society of London
publist_id: '219'
quality_controlled: 0
status: public
title: 'Two challenges in embedded systems design: Predictability and robustness'
type: journal_article
volume: 366
year: '2008'
...
---
_id: '4521'
abstract:
- lang: eng
text: The search for proof and the search for counterexamples (bugs) are complementary
activities that need to be pursued concurrently in order to maximize the practical
success rate of verification tools.While this is well-understood in safety verification,
the current focus of liveness verification has been almost exclusively on the
search for termination proofs. A counterexample to termination is an infinite
programexecution. In this paper, we propose a method to search for such counterexamples.
The search proceeds in two phases. We first dynamically enumerate lasso-shaped
candidate paths for counterexamples, and then statically prove their feasibility.
We illustrate the utility of our nontermination prover, called TNT, on several
nontrivial examples, some of which require bit-level reasoning about integer representations.
author:
- first_name: Ashutosh
full_name: Ashutosh Gupta
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- 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: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
- first_name: Ru
full_name: Xu, Ru-Gang
last_name: Xu
citation:
ama: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. Proving non-termination.
In: ACM; 2008:147-158. doi:10.1145/1328438.1328459'
apa: 'Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., & Xu, R. (2008).
Proving non-termination (pp. 147–158). Presented at the POPL: Principles of Programming
Languages, ACM. https://doi.org/10.1145/1328438.1328459'
chicago: Gupta, Ashutosh, Thomas A Henzinger, Ritankar Majumdar, Andrey Rybalchenko,
and Ru Xu. “Proving Non-Termination,” 147–58. ACM, 2008. https://doi.org/10.1145/1328438.1328459.
ieee: 'A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu, “Proving
non-termination,” presented at the POPL: Principles of Programming Languages,
2008, pp. 147–158.'
ista: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination.
POPL: Principles of Programming Languages, 147–158.'
mla: Gupta, Ashutosh, et al. Proving Non-Termination. ACM, 2008, pp. 147–58,
doi:10.1145/1328438.1328459.
short: A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008,
pp. 147–158.
conference:
name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:09:17Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:25Z
day: '01'
doi: 10.1145/1328438.1328459
extern: 1
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf
month: '01'
page: 147 - 158
publication_status: published
publisher: ACM
publist_id: '208'
quality_controlled: 0
status: public
title: Proving non-termination
type: conference
year: '2008'
...
---
_id: '4524'
abstract:
- lang: eng
text: "Complex requirements, time-to-market pressure and regulatory constraints
have made the designing of embedded systems extremely challenging. This is evident
by the increase in effort and expenditure for design of safety-driven real-time
control-dominated applications like automotive and avionic controllers. Design
processes are often challenged by lack of proper programming tools for specifying
and verifying critical requirements (e.g. timing and reliability) of such applications.
Platform based design, an approach for designing embedded systems, addresses the
above concerns by separating requirement from architecture. The requirement specifies
the intended behavior of an application while the architecture specifies the guarantees
(e.g. execution speed, failure rate etc). An implementation, a mapping of the
requirement on the architecture, is then analyzed for correctness. The orthogonalization
of concerns makes the specification and analyses simpler. An effective use of
such design methodology has been proposed in Logical Execution Time (LET) model
of real-time tasks. The model separates the timing requirements (specified by
release and termination instances of a task) from the architecture guarantees
(specified by worst-case execution time of the task).\r\n\r\nThis dissertation
proposes a coordination language, Hierarchical Timing Language (HTL), that captures
the timing and reliability requirements of real-time applications. An implementation
of the program on an architecture is then analyzed to check whether desired timing
and reliability requirements are met or not. The core framework extends the LET
model by accounting for reliability and refinement. The reliability model separates
the reliability requirements of tasks from the reliability guarantees of the architecture.
The requirement expresses the desired long-term reliability while the architecture
provides a short-term reliability guarantee (e.g. failure rate for each iteration).
The analysis checks if the short-term guarantee ensures the desired long-term
reliability. The refinement model allows replacing a task by another task during
program execution. Refinement preserves schedulability and reliability, i.e.,
if a refined task is schedulable and reliable for an implementation, then the
refining task is also schedulable and reliable for the implementation. Refinement
helps in concise specification without overloading analysis.\r\n\r\nThe work presents
the formal model, the analyses (both with and without refinement), and a compiler
for HTL programs. The compiler checks composition and refinement constraints,
performs schedulability and reliability analyses, and generates code for implementation
of an HTL program on a virtual machine. Three real-time controllers, one each
from automatic control, automotive control and avionic control, are used to illustrate
the steps in modeling and analyzing HTL programs."
acknowledgement: 978-0-549-83679-7
article_processing_charge: No
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
citation:
ama: Ghosal A. A hierarchical coordination language for reliable real-time tasks.
2008:1-210.
apa: Ghosal, A. (2008). A hierarchical coordination language for reliable real-time
tasks. University of California, Berkeley.
chicago: Ghosal, Arkadeb. “A Hierarchical Coordination Language for Reliable Real-Time
Tasks.” University of California, Berkeley, 2008.
ieee: A. Ghosal, “A hierarchical coordination language for reliable real-time tasks,”
University of California, Berkeley, 2008.
ista: Ghosal A. 2008. A hierarchical coordination language for reliable real-time
tasks. University of California, Berkeley.
mla: Ghosal, Arkadeb. A Hierarchical Coordination Language for Reliable Real-Time
Tasks. University of California, Berkeley, 2008, pp. 1–210.
short: A. Ghosal, A Hierarchical Coordination Language for Reliable Real-Time Tasks,
University of California, Berkeley, 2008.
date_created: 2018-12-11T12:09:18Z
date_published: 2008-01-31T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '31'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 210
publication_status: published
publisher: University of California, Berkeley
publist_id: '199'
status: public
supervisor:
- first_name: Alberto
full_name: Sangiovanni-Vincentelli, Alberto
last_name: Sangiovanni-Vincentelli
- 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: Edward
full_name: Lee, Edward
last_name: Lee
- first_name: Karl
full_name: Hedrick, Karl
last_name: Hedrick
title: A hierarchical coordination language for reliable real-time tasks
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2008'
...
---
_id: '4527'
abstract:
- lang: eng
text: |-
We introduce bounded asynchrony, a notion of concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability observed in cells that, although equally potent, assume distinct fates. Real-life cells are not “scheduled”, but we show that distributed real-time behavior can lead to component interactions that are observationally equivalent to bounded asynchrony; this provides a possible mechanistic explanation for the phenomena observed during cell fate specification.
We use model checking to determine cell fates. The nondeterminism of bounded asynchrony causes state explosion during model checking, but partial-order methods are not directly applicable. We present a new algorithm that reduces the number of states that need to be explored: our optimization takes advantage of the bounded-asynchronous progress and the spatially local interactions of components that model cells. We compare our own communication-based reduction with partial-order reduction (on a restricted form of bounded asynchrony) and experiments illustrate that our algorithm leads to significant savings.
acknowledgement: Supported in part by the Swiss National Science Foundation (grant
205321-111840).
alternative_title:
- LNCS
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
- first_name: Maria
full_name: Maria Mateescu
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. Bounded asynchrony: Concurrency
for modeling cell-cell interactions. In: Vol 5054. Springer; 2008:17-32. doi:10.1007/978-3-540-68413-8_2'
apa: 'Fisher, J., Henzinger, T. A., Mateescu, M., & Piterman, N. (2008). Bounded
asynchrony: Concurrency for modeling cell-cell interactions (Vol. 5054, pp. 17–32).
Presented at the FMSB: Formal Methods in Systems Biology, Springer. https://doi.org/10.1007/978-3-540-68413-8_2'
chicago: 'Fisher, Jasmin, Thomas A Henzinger, Maria Mateescu, and Nir Piterman.
“Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions,” 5054:17–32.
Springer, 2008. https://doi.org/10.1007/978-3-540-68413-8_2.'
ieee: 'J. Fisher, T. A. Henzinger, M. Mateescu, and N. Piterman, “Bounded asynchrony:
Concurrency for modeling cell-cell interactions,” presented at the FMSB: Formal
Methods in Systems Biology, 2008, vol. 5054, pp. 17–32.'
ista: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. 2008. Bounded asynchrony:
Concurrency for modeling cell-cell interactions. FMSB: Formal Methods in Systems
Biology, LNCS, vol. 5054, 17–32.'
mla: 'Fisher, Jasmin, et al. Bounded Asynchrony: Concurrency for Modeling Cell-Cell
Interactions. Vol. 5054, Springer, 2008, pp. 17–32, doi:10.1007/978-3-540-68413-8_2.'
short: J. Fisher, T.A. Henzinger, M. Mateescu, N. Piterman, in:, Springer, 2008,
pp. 17–32.
conference:
name: 'FMSB: Formal Methods in Systems Biology'
date_created: 2018-12-11T12:09:19Z
date_published: 2008-05-26T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '26'
doi: 10.1007/978-3-540-68413-8_2
extern: 1
intvolume: ' 5054'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/bounded_asynchrony.pdf
month: '05'
page: 17 - 32
publication_status: published
publisher: Springer
publist_id: '196'
quality_controlled: 0
status: public
title: 'Bounded asynchrony: Concurrency for modeling cell-cell interactions'
type: conference
volume: 5054
year: '2008'
...
---
_id: '4532'
abstract:
- lang: eng
text: We consider the equivalence problem for labeled Markov chains (LMCs), where
each state is labeled with an observation. Two LMCs are equivalent if every finite
sequence of observations has the same probability of occurrence in the two LMCs.
We show that equivalence can be decided in polynomial time, using a reduction
to the equivalence problem for probabilistic automata, which is known to be solvable
in polynomial time. We provide an alternative algorithm to solve the equivalence
problem, which is based on a new definition of bisimulation for probabilistic
automata. We also extend the technique to decide the equivalence of weighted probabilistic
automata.
author:
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jean
full_name: Raskin, Jean-François
last_name: Raskin
citation:
ama: Doyen L, Henzinger TA, Raskin J. Equivalence of labeled Markov chains. International
Journal of Foundations of Computer Science. 2008;19(3):549-563. doi:10.1142/S0129054108005814
apa: Doyen, L., Henzinger, T. A., & Raskin, J. (2008). Equivalence of labeled
Markov chains. International Journal of Foundations of Computer Science.
World Scientific Publishing. https://doi.org/10.1142/S0129054108005814
chicago: Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Equivalence of Labeled
Markov Chains.” International Journal of Foundations of Computer Science.
World Scientific Publishing, 2008. https://doi.org/10.1142/S0129054108005814 .
ieee: L. Doyen, T. A. Henzinger, and J. Raskin, “Equivalence of labeled Markov chains,”
International Journal of Foundations of Computer Science, vol. 19, no.
3. World Scientific Publishing, pp. 549–563, 2008.
ista: Doyen L, Henzinger TA, Raskin J. 2008. Equivalence of labeled Markov chains.
International Journal of Foundations of Computer Science. 19(3), 549–563.
mla: Doyen, Laurent, et al. “Equivalence of Labeled Markov Chains.” International
Journal of Foundations of Computer Science, vol. 19, no. 3, World Scientific
Publishing, 2008, pp. 549–63, doi:10.1142/S0129054108005814 .
short: L. Doyen, T.A. Henzinger, J. Raskin, International Journal of Foundations
of Computer Science 19 (2008) 549–563.
date_created: 2018-12-11T12:09:20Z
date_published: 2008-06-01T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '01'
doi: '10.1142/S0129054108005814 '
extern: 1
intvolume: ' 19'
issue: '3'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/equivalence_of_labeled_markov_chains.pdf
month: '06'
page: 549 - 563
publication: International Journal of Foundations of Computer Science
publication_status: published
publisher: World Scientific Publishing
publist_id: '192'
quality_controlled: 0
status: public
title: Equivalence of labeled Markov chains
type: journal_article
volume: 19
year: '2008'
...
---
_id: '4533'
abstract:
- lang: eng
text: Interface theories have been proposed to support incremental design and independent
implementability. Incremental design means that the compatibility checking of
interfaces can proceed for partial system descriptions, without knowing the interfaces
of all components. Independent implementability means that compatible interfaces
can be refined separately, maintaining compatibility. We show that these interface
theories provide no formal support for component reuse, meaning that the same
component cannot be used to implement several different interfaces in a design.
We add a new operation to interface theories in order to support such reuse. For
example, different interfaces for the same component may refer to different aspects
such as functionality, timing, and power consumption. We give both stateless and
stateful examples for interface theories with component reuse. To illustrate component
reuse in interface-based design, we show how the stateful theory provides a natural
framework for specifying and refining PCI bus clients.
author:
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Tatjana
full_name: Tatjana Petrov
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Doyen L, Henzinger TA, Jobstmann B, Petrov T. Interface theories with component
reuse. In: ACM; 2008:79-88. doi:10.1145/1450058.1450070'
apa: 'Doyen, L., Henzinger, T. A., Jobstmann, B., & Petrov, T. (2008). Interface
theories with component reuse (pp. 79–88). Presented at the EMSOFT: Embedded Software
, ACM. https://doi.org/10.1145/1450058.1450070'
chicago: Doyen, Laurent, Thomas A Henzinger, Barbara Jobstmann, and Tatjana Petrov.
“Interface Theories with Component Reuse,” 79–88. ACM, 2008. https://doi.org/10.1145/1450058.1450070.
ieee: 'L. Doyen, T. A. Henzinger, B. Jobstmann, and T. Petrov, “Interface theories
with component reuse,” presented at the EMSOFT: Embedded Software , 2008, pp.
79–88.'
ista: 'Doyen L, Henzinger TA, Jobstmann B, Petrov T. 2008. Interface theories with
component reuse. EMSOFT: Embedded Software , 79–88.'
mla: Doyen, Laurent, et al. Interface Theories with Component Reuse. ACM,
2008, pp. 79–88, doi:10.1145/1450058.1450070.
short: L. Doyen, T.A. Henzinger, B. Jobstmann, T. Petrov, in:, ACM, 2008, pp. 79–88.
conference:
name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:09:21Z
date_published: 2008-10-01T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '01'
doi: 10.1145/1450058.1450070
extern: 1
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/interface_theories_with_component_reuse.pdf
month: '10'
page: 79 - 88
publication_status: published
publisher: ACM
publist_id: '193'
quality_controlled: 0
status: public
title: Interface theories with component reuse
type: conference
year: '2008'
...
---
_id: '4534'
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, and mean-payoff (or limit-average) objectives.
These games lie in NP ∩ coNP. We present a polynomial-time Turing reduction of
stochastic parity games to stochastic mean-payoff games.
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. Reduction of stochastic parity to stochastic mean-payoff
games. Information Processing Letters. 2008;106(1):1-7. doi:10.1016/j.ipl.2007.08.035
apa: Chatterjee, K., & Henzinger, T. A. (2008). Reduction of stochastic parity
to stochastic mean-payoff games. Information Processing Letters. Elsevier.
https://doi.org/10.1016/j.ipl.2007.08.035
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Reduction of Stochastic
Parity to Stochastic Mean-Payoff Games.” Information Processing Letters.
Elsevier, 2008. https://doi.org/10.1016/j.ipl.2007.08.035.
ieee: K. Chatterjee and T. A. Henzinger, “Reduction of stochastic parity to stochastic
mean-payoff games,” Information Processing Letters, vol. 106, no. 1. Elsevier,
pp. 1–7, 2008.
ista: Chatterjee K, Henzinger TA. 2008. Reduction of stochastic parity to stochastic
mean-payoff games. Information Processing Letters. 106(1), 1–7.
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. “Reduction of Stochastic Parity
to Stochastic Mean-Payoff Games.” Information Processing Letters, vol.
106, no. 1, Elsevier, 2008, pp. 1–7, doi:10.1016/j.ipl.2007.08.035.
short: K. Chatterjee, T.A. Henzinger, Information Processing Letters 106 (2008)
1–7.
date_created: 2018-12-11T12:09:21Z
date_published: 2008-03-31T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '31'
doi: 10.1016/j.ipl.2007.08.035
extern: 1
intvolume: ' 106'
issue: '1'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/reduction_of_stochastic_parity_to_stochastic_mean-payoff_games.pdf
month: '03'
page: 1 - 7
publication: Information Processing Letters
publication_status: published
publisher: Elsevier
publist_id: '188'
quality_controlled: 0
status: public
title: Reduction of stochastic parity to stochastic mean-payoff games
type: journal_article
volume: 106
year: '2008'
...
---
_id: '4546'
abstract:
- lang: eng
text: We propose the notion of logical reliability for real-time program tasks that
interact through periodically updated program variables. We describe a reliability
analysis that checks if the given short-term (e.g., single-period) reliability
of a program variable update in an implementation is sufficient to meet the logical
reliability requirement (of the program variable) in the long run. We then present
a notion of design by refinement where a task can be refined by another task that
writes to program variables with less logical reliability. The resulting analysis
can be combined with an incremental schedulability analysis for interacting real-time
tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination
language for distributed real-time systems. We implemented a logical-reliability-enhanced
prototype of the compiler and runtime infrastructure for HTL.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Claudio
full_name: Pinello, Claudio
last_name: Pinello
- first_name: Alberto
full_name: Sangiovanni-Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: 'Chatterjee K, Ghosal A, Henzinger TA, et al. Logical reliability of interacting
real-time tasks. In: IEEE; 2008:909-914. doi:10.1145/1403375.1403595'
apa: 'Chatterjee, K., Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., Pinello,
C., & Sangiovanni Vincentelli, A. (2008). Logical reliability of interacting
real-time tasks (pp. 909–914). Presented at the DATE: Design, Automation and Test
in Europe, IEEE. https://doi.org/10.1145/1403375.1403595'
chicago: Chatterjee, Krishnendu, Arkadeb Ghosal, Thomas A Henzinger, Daniel Iercan,
Christoph Kirsch, Claudio Pinello, and Alberto Sangiovanni Vincentelli. “Logical
Reliability of Interacting Real-Time Tasks,” 909–14. IEEE, 2008. https://doi.org/10.1145/1403375.1403595.
ieee: 'K. Chatterjee et al., “Logical reliability of interacting real-time
tasks,” presented at the DATE: Design, Automation and Test in Europe, 2008, pp.
909–914.'
ista: 'Chatterjee K, Ghosal A, Henzinger TA, Iercan D, Kirsch C, Pinello C, Sangiovanni
Vincentelli A. 2008. Logical reliability of interacting real-time tasks. DATE:
Design, Automation and Test in Europe, 909–914.'
mla: Chatterjee, Krishnendu, et al. Logical Reliability of Interacting Real-Time
Tasks. IEEE, 2008, pp. 909–14, doi:10.1145/1403375.1403595.
short: K. Chatterjee, A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, C. Pinello,
A. Sangiovanni Vincentelli, in:, IEEE, 2008, pp. 909–914.
conference:
name: 'DATE: Design, Automation and Test in Europe'
date_created: 2018-12-11T12:09:25Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:36Z
day: '01'
doi: 10.1145/1403375.1403595
extern: 1
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/logical_reliability_of_interacting_real-time_tasks.pdf
month: '01'
page: 909 - 914
publication_status: published
publisher: IEEE
publist_id: '171'
quality_controlled: 0
status: public
title: Logical reliability of interacting real-time tasks
type: conference
year: '2008'
...
---
_id: '4548'
abstract:
- lang: eng
text: The value of a finite-state two-player zero-sum stochastic game with limit-average
payoff can be approximated to within ε in time exponential in a polynomial in
the size of the game times polynomial in logarithmic in 1/ε, for all ε > 0.
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. Stochastic limit-average games are
in EXPTIME. International Journal of Game Theory. 2008;37(2):219-234. doi:10.1007/s00182-007-0110-5
apa: Chatterjee, K., Majumdar, R., & Henzinger, T. A. (2008). Stochastic limit-average
games are in EXPTIME. International Journal of Game Theory. Springer. https://doi.org/10.1007/s00182-007-0110-5
chicago: Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Stochastic
Limit-Average Games Are in EXPTIME.” International Journal of Game Theory.
Springer, 2008. https://doi.org/10.1007/s00182-007-0110-5.
ieee: K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Stochastic limit-average
games are in EXPTIME,” International Journal of Game Theory, vol. 37, no.
2. Springer, pp. 219–234, 2008.
ista: Chatterjee K, Majumdar R, Henzinger TA. 2008. Stochastic limit-average games
are in EXPTIME. International Journal of Game Theory. 37(2), 219–234.
mla: Chatterjee, Krishnendu, et al. “Stochastic Limit-Average Games Are in EXPTIME.”
International Journal of Game Theory, vol. 37, no. 2, Springer, 2008, pp.
219–34, doi:10.1007/s00182-007-0110-5.
short: K. Chatterjee, R. Majumdar, T.A. Henzinger, International Journal of Game
Theory 37 (2008) 219–234.
date_created: 2018-12-11T12:09:25Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:37Z
day: '01'
doi: 10.1007/s00182-007-0110-5
extern: 1
intvolume: ' 37'
issue: '2'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/stochastic_limit-average_games_are_in_exptime.pdf
month: '01'
page: 219 - 234
publication: International Journal of Game Theory
publication_status: published
publisher: Springer
publist_id: '168'
quality_controlled: 0
status: public
title: Stochastic limit-average games are in EXPTIME
type: journal_article
volume: 37
year: '2008'
...
---
_id: '4568'
abstract:
- lang: eng
text: We present and evaluate a framework and tool for combining multiple program
analyses which allows the dynamic (on-line) adjustment of the precision of each
analysis depending on the accumulated results. For example, the explicit tracking
of the values of a variable may be switched off in favor of a predicate abstraction
when and where the number of different variable values that have been encountered
has exceeded a specified threshold. The method is evaluated on verifying the SSH
client/server software and shows significant gains compared with predicate abstraction-based
model checking.
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Grégory
full_name: Théoduloz, Grégory
last_name: Théoduloz
citation:
ama: 'Beyer D, Henzinger TA, Théoduloz G. Program analysis with dynamic change of
precision. In: ACM; 2008:29-38. doi:10.1109/ASE.2008.13'
apa: 'Beyer, D., Henzinger, T. A., & Théoduloz, G. (2008). Program analysis
with dynamic change of precision (pp. 29–38). Presented at the ASE: Automated
Software Engineering, ACM. https://doi.org/10.1109/ASE.2008.13'
chicago: Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Program Analysis
with Dynamic Change of Precision,” 29–38. ACM, 2008. https://doi.org/10.1109/ASE.2008.13.
ieee: 'D. Beyer, T. A. Henzinger, and G. Théoduloz, “Program analysis with dynamic
change of precision,” presented at the ASE: Automated Software Engineering, 2008,
pp. 29–38.'
ista: 'Beyer D, Henzinger TA, Théoduloz G. 2008. Program analysis with dynamic change
of precision. ASE: Automated Software Engineering, 29–38.'
mla: Beyer, Dirk, et al. Program Analysis with Dynamic Change of Precision.
ACM, 2008, pp. 29–38, doi:10.1109/ASE.2008.13.
short: D. Beyer, T.A. Henzinger, G. Théoduloz, in:, ACM, 2008, pp. 29–38.
conference:
name: 'ASE: Automated Software Engineering'
date_created: 2018-12-11T12:09:31Z
date_published: 2008-10-07T00:00:00Z
date_updated: 2021-01-12T07:59:46Z
day: '07'
doi: 10.1109/ASE.2008.13
extern: 1
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/program_analysis_with_dynamic_change_of_precision.pdf
month: '10'
page: 29 - 38
publication_status: published
publisher: ACM
publist_id: '140'
quality_controlled: 0
status: public
title: Program analysis with dynamic change of precision
type: conference
year: '2008'
...
---
_id: '517'
article_processing_charge: No
article_type: comment
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. Identity and coalescence in structured populations: A commentary
on “Inbreeding coefficients and coalescence times” by Montgomery Slatkin. Genetics
Research. 2008;89(5-6):475-477. doi:10.1017/S0016672308009683'
apa: 'Barton, N. H. (2008). Identity and coalescence in structured populations:
A commentary on “Inbreeding coefficients and coalescence times” by Montgomery
Slatkin. Genetics Research. Cambridge University Press. https://doi.org/10.1017/S0016672308009683'
chicago: 'Barton, Nicholas H. “Identity and Coalescence in Structured Populations:
A Commentary on ‘Inbreeding Coefficients and Coalescence Times’ by Montgomery
Slatkin.” Genetics Research. Cambridge University Press, 2008. https://doi.org/10.1017/S0016672308009683.'
ieee: 'N. H. Barton, “Identity and coalescence in structured populations: A commentary
on ‘Inbreeding coefficients and coalescence times’ by Montgomery Slatkin,” Genetics
Research, vol. 89, no. 5–6. Cambridge University Press, pp. 475–477, 2008.'
ista: 'Barton NH. 2008. Identity and coalescence in structured populations: A commentary
on ‘Inbreeding coefficients and coalescence times’ by Montgomery Slatkin. Genetics
Research. 89(5–6), 475–477.'
mla: 'Barton, Nicholas H. “Identity and Coalescence in Structured Populations: A
Commentary on ‘Inbreeding Coefficients and Coalescence Times’ by Montgomery Slatkin.”
Genetics Research, vol. 89, no. 5–6, Cambridge University Press, 2008,
pp. 475–77, doi:10.1017/S0016672308009683.'
short: N.H. Barton, Genetics Research 89 (2008) 475–477.
date_created: 2018-12-11T11:46:55Z
date_published: 2008-10-29T00:00:00Z
date_updated: 2026-04-29T07:15:43Z
day: '29'
department:
- _id: NiBa
doi: 10.1017/S0016672308009683
external_id:
isi:
- '000207048900023'
intvolume: ' 89'
isi: 1
issue: 5-6
language:
- iso: eng
month: '10'
oa_version: None
page: 475 - 477
publication: Genetics Research
publication_status: published
publisher: Cambridge University Press
publist_id: '7302'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Identity and coalescence in structured populations: A commentary on ''Inbreeding
coefficients and coalescence times'' by Montgomery Slatkin'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 89
year: '2008'
...
---
_id: '2892'
author:
- first_name: Ricardo
full_name: Azevedo, Ricardo B
last_name: Azevedo
- first_name: Rolf
full_name: Lohaus, Rolf
last_name: Lohaus
- first_name: Tiago
full_name: Tiago Paixao
id: 2C5658E6-F248-11E8-B48F-1D18A9856A87
last_name: Paixao
orcid: 0000-0003-2361-3953
citation:
ama: Azevedo R, Lohaus R, Paixao T. Networking networks. Evolution & Development.
2008;10(5):514-515. doi:10.1111/j.1525-142X.2008.00265.x
apa: Azevedo, R., Lohaus, R., & Paixao, T. (2008). Networking networks. Evolution
& Development. Wiley-Blackwell. https://doi.org/10.1111/j.1525-142X.2008.00265.x
chicago: Azevedo, Ricardo, Rolf Lohaus, and Tiago Paixao. “Networking Networks.”
Evolution & Development. Wiley-Blackwell, 2008. https://doi.org/10.1111/j.1525-142X.2008.00265.x.
ieee: R. Azevedo, R. Lohaus, and T. Paixao, “Networking networks,” Evolution
& Development, vol. 10, no. 5. Wiley-Blackwell, pp. 514–515, 2008.
ista: Azevedo R, Lohaus R, Paixao T. 2008. Networking networks. Evolution &
Development. 10(5), 514–515.
mla: Azevedo, Ricardo, et al. “Networking Networks.” Evolution & Development,
vol. 10, no. 5, Wiley-Blackwell, 2008, pp. 514–15, doi:10.1111/j.1525-142X.2008.00265.x.
short: R. Azevedo, R. Lohaus, T. Paixao, Evolution & Development 10 (2008) 514–515.
date_created: 2018-12-11T12:00:11Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:00:31Z
day: '01'
doi: 10.1111/j.1525-142X.2008.00265.x
extern: 1
intvolume: ' 10'
issue: '5'
month: '01'
page: 514 - 515
publication: Evolution & Development
publication_status: published
publisher: Wiley-Blackwell
publist_id: '3866'
quality_controlled: 0
status: public
title: Networking networks
type: journal_article
volume: 10
year: '2008'
...
---
_id: '3030'
abstract:
- lang: eng
text: Telomeres in many eukaryotes are maintained by telomerase in whose absence
telomere shortening occurs. However, telomerase-deficient Arabidopsis thaliana
mutants (Attert -/-) show extremely low rates of telomere shortening per plant
generation (250-500 bp), which does not correspond to the expected outcome of
replicative telomere shortening resulting from ca. 1,000 meristem cell divisions
per seed-to-seed generation. To investigate the influence of the number of cell
divisions per seed-to-seed generation, Attert -/- mutant plants were propagated
from seeds coming either from the lower-most or the upper-most siliques (L- and
U-plants) and the length of their telomeres were followed over several generations.
The rate of telomere shortening was faster in U-plants, than in L-plants, as would
be expected from their higher number of cell divisions per generation. However,
this trend was observed only in telomeres whose initial length is relatively high
and the differences decreased with progressive general telomere shortening over
generations. But in generation 4, the L-plants frequently show a net telomere
elongation, while the U-plants fail to do so. We propose that this is due to the
activation of alternative telomere lengthening (ALT), a process which is activated
in early embryonic development in both U- and L-plants, but is overridden in U-plants
due to their higher number of cell divisions per generation. These data demonstrate
what so far has only been speculated, that in the absence of telomerase, the number
of cell divisions within one generation influences the control of telomere lengths.
These results also reveal a fast and efficient activation of ALT mechanism(s)
in response to the loss of telomerase activity and imply that ALT is probably
involved also in normal plant development.
author:
- first_name: Eva
full_name: Růčková, Eva
last_name: Růčková
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
- first_name: Petra
full_name: Procházková Schrumpfová, Petra
last_name: Procházková Schrumpfová
- first_name: Jiří
full_name: Fajkus, Jiří
last_name: Fajkus
citation:
ama: Růčková E, Friml J, Procházková Schrumpfová P, Fajkus J. Role of alternative
telomere lengthening unmasked in telomerase knock-out mutant plants. Plant
Molecular Biology. 2008;66(6):637-646. doi:10.1007/s11103-008-9295-7
apa: Růčková, E., Friml, J., Procházková Schrumpfová, P., & Fajkus, J. (2008).
Role of alternative telomere lengthening unmasked in telomerase knock-out mutant
plants. Plant Molecular Biology. Springer. https://doi.org/10.1007/s11103-008-9295-7
chicago: Růčková, Eva, Jiří Friml, Petra Procházková Schrumpfová, and Jiří Fajkus.
“Role of Alternative Telomere Lengthening Unmasked in Telomerase Knock-out Mutant
Plants.” Plant Molecular Biology. Springer, 2008. https://doi.org/10.1007/s11103-008-9295-7.
ieee: E. Růčková, J. Friml, P. Procházková Schrumpfová, and J. Fajkus, “Role of
alternative telomere lengthening unmasked in telomerase knock-out mutant plants,”
Plant Molecular Biology, vol. 66, no. 6. Springer, pp. 637–646, 2008.
ista: Růčková E, Friml J, Procházková Schrumpfová P, Fajkus J. 2008. Role of alternative
telomere lengthening unmasked in telomerase knock-out mutant plants. Plant Molecular
Biology. 66(6), 637–646.
mla: Růčková, Eva, et al. “Role of Alternative Telomere Lengthening Unmasked in
Telomerase Knock-out Mutant Plants.” Plant Molecular Biology, vol. 66,
no. 6, Springer, 2008, pp. 637–46, doi:10.1007/s11103-008-9295-7.
short: E. Růčková, J. Friml, P. Procházková Schrumpfová, J. Fajkus, Plant Molecular
Biology 66 (2008) 637–646.
date_created: 2018-12-11T12:00:57Z
date_published: 2008-04-01T00:00:00Z
date_updated: 2021-01-12T07:40:34Z
day: '01'
doi: 10.1007/s11103-008-9295-7
extern: 1
intvolume: ' 66'
issue: '6'
month: '04'
page: 637 - 646
publication: Plant Molecular Biology
publication_status: published
publisher: Springer
publist_id: '3671'
quality_controlled: 0
status: public
title: Role of alternative telomere lengthening unmasked in telomerase knock-out mutant
plants
type: journal_article
volume: 66
year: '2008'
...
---
_id: '3031'
abstract:
- lang: eng
text: Many aspects of plant development, including patterning and tropisms, are
largely dependent on the asymmetric distribution of the plant signaling molecule
auxin. Auxin transport inhibitors (ATIs), which interfere with directional auxin
transport, have been essential tools in formulating this concept. However, despite
the use of ATIs in plant research for many decades, the mechanism of ATI action
has remained largely elusive. Using real-time live-cell microscopy, we show here
that prominent ATIs such as 2,3,5-triiodobenzoic acid (TIBA) and 2-(1-pyrenoyl)
benzoic acid (PBA) inhibit vesicle trafficking in plant, yeast, and mammalian
cells. Effects on micropinocytosis, rab5-labeled endosomal motility at the periphery
of HeLa cells and on fibroblast mobility indicate that ATIs influence actin cytoskeleton.
Visualization of actin cytoskeleton dynamics in plants, yeast, and mammalian cells
show that ATIs stabilize actin. Conversely, stabilizing actin by chemical or genetic
means interferes with endocytosis, vesicle motility, auxin transport, and plant
development, including auxin transport-dependent processes. Our results show that
a class of ATIs act as actin stabilizers and advocate that actin-dependent trafficking
of auxin transport components participates in the mechanism of auxin transport.
These studies also provide an example of how the common eukaryotic process of
actin-based vesicle motility can fulfill a plant-specific physiological role.
author:
- first_name: Pankaj
full_name: Dhonukshe, Pankaj
last_name: Dhonukshe
- first_name: Ilya
full_name: Grigoriev, Ilya S
last_name: Grigoriev
- first_name: Rainer
full_name: Fischer, Rainer
last_name: Fischer
- first_name: Motoki
full_name: Tominaga, Motoki
last_name: Tominaga
- first_name: David
full_name: Robinson, David G
last_name: Robinson
- first_name: Jiří
full_name: Hašek, Jiří
last_name: Hašek
- first_name: Tomasz
full_name: Paciorek, Tomasz
last_name: Paciorek
- first_name: Jan
full_name: Petrášek, Jan
last_name: Petrášek
- first_name: Daniela
full_name: Seifertová, Daniela
last_name: Seifertová
- first_name: Ricardo
full_name: Tejos, Ricardo
last_name: Tejos
- first_name: Lee
full_name: Meisel, Lee A
last_name: Meisel
- first_name: Eva
full_name: Zažímalová, Eva
last_name: Zažímalová
- first_name: Theodorus
full_name: Gadella, Theodorus W
last_name: Gadella
- first_name: York
full_name: Stierhof, York-Dieter
last_name: Stierhof
- first_name: Takashi
full_name: Ueda, Takashi
last_name: Ueda
- first_name: Kazuhiro
full_name: Oiwa, Kazuhiro
last_name: Oiwa
- first_name: Anna
full_name: Akhmanova, Anna
last_name: Akhmanova
- first_name: Roland
full_name: Brock, Roland
last_name: Brock
- first_name: Anne
full_name: Spang, Anne
last_name: Spang
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
citation:
ama: Dhonukshe P, Grigoriev I, Fischer R, et al. Auxin transport inhibitors impair
vesicle motility and actin cytoskeleton dynamics in diverse eukaryotes. PNAS.
2008;105(11):4489-4494. doi:10.1073/pnas.0711414105
apa: Dhonukshe, P., Grigoriev, I., Fischer, R., Tominaga, M., Robinson, D., Hašek,
J., … Friml, J. (2008). Auxin transport inhibitors impair vesicle motility and
actin cytoskeleton dynamics in diverse eukaryotes. PNAS. National Academy
of Sciences. https://doi.org/10.1073/pnas.0711414105
chicago: Dhonukshe, Pankaj, Ilya Grigoriev, Rainer Fischer, Motoki Tominaga, David
Robinson, Jiří Hašek, Tomasz Paciorek, et al. “Auxin Transport Inhibitors Impair
Vesicle Motility and Actin Cytoskeleton Dynamics in Diverse Eukaryotes.” PNAS.
National Academy of Sciences, 2008. https://doi.org/10.1073/pnas.0711414105.
ieee: P. Dhonukshe et al., “Auxin transport inhibitors impair vesicle motility
and actin cytoskeleton dynamics in diverse eukaryotes,” PNAS, vol. 105,
no. 11. National Academy of Sciences, pp. 4489–4494, 2008.
ista: Dhonukshe P, Grigoriev I, Fischer R, Tominaga M, Robinson D, Hašek J, Paciorek
T, Petrášek J, Seifertová D, Tejos R, Meisel L, Zažímalová E, Gadella T, Stierhof
Y, Ueda T, Oiwa K, Akhmanova A, Brock R, Spang A, Friml J. 2008. Auxin transport
inhibitors impair vesicle motility and actin cytoskeleton dynamics in diverse
eukaryotes. PNAS. 105(11), 4489–4494.
mla: Dhonukshe, Pankaj, et al. “Auxin Transport Inhibitors Impair Vesicle Motility
and Actin Cytoskeleton Dynamics in Diverse Eukaryotes.” PNAS, vol. 105,
no. 11, National Academy of Sciences, 2008, pp. 4489–94, doi:10.1073/pnas.0711414105.
short: P. Dhonukshe, I. Grigoriev, R. Fischer, M. Tominaga, D. Robinson, J. Hašek,
T. Paciorek, J. Petrášek, D. Seifertová, R. Tejos, L. Meisel, E. Zažímalová, T.
Gadella, Y. Stierhof, T. Ueda, K. Oiwa, A. Akhmanova, R. Brock, A. Spang, J. Friml,
PNAS 105 (2008) 4489–4494.
date_created: 2018-12-11T12:00:58Z
date_published: 2008-03-18T00:00:00Z
date_updated: 2021-01-12T07:40:34Z
day: '18'
doi: 10.1073/pnas.0711414105
extern: 1
intvolume: ' 105'
issue: '11'
month: '03'
page: 4489 - 4494
publication: PNAS
publication_status: published
publisher: National Academy of Sciences
publist_id: '3672'
quality_controlled: 0
status: public
title: Auxin transport inhibitors impair vesicle motility and actin cytoskeleton dynamics
in diverse eukaryotes
type: journal_article
volume: 105
year: '2008'
...
---
_id: '3032'
abstract:
- lang: eng
text: |2-
Cell polarity manifested by the polar cargo delivery to different plasma-membrane domains is a fundamental feature of multicellular organisms. Pathways for polar delivery have been identified in animals; prominent among them is transcytosis, which involves cargo movement between different sides of the cell [1]. PIN transporters are prominent polar cargoes in plants, whose polar subcellular localization determines the directional flow of the signaling molecule auxin [2, 3]. In this study, we address the cellular mechanisms of PIN polar targeting and dynamic polarity changes. We show that apical and basal PIN targeting pathways are interconnected but molecularly distinct by means of ARF GEF vesicle-trafficking regulators. Pharmacological or genetic interference with the Arabidopsis ARF GEF GNOM leads specifically to apicalization of basal cargoes such as PIN1. We visualize the translocation of PIN proteins between the opposite sides of polarized cells in vivo and show that this PIN transcytosis occurs by endocytic recycling and alternative recruitment of the same cargo molecules by apical and basal targeting machineries. Our data suggest that an ARF GEF-dependent transcytosis-like mechanism is operational in plants and provides a plausible mechanism to trigger changes in PIN polarity and hence auxin fluxes during embryogenesis and organogenesis.
author:
- first_name: Jürgen
full_name: Kleine-Vehn, Jürgen
last_name: Kleine Vehn
- first_name: Pankaj
full_name: Dhonukshe, Pankaj
last_name: Dhonukshe
- first_name: Michael
full_name: Sauer, Michael
last_name: Sauer
- first_name: Philip
full_name: Brewer, Philip B
last_name: Brewer
- first_name: Justyna
full_name: Wiśniewska, Justyna
last_name: Wiśniewska
- first_name: Tomasz
full_name: Paciorek, Tomasz
last_name: Paciorek
- first_name: Eva
full_name: Eva Benková
id: 38F4F166-F248-11E8-B48F-1D18A9856A87
last_name: Benková
orcid: 0000-0002-8510-9739
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
citation:
ama: Kleine Vehn J, Dhonukshe P, Sauer M, et al. ARF GEF dependent transcytosis
and polar delivery of PIN auxin carriers in Arabidopsis. Current Biology.
2008;18(7):526-531. doi:10.1016/j.cub.2008.03.021
apa: Kleine Vehn, J., Dhonukshe, P., Sauer, M., Brewer, P., Wiśniewska, J., Paciorek,
T., … Friml, J. (2008). ARF GEF dependent transcytosis and polar delivery of PIN
auxin carriers in Arabidopsis. Current Biology. Cell Press. https://doi.org/10.1016/j.cub.2008.03.021
chicago: Kleine Vehn, Jürgen, Pankaj Dhonukshe, Michael Sauer, Philip Brewer, Justyna
Wiśniewska, Tomasz Paciorek, Eva Benková, and Jiří Friml. “ARF GEF Dependent Transcytosis
and Polar Delivery of PIN Auxin Carriers in Arabidopsis.” Current Biology.
Cell Press, 2008. https://doi.org/10.1016/j.cub.2008.03.021.
ieee: J. Kleine Vehn et al., “ARF GEF dependent transcytosis and polar delivery
of PIN auxin carriers in Arabidopsis,” Current Biology, vol. 18, no. 7.
Cell Press, pp. 526–531, 2008.
ista: Kleine Vehn J, Dhonukshe P, Sauer M, Brewer P, Wiśniewska J, Paciorek T, Benková
E, Friml J. 2008. ARF GEF dependent transcytosis and polar delivery of PIN auxin
carriers in Arabidopsis. Current Biology. 18(7), 526–531.
mla: Kleine Vehn, Jürgen, et al. “ARF GEF Dependent Transcytosis and Polar Delivery
of PIN Auxin Carriers in Arabidopsis.” Current Biology, vol. 18, no. 7,
Cell Press, 2008, pp. 526–31, doi:10.1016/j.cub.2008.03.021.
short: J. Kleine Vehn, P. Dhonukshe, M. Sauer, P. Brewer, J. Wiśniewska, T. Paciorek,
E. Benková, J. Friml, Current Biology 18 (2008) 526–531.
date_created: 2018-12-11T12:00:58Z
date_published: 2008-04-08T00:00:00Z
date_updated: 2021-01-12T07:40:34Z
day: '08'
doi: 10.1016/j.cub.2008.03.021
extern: 1
intvolume: ' 18'
issue: '7'
month: '04'
page: 526 - 531
publication: Current Biology
publication_status: published
publisher: Cell Press
publist_id: '3670'
quality_controlled: 0
status: public
title: ARF GEF dependent transcytosis and polar delivery of PIN auxin carriers in
Arabidopsis
type: journal_article
volume: 18
year: '2008'
...
---
_id: '3033'
abstract:
- lang: eng
text: |2-
Embryogenesis in Arabidopsis thaliana depends on the proper establishment and maintenance of local auxin accumulation. In the course of elucidating the connections between developmental progress and auxin distribution, several techniques have been developed to investigate spatial and temporal distribution of auxin response or accumulation in Arabidopsis embryos. This chapter reviews and describes two independent methods, the detection of the activity of auxin responsive transgenes and immunolocalization of auxin itself.
alternative_title:
- Methods In Molecular Biology
author:
- first_name: Michael
full_name: Sauer, Michael
last_name: Sauer
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
citation:
ama: 'Sauer M, Friml J. Visualization of auxin gradients in embryogenesis . In:
Suárez M, Bozhkov P, eds. Plant Embryogenesis. Vol 427. Humana Press; 2008:137-144.
doi:10.1007/978-1-59745-273-1_11'
apa: Sauer, M., & Friml, J. (2008). Visualization of auxin gradients in embryogenesis
. In M. Suárez & P. Bozhkov (Eds.), Plant Embryogenesis (Vol. 427,
pp. 137–144). Humana Press. https://doi.org/10.1007/978-1-59745-273-1_11
chicago: Sauer, Michael, and Jiří Friml. “Visualization of Auxin Gradients in Embryogenesis
.” In Plant Embryogenesis, edited by María Suárez and Peter Bozhkov, 427:137–44.
Humana Press, 2008. https://doi.org/10.1007/978-1-59745-273-1_11.
ieee: M. Sauer and J. Friml, “Visualization of auxin gradients in embryogenesis
,” in Plant Embryogenesis, vol. 427, M. Suárez and P. Bozhkov, Eds. Humana
Press, 2008, pp. 137–144.
ista: 'Sauer M, Friml J. 2008.Visualization of auxin gradients in embryogenesis
. In: Plant Embryogenesis. Methods In Molecular Biology, vol. 427, 137–144.'
mla: Sauer, Michael, and Jiří Friml. “Visualization of Auxin Gradients in Embryogenesis
.” Plant Embryogenesis, edited by María Suárez and Peter Bozhkov, vol.
427, Humana Press, 2008, pp. 137–44, doi:10.1007/978-1-59745-273-1_11.
short: M. Sauer, J. Friml, in:, M. Suárez, P. Bozhkov (Eds.), Plant Embryogenesis,
Humana Press, 2008, pp. 137–144.
date_created: 2018-12-11T12:00:58Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:40:35Z
day: '01'
doi: 10.1007/978-1-59745-273-1_11
editor:
- first_name: María
full_name: Suárez, María F
last_name: Suárez
- first_name: Peter
full_name: Bozhkov, Peter V
last_name: Bozhkov
extern: 1
intvolume: ' 427'
month: '01'
page: 137 - 144
publication: Plant Embryogenesis
publication_status: published
publisher: Humana Press
publist_id: '3668'
quality_controlled: 0
status: public
title: 'Visualization of auxin gradients in embryogenesis '
type: book_chapter
volume: 427
year: '2008'
...
---
_id: '3034'
abstract:
- lang: eng
text: 'They can''t move away from shade, so plants resort to a molecular solution
to find a place in the sun. The action they take is quite radical, and involves
a reprogramming of their development. '
article_type: letter_note
author:
- first_name: Jirí
full_name: Friml, Jirí
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
- first_name: Michael
full_name: Sauer, Michael
last_name: Sauer
citation:
ama: 'Friml J, Sauer M. Plant biology: In their neighbour’s shadow. Nature.
2008;453(7193):298-299. doi:10.1038/453298a'
apa: 'Friml, J., & Sauer, M. (2008). Plant biology: In their neighbour’s shadow.
Nature. Nature Publishing Group. https://doi.org/10.1038/453298a'
chicago: 'Friml, Jiří, and Michael Sauer. “Plant Biology: In Their Neighbour’s Shadow.”
Nature. Nature Publishing Group, 2008. https://doi.org/10.1038/453298a.'
ieee: 'J. Friml and M. Sauer, “Plant biology: In their neighbour’s shadow,” Nature,
vol. 453, no. 7193. Nature Publishing Group, pp. 298–299, 2008.'
ista: 'Friml J, Sauer M. 2008. Plant biology: In their neighbour’s shadow. Nature.
453(7193), 298–299.'
mla: 'Friml, Jiří, and Michael Sauer. “Plant Biology: In Their Neighbour’s Shadow.”
Nature, vol. 453, no. 7193, Nature Publishing Group, 2008, pp. 298–99,
doi:10.1038/453298a.'
short: J. Friml, M. Sauer, Nature 453 (2008) 298–299.
date_created: 2018-12-11T12:00:59Z
date_published: 2008-05-15T00:00:00Z
date_updated: 2021-01-12T07:40:35Z
day: '15'
doi: 10.1038/453298a
extern: '1'
intvolume: ' 453'
issue: '7193'
language:
- iso: eng
month: '05'
oa_version: None
page: 298 - 299
publication: Nature
publication_status: published
publisher: Nature Publishing Group
publist_id: '3669'
quality_controlled: '1'
status: public
title: 'Plant biology: In their neighbour''s shadow'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 453
year: '2008'
...
---
_id: '3035'
abstract:
- lang: eng
text: Embryogenesis of Arabidopsis thaliana follows a nearly invariant cell division
pattern and provides an ideal system for studies of early plant development. However,
experimental manipulation with embryogenesis is difficult, as the embryo develops
deeply inside maternal tissues. Here, we present a method to culture zygotic Arabidopsis
embryos in vitro. It enables culturing for prolonged periods of time from the
first developmental stages on. The technique omits excision of the embryo by culturing
the entire ovule, which facilitates the manual procedure. It allows pharmacological
manipulation of embryo development and does not interfere with standard techniques
for localizing gene expression and protein localization in the cultivated embryos.
alternative_title:
- Methods In Molecular Biology
author:
- first_name: Michael
full_name: Sauer, Michael
last_name: Sauer
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
citation:
ama: 'Sauer M, Friml J. In vitro culture of Arabidopsis embryos . In: Suárez M,
Bozhkov P, eds. Plant Embryogenesis. Vol 427. Humana Press; 2008:71-76.
doi:10.1007/978-1-59745-273-1_5'
apa: Sauer, M., & Friml, J. (2008). In vitro culture of Arabidopsis embryos
. In M. Suárez & P. Bozhkov (Eds.), Plant Embryogenesis (Vol. 427,
pp. 71–76). Humana Press. https://doi.org/10.1007/978-1-59745-273-1_5
chicago: Sauer, Michael, and Jiří Friml. “In Vitro Culture of Arabidopsis Embryos
.” In Plant Embryogenesis, edited by María Suárez and Peter Bozhkov, 427:71–76.
Humana Press, 2008. https://doi.org/10.1007/978-1-59745-273-1_5.
ieee: M. Sauer and J. Friml, “In vitro culture of Arabidopsis embryos ,” in Plant
Embryogenesis, vol. 427, M. Suárez and P. Bozhkov, Eds. Humana Press, 2008,
pp. 71–76.
ista: 'Sauer M, Friml J. 2008.In vitro culture of Arabidopsis embryos . In: Plant
Embryogenesis. Methods In Molecular Biology, vol. 427, 71–76.'
mla: Sauer, Michael, and Jiří Friml. “In Vitro Culture of Arabidopsis Embryos .”
Plant Embryogenesis, edited by María Suárez and Peter Bozhkov, vol. 427,
Humana Press, 2008, pp. 71–76, doi:10.1007/978-1-59745-273-1_5.
short: M. Sauer, J. Friml, in:, M. Suárez, P. Bozhkov (Eds.), Plant Embryogenesis,
Humana Press, 2008, pp. 71–76.
date_created: 2018-12-11T12:00:59Z
date_published: 2008-03-07T00:00:00Z
date_updated: 2021-01-12T07:40:35Z
day: '07'
doi: 10.1007/978-1-59745-273-1_5
editor:
- first_name: María
full_name: Suárez, María F
last_name: Suárez
- first_name: Peter
full_name: Bozhkov, Peter V
last_name: Bozhkov
extern: 1
intvolume: ' 427'
month: '03'
page: 71 - 76
publication: Plant Embryogenesis
publication_status: published
publisher: Humana Press
publist_id: '3667'
quality_controlled: 0
status: public
title: 'In vitro culture of Arabidopsis embryos '
type: book_chapter
volume: 427
year: '2008'
...
---
_id: '3036'
abstract:
- lang: eng
text: Plants exhibit an exceptional adaptability to different environmental conditions.
To a large extent, this adaptability depends on their ability to initiate and
form new organs throughout their entire postembryonic life. Plant shoot and root
systems unceasingly branch and form axillary shoots or lateral roots, respectively.
The first event in the formation of a new organ is specification of founder cells.
Several plant hormones, prominent among them auxin, have been implicated in the
acquisition of founder cell identity by differentiated cells, but the mechanisms
underlying this process are largely elusive. Here, we show that auxin and its
local accumulation in root pericycle cells is a necessary and sufficient signal
to respecify these cells into lateral root founder cells. Analysis of the alf4-1
mutant suggests that specification of founder cells and the subsequent activation
of cell division leading to primordium formation represent two genetically separable
events. Time-lapse experiments show that the activation of an auxin response is
the earliest detectable event in founder cell specification. Accordingly, local
activation of auxin response correlates absolutely with the acquisition of founder
cell identity and precedes the actual formation of a lateral root primordium through
patterned cell division. Local production and subsequent accumulation of auxin
in single pericycle cells induced by Cre-Lox-based activation of auxin synthesis
converts them into founder cells. Thus, auxin is the local instructive signal
that is sufficient for acquisition of founder cell identity and can be considered
a morphogenetic trigger in postembryonic plant organogenesis.
author:
- first_name: Joseph
full_name: Dubrovsky, Joseph G
last_name: Dubrovsky
- first_name: Michael
full_name: Sauer, Michael
last_name: Sauer
- first_name: Selene
full_name: Napsucialy-Mendivil, Selene
last_name: Napsucialy Mendivil
- first_name: Maria
full_name: Ivanchenko, Maria G
last_name: Ivanchenko
- first_name: Jirí
full_name: Jirí Friml
id: 4159519E-F248-11E8-B48F-1D18A9856A87
last_name: Friml
orcid: 0000-0002-8302-7596
- first_name: Svetlana
full_name: Shishkova, Svetlana
last_name: Shishkova
- first_name: John
full_name: Celenza, John
last_name: Celenza
- first_name: Eva
full_name: Eva Benková
id: 38F4F166-F248-11E8-B48F-1D18A9856A87
last_name: Benková
orcid: 0000-0002-8510-9739
citation:
ama: Dubrovsky J, Sauer M, Napsucialy Mendivil S, et al. Auxin acts as a local morphogenetic
trigger to specify lateral root founder cells. PNAS. 2008;105(25):8790-8794.
doi:10.1073/pnas.0712307105
apa: Dubrovsky, J., Sauer, M., Napsucialy Mendivil, S., Ivanchenko, M., Friml, J.,
Shishkova, S., … Benková, E. (2008). Auxin acts as a local morphogenetic trigger
to specify lateral root founder cells. PNAS. National Academy of Sciences.
https://doi.org/10.1073/pnas.0712307105
chicago: Dubrovsky, Joseph, Michael Sauer, Selene Napsucialy Mendivil, Maria Ivanchenko,
Jiří Friml, Svetlana Shishkova, John Celenza, and Eva Benková. “Auxin Acts as
a Local Morphogenetic Trigger to Specify Lateral Root Founder Cells.” PNAS.
National Academy of Sciences, 2008. https://doi.org/10.1073/pnas.0712307105.
ieee: J. Dubrovsky et al., “Auxin acts as a local morphogenetic trigger to
specify lateral root founder cells,” PNAS, vol. 105, no. 25. National Academy
of Sciences, pp. 8790–8794, 2008.
ista: Dubrovsky J, Sauer M, Napsucialy Mendivil S, Ivanchenko M, Friml J, Shishkova
S, Celenza J, Benková E. 2008. Auxin acts as a local morphogenetic trigger to
specify lateral root founder cells. PNAS. 105(25), 8790–8794.
mla: Dubrovsky, Joseph, et al. “Auxin Acts as a Local Morphogenetic Trigger to Specify
Lateral Root Founder Cells.” PNAS, vol. 105, no. 25, National Academy of
Sciences, 2008, pp. 8790–94, doi:10.1073/pnas.0712307105.
short: J. Dubrovsky, M. Sauer, S. Napsucialy Mendivil, M. Ivanchenko, J. Friml,
S. Shishkova, J. Celenza, E. Benková, PNAS 105 (2008) 8790–8794.
date_created: 2018-12-11T12:00:59Z
date_published: 2008-06-24T00:00:00Z
date_updated: 2021-01-12T07:40:36Z
day: '24'
doi: 10.1073/pnas.0712307105
extern: 1
intvolume: ' 105'
issue: '25'
month: '06'
page: 8790 - 8794
publication: PNAS
publication_status: published
publisher: National Academy of Sciences
publist_id: '3666'
quality_controlled: 0
status: public
title: Auxin acts as a local morphogenetic trigger to specify lateral root founder
cells
type: journal_article
volume: 105
year: '2008'
...