---
_id: '4457'
abstract:
- lang: eng
text: We present a compositional approach to the implementation of hard real-time
software running on a distributed platform. We explain how several code suppliers,
coordinated by a system integrator, can independently generate different parts
of the distributed software. The task structure, interaction, and timing is specified
as a Giotto program. Each supplier is given a part of the Giotto program and a
timing interface, from which the supplier generates task and scheduling code.
The integrator then checks, individually for each supplier, in pseudo-polynomial
time, if the supplied code meets its timing specification. If all checks succeed,
then the supplied software parts are guaranteed to work together and implement
the original Giotto program. The feasibility of the approach is demonstrated by
a prototype implementation.
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: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Kirsch C, Matic S. Composable code generation for distributed
Giotto. In: ACM; 2005:21-30. doi:10.1145/1065910.1065914'
apa: 'Henzinger, T. A., Kirsch, C., & Matic, S. (2005). Composable code generation
for distributed Giotto (pp. 21–30). Presented at the LCTES: Languages, Compilers,
and Tools for Embedded Systems, ACM. https://doi.org/10.1145/1065910.1065914'
chicago: Henzinger, Thomas A, Christoph Kirsch, and Slobodan Matic. “Composable
Code Generation for Distributed Giotto,” 21–30. ACM, 2005. https://doi.org/10.1145/1065910.1065914.
ieee: 'T. A. Henzinger, C. Kirsch, and S. Matic, “Composable code generation for
distributed Giotto,” presented at the LCTES: Languages, Compilers, and Tools for
Embedded Systems, 2005, pp. 21–30.'
ista: 'Henzinger TA, Kirsch C, Matic S. 2005. Composable code generation for distributed
Giotto. LCTES: Languages, Compilers, and Tools for Embedded Systems, 21–30.'
mla: Henzinger, Thomas A., et al. Composable Code Generation for Distributed
Giotto. ACM, 2005, pp. 21–30, doi:10.1145/1065910.1065914.
short: T.A. Henzinger, C. Kirsch, S. Matic, in:, ACM, 2005, pp. 21–30.
conference:
name: 'LCTES: Languages, Compilers, and Tools for Embedded Systems'
date_created: 2018-12-11T12:08:57Z
date_published: 2005-06-01T00:00:00Z
date_updated: 2021-01-12T07:57:06Z
day: '01'
doi: 10.1145/1065910.1065914
extern: 1
month: '06'
page: 21 - 30
publication_status: published
publisher: ACM
publist_id: '275'
quality_controlled: 0
status: public
title: Composable code generation for distributed Giotto
type: conference
year: '2005'
...
---
_id: '4536'
abstract:
- lang: eng
text: 'We show how to automatically construct and refine rectangular abstractions
of systems of linear differential equations. From a hybrid automaton whose dynamics
are given by a system of linear differential equations, our method computes automatically
a sequence of rectangular hybrid automata that are increasingly precise overapproximations
of the original hybrid automaton. We prove an optimality criterion for successive
refinements. We also show that this method can take into account a safety property
to be verified, refining only relevant parts of the state space. The practicability
of the method is illustrated on a benchmark case study. '
acknowledgement: Supported in part by the AFOSR MURI grant F49620-00-1-0327 and the
NSF grants CCR-0208875 and CCR-0225610.
alternative_title:
- LNCS
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. Automatic rectangular refinement of affine
hybrid systems. In: Vol 3829. Springer; 2005:144-161. doi:DOI: 10.1007/11603009_13'
apa: 'Doyen, L., Henzinger, T. A., & Raskin, J. (2005). Automatic rectangular
refinement of affine hybrid systems (Vol. 3829, pp. 144–161). Presented at the
FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. https://doi.org/DOI: 10.1007/11603009_13'
chicago: 'Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Automatic Rectangular
Refinement of Affine Hybrid Systems,” 3829:144–61. Springer, 2005. https://doi.org/DOI: 10.1007/11603009_13.'
ieee: 'L. Doyen, T. A. Henzinger, and J. Raskin, “Automatic rectangular refinement
of affine hybrid systems,” presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, 2005, vol. 3829, pp. 144–161.'
ista: 'Doyen L, Henzinger TA, Raskin J. 2005. Automatic rectangular refinement of
affine hybrid systems. FORMATS: Formal Modeling and Analysis of Timed Systems,
LNCS, vol. 3829, 144–161.'
mla: 'Doyen, Laurent, et al. Automatic Rectangular Refinement of Affine Hybrid
Systems. Vol. 3829, Springer, 2005, pp. 144–61, doi:DOI: 10.1007/11603009_13.'
short: L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2005, pp. 144–161.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2005-12-13T00:00:00Z
date_updated: 2021-01-12T07:59:31Z
day: '13'
doi: 'DOI: 10.1007/11603009_13'
extern: 1
intvolume: ' 3829'
month: '12'
page: 144 - 161
publication_status: published
publisher: Springer
publist_id: '190'
quality_controlled: 0
status: public
title: Automatic rectangular refinement of affine hybrid systems
type: conference
volume: 3829
year: '2005'
...
---
_id: '4541'
abstract:
- lang: eng
text: |
Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete.
We study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Semiperfect-information games. In: Vol 3821. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2005:1-18. doi:10.1007/11590156_1'
apa: 'Chatterjee, K., & Henzinger, T. A. (2005). Semiperfect-information games
(Vol. 3821, pp. 1–18). Presented at the FSTTCS: Foundations of Software Technology
and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.1007/11590156_1'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Semiperfect-Information
Games,” 3821:1–18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2005. https://doi.org/10.1007/11590156_1.
ieee: 'K. Chatterjee and T. A. Henzinger, “Semiperfect-information games,” presented
at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science,
2005, vol. 3821, pp. 1–18.'
ista: 'Chatterjee K, Henzinger TA. 2005. Semiperfect-information games. FSTTCS:
Foundations of Software Technology and Theoretical Computer Science, LNCS, vol.
3821, 1–18.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Semiperfect-Information
Games. Vol. 3821, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2005,
pp. 1–18, doi:10.1007/11590156_1.
short: K. Chatterjee, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2005, pp. 1–18.
conference:
name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
date_created: 2018-12-11T12:09:23Z
date_published: 2005-12-07T00:00:00Z
date_updated: 2021-01-12T07:59:34Z
day: '07'
doi: 10.1007/11590156_1
extern: 1
intvolume: ' 3821'
month: '12'
page: 1 - 18
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '182'
quality_controlled: 0
status: public
title: Semiperfect-information games
type: conference
volume: 3821
year: '2005'
...
---
_id: '4553'
abstract:
- lang: eng
text: 'The theory of graph games with ω-regular winning conditions is the foundation
for modeling and synthesizing reactive processes. In the case of stochastic reactive
processes, the corresponding stochastic graph games have three players, two of
them (System and Environment) behaving adversarially, and the third (Uncertainty)
behaving probabilistically. We consider two problems for stochastic graph games:
the qualitative problem asks for the set of states from which a player can win
with probability 1 (almost-sure winning); the quantitative problem asks for the
maximal probability of winning (optimal winning) from each state. We show that
for Rabin winning conditions, both problems are in NP. As these problems were
known to be NP-hard, it follows that they are NP-complete for Rabin conditions,
and dually, coNP-complete for Streett conditions. The proof proceeds by showing
that pure memoryless strategies suffice for qualitatively and quantitatively winning
stochastic graph games with Rabin conditions. This insight is of interest in its
own right, as it implies that controllers for Rabin objectives have simple implementations.
We also prove that for every ω-regular condition, optimal winning strategies are
no more complex than almost-sure winning strategies.'
acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671,
the AFOSR MURI grant F49620-00-1-0327, and the NSF grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, De Alfaro L, Henzinger TA. The complexity of stochastic Rabin
and Streett games. In: Vol 3580. Springer; 2005:878-890. doi:10.1007/11523468_71'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2005). The complexity
of stochastic Rabin and Streett games (Vol. 3580, pp. 878–890). Presented at the
ICALP: Automata, Languages and Programming, Springer. https://doi.org/10.1007/11523468_71'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “The Complexity
of Stochastic Rabin and Streett Games,” 3580:878–90. Springer, 2005. https://doi.org/10.1007/11523468_71.
ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “The complexity of stochastic
Rabin and Streett games,” presented at the ICALP: Automata, Languages and Programming,
2005, vol. 3580, pp. 878–890.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2005. The complexity of stochastic
Rabin and Streett games. ICALP: Automata, Languages and Programming, LNCS, vol.
3580, 878–890.'
mla: Chatterjee, Krishnendu, et al. The Complexity of Stochastic Rabin and Streett
Games. Vol. 3580, Springer, 2005, pp. 878–90, doi:10.1007/11523468_71.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, Springer, 2005, pp. 878–890.
conference:
name: 'ICALP: Automata, Languages and Programming'
date_created: 2018-12-11T12:09:27Z
date_published: 2005-06-24T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '24'
doi: 10.1007/11523468_71
extern: 1
intvolume: ' 3580'
month: '06'
page: 878 - 890
publication_status: published
publisher: Springer
publist_id: '158'
quality_controlled: 0
status: public
title: The complexity of stochastic Rabin and Streett games
type: conference
volume: 3580
year: '2005'
...
---
_id: '4554'
abstract:
- lang: eng
text: Games played on graphs may have qualitative objectives, such as the satisfaction
of an ω-regular property, or quantitative objectives, such as the optimization
of a real-valued reward. When games are used to model reactive systems with both
fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding
objective combines both a qualitative and a quantitative component. In a general
case of interest, the qualitative component is a parity condition and the quantitative
component is a mean-payoff reward. We study and solve such mean-payoff parity
games. We also prove some interesting facts about mean-payoff parity games which
distinguish them both from mean-payoff and from parity games. In particular, we
show that optimal strategies exist in mean-payoff parity games, but they may require
infinite memory.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
citation:
ama: 'Chatterjee K, Henzinger TA, Jurdziński M. Mean-payoff parity games. In: IEEE;
2005:178-187. doi:10.1109/LICS.2005.26'
apa: 'Chatterjee, K., Henzinger, T. A., & Jurdziński, M. (2005). Mean-payoff
parity games (pp. 178–187). Presented at the LICS: Logic in Computer Science,
IEEE. https://doi.org/10.1109/LICS.2005.26'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Mean-Payoff
Parity Games,” 178–87. IEEE, 2005. https://doi.org/10.1109/LICS.2005.26.
ieee: 'K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Mean-payoff parity games,”
presented at the LICS: Logic in Computer Science, 2005, pp. 178–187.'
ista: 'Chatterjee K, Henzinger TA, Jurdziński M. 2005. Mean-payoff parity games.
LICS: Logic in Computer Science, 178–187.'
mla: Chatterjee, Krishnendu, et al. Mean-Payoff Parity Games. IEEE, 2005,
pp. 178–87, doi:10.1109/LICS.2005.26.
short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, in:, IEEE, 2005, pp. 178–187.
conference:
name: 'LICS: Logic in Computer Science'
date_created: 2018-12-11T12:09:27Z
date_published: 2005-09-19T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '19'
doi: 10.1109/LICS.2005.26
extern: 1
month: '09'
page: 178 - 187
publication_status: published
publisher: IEEE
publist_id: '159'
quality_controlled: 0
status: public
title: Mean-payoff parity games
type: conference
year: '2005'
...
---
_id: '4557'
abstract:
- lang: eng
text: 'Planning in adversarial and uncertain environments can be modeled as the
problem of devising strategies in stochastic perfect information games. These
games are generalizations of Markov decision processes (MDPs): there are two (adversarial)
players, and a source of randomness. The main practical obstacle to computing
winning strategies in such games is the size of the state space. In practice therefore,
one typically works with abstractions of the model. The diffculty is to come up
with an abstraction that is neither too coarse to remove all winning strategies
(plans), nor too fine to be intractable. In verification, the paradigm of counterexample-guided
abstraction refinement has been successful to construct useful but parsimonious
abstractions automatically. We extend this paradigm to probabilistic models (namely,
perfect information games and, as a special case, MDPs). This allows us to apply
the counterexample-guided abstraction paradigm to the AI planning problem. As
special cases, we get planning algorithms for MDPs and deterministic systems that
automatically construct system abstractions.'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Chatterjee K, Henzinger TA, Jhala R, Majumdar R. Counterexample-guided planning.
In: AUAI Press; 2005:104-111.'
apa: 'Chatterjee, K., Henzinger, T. A., Jhala, R., & Majumdar, R. (2005). Counterexample-guided
planning (pp. 104–111). Presented at the UAI: Uncertainty in Artificial Intelligence,
AUAI Press.'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Ranjit Jhala, and Ritankar
Majumdar. “Counterexample-Guided Planning,” 104–11. AUAI Press, 2005.
ieee: 'K. Chatterjee, T. A. Henzinger, R. Jhala, and R. Majumdar, “Counterexample-guided
planning,” presented at the UAI: Uncertainty in Artificial Intelligence, 2005,
pp. 104–111.'
ista: 'Chatterjee K, Henzinger TA, Jhala R, Majumdar R. 2005. Counterexample-guided
planning. UAI: Uncertainty in Artificial Intelligence, 104–111.'
mla: Chatterjee, Krishnendu, et al. Counterexample-Guided Planning. AUAI
Press, 2005, pp. 104–11.
short: K. Chatterjee, T.A. Henzinger, R. Jhala, R. Majumdar, in:, AUAI Press, 2005,
pp. 104–111.
conference:
name: 'UAI: Uncertainty in Artificial Intelligence'
date_created: 2018-12-11T12:09:28Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:41Z
day: '01'
extern: 1
main_file_link:
- open_access: '0'
url: http://uai.sis.pitt.edu/papers/05/p104-chatterjee.pdf
month: '01'
page: 104 - 111
publication_status: published
publisher: AUAI Press
publist_id: '157'
quality_controlled: 0
status: public
title: Counterexample-guided planning
type: conference
year: '2005'
...
---
_id: '4560'
abstract:
- lang: eng
text: |
We define and study a quantitative generalization of the traditional boolean framework of model-based specification and verification. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a system with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values.
Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quantitative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specified by quantitative-bound automata, which are finite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an integer f(K). Along with the linear-time, automaton-based view of quantitative verification, we present a corresponding branching-time view based on a quantitative-bound μ-calculus, and we study the relationship, expressive power, and complexity of both views.
alternative_title:
- LNCS
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. Verifying
quantitative properties using bound functions. In: Vol 3725. Springer; 2005:50-64.
doi:10.1007/11560548_7'
apa: 'Chakrabarti, A., Chatterjee, K., Henzinger, T. A., Kupferman, O., & Majumdar,
R. (2005). Verifying quantitative properties using bound functions (Vol. 3725,
pp. 50–64). Presented at the CHARME: Correct Hardware Design and Verification
Methods, Springer. https://doi.org/10.1007/11560548_7'
chicago: Chakrabarti, Arindam, Krishnendu Chatterjee, Thomas A Henzinger, Orna Kupferman,
and Ritankar Majumdar. “Verifying Quantitative Properties Using Bound Functions,”
3725:50–64. Springer, 2005. https://doi.org/10.1007/11560548_7.
ieee: 'A. Chakrabarti, K. Chatterjee, T. A. Henzinger, O. Kupferman, and R. Majumdar,
“Verifying quantitative properties using bound functions,” presented at the CHARME:
Correct Hardware Design and Verification Methods, 2005, vol. 3725, pp. 50–64.'
ista: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. 2005.
Verifying quantitative properties using bound functions. CHARME: Correct Hardware
Design and Verification Methods, LNCS, vol. 3725, 50–64.'
mla: Chakrabarti, Arindam, et al. Verifying Quantitative Properties Using Bound
Functions. Vol. 3725, Springer, 2005, pp. 50–64, doi:10.1007/11560548_7.
short: A. Chakrabarti, K. Chatterjee, T.A. Henzinger, O. Kupferman, R. Majumdar,
in:, Springer, 2005, pp. 50–64.
conference:
name: 'CHARME: Correct Hardware Design and Verification Methods'
date_created: 2018-12-11T12:09:29Z
date_published: 2005-09-19T00:00:00Z
date_updated: 2021-01-12T07:59:42Z
day: '19'
doi: 10.1007/11560548_7
extern: 1
intvolume: ' 3725'
month: '09'
page: 50 - 64
publication_status: published
publisher: Springer
publist_id: '149'
quality_controlled: 0
status: public
title: Verifying quantitative properties using bound functions
type: conference
volume: 3725
year: '2005'
...
---
_id: '4576'
abstract:
- lang: eng
text: We present a language for specifying web service interfaces. A web service
interface puts three kinds of constraints on the users of the service. First,
the interface specifies the methods that can be called by a client, together with
types of input and output parameters; these are called signature constraints.
Second, the interface may specify propositional constraints on method calls and
output values that may oc- cur in a web service conversation; these are called
consis- tency constraints. Third, the interface may specify temporal constraints
on the ordering of method calls; these are called protocol constraints. The interfaces
can be used to check, first, if two or more web services are compatible, and second,
if a web service A can be safely substituted for a web ser- vice B. The algorithm
for compatibility checking verifies that two or more interfaces fulfill each others’
constraints. The algorithm for substitutivity checking verifies that service A
demands fewer and fulfills more constraints than service B.
acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671
and by the NSF grants CCR-0234690 and CCR-0225610.
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Beyer D, Chakrabarti A, Henzinger TA. Web service interfaces. In: ACM; 2005:148-159.
doi:10.1145/1060745.1060770'
apa: 'Beyer, D., Chakrabarti, A., & Henzinger, T. A. (2005). Web service interfaces
(pp. 148–159). Presented at the WWW: World Wide Web Conference, ACM. https://doi.org/10.1145/1060745.1060770'
chicago: Beyer, Dirk, Arindam Chakrabarti, and Thomas A Henzinger. “Web Service
Interfaces,” 148–59. ACM, 2005. https://doi.org/10.1145/1060745.1060770.
ieee: 'D. Beyer, A. Chakrabarti, and T. A. Henzinger, “Web service interfaces,”
presented at the WWW: World Wide Web Conference, 2005, pp. 148–159.'
ista: 'Beyer D, Chakrabarti A, Henzinger TA. 2005. Web service interfaces. WWW:
World Wide Web Conference, 148–159.'
mla: Beyer, Dirk, et al. Web Service Interfaces. ACM, 2005, pp. 148–59, doi:10.1145/1060745.1060770.
short: D. Beyer, A. Chakrabarti, T.A. Henzinger, in:, ACM, 2005, pp. 148–159.
conference:
name: 'WWW: World Wide Web Conference'
date_created: 2018-12-11T12:09:33Z
date_published: 2005-05-01T00:00:00Z
date_updated: 2021-01-12T07:59:50Z
day: '01'
doi: 10.1145/1060745.1060770
extern: 1
month: '05'
page: 148 - 159
publication_status: published
publisher: ACM
publist_id: '132'
quality_controlled: 0
status: public
title: Web service interfaces
type: conference
year: '2005'
...
---
_id: '4579'
abstract:
- lang: eng
text: BLAST is an automatic verification tool for checking temporal safety properties
of C programs. Given a C program and a temporal safety property, BLAST statically
proves that either the program satisfies the safety property or the program has
an execution trace that exhibits a violation of the property. BLAST constructs,
explores, and refines abstractions of the program state space based on lazy predicate
abstraction and interpolation-based predicate discovery. We show how BLAST can
be used to statically prove memory safety for C programs. We take a two-step approach.
First, we use Ccured, a type-based memory safety analyzer, to annotate with run-time
checks all program points that cannot be proved memory safe by the type system.
Second, we use BLAST to remove as many of the run-time checks as possible (by
proving that these checks never fail), and to generate for the remaining run-time
checks execution traces that witness them fail. Our experience shows that BLAST
can remove many of the run-time checks added by Ccured and provide useful information
to the programmer about many of the remaining checks.
acknowledgement: This research was supported in part by the NSF grants CCR-0234690,
CCR-0225610, and ITR-0326577.
alternative_title:
- LNCS
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: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. Checking memory safety with BLAST.
In: Vol 3442. Springer; 2005:2-18. doi:10.1007/978-3-540-31984-9_2'
apa: 'Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2005). Checking
memory safety with BLAST (Vol. 3442, pp. 2–18). Presented at the FASE: Fundamental
Approaches To Software Engineering, Springer. https://doi.org/10.1007/978-3-540-31984-9_2'
chicago: Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Checking
Memory Safety with BLAST,” 3442:2–18. Springer, 2005. https://doi.org/10.1007/978-3-540-31984-9_2.
ieee: 'D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “Checking memory safety
with BLAST,” presented at the FASE: Fundamental Approaches To Software Engineering,
2005, vol. 3442, pp. 2–18.'
ista: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. 2005. Checking memory safety
with BLAST. FASE: Fundamental Approaches To Software Engineering, LNCS, vol. 3442,
2–18.'
mla: Beyer, Dirk, et al. Checking Memory Safety with BLAST. Vol. 3442, Springer,
2005, pp. 2–18, doi:10.1007/978-3-540-31984-9_2.
short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Springer, 2005, pp.
2–18.
conference:
name: 'FASE: Fundamental Approaches To Software Engineering'
date_created: 2018-12-11T12:09:34Z
date_published: 2005-03-24T00:00:00Z
date_updated: 2021-01-12T07:59:51Z
day: '24'
doi: 10.1007/978-3-540-31984-9_2
extern: 1
intvolume: ' 3442'
month: '03'
page: 2 - 18
publication_status: published
publisher: Springer
publist_id: '131'
quality_controlled: 0
status: public
title: Checking memory safety with BLAST
type: conference
volume: 3442
year: '2005'
...
---
_id: '4624'
abstract:
- lang: eng
text: Surveying results from [5] and [6], we motivate and introduce the theory behind
formalizing rich interfaces for software and hardware components. Rich interfaces
specify the protocol aspects of component interaction. Their formalization, called
interface automata, permits a compiler to check the compatibility of component
interaction protocols. Interface automata 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, while still maintaining compatibility.
alternative_title:
- 'NATO Science Series: Mathematics, Physics, and Chemistry'
author:
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'De Alfaro L, Henzinger TA. Interface-based design. In: Vol 195. Springer;
2005:83-104. doi:10.1007/1-4020-3532-2_3'
apa: De Alfaro, L., & Henzinger, T. A. (2005). Interface-based design (Vol.
195, pp. 83–104). Presented at the Engineering Theories of Software Intensive
Systems, Springer. https://doi.org/10.1007/1-4020-3532-2_3
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Interface-Based Design,” 195:83–104.
Springer, 2005. https://doi.org/10.1007/1-4020-3532-2_3.
ieee: L. De Alfaro and T. A. Henzinger, “Interface-based design,” presented at the
Engineering Theories of Software Intensive Systems, 2005, vol. 195, pp. 83–104.
ista: 'De Alfaro L, Henzinger TA. 2005. Interface-based design. Engineering Theories
of Software Intensive Systems, NATO Science Series: Mathematics, Physics, and
Chemistry, vol. 195, 83–104.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. Interface-Based Design. Vol.
195, Springer, 2005, pp. 83–104, doi:10.1007/1-4020-3532-2_3.
short: L. De Alfaro, T.A. Henzinger, in:, Springer, 2005, pp. 83–104.
conference:
name: Engineering Theories of Software Intensive Systems
date_created: 2018-12-11T12:09:49Z
date_published: 2005-07-15T00:00:00Z
date_updated: 2021-01-12T08:00:36Z
day: '15'
doi: 10.1007/1-4020-3532-2_3
extern: 1
intvolume: ' 195'
month: '07'
page: 83 - 104
publication_status: published
publisher: Springer
publist_id: '85'
quality_controlled: 0
status: public
title: Interface-based design
type: conference
volume: 195
year: '2005'
...
---
_id: '4625'
abstract:
- lang: eng
text: |-
Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators ⋄ and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path.
We interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics.
author:
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Marco
full_name: Faella, Marco
last_name: Faella
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Model checking
discounted temporal properties. Theoretical Computer Science. 2005;345(1):139-170.
doi:10.1016/j.tcs.2005.07.033
apa: De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., & Stoelinga,
M. (2005). Model checking discounted temporal properties. Theoretical Computer
Science. Elsevier. https://doi.org/10.1016/j.tcs.2005.07.033
chicago: De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and
Mariëlle Stoelinga. “Model Checking Discounted Temporal Properties.” Theoretical
Computer Science. Elsevier, 2005. https://doi.org/10.1016/j.tcs.2005.07.033.
ieee: L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “Model
checking discounted temporal properties,” Theoretical Computer Science,
vol. 345, no. 1. Elsevier, pp. 139–170, 2005.
ista: De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2005. Model
checking discounted temporal properties. Theoretical Computer Science. 345(1),
139–170.
mla: De Alfaro, Luca, et al. “Model Checking Discounted Temporal Properties.” Theoretical
Computer Science, vol. 345, no. 1, Elsevier, 2005, pp. 139–70, doi:10.1016/j.tcs.2005.07.033.
short: L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, Theoretical
Computer Science 345 (2005) 139–170.
date_created: 2018-12-11T12:09:49Z
date_published: 2005-11-21T00:00:00Z
date_updated: 2021-01-12T08:00:37Z
day: '21'
doi: 10.1016/j.tcs.2005.07.033
extern: 1
intvolume: ' 345'
issue: '1'
month: '11'
page: 139 - 170
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '80'
quality_controlled: 0
status: public
title: Model checking discounted temporal properties
type: journal_article
volume: 345
year: '2005'
...
---
_id: '12203'
abstract:
- lang: eng
text: 'Geranylgeranyl diphosphate synthase (GGPPS, EC: 2.5.1.29) catalyzes the biosynthesis
of geranylgeranyl diphosphate (GGPP), which is a key precursor for ginkgolide
biosynthesis. Here we reported for the first time the cloning of a new full-length
cDNA encoding GGPPS from the living fossil plant Ginkgo biloba. The full-length
cDNA encoding G. biloba GGPPS (designated as GbGGPPS) was 1657bp long and contained
a 1176bp open reading frame encoding a 391 amino acid protein. Comparative analysis
showed that GbGGPPS possessed a 79 amino acid transit peptide at its N-terminal,
which directed GbGGPPS to target to the plastids. Bioinformatic analysis revealed
that GbGGPPS was a member of polyprenyltransferases with two highly conserved
aspartate-rich motifs like other plant GGPPSs. Phylogenetic tree analysis indicated
that plant GGPPSs could be classified into two groups, angiosperm and gymnosperm
GGPPSs, while GbGGPPS had closer relationship with gymnosperm plant GGPPSs.'
acknowledgement: This study was financially supported by China National High-Tech
“863” Program. The authors are very thankful to Dr Li Wang (School of Life Sciences,
Fudan University, Shanghai, China) for her kind help with constructing the phylogenetic
tree.
article_processing_charge: No
article_type: original
author:
- first_name: Zhihua
full_name: Liao, Zhihua
last_name: Liao
- first_name: Min
full_name: Chen, Min
last_name: Chen
- first_name: Yifu
full_name: Gong, Yifu
last_name: Gong
- first_name: Liang
full_name: Guo, Liang
last_name: Guo
- first_name: Qiumin
full_name: Tan, Qiumin
last_name: Tan
- first_name: Xiaoqi
full_name: Feng, Xiaoqi
id: e0164712-22ee-11ed-b12a-d80fcdf35958
last_name: Feng
orcid: 0000-0002-4008-1234
- first_name: Xiaofen
full_name: Sun, Xiaofen
last_name: Sun
- first_name: Feng
full_name: Tan, Feng
last_name: Tan
- first_name: Kexuan
full_name: Tang, Kexuan
last_name: Tang
citation:
ama: Liao Z, Chen M, Gong Y, et al. A new geranylgeranyl Diphosphate synthase gene
from Ginkgo biloba, which intermediates the biosynthesis of the key precursor
for ginkgolides. DNA Sequence. 2004;15(2):153-158. doi:10.1080/10425170410001667348
apa: Liao, Z., Chen, M., Gong, Y., Guo, L., Tan, Q., Feng, X., … Tang, K. (2004).
A new geranylgeranyl Diphosphate synthase gene from Ginkgo biloba, which intermediates
the biosynthesis of the key precursor for ginkgolides. DNA Sequence. Informa
UK Limited. https://doi.org/10.1080/10425170410001667348
chicago: Liao, Zhihua, Min Chen, Yifu Gong, Liang Guo, Qiumin Tan, Xiaoqi Feng,
Xiaofen Sun, Feng Tan, and Kexuan Tang. “A New Geranylgeranyl Diphosphate Synthase
Gene from Ginkgo Biloba, Which Intermediates the Biosynthesis of the Key Precursor
for Ginkgolides.” DNA Sequence. Informa UK Limited, 2004. https://doi.org/10.1080/10425170410001667348.
ieee: Z. Liao et al., “A new geranylgeranyl Diphosphate synthase gene from
Ginkgo biloba, which intermediates the biosynthesis of the key precursor for ginkgolides,”
DNA Sequence, vol. 15, no. 2. Informa UK Limited, pp. 153–158, 2004.
ista: Liao Z, Chen M, Gong Y, Guo L, Tan Q, Feng X, Sun X, Tan F, Tang K. 2004.
A new geranylgeranyl Diphosphate synthase gene from Ginkgo biloba, which intermediates
the biosynthesis of the key precursor for ginkgolides. DNA Sequence. 15(2), 153–158.
mla: Liao, Zhihua, et al. “A New Geranylgeranyl Diphosphate Synthase Gene from Ginkgo
Biloba, Which Intermediates the Biosynthesis of the Key Precursor for Ginkgolides.”
DNA Sequence, vol. 15, no. 2, Informa UK Limited, 2004, pp. 153–58, doi:10.1080/10425170410001667348.
short: Z. Liao, M. Chen, Y. Gong, L. Guo, Q. Tan, X. Feng, X. Sun, F. Tan, K. Tang,
DNA Sequence 15 (2004) 153–158.
date_created: 2023-01-16T09:24:50Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2023-05-08T10:58:29Z
department:
- _id: XiFe
doi: 10.1080/10425170410001667348
extern: '1'
external_id:
pmid:
- '15352294'
intvolume: ' 15'
issue: '2'
keyword:
- Endocrinology
- Genetics
- Molecular Biology
- Biochemistry
language:
- iso: eng
oa_version: None
page: 153-158
pmid: 1
publication: DNA Sequence
publication_identifier:
issn:
- 1042-5179
publication_status: published
publisher: Informa UK Limited
quality_controlled: '1'
scopus_import: '1'
status: public
title: A new geranylgeranyl Diphosphate synthase gene from Ginkgo biloba, which intermediates
the biosynthesis of the key precursor for ginkgolides
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2004'
...
---
_id: '12658'
abstract:
- lang: eng
text: '[1] During the ablation period 2001 a glaciometeorological experiment was
carried out on Haut Glacier d''Arolla, Switzerland. Five meteorological stations
were installed on the glacier, and one permanent automatic weather station in
the glacier foreland. The altitudes of the stations ranged between 2500 and 3000
m a.s.l., and they were in operation from end of May to beginning of September
2001. The spatial arrangement of the stations and temporal duration of the measurements
generated a unique data set enabling the analysis of the spatial and temporal
variability of the meteorological variables across an alpine glacier. All measurements
were taken at a nominal height of 2 m, and hourly averages were derived for the
analysis. The wind regime was dominated by the glacier wind (mean value 2.8 m
s−1) but due to erosion by the synoptic gradient wind, occasionally the wind would
blow up the valley. A slight decrease in mean 2 m air temperatures with altitude
was found, however the 2 m air temperature gradient varied greatly and frequently
changed its sign. Mean relative humidity was 71% and exhibited limited spatial
variation. Mean incoming shortwave radiation and albedo both generally increased
with elevation. The different components of shortwave radiation are quantified
with a parameterization scheme. Resulting spatial variations are mainly due to
horizon obstruction and reflections from surrounding slopes, i.e., topography.
The effect of clouds accounts for a loss of 30% of the extraterrestrial flux.
Albedos derived from a Landsat TM image of 30 July show remarkably constant values,
in the range 0.49 to 0.50, across snow covered parts of the glacier, while albedo
is highly spatially variable below the zone of continuous snow cover. These results
are verified with ground measurements and compared with parameterized albedo.
Mean longwave radiative fluxes decreased with elevation due to lower air temperatures
and the effect of upper hemisphere slopes. It is shown through parameterization
that this effect would even be more pronounced without the effect of clouds. Results
are discussed with respect to a similar study which has been carried out on Pasterze
Glacier (Austria). The presented algorithms for interpolating, parameterizing
and simulating variables and parameters in alpine regions are integrated in the
software package AMUNDSEN which is freely available to be adapted and further
developed by the community.'
article_number: D03103
article_processing_charge: No
article_type: original
author:
- first_name: Ulrich
full_name: Strasser, Ulrich
last_name: Strasser
- first_name: Javier
full_name: Corripio, Javier
last_name: Corripio
- first_name: Francesca
full_name: Pellicciotti, Francesca
id: b28f055a-81ea-11ed-b70c-a9fe7f7b0e70
last_name: Pellicciotti
- first_name: Paolo
full_name: Burlando, Paolo
last_name: Burlando
- first_name: Ben
full_name: Brock, Ben
last_name: Brock
- first_name: Martin
full_name: Funk, Martin
last_name: Funk
citation:
ama: 'Strasser U, Corripio J, Pellicciotti F, Burlando P, Brock B, Funk M. Spatial
and temporal variability of meteorological variables at Haut Glacier d’Arolla
(Switzerland) during the ablation season 2001: Measurements and simulations. Journal
of Geophysical Research: Atmospheres. 2004;109(D3). doi:10.1029/2003jd003973'
apa: 'Strasser, U., Corripio, J., Pellicciotti, F., Burlando, P., Brock, B., &
Funk, M. (2004). Spatial and temporal variability of meteorological variables
at Haut Glacier d’Arolla (Switzerland) during the ablation season 2001: Measurements
and simulations. Journal of Geophysical Research: Atmospheres. American
Geophysical Union. https://doi.org/10.1029/2003jd003973'
chicago: 'Strasser, Ulrich, Javier Corripio, Francesca Pellicciotti, Paolo Burlando,
Ben Brock, and Martin Funk. “Spatial and Temporal Variability of Meteorological
Variables at Haut Glacier d’Arolla (Switzerland) during the Ablation Season 2001:
Measurements and Simulations.” Journal of Geophysical Research: Atmospheres.
American Geophysical Union, 2004. https://doi.org/10.1029/2003jd003973.'
ieee: 'U. Strasser, J. Corripio, F. Pellicciotti, P. Burlando, B. Brock, and M.
Funk, “Spatial and temporal variability of meteorological variables at Haut Glacier
d’Arolla (Switzerland) during the ablation season 2001: Measurements and simulations,”
Journal of Geophysical Research: Atmospheres, vol. 109, no. D3. American
Geophysical Union, 2004.'
ista: 'Strasser U, Corripio J, Pellicciotti F, Burlando P, Brock B, Funk M. 2004.
Spatial and temporal variability of meteorological variables at Haut Glacier d’Arolla
(Switzerland) during the ablation season 2001: Measurements and simulations. Journal
of Geophysical Research: Atmospheres. 109(D3), D03103.'
mla: 'Strasser, Ulrich, et al. “Spatial and Temporal Variability of Meteorological
Variables at Haut Glacier d’Arolla (Switzerland) during the Ablation Season 2001:
Measurements and Simulations.” Journal of Geophysical Research: Atmospheres,
vol. 109, no. D3, D03103, American Geophysical Union, 2004, doi:10.1029/2003jd003973.'
short: 'U. Strasser, J. Corripio, F. Pellicciotti, P. Burlando, B. Brock, M. Funk,
Journal of Geophysical Research: Atmospheres 109 (2004).'
date_created: 2023-02-20T08:18:57Z
date_published: 2004-02-16T00:00:00Z
date_updated: 2023-02-20T08:40:21Z
day: '16'
doi: 10.1029/2003jd003973
extern: '1'
intvolume: ' 109'
issue: D3
keyword:
- Paleontology
- Space and Planetary Science
- Earth and Planetary Sciences (miscellaneous)
- Atmospheric Science
- Earth-Surface Processes
- Geochemistry and Petrology
- Soil Science
- Water Science and Technology
- Ecology
- Aquatic Science
- Forestry
- Oceanography
- Geophysics
language:
- iso: eng
month: '02'
oa_version: None
publication: 'Journal of Geophysical Research: Atmospheres'
publication_identifier:
issn:
- 0148-0227
publication_status: published
publisher: American Geophysical Union
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Spatial and temporal variability of meteorological variables at Haut Glacier
d''Arolla (Switzerland) during the ablation season 2001: Measurements and simulations'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 109
year: '2004'
...
---
_id: '8517'
abstract:
- lang: eng
text: We consider the evolution of a connected set on the plane carried by a space
periodic incompressible stochastic flow. While for almost every realization of
the stochastic flow at time t most of the particles are at a distance of order
equation image away from the origin, there is a measure zero set of points that
escape to infinity at the linear rate. We study the set of points visited by the
original set by time t and show that such a set, when scaled down by the factor
of t, has a limiting nonrandom shape.
article_processing_charge: No
article_type: original
author:
- first_name: Dmitry
full_name: Dolgopyat, Dmitry
last_name: Dolgopyat
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
- first_name: Leonid
full_name: Koralov, Leonid
last_name: Koralov
citation:
ama: Dolgopyat D, Kaloshin V, Koralov L. A limit shape theorem for periodic stochastic
dispersion. Communications on Pure and Applied Mathematics. 2004;57(9):1127-1158.
doi:10.1002/cpa.20032
apa: Dolgopyat, D., Kaloshin, V., & Koralov, L. (2004). A limit shape theorem
for periodic stochastic dispersion. Communications on Pure and Applied Mathematics.
Wiley. https://doi.org/10.1002/cpa.20032
chicago: Dolgopyat, Dmitry, Vadim Kaloshin, and Leonid Koralov. “A Limit Shape Theorem
for Periodic Stochastic Dispersion.” Communications on Pure and Applied Mathematics.
Wiley, 2004. https://doi.org/10.1002/cpa.20032.
ieee: D. Dolgopyat, V. Kaloshin, and L. Koralov, “A limit shape theorem for periodic
stochastic dispersion,” Communications on Pure and Applied Mathematics,
vol. 57, no. 9. Wiley, pp. 1127–1158, 2004.
ista: Dolgopyat D, Kaloshin V, Koralov L. 2004. A limit shape theorem for periodic
stochastic dispersion. Communications on Pure and Applied Mathematics. 57(9),
1127–1158.
mla: Dolgopyat, Dmitry, et al. “A Limit Shape Theorem for Periodic Stochastic Dispersion.”
Communications on Pure and Applied Mathematics, vol. 57, no. 9, Wiley,
2004, pp. 1127–58, doi:10.1002/cpa.20032.
short: D. Dolgopyat, V. Kaloshin, L. Koralov, Communications on Pure and Applied
Mathematics 57 (2004) 1127–1158.
date_created: 2020-09-18T10:49:12Z
date_published: 2004-09-01T00:00:00Z
date_updated: 2021-01-12T08:19:50Z
day: '01'
doi: 10.1002/cpa.20032
extern: '1'
intvolume: ' 57'
issue: '9'
keyword:
- Applied Mathematics
- General Mathematics
language:
- iso: eng
month: '09'
oa_version: None
page: 1127-1158
publication: Communications on Pure and Applied Mathematics
publication_identifier:
issn:
- 0010-3640
- 1097-0312
publication_status: published
publisher: Wiley
quality_controlled: '1'
status: public
title: A limit shape theorem for periodic stochastic dispersion
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 57
year: '2004'
...
---
_id: '8518'
article_processing_charge: No
article_type: original
author:
- first_name: Leonid
full_name: Koralov, Leonid
last_name: Koralov
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
- first_name: Dmitry
full_name: Dolgopyat, Dmitry
last_name: Dolgopyat
citation:
ama: Koralov L, Kaloshin V, Dolgopyat D. Sample path properties of the stochastic
flows. The Annals of Probability. 2004;32(1A):1-27. doi:10.1214/aop/1078415827
apa: Koralov, L., Kaloshin, V., & Dolgopyat, D. (2004). Sample path properties
of the stochastic flows. The Annals of Probability. Institute of Mathematical
Statistics. https://doi.org/10.1214/aop/1078415827
chicago: Koralov, Leonid, Vadim Kaloshin, and Dmitry Dolgopyat. “Sample Path Properties
of the Stochastic Flows.” The Annals of Probability. Institute of Mathematical
Statistics, 2004. https://doi.org/10.1214/aop/1078415827.
ieee: L. Koralov, V. Kaloshin, and D. Dolgopyat, “Sample path properties of the
stochastic flows,” The Annals of Probability, vol. 32, no. 1A. Institute
of Mathematical Statistics, pp. 1–27, 2004.
ista: Koralov L, Kaloshin V, Dolgopyat D. 2004. Sample path properties of the stochastic
flows. The Annals of Probability. 32(1A), 1–27.
mla: Koralov, Leonid, et al. “Sample Path Properties of the Stochastic Flows.” The
Annals of Probability, vol. 32, no. 1A, Institute of Mathematical Statistics,
2004, pp. 1–27, doi:10.1214/aop/1078415827.
short: L. Koralov, V. Kaloshin, D. Dolgopyat, The Annals of Probability 32 (2004)
1–27.
date_created: 2020-09-18T10:49:19Z
date_published: 2004-03-04T00:00:00Z
date_updated: 2021-01-12T08:19:50Z
day: '04'
doi: 10.1214/aop/1078415827
extern: '1'
intvolume: ' 32'
issue: 1A
language:
- iso: eng
month: '03'
oa_version: None
page: 1-27
publication: The Annals of Probability
publication_identifier:
issn:
- 0091-1798
publication_status: published
publisher: Institute of Mathematical Statistics
quality_controlled: '1'
status: public
title: Sample path properties of the stochastic flows
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 32
year: '2004'
...
---
_id: '864'
abstract:
- lang: eng
text: 'We present a method for prediction of functional sites in a set of aligned
protein sequences. The method selects sites which are both well conserved and
clustered together in space, as inferred from the 3D structures of proteins included
in the alignment. We tested the method using 86 alignments from the NCBI CDD database,
where the sites of experimentally determined ligand and/or macromolecular interactions
are annotated. In agreement with earlier investigations, we found that functional
site predictions are most successful when overall background sequence conservation
is low, such that sites under evolutionary constraint become apparent. In addition,
we found that averaging of conservation values across spatially clustered sites
improves predictions under certain conditions: that is, when overall conservation
is relatively high and when the site in question involves a large macromolecular
binding interface. Under these conditions it is better to look for clusters of
conserved sites than to look for particular conserved sites.'
acknowledgement: We thank John Spouge, Ben Shoemaker, and Michael Galperin forhelpful
suggestions, and the NIH Intramural Research Program forsupport.
author:
- first_name: Anna
full_name: Panchenko, Anna R
last_name: Panchenko
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Stephen
full_name: Bryant, Stephen H
last_name: Bryant
citation:
ama: Panchenko A, Kondrashov F, Bryant S. Prediction of functional sites by analysis
of sequence and structure conservation. Protein Science. 2004;13(4):884-892.
doi:10.1110/ps.03465504
apa: Panchenko, A., Kondrashov, F., & Bryant, S. (2004). Prediction of functional
sites by analysis of sequence and structure conservation. Protein Science.
Wiley-Blackwell. https://doi.org/10.1110/ps.03465504
chicago: Panchenko, Anna, Fyodor Kondrashov, and Stephen Bryant. “Prediction of
Functional Sites by Analysis of Sequence and Structure Conservation.” Protein
Science. Wiley-Blackwell, 2004. https://doi.org/10.1110/ps.03465504.
ieee: A. Panchenko, F. Kondrashov, and S. Bryant, “Prediction of functional sites
by analysis of sequence and structure conservation,” Protein Science, vol.
13, no. 4. Wiley-Blackwell, pp. 884–892, 2004.
ista: Panchenko A, Kondrashov F, Bryant S. 2004. Prediction of functional sites
by analysis of sequence and structure conservation. Protein Science. 13(4), 884–892.
mla: Panchenko, Anna, et al. “Prediction of Functional Sites by Analysis of Sequence
and Structure Conservation.” Protein Science, vol. 13, no. 4, Wiley-Blackwell,
2004, pp. 884–92, doi:10.1110/ps.03465504.
short: A. Panchenko, F. Kondrashov, S. Bryant, Protein Science 13 (2004) 884–892.
date_created: 2018-12-11T11:48:55Z
date_published: 2004-04-01T00:00:00Z
date_updated: 2021-01-12T08:20:22Z
day: '01'
doi: 10.1110/ps.03465504
extern: 1
intvolume: ' 13'
issue: '4'
month: '04'
page: 884 - 892
publication: Protein Science
publication_status: published
publisher: Wiley-Blackwell
publist_id: '6786'
quality_controlled: 0
status: public
title: Prediction of functional sites by analysis of sequence and structure conservation
type: journal_article
volume: 13
year: '2004'
...
---
_id: '870'
abstract:
- lang: eng
text: Only a fraction of eukaryotic genes affect the phenotype drastically. We compared
18 parameters in 1273 human morbid genes, known to cause diseases, and in the
remaining 16 580 unambiguous human genes. Morbid genes evolve more slowly, have
wider phylogenetic distributions, are more similar to essential genes of Drosophila
melanogaster, code for longer proteins containing more alanine and glycine and
less histidine, lysine and methionine, possess larger numbers of longer introns
with more accurate splicing signals and have higher and broader expressions. These
differences make it possible to classify as non-morbid 34% of human genes with
unknown morbidity, when only 5% of known morbid genes are incorrectly classified
as non-morbid. This classification can help to identify disease-causing genes
among multiple candidates.
author:
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Aleksey
full_name: Ogurtsov, Aleksey Yu
last_name: Ogurtsov
- first_name: Alexey
full_name: Kondrashov, Alexey S
last_name: Kondrashov
citation:
ama: Kondrashov F, Ogurtsov A, Kondrashov A. Bioinformatical assay of human gene
morbidity. Nucleic Acids Research. 2004;32(5):1731-1737. doi:10.1093/nar/gkh330
apa: Kondrashov, F., Ogurtsov, A., & Kondrashov, A. (2004). Bioinformatical
assay of human gene morbidity. Nucleic Acids Research. Oxford University
Press. https://doi.org/10.1093/nar/gkh330
chicago: Kondrashov, Fyodor, Aleksey Ogurtsov, and Alexey Kondrashov. “Bioinformatical
Assay of Human Gene Morbidity.” Nucleic Acids Research. Oxford University
Press, 2004. https://doi.org/10.1093/nar/gkh330.
ieee: F. Kondrashov, A. Ogurtsov, and A. Kondrashov, “Bioinformatical assay of human
gene morbidity,” Nucleic Acids Research, vol. 32, no. 5. Oxford University
Press, pp. 1731–1737, 2004.
ista: Kondrashov F, Ogurtsov A, Kondrashov A. 2004. Bioinformatical assay of human
gene morbidity. Nucleic Acids Research. 32(5), 1731–1737.
mla: Kondrashov, Fyodor, et al. “Bioinformatical Assay of Human Gene Morbidity.”
Nucleic Acids Research, vol. 32, no. 5, Oxford University Press, 2004,
pp. 1731–37, doi:10.1093/nar/gkh330.
short: F. Kondrashov, A. Ogurtsov, A. Kondrashov, Nucleic Acids Research 32 (2004)
1731–1737.
date_created: 2018-12-11T11:48:56Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T08:20:37Z
day: '01'
doi: 10.1093/nar/gkh330
extern: 1
intvolume: ' 32'
issue: '5'
month: '01'
page: 1731 - 1737
publication: Nucleic Acids Research
publication_status: published
publisher: Oxford University Press
publist_id: '6780'
quality_controlled: 0
status: public
title: Bioinformatical assay of human gene morbidity
type: journal_article
volume: 32
year: '2004'
...
---
_id: '875'
abstract:
- lang: eng
text: The dominance of wild-type alleles and the concomitant recessivity of deleterious
mutant alleles might have evolved by natural selection or could be a by-product
of the molecular and physiological mechanisms of gene action. We compared the
properties of human haplosufficient genes, whose wild-type alleles are dominant
over loss-of-function alleles, with haploinsufficient (recessive wild-type) genes,
which produce an abnormal phenotype when heterozygous for a loss-of-function allele.
The fraction of haplosufficient genes is the highest among the genes that encode
enzymes, which is best compatible with the physiological theory. Haploinsufficient
genes, on average, have more paralogs than haplosufficient genes, supporting the
idea that gene dosage could be important for the initial fixation of duplications.
Thus, haplo(in)sufficiency of a gene and its propensity for duplication might
have a common evolutionary basis.
author:
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Eugene
full_name: Koonin, Eugene V
last_name: Koonin
citation:
ama: Kondrashov F, Koonin E. A common framework for understanding the origin of
genetic dominance and evolutionary fates of gene duplications. Trends in Genetics.
2004;20(7):287-291. doi:10.1016/j.tig.2004.05.001
apa: Kondrashov, F., & Koonin, E. (2004). A common framework for understanding
the origin of genetic dominance and evolutionary fates of gene duplications. Trends
in Genetics. Elsevier. https://doi.org/10.1016/j.tig.2004.05.001
chicago: Kondrashov, Fyodor, and Eugene Koonin. “A Common Framework for Understanding
the Origin of Genetic Dominance and Evolutionary Fates of Gene Duplications.”
Trends in Genetics. Elsevier, 2004. https://doi.org/10.1016/j.tig.2004.05.001.
ieee: F. Kondrashov and E. Koonin, “A common framework for understanding the origin
of genetic dominance and evolutionary fates of gene duplications,” Trends in
Genetics, vol. 20, no. 7. Elsevier, pp. 287–291, 2004.
ista: Kondrashov F, Koonin E. 2004. A common framework for understanding the origin
of genetic dominance and evolutionary fates of gene duplications. Trends in Genetics.
20(7), 287–291.
mla: Kondrashov, Fyodor, and Eugene Koonin. “A Common Framework for Understanding
the Origin of Genetic Dominance and Evolutionary Fates of Gene Duplications.”
Trends in Genetics, vol. 20, no. 7, Elsevier, 2004, pp. 287–91, doi:10.1016/j.tig.2004.05.001.
short: F. Kondrashov, E. Koonin, Trends in Genetics 20 (2004) 287–291.
date_created: 2018-12-11T11:48:58Z
date_published: 2004-07-01T00:00:00Z
date_updated: 2021-01-12T08:20:54Z
day: '01'
doi: 10.1016/j.tig.2004.05.001
extern: 1
intvolume: ' 20'
issue: '7'
month: '07'
page: 287 - 291
publication: Trends in Genetics
publication_status: published
publisher: Elsevier
publist_id: '6775'
quality_controlled: 0
status: public
title: A common framework for understanding the origin of genetic dominance and evolutionary
fates of gene duplications
type: journal_article
volume: 20
year: '2004'
...
---
_id: '889'
abstract:
- lang: eng
text: 'The function of protein and RNA molecules depends on complex epistatic interactions
between sites. Therefore, the deleterious effect of a mutation can be suppressed
by a compensatory second-site substitution. In relating a list of 86 pathogenic
mutations in human IRNAs encoded by mitochondrial genes to the sequences of their
mammalian orthologs, we noted that 52 pathogenic mutations were present in normal
tRNAs of one or several nonhuman mammals. We found at least five mechanisms of
compensation for 32 pathogenic mutations that destroyed a Watson-Crick pair in
one of the four tRNA stems: restoration of the affected Watson-Crick interaction
(25 cases), strengthening of another pair (4 cases), creation of a new pair (8
cases), changes of multiple interactions in the affected stem (11 cases) and changes
involving the interaction between the loop and stem structures (3 cases). A pathogenic
mutation and its compensating substitution are fixed in a lineage in rapid succession,
and often a compensatory interaction evolves convergently in different clades.
At least 10%, and perhaps as many as 50%, of all nucleotide substitutions in evolving
mammalian (RNAs participate in such interactions, indicating that the evolution
of tRNAs proceeds along highly epistatic fitness ridges.'
acknowledgement: We thank J. Gillespie, M. Hahn, L. Horth, A. Kondrashov, A. Kopp,
S. Nuzhdin, M. Turelli and D. Weinreich for their contributions. The authors were
supported by a grant from the US National Institutes of Health to S. Nuzhdin, and
A.D.K. is a Howard Hughes
author:
- first_name: Andrew
full_name: Kern, Andrew D
last_name: Kern
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
citation:
ama: Kern A, Kondrashov F. Mechanisms and convergence of compensatory evolution
in mammalian mitochondrial tRNAs. Nature Genetics. 2004;36(11):1207-1212.
doi:10.1038/ng1451
apa: Kern, A., & Kondrashov, F. (2004). Mechanisms and convergence of compensatory
evolution in mammalian mitochondrial tRNAs. Nature Genetics. Nature Publishing
Group. https://doi.org/10.1038/ng1451
chicago: Kern, Andrew, and Fyodor Kondrashov. “Mechanisms and Convergence of Compensatory
Evolution in Mammalian Mitochondrial TRNAs.” Nature Genetics. Nature Publishing
Group, 2004. https://doi.org/10.1038/ng1451.
ieee: A. Kern and F. Kondrashov, “Mechanisms and convergence of compensatory evolution
in mammalian mitochondrial tRNAs,” Nature Genetics, vol. 36, no. 11. Nature
Publishing Group, pp. 1207–1212, 2004.
ista: Kern A, Kondrashov F. 2004. Mechanisms and convergence of compensatory evolution
in mammalian mitochondrial tRNAs. Nature Genetics. 36(11), 1207–1212.
mla: Kern, Andrew, and Fyodor Kondrashov. “Mechanisms and Convergence of Compensatory
Evolution in Mammalian Mitochondrial TRNAs.” Nature Genetics, vol. 36,
no. 11, Nature Publishing Group, 2004, pp. 1207–12, doi:10.1038/ng1451.
short: A. Kern, F. Kondrashov, Nature Genetics 36 (2004) 1207–1212.
date_created: 2018-12-11T11:49:02Z
date_published: 2004-11-01T00:00:00Z
date_updated: 2021-01-12T08:21:17Z
day: '01'
doi: 10.1038/ng1451
extern: 1
intvolume: ' 36'
issue: '11'
month: '11'
page: 1207 - 1212
publication: Nature Genetics
publication_status: published
publisher: Nature Publishing Group
publist_id: '6759'
quality_controlled: 0
status: public
title: Mechanisms and convergence of compensatory evolution in mammalian mitochondrial
tRNAs
type: journal_article
volume: 36
year: '2004'
...
---
_id: '898'
abstract:
- lang: eng
text: New alleles become fixed owing to random drift of nearly neutral mutations
or to positive selection of substantially advantageous mutations. After decades
of debate, the fraction of fixations driven by selection remains uncertain. Within
9,390 genes, we analysed 28,196 codons at which rat and mouse differ from each
other at two nucleotide sites and 1,982 codons with three differences. At codons
where rat-mouse divergence involved two non-synonymous substitutions, both of
them occurred in the same lineage, either rat or mouse, in 64% of cases; however,
independent substitutions would occur in the same lineage with a probability of
only 50%. All three non-synonymous substitutions occurred in the same lineage
for 46% of codons, instead of the 25% expected. Furthermore, comparison of 12
pairs of prokaryotic genomes also shows clumping of multiple non-synonymous substitutions
in the same lineage. This pattern cannot be explained by correlated mutation or
episodes of relaxed negative selection, but instead indicates that positive selection
acts at many sites of rapid, successive amino acid replacement.
acknowledgement: We thank N. Bierne for a number of suggestions. G.A.B. was supported
by a BWF graduate fellowship. S.S. was supported by Genome Canada Foundation.
author:
- first_name: Georgii
full_name: Bazykin, Georgii A
last_name: Bazykin
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Aleksey
full_name: Ogurtsov, Aleksey Yu
last_name: Ogurtsov
- first_name: Shamil
full_name: Sunyaev, Shamil R
last_name: Sunyaev
- first_name: Alexey
full_name: Kondrashov, Alexey S
last_name: Kondrashov
citation:
ama: Bazykin G, Kondrashov F, Ogurtsov A, Sunyaev S, Kondrashov A. Positive selection
at sites of multiple amino acid replacements since rat-mouse divergence. Nature.
2004;429(6991):558-562. doi:10.1038/nature02601
apa: Bazykin, G., Kondrashov, F., Ogurtsov, A., Sunyaev, S., & Kondrashov, A.
(2004). Positive selection at sites of multiple amino acid replacements since
rat-mouse divergence. Nature. Nature Publishing Group. https://doi.org/10.1038/nature02601
chicago: Bazykin, Georgii, Fyodor Kondrashov, Aleksey Ogurtsov, Shamil Sunyaev,
and Alexey Kondrashov. “Positive Selection at Sites of Multiple Amino Acid Replacements
since Rat-Mouse Divergence.” Nature. Nature Publishing Group, 2004. https://doi.org/10.1038/nature02601.
ieee: G. Bazykin, F. Kondrashov, A. Ogurtsov, S. Sunyaev, and A. Kondrashov, “Positive
selection at sites of multiple amino acid replacements since rat-mouse divergence,”
Nature, vol. 429, no. 6991. Nature Publishing Group, pp. 558–562, 2004.
ista: Bazykin G, Kondrashov F, Ogurtsov A, Sunyaev S, Kondrashov A. 2004. Positive
selection at sites of multiple amino acid replacements since rat-mouse divergence.
Nature. 429(6991), 558–562.
mla: Bazykin, Georgii, et al. “Positive Selection at Sites of Multiple Amino Acid
Replacements since Rat-Mouse Divergence.” Nature, vol. 429, no. 6991, Nature
Publishing Group, 2004, pp. 558–62, doi:10.1038/nature02601.
short: G. Bazykin, F. Kondrashov, A. Ogurtsov, S. Sunyaev, A. Kondrashov, Nature
429 (2004) 558–562.
date_created: 2018-12-11T11:49:05Z
date_published: 2004-06-03T00:00:00Z
date_updated: 2021-01-12T08:21:37Z
day: '03'
doi: 10.1038/nature02601
extern: 1
intvolume: ' 429'
issue: '6991'
month: '06'
page: 558 - 562
publication: Nature
publication_status: published
publisher: Nature Publishing Group
publist_id: '6746'
quality_controlled: 0
status: public
title: Positive selection at sites of multiple amino acid replacements since rat-mouse
divergence
type: journal_article
volume: 429
year: '2004'
...