---
_id: '4409'
abstract:
- lang: eng
text: "Models of timed systems must incorporate not only the sequence of system
events, but the timings of these events as well to capture the real-time aspects
of physical systems. Timed automata are models of real-time systems in which states
consist of discrete locations and values for real-time clocks. The presence of
real-time clocks leads to an uncountable state space. This thesis studies verification
problems on timed automata in a game theoretic framework.\r\n\r\nFor untimed systems,
two systems are close if every sequence of events of one system is also observable
in the second system. For timed systems, the difference in timings of the two
corresponding sequences is also of importance. We propose the notion of bisimulation
distance which quantifies timing differences; if the bisimulation distance between
two systems is epsilon, then (a) every sequence of events of one system has a
corresponding matching sequence in the other, and (b) the timings of matching
events in between the two corresponding traces do not differ by more than epsilon.
We show that we can compute the bisimulation distance between two timed automata
to within any desired degree of accuracy. We also show that the timed verification
logic TCTL is robust with respect to our notion of quantitative bisimilarity,
in particular, if a system satisfies a formula, then every close system satisfies
a close formula.\r\n\r\nTimed games are used for distinguishing between the actions
of several agents, typically a controller and an environment. The controller must
achieve its objective against all possible choices of the environment. The modeling
of the passage of time leads to the presence of zeno executions, and corresponding
unrealizable strategies of the controller which may achieve objectives by blocking
time. We disallow such unreasonable strategies by restricting all agents to use
only receptive strategies --strategies which while not being required to ensure
time divergence by any agent, are such that no agent is responsible for blocking
time. Time divergence is guaranteed when all players use receptive strategies.
We show that timed automaton games with receptive strategies can be solved by
a reduction to finite state turn based game graphs. We define the logic timed
alternating-time temporal logic for verification of timed automaton games and
show that the logic can be model checked in EXPTIME. We also show that the minimum
time required by an agent to reach a desired location, and the maximum time an
agent can stay safe within a set of locations, against all possible actions of
its adversaries are both computable.\r\n\r\nWe next study the memory requirements
of winning strategies for timed automaton games. We prove that finite memory strategies
suffice for safety objectives, and that winning strategies for reachability objectives
may require infinite memory in general. We introduce randomized strategies in
which an agent can propose a probabilistic distribution of moves and show that
finite memory randomized strategies suffice for all omega-regular objectives.
We also show that while randomization helps in simplifying winning strategies,
and thus allows the construction of simpler controllers, it does not help a player
in winning at more states, and thus does not allow the construction of more powerful
controllers.\r\n\r\nFinally we study robust winning strategies in timed games.
In a physical system, a controller may propose an action together with a time
delay, but the action cannot be assumed to be executed at the exact proposed time
delay. We present robust strategies which incorporate such jitters and show that
the set of states from which an agent can win robustly is computable."
article_processing_charge: No
author:
- first_name: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: Prabhu V. Games for the verification of timed systems. 2008:1-137.
apa: Prabhu, V. (2008). Games for the verification of timed systems. University
of California, Berkeley.
chicago: Prabhu, Vinayak. “Games for the Verification of Timed Systems.” University
of California, Berkeley, 2008.
ieee: V. Prabhu, “Games for the verification of timed systems,” University of California,
Berkeley, 2008.
ista: Prabhu V. 2008. Games for the verification of timed systems. University of
California, Berkeley.
mla: Prabhu, Vinayak. Games for the Verification of Timed Systems. University
of California, Berkeley, 2008, pp. 1–137.
short: V. Prabhu, Games for the Verification of Timed Systems, University of California,
Berkeley, 2008.
date_created: 2018-12-11T12:08:42Z
date_published: 2008-09-01T00:00:00Z
date_updated: 2022-02-14T14:35:11Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.html
month: '09'
oa: 1
oa_version: None
page: 1 - 137
publication_status: published
publisher: University of California, Berkeley
publist_id: '319'
status: public
supervisor:
- 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: John
full_name: Steel, John
last_name: Steel
- first_name: Pravin
full_name: Varaiya, Pravin
last_name: Varaiya
title: Games for the verification of timed systems
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2008'
...
---
_id: '4415'
abstract:
- lang: eng
text: 'Many computing applications, especially those in safety critical embedded
systems, require highly predictable timing properties. However, time is often
not present in the prevailing computing and networking abstractions. In fact,
most advances in computer architecture, software, and networking favor average-case
performance over timing predictability. This thesis studies several methods for
the design of concurrent and/or distributed embedded systems with precise timing
guarantees. The focus is on flexible and compositional methods for programming
and verification of the timing properties. The presented methods together with
related formalisms cover two levels of design: (1) Programming language/model
level. We propose the distributed variant of Giotto, a coordination programming
language with an explicit temporal semantics—the logical execution time (LET)
semantics. The LET of a task is an interval of time that specifies the time instants
at which task inputs and outputs become available (task release and termination
instants). The LET of a task is always non-zero. This allows us to communicate
values across the network without changing the timing information of the task,
and without introducing nondeterminism. We show how this methodology supports
distributed code generation for distributed real-time systems. The method gives
up some performance in favor of composability and predictability. We characterize
the tradeoff by comparing the LET semantics with the semantics used in Simulink.
(2) Abstract task graph level. We study interface-based design and verification
of applications represented with task graphs. We consider task sequence graphs
with general event models, and cyclic graphs with periodic event models with jitter
and phase. Here an interface of a component exposes time and resource constraints
of the component. Together with interfaces we formally define interface composition
operations and the refinement relation. For efficient and flexible composability
checking two properties are important: incremental design and independent refinement.
According to the incremental design property the composition of interfaces can
be performed in any order, even if interfaces for some components are not known.
The refinement relation is defined such that in a design we can always substitute
a refined interface for an abstract one. We show that the framework supports independent
refinement, i.e., the refinement relation is preserved under composition operations.'
acknowledgement: 978-0-549-83480-9
article_processing_charge: No
author:
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: Matic S. Compositionality in deterministic real-time embedded systems. 2008:1-148.
apa: Matic, S. (2008). Compositionality in deterministic real-time embedded systems.
University of California, Berkeley.
chicago: Matic, Slobodan. “Compositionality in Deterministic Real-Time Embedded
Systems.” University of California, Berkeley, 2008.
ieee: S. Matic, “Compositionality in deterministic real-time embedded systems,”
University of California, Berkeley, 2008.
ista: Matic S. 2008. Compositionality in deterministic real-time embedded systems.
University of California, Berkeley.
mla: Matic, Slobodan. Compositionality in Deterministic Real-Time Embedded Systems.
University of California, Berkeley, 2008, pp. 1–148.
short: S. Matic, Compositionality in Deterministic Real-Time Embedded Systems, University
of California, Berkeley, 2008.
date_created: 2018-12-11T12:08:44Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2022-02-14T14:08:50Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 148
publication_status: published
publisher: University of California, Berkeley
publist_id: '316'
status: public
supervisor:
- 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: Raja
full_name: Sengupta, Raja
last_name: Sengupta
title: Compositionality in deterministic real-time embedded systems
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2008'
...
---
_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: '581'
abstract:
- lang: eng
text: We have detected a spin-dependent displacement perpendicular to the refractive
index gradient for photons passing through an air-glass interface. The effect
is the photonic version of the spin Hall effect in electronic systems, indicating
the universality of the effect for particles of different nature. Treating the
effect as a weak measurement of the spin projection of the photons, we used a
preselection and postselection technique on the spin state to enhance the original
displacement by nearly four orders of magnitude, attaining sensitivity to displacements
of ∼1 angstrom. The spin Hall effect can be used for manipulating photonic angular
momentum states, and the measurement technique holds promise for precision metrology.
author:
- first_name: Onur
full_name: Onur Hosten
id: 4C02D85E-F248-11E8-B48F-1D18A9856A87
last_name: Hosten
orcid: 0000-0002-2031-204X
- first_name: Paul
full_name: Kwiat, Paul
last_name: Kwiat
citation:
ama: Hosten O, Kwiat P. Observation of the spin hall effect of light via weak measurements.
Science. 2008;319(5864):787-790. doi:10.1126/science.1152697
apa: Hosten, O., & Kwiat, P. (2008). Observation of the spin hall effect of
light via weak measurements. Science. American Association for the Advancement
of Science. https://doi.org/10.1126/science.1152697
chicago: Hosten, Onur, and Paul Kwiat. “Observation of the Spin Hall Effect of Light
via Weak Measurements.” Science. American Association for the Advancement
of Science, 2008. https://doi.org/10.1126/science.1152697.
ieee: O. Hosten and P. Kwiat, “Observation of the spin hall effect of light via
weak measurements,” Science, vol. 319, no. 5864. American Association for
the Advancement of Science, pp. 787–790, 2008.
ista: Hosten O, Kwiat P. 2008. Observation of the spin hall effect of light via
weak measurements. Science. 319(5864), 787–790.
mla: Hosten, Onur, and Paul Kwiat. “Observation of the Spin Hall Effect of Light
via Weak Measurements.” Science, vol. 319, no. 5864, American Association
for the Advancement of Science, 2008, pp. 787–90, doi:10.1126/science.1152697.
short: O. Hosten, P. Kwiat, Science 319 (2008) 787–790.
date_created: 2018-12-11T11:47:19Z
date_published: 2008-02-08T00:00:00Z
date_updated: 2021-01-12T08:03:38Z
day: '08'
doi: 10.1126/science.1152697
extern: 1
intvolume: ' 319'
issue: '5864'
month: '02'
page: 787 - 790
publication: Science
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '7226'
quality_controlled: 0
status: public
title: Observation of the spin hall effect of light via weak measurements
type: journal_article
volume: 319
year: '2008'
...
---
_id: '584'
abstract:
- lang: eng
text: Using “quantum weak-measurements” as a coherent enhancement technique for
small signals, we have measured the recently proposed “spin Hall effect” of light
at an air-glass interface, and are working on the smoothly varying refractive-index
case.
alternative_title:
- Optics InfoBase Conference Papers
article_processing_charge: No
author:
- first_name: Onur
full_name: Hosten, Onur
id: 4C02D85E-F248-11E8-B48F-1D18A9856A87
last_name: Hosten
orcid: 0000-0002-2031-204X
- first_name: Paul
full_name: Kwiat, Paul
last_name: Kwiat
citation:
ama: 'Hosten O, Kwiat P. Spin hall effect of light via weak measurements: Sharp
and smooth index variations. In: Optica Publishing Group; 2008.'
apa: 'Hosten, O., & Kwiat, P. (2008). Spin hall effect of light via weak measurements:
Sharp and smooth index variations. Presented at the QELS: Quantum Electronics
and Laser Science Conference, San Jose, CA, United States: Optica Publishing Group.'
chicago: 'Hosten, Onur, and Paul Kwiat. “Spin Hall Effect of Light via Weak Measurements:
Sharp and Smooth Index Variations.” Optica Publishing Group, 2008.'
ieee: 'O. Hosten and P. Kwiat, “Spin hall effect of light via weak measurements:
Sharp and smooth index variations,” presented at the QELS: Quantum Electronics
and Laser Science Conference, San Jose, CA, United States, 2008.'
ista: 'Hosten O, Kwiat P. 2008. Spin hall effect of light via weak measurements:
Sharp and smooth index variations. QELS: Quantum Electronics and Laser Science
Conference, Optics InfoBase Conference Papers, .'
mla: 'Hosten, Onur, and Paul Kwiat. Spin Hall Effect of Light via Weak Measurements:
Sharp and Smooth Index Variations. Optica Publishing Group, 2008.'
short: O. Hosten, P. Kwiat, in:, Optica Publishing Group, 2008.
conference:
end_date: 2008-05-09
location: San Jose, CA, United States
name: 'QELS: Quantum Electronics and Laser Science Conference'
start_date: 2008-05-04
corr_author: '1'
date_created: 2018-12-11T11:47:20Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2024-10-09T20:53:53Z
day: '01'
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://opg.optica.org/abstract.cfm?URI=QELS-2008-QFB7
month: '01'
oa_version: None
publication_identifier:
isbn:
- 978-155752859-9
issn:
- '21622701'
publication_status: published
publisher: Optica Publishing Group
publist_id: '7227'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Spin hall effect of light via weak measurements: Sharp and smooth index variations'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2008'
...
---
_id: '6146'
abstract:
- lang: eng
text: Homeostasis of internal carbon dioxide (CO2) and oxygen (O2) levels is fundamental
to all animals. Here we examine the CO2 response of the nematode Caenorhabditis
elegans. This species inhabits rotting material, which typically has a broad CO2
concentration range. We show that well fed C. elegans avoid CO2 levels above 0.5%.
Animals can respond to both absolute CO2 concentrations and changes in CO2 levels
within seconds. Responses to CO2 do not reflect avoidance of acid pH but appear
to define a new sensory response. Sensation of CO2 is promoted by the cGMP-gated
ion channel subunits TAX-2 and TAX-4, but other pathways are also important. Robust
CO2 avoidance in well fed animals requires inhibition of the DAF-16 forkhead transcription
factor by the insulin-like receptor DAF-2. Starvation, which activates DAF-16,
strongly suppresses CO2 avoidance. Exposure to hypoxia (<1% O2) also suppresses
CO2 avoidance via activation of the hypoxia-inducible transcription factor HIF-1.
The npr-1 215V allele of the naturally polymorphic neuropeptide receptor npr-1,
besides inhibiting avoidance of high ambient O2 in feeding C. elegans, also promotes
avoidance of high CO2. C. elegans integrates competing O2 and CO2 sensory inputs
so that one response dominates. Food and allelic variation at NPR-1 regulate which
response prevails. Our results suggest that multiple sensory inputs are coordinated
by C. elegans to generate different coherent foraging strategies.
author:
- first_name: A. J.
full_name: Bretscher, A. J.
last_name: Bretscher
- first_name: K. E.
full_name: Busch, K. E.
last_name: Busch
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
citation:
ama: Bretscher AJ, Busch KE, de Bono M. A carbon dioxide avoidance behavior is integrated
with responses to ambient oxygen and food in Caenorhabditis elegans. Proceedings
of the National Academy of Sciences. 2008;105(23):8044-8049. doi:10.1073/pnas.0707607105
apa: Bretscher, A. J., Busch, K. E., & de Bono, M. (2008). A carbon dioxide
avoidance behavior is integrated with responses to ambient oxygen and food in
Caenorhabditis elegans. Proceedings of the National Academy of Sciences.
Proceedings of the National Academy of Sciences. https://doi.org/10.1073/pnas.0707607105
chicago: Bretscher, A. J., K. E. Busch, and Mario de Bono. “A Carbon Dioxide Avoidance
Behavior Is Integrated with Responses to Ambient Oxygen and Food in Caenorhabditis
Elegans.” Proceedings of the National Academy of Sciences. Proceedings
of the National Academy of Sciences, 2008. https://doi.org/10.1073/pnas.0707607105.
ieee: A. J. Bretscher, K. E. Busch, and M. de Bono, “A carbon dioxide avoidance
behavior is integrated with responses to ambient oxygen and food in Caenorhabditis
elegans,” Proceedings of the National Academy of Sciences, vol. 105, no.
23. Proceedings of the National Academy of Sciences, pp. 8044–8049, 2008.
ista: Bretscher AJ, Busch KE, de Bono M. 2008. A carbon dioxide avoidance behavior
is integrated with responses to ambient oxygen and food in Caenorhabditis elegans.
Proceedings of the National Academy of Sciences. 105(23), 8044–8049.
mla: Bretscher, A. J., et al. “A Carbon Dioxide Avoidance Behavior Is Integrated
with Responses to Ambient Oxygen and Food in Caenorhabditis Elegans.” Proceedings
of the National Academy of Sciences, vol. 105, no. 23, Proceedings of the
National Academy of Sciences, 2008, pp. 8044–49, doi:10.1073/pnas.0707607105.
short: A.J. Bretscher, K.E. Busch, M. de Bono, Proceedings of the National Academy
of Sciences 105 (2008) 8044–8049.
date_created: 2019-03-21T08:10:15Z
date_published: 2008-06-10T00:00:00Z
date_updated: 2021-01-12T08:06:21Z
day: '10'
ddc:
- '570'
doi: 10.1073/pnas.0707607105
extern: '1'
external_id:
pmid:
- '18524954'
file:
- access_level: open_access
checksum: eac0413064b022c1489f7b6719e7228c
content_type: application/pdf
creator: kschuh
date_created: 2019-03-21T08:14:54Z
date_updated: 2020-07-14T12:47:20Z
file_id: '6147'
file_name: 2008_PNAS_Bretscher.pdf
file_size: 501506
relation: main_file
file_date_updated: 2020-07-14T12:47:20Z
has_accepted_license: '1'
intvolume: ' 105'
issue: '23'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 8044-8049
pmid: 1
publication: Proceedings of the National Academy of Sciences
publication_identifier:
issn:
- 0027-8424
- 1091-6490
publication_status: published
publisher: Proceedings of the National Academy of Sciences
quality_controlled: '1'
status: public
title: A carbon dioxide avoidance behavior is integrated with responses to ambient
oxygen and food in Caenorhabditis elegans
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 105
year: '2008'
...
---
_id: '6148'
author:
- first_name: Jan E.
full_name: Kammenga, Jan E.
last_name: Kammenga
- first_name: Patrick C.
full_name: Phillips, Patrick C.
last_name: Phillips
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
- first_name: Agnieszka
full_name: Doroszuk, Agnieszka
last_name: Doroszuk
citation:
ama: 'Kammenga JE, Phillips PC, de Bono M, Doroszuk A. Beyond induced mutants: using
worms to study natural variation in genetic pathways. Trends in Genetics.
2008;24(4):178-185. doi:10.1016/j.tig.2008.01.001'
apa: 'Kammenga, J. E., Phillips, P. C., de Bono, M., & Doroszuk, A. (2008).
Beyond induced mutants: using worms to study natural variation in genetic pathways.
Trends in Genetics. Elsevier. https://doi.org/10.1016/j.tig.2008.01.001'
chicago: 'Kammenga, Jan E., Patrick C. Phillips, Mario de Bono, and Agnieszka Doroszuk.
“Beyond Induced Mutants: Using Worms to Study Natural Variation in Genetic Pathways.”
Trends in Genetics. Elsevier, 2008. https://doi.org/10.1016/j.tig.2008.01.001.'
ieee: 'J. E. Kammenga, P. C. Phillips, M. de Bono, and A. Doroszuk, “Beyond induced
mutants: using worms to study natural variation in genetic pathways,” Trends
in Genetics, vol. 24, no. 4. Elsevier, pp. 178–185, 2008.'
ista: 'Kammenga JE, Phillips PC, de Bono M, Doroszuk A. 2008. Beyond induced mutants:
using worms to study natural variation in genetic pathways. Trends in Genetics.
24(4), 178–185.'
mla: 'Kammenga, Jan E., et al. “Beyond Induced Mutants: Using Worms to Study Natural
Variation in Genetic Pathways.” Trends in Genetics, vol. 24, no. 4, Elsevier,
2008, pp. 178–85, doi:10.1016/j.tig.2008.01.001.'
short: J.E. Kammenga, P.C. Phillips, M. de Bono, A. Doroszuk, Trends in Genetics
24 (2008) 178–185.
date_created: 2019-03-21T08:19:45Z
date_published: 2008-04-01T00:00:00Z
date_updated: 2021-01-12T08:06:21Z
day: '01'
doi: 10.1016/j.tig.2008.01.001
extern: '1'
external_id:
pmid:
- '18325626'
intvolume: ' 24'
issue: '4'
language:
- iso: eng
month: '04'
oa_version: None
page: 178-185
pmid: 1
publication: Trends in Genetics
publication_identifier:
issn:
- 0168-9525
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: 'Beyond induced mutants: using worms to study natural variation in genetic
pathways'
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 24
year: '2008'
...
---
_id: '6149'
article_processing_charge: No
author:
- first_name: Birgitta
full_name: Olofsson, Birgitta
last_name: Olofsson
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
citation:
ama: 'Olofsson B, de Bono M. Sleep: dozy worms and sleepy flies. Current Biology.
2008;18(5):R204-R206. doi:10.1016/j.cub.2008.01.002'
apa: 'Olofsson, B., & de Bono, M. (2008). Sleep: dozy worms and sleepy flies.
Current Biology. Elsevier. https://doi.org/10.1016/j.cub.2008.01.002'
chicago: 'Olofsson, Birgitta, and Mario de Bono. “Sleep: Dozy Worms and Sleepy Flies.”
Current Biology. Elsevier, 2008. https://doi.org/10.1016/j.cub.2008.01.002.'
ieee: 'B. Olofsson and M. de Bono, “Sleep: dozy worms and sleepy flies,” Current
Biology, vol. 18, no. 5. Elsevier, pp. R204–R206, 2008.'
ista: 'Olofsson B, de Bono M. 2008. Sleep: dozy worms and sleepy flies. Current
Biology. 18(5), R204–R206.'
mla: 'Olofsson, Birgitta, and Mario de Bono. “Sleep: Dozy Worms and Sleepy Flies.”
Current Biology, vol. 18, no. 5, Elsevier, 2008, pp. R204–06, doi:10.1016/j.cub.2008.01.002.'
short: B. Olofsson, M. de Bono, Current Biology 18 (2008) R204–R206.
date_created: 2019-03-21T08:23:24Z
date_published: 2008-03-11T00:00:00Z
date_updated: 2022-08-25T15:03:41Z
day: '11'
doi: 10.1016/j.cub.2008.01.002
extern: '1'
external_id:
pmid:
- '18334193'
intvolume: ' 18'
issue: '5'
language:
- iso: eng
month: '03'
oa_version: None
page: R204-R206
pmid: 1
publication: Current Biology
publication_identifier:
issn:
- 0960-9822
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: 'Sleep: dozy worms and sleepy flies'
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2008'
...
---
_id: '1982'
abstract:
- lang: eng
text: In the bacterium Escherichia coli, the Min proteins oscillate between the
cell poles to select the cell center as division site. This dynamic pattern has
been proposed to arise by self-organization of these proteins, and several models
have suggested a reaction-diffusion type mechanism. Here, we found that the Min
proteins spontaneously formed planar surface waves on a flat membrane in vitro.
The formation and maintenance of these patterns, which extended for hundreds of
micrometers, required adenosine 5′-triphosphate (ATP), and they persisted for
hours. We present a reaction-diffusion model of the MinD and MinE dynamics that
accounts for our experimental observations and also captures the in vivo oscillations.
acknowledgement: 'This work was supported by the Max-Planck-Society (M.L., P.S., E.F.). '
author:
- first_name: Martin
full_name: Martin Loose
id: 462D4284-F248-11E8-B48F-1D18A9856A87
last_name: Loose
orcid: 0000-0001-7309-9724
- first_name: Elisabeth
full_name: Fischer-Friedrich, Elisabeth
last_name: Fischer Friedrich
- first_name: Jonas
full_name: 'Ries, Jonas '
last_name: Ries
- first_name: Karsten
full_name: Kruse, Karsten
last_name: Kruse
- first_name: Petra
full_name: 'Schwille, Petra '
last_name: Schwille
citation:
ama: Loose M, Fischer Friedrich E, Ries J, Kruse K, Schwille P. Spatial regulators
for bacterial cell division self-organize into surface waves in vitro. Science.
2008;320(5877):789-792. doi:10.1126/science.1154413
apa: Loose, M., Fischer Friedrich, E., Ries, J., Kruse, K., & Schwille, P. (2008).
Spatial regulators for bacterial cell division self-organize into surface waves
in vitro. Science. American Association for the Advancement of Science.
https://doi.org/10.1126/science.1154413
chicago: Loose, Martin, Elisabeth Fischer Friedrich, Jonas Ries, Karsten Kruse,
and Petra Schwille. “Spatial Regulators for Bacterial Cell Division Self-Organize
into Surface Waves in Vitro.” Science. American Association for the Advancement
of Science, 2008. https://doi.org/10.1126/science.1154413.
ieee: M. Loose, E. Fischer Friedrich, J. Ries, K. Kruse, and P. Schwille, “Spatial
regulators for bacterial cell division self-organize into surface waves in vitro,”
Science, vol. 320, no. 5877. American Association for the Advancement of
Science, pp. 789–792, 2008.
ista: Loose M, Fischer Friedrich E, Ries J, Kruse K, Schwille P. 2008. Spatial regulators
for bacterial cell division self-organize into surface waves in vitro. Science.
320(5877), 789–792.
mla: Loose, Martin, et al. “Spatial Regulators for Bacterial Cell Division Self-Organize
into Surface Waves in Vitro.” Science, vol. 320, no. 5877, American Association
for the Advancement of Science, 2008, pp. 789–92, doi:10.1126/science.1154413.
short: M. Loose, E. Fischer Friedrich, J. Ries, K. Kruse, P. Schwille, Science 320
(2008) 789–792.
date_created: 2018-12-11T11:55:02Z
date_published: 2008-05-09T00:00:00Z
date_updated: 2021-01-12T06:54:30Z
day: '09'
doi: 10.1126/science.1154413
extern: 1
intvolume: ' 320'
issue: '5877'
month: '05'
page: 789 - 792
publication: Science
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '5101'
quality_controlled: 0
status: public
title: Spatial regulators for bacterial cell division self-organize into surface waves
in vitro
type: journal_article
volume: 320
year: '2008'
...