---
_id: '6158'
abstract:
- lang: eng
text: Wild isolates of Caenorhabditis elegans can feed either alone or in groups1,2.
This natural variation in behaviour is associated with a single residue difference
in NPR-1, a predicted G-protein-coupled neuropeptide receptor related to Neuropeptide
Y receptors2. Here we show that the NPR-1 isoform associated with solitary feeding
acts in neurons exposed to the body fluid to inhibit social feeding. Furthermore,
suppressing the activity of these neurons, called AQR, PQR and URX, using an activated
K+ channel, inhibits social feeding. NPR-1 activity in AQR, PQR and URX neurons
seems to suppress social feeding by antagonizing signalling through a cyclic GMP-gated
ion channel encoded by tax-2 and tax-4. We show that mutations in tax-2 or tax-4
disrupt social feeding, and that tax-4 is required in several neurons for social
feeding, including one or more of AQR, PQR and URX. The AQR, PQR and URX neurons
are unusual in C. elegans because they are directly exposed to the pseudocoelomic
body fluid3. Our data suggest a model in which these neurons integrate antagonistic
signals to control the choice between social and solitary feeding behaviour.
author:
- first_name: Juliet C.
full_name: Coates, Juliet C.
last_name: Coates
- 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: Coates JC, de Bono M. Antagonistic pathways in neurons exposed to body fluid
regulate social feeding in Caenorhabditis elegans. Nature. 2002;419(6910):925-929.
doi:10.1038/nature01170
apa: Coates, J. C., & de Bono, M. (2002). Antagonistic pathways in neurons exposed
to body fluid regulate social feeding in Caenorhabditis elegans. Nature.
Springer Nature. https://doi.org/10.1038/nature01170
chicago: Coates, Juliet C., and Mario de Bono. “Antagonistic Pathways in Neurons
Exposed to Body Fluid Regulate Social Feeding in Caenorhabditis Elegans.” Nature.
Springer Nature, 2002. https://doi.org/10.1038/nature01170.
ieee: J. C. Coates and M. de Bono, “Antagonistic pathways in neurons exposed to
body fluid regulate social feeding in Caenorhabditis elegans,” Nature,
vol. 419, no. 6910. Springer Nature, pp. 925–929, 2002.
ista: Coates JC, de Bono M. 2002. Antagonistic pathways in neurons exposed to body
fluid regulate social feeding in Caenorhabditis elegans. Nature. 419(6910), 925–929.
mla: Coates, Juliet C., and Mario de Bono. “Antagonistic Pathways in Neurons Exposed
to Body Fluid Regulate Social Feeding in Caenorhabditis Elegans.” Nature,
vol. 419, no. 6910, Springer Nature, 2002, pp. 925–29, doi:10.1038/nature01170.
short: J.C. Coates, M. de Bono, Nature 419 (2002) 925–929.
date_created: 2019-03-21T10:09:20Z
date_published: 2002-10-31T00:00:00Z
date_updated: 2021-01-12T08:06:26Z
day: '31'
doi: 10.1038/nature01170
extern: '1'
external_id:
pmid:
- '12410311'
intvolume: ' 419'
issue: '6910'
language:
- iso: eng
month: '10'
oa_version: None
page: 925-929
pmid: 1
publication: Nature
publication_identifier:
issn:
- 0028-0836
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Antagonistic pathways in neurons exposed to body fluid regulate social feeding
in Caenorhabditis elegans
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 419
year: '2002'
...
---
_id: '6159'
abstract:
- lang: eng
text: 'Natural Caenorhabditis elegans isolates exhibit either social or solitary
feeding on bacteria. We show here that social feeding is induced by nociceptive
neurons that detect adverse or stressful conditions. Ablation of the nociceptive
neurons ASH and ADL transforms social animals into solitary feeders. Social feeding
is probably due to the sensation of noxious chemicals by ASH and ADL neurons;
it requires the genes ocr-2 and osm-9, which encode TRP-related transduction channels,
and odr-4 and odr-8, which are required to localize sensory chemoreceptors to
cilia. Other sensory neurons may suppress social feeding, as social feeding in
ocr-2 and odr-4 mutants is restored by mutations in osm-3, a gene required for
the development of 26 ciliated sensory neurons. Our data suggest a model for regulation
of social feeding by opposing sensory inputs: aversive inputs to nociceptive neurons
promote social feeding, whereas antagonistic inputs from neurons that express
osm-3 inhibit aggregation.'
author:
- 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: David M.
full_name: Tobin, David M.
last_name: Tobin
- first_name: M. Wayne
full_name: Davis, M. Wayne
last_name: Davis
- first_name: Leon
full_name: Avery, Leon
last_name: Avery
- first_name: Cornelia I.
full_name: Bargmann, Cornelia I.
last_name: Bargmann
citation:
ama: de Bono M, Tobin DM, Davis MW, Avery L, Bargmann CI. Social feeding in Caenorhabditis
elegans is induced by neurons that detect aversive stimuli. Nature. 2002;419(6910):899-903.
doi:10.1038/nature01169
apa: de Bono, M., Tobin, D. M., Davis, M. W., Avery, L., & Bargmann, C. I. (2002).
Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive
stimuli. Nature. Springer Nature. https://doi.org/10.1038/nature01169
chicago: Bono, Mario de, David M. Tobin, M. Wayne Davis, Leon Avery, and Cornelia
I. Bargmann. “Social Feeding in Caenorhabditis Elegans Is Induced by Neurons That
Detect Aversive Stimuli.” Nature. Springer Nature, 2002. https://doi.org/10.1038/nature01169.
ieee: M. de Bono, D. M. Tobin, M. W. Davis, L. Avery, and C. I. Bargmann, “Social
feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli,”
Nature, vol. 419, no. 6910. Springer Nature, pp. 899–903, 2002.
ista: de Bono M, Tobin DM, Davis MW, Avery L, Bargmann CI. 2002. Social feeding
in Caenorhabditis elegans is induced by neurons that detect aversive stimuli.
Nature. 419(6910), 899–903.
mla: de Bono, Mario, et al. “Social Feeding in Caenorhabditis Elegans Is Induced
by Neurons That Detect Aversive Stimuli.” Nature, vol. 419, no. 6910, Springer
Nature, 2002, pp. 899–903, doi:10.1038/nature01169.
short: M. de Bono, D.M. Tobin, M.W. Davis, L. Avery, C.I. Bargmann, Nature 419 (2002)
899–903.
date_created: 2019-03-21T10:27:04Z
date_published: 2002-10-31T00:00:00Z
date_updated: 2021-01-12T08:06:27Z
day: '31'
doi: 10.1038/nature01169
extern: '1'
external_id:
pmid:
- '12410303'
intvolume: ' 419'
issue: '6910'
language:
- iso: eng
month: '10'
oa_version: None
page: 899-903
pmid: 1
publication: Nature
publication_identifier:
issn:
- 0028-0836
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Social feeding in Caenorhabditis elegans is induced by neurons that detect
aversive stimuli
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 419
year: '2002'
...
---
_id: '4631'
abstract:
- lang: eng
text: We present a theory of timed interfaces, which is capable of specifying both
the timing of the inputs a component expects from the environment, and the timing
of the outputs it can produce. Two timed interfaces are compatible if there is
a way to use them together such that their timing expectations are met. Our theory
provides algorithms for checking the compatibility between two interfaces and
for deriving the composite interface; the theory can thus be viewed as a type
system for real-time interaction. Technically, a timed interface is encoded as
a timed game between two players, representing the inputs and outputs of the component.
The algorithms for compatibility checking and interface composition are thus derived
from algorithms for solving timed games.
acknowledgement: This research was supported in part by the NSF CAREER award CCR-0132780,
the NSF grant CCR-9988172 the AFOSR MURI grant F49620-00-1-0327, the DARPA PCES
grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, and the ONR grant N00014-02-1-0671.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: 'De Alfaro L, Henzinger TA, Stoelinga M. Timed interfaces. In: Proceedings
of the 2nd International Conference on Embedded Software. Vol 2491. ACM; 2002:108-122.
doi:10.1007/3-540-45828-X_9'
apa: 'De Alfaro, L., Henzinger, T. A., & Stoelinga, M. (2002). Timed interfaces.
In Proceedings of the 2nd International Conference on Embedded Software
(Vol. 2491, pp. 108–122). Grenoble, France: ACM. https://doi.org/10.1007/3-540-45828-X_9'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Mariëlle Stoelinga. “Timed Interfaces.”
In Proceedings of the 2nd International Conference on Embedded Software,
2491:108–22. ACM, 2002. https://doi.org/10.1007/3-540-45828-X_9.
ieee: L. De Alfaro, T. A. Henzinger, and M. Stoelinga, “Timed interfaces,” in Proceedings
of the 2nd International Conference on Embedded Software, Grenoble, France,
2002, vol. 2491, pp. 108–122.
ista: 'De Alfaro L, Henzinger TA, Stoelinga M. 2002. Timed interfaces. Proceedings
of the 2nd International Conference on Embedded Software. EMSOFT: Embedded Software
, LNCS, vol. 2491, 108–122.'
mla: De Alfaro, Luca, et al. “Timed Interfaces.” Proceedings of the 2nd International
Conference on Embedded Software, vol. 2491, ACM, 2002, pp. 108–22, doi:10.1007/3-540-45828-X_9.
short: L. De Alfaro, T.A. Henzinger, M. Stoelinga, in:, Proceedings of the 2nd International
Conference on Embedded Software, ACM, 2002, pp. 108–122.
conference:
end_date: 2002-10-09
location: Grenoble, France
name: 'EMSOFT: Embedded Software '
start_date: 2002-10-07
date_created: 2018-12-11T12:09:51Z
date_published: 2002-10-24T00:00:00Z
date_updated: 2023-06-02T10:00:32Z
day: '24'
doi: 10.1007/3-540-45828-X_9
extern: '1'
intvolume: ' 2491'
language:
- iso: eng
month: '10'
oa_version: None
page: 108 - 122
publication: Proceedings of the 2nd International Conference on Embedded Software
publication_identifier:
isbn:
- '9783540443070'
publication_status: published
publisher: ACM
publist_id: '76'
quality_controlled: '1'
status: public
title: Timed interfaces
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2491
year: '2002'
...
---
_id: '4562'
abstract:
- lang: eng
text: We present interface models that describe both the input assumptions of a
component, and its output behavior. By enabling us to check that the input assumptions
of a component are met in a design, interface models provide a compatibility check
for component-based design. When refining a design into an implementation, interface
models require that the output behavior of a component satisfies the design specification
only when the input assumptions of the specification are satisfied, yielding greater
flexibility in the choice of implementations. Technically, our interface models
are games between two players, Input and Output; the duality of the players accounts
for the dual roles of inputs and outputs in composition and refinement. We present
two interface models in detail, one for a simple synchronous form of interaction
between components typical in hardware, and the other for more complex synchronous
interactions on bidirectional connections. As an example, we specify the interface
of a bidirectional bus, with the input assumption that at any time at most one
component has write access to the bus. For these interface models, we present
algorithms for compatibility and refinement checking, and we describe efficient
symbolic implementations.
acknowledgement: This research was supported in part by the AFOSR grant F49620-00-1-0327,
the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the NSF grant CCR-9988172,
the SRC grant 99-TJ-683.003, and the NSF CAREER award CCR-0132780.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'Chakrabarti A, De Alfaro L, Henzinger TA, Mang F. Synchronous and bidirectional
component interfaces. In: Proceedings of the 14th International Conference
on Computer Aided Verification. Vol 2404. Springer; 2002:414-427. doi:10.1007/3-540-45657-0_34'
apa: 'Chakrabarti, A., De Alfaro, L., Henzinger, T. A., & Mang, F. (2002). Synchronous
and bidirectional component interfaces. In Proceedings of the 14th International
Conference on Computer Aided Verification (Vol. 2404, pp. 414–427). Copenhagen,
Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_34'
chicago: Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, and Freddy Mang.
“Synchronous and Bidirectional Component Interfaces.” In Proceedings of the
14th International Conference on Computer Aided Verification, 2404:414–27.
Springer, 2002. https://doi.org/10.1007/3-540-45657-0_34.
ieee: A. Chakrabarti, L. De Alfaro, T. A. Henzinger, and F. Mang, “Synchronous and
bidirectional component interfaces,” in Proceedings of the 14th International
Conference on Computer Aided Verification, Copenhagen, Denmark, 2002, vol.
2404, pp. 414–427.
ista: 'Chakrabarti A, De Alfaro L, Henzinger TA, Mang F. 2002. Synchronous and bidirectional
component interfaces. Proceedings of the 14th International Conference on Computer
Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 414–427.'
mla: Chakrabarti, Arindam, et al. “Synchronous and Bidirectional Component Interfaces.”
Proceedings of the 14th International Conference on Computer Aided Verification,
vol. 2404, Springer, 2002, pp. 414–27, doi:10.1007/3-540-45657-0_34.
short: A. Chakrabarti, L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of
the 14th International Conference on Computer Aided Verification, Springer, 2002,
pp. 414–427.
conference:
end_date: 2002-07-31
location: Copenhagen, Denmark
name: 'CAV: Computer Aided Verification'
start_date: 2002-07-27
date_created: 2018-12-11T12:09:29Z
date_published: 2002-06-19T00:00:00Z
date_updated: 2023-06-02T12:01:22Z
day: '19'
doi: 10.1007/3-540-45657-0_34
extern: '1'
intvolume: ' 2404'
language:
- iso: eng
month: '06'
oa_version: None
page: 414 - 427
publication: Proceedings of the 14th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540439974'
publication_status: published
publisher: Springer
publist_id: '146'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synchronous and bidirectional component interfaces
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2404
year: '2002'
...
---
_id: '4565'
abstract:
- lang: eng
text: "In the literature, we find several formulations of the control\r\nproblem
for timed and hybrid systems. We argue that formulations where\r\na controller
can cause an action at any point in dense (rational or real)\r\ntime are problematic,
by presenting an example where the controller\r\nmust act faster and faster, yet
causes no Zeno effects (say, the control\r\nactions are at times 0, 1/2, 1, 1
1/4, 2, 2 1/8, 3, 3 1/16 ,...). Such a controller is,\r\nof course, not implementable
in software. Such controllers are avoided by formulations where the controller
can cause actions only at discrete (integer) points in time. While the resulting
control problem is well- understood if the time unit, or “sampling rate” of the
controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time
control problem with unknown sampling rate asks if a sampling controller exists
for some sampling rate. We prove that this problem is undecidable even in the
special case of timed automata."
acknowledgement: "Partially supported by the FNRS, Belgium, under grant 1.5.096.01.\r\nPartially
supported by the DARPA SEC grant F33615-C-98-3614, the AFOSR MURI grant F49620-00-1-0327,
the NSF Theory grant CCR-9988172, and the MARCO GSRC grant 98-DT-660.\r\nPartially
supported by a “Crédit aux chercheurs” from the Belgian National Fund for Scientific
Research."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Franck
full_name: Cassez, Franck
last_name: Cassez
- 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: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: 'Cassez F, Henzinger TA, Raskin J. A comparison of control problems for timed
and hybrid systems. In: Proceedings of the 5th International Workshop on Hybrid
Systems: Computation and Control. Vol 2289. Springer; 2002:134-148. doi:10.1007/3-540-45873-5_13'
apa: 'Cassez, F., Henzinger, T. A., & Raskin, J. (2002). A comparison of control
problems for timed and hybrid systems. In Proceedings of the 5th International
Workshop on Hybrid Systems: Computation and Control (Vol. 2289, pp. 134–148).
Stanford, CA, USA: Springer. https://doi.org/10.1007/3-540-45873-5_13'
chicago: 'Cassez, Franck, Thomas A Henzinger, and Jean Raskin. “A Comparison of
Control Problems for Timed and Hybrid Systems.” In Proceedings of the 5th International
Workshop on Hybrid Systems: Computation and Control, 2289:134–48. Springer,
2002. https://doi.org/10.1007/3-540-45873-5_13.'
ieee: 'F. Cassez, T. A. Henzinger, and J. Raskin, “A comparison of control problems
for timed and hybrid systems,” in Proceedings of the 5th International Workshop
on Hybrid Systems: Computation and Control, Stanford, CA, USA, 2002, vol.
2289, pp. 134–148.'
ista: 'Cassez F, Henzinger TA, Raskin J. 2002. A comparison of control problems
for timed and hybrid systems. Proceedings of the 5th International Workshop on
Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and
Control, LNCS, vol. 2289, 134–148.'
mla: 'Cassez, Franck, et al. “A Comparison of Control Problems for Timed and Hybrid
Systems.” Proceedings of the 5th International Workshop on Hybrid Systems:
Computation and Control, vol. 2289, Springer, 2002, pp. 134–48, doi:10.1007/3-540-45873-5_13.'
short: 'F. Cassez, T.A. Henzinger, J. Raskin, in:, Proceedings of the 5th International
Workshop on Hybrid Systems: Computation and Control, Springer, 2002, pp. 134–148.'
conference:
end_date: 2002-03-27
location: Stanford, CA, USA
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2002-03-25
date_created: 2018-12-11T12:09:30Z
date_published: 2002-03-14T00:00:00Z
date_updated: 2023-06-02T10:29:10Z
day: '14'
doi: 10.1007/3-540-45873-5_13
extern: '1'
intvolume: ' 2289'
language:
- iso: eng
month: '03'
oa_version: None
page: 134 - 148
publication: 'Proceedings of the 5th International Workshop on Hybrid Systems: Computation
and Control'
publication_identifier:
isbn:
- '9783540433217'
publication_status: published
publisher: Springer
publist_id: '144'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A comparison of control problems for timed and hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2289
year: '2002'
...
---
_id: '4595'
abstract:
- lang: eng
text: 'Temporal logic comes in two varieties: linear-time temporal logic assumes
implicit universal quantification over all paths that are generated by the execution
of a system; branching-time temporal logic allows explicit existential and universal
quantification over all paths. We introduce a third, more general variety of temporal
logic: alternating-time temporal logic offers selective quantification over those
paths that are possible outcomes of games, such as the game in which the system
and the environment alternate moves. While linear-time and branching-time logics
are natural specification languages for closed systems, alternating-time logics
are natural specification languages for open systems. For example, by preceding
the temporal operator "eventually" with a selective path quantifier,
we can specify that in the game between the system and the environment, the system
has a strategy to reach a certain state. The problems of receptiveness, realizability,
and controllability can be formulated as model-checking problems for alternating-time
formulas. Depending on whether or not we admit arbitrary nesting of selective
path quantifiers and temporal operators, we obtain the two alternating-time temporal
logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures.
Every state transition of a concurrent game structure results from a choice of
moves, one for each player. The players represent individual components and the
environment of an open system. Concurrent game structures can capture various
forms of synchronous composition for open systems, and if augmented with fairness
constraints, also asynchronous composition. Over structures without fairness constraints,
the model-checking complexity of ATL is linear in the size of the game structure
and length of the formula, and the symbolic model-checking algorithm for CTL extends
with few modifications to ATL. Over structures with weak-fairness constraints,
ATL model checking requires the solution of 1-pair Rabin games, and can be done
in polynomial time. Over structures with strong-fairness constraints, ATL model
checking requires the solution of games with Boolean combinations of Büchi conditions,
and can be done in PSPACE. In the case of ATL*, the model-checking problem is
closely related to the synthesis problem for linear-time formulas, and requires
doubly exponential time.'
acknowledgement: We thank Luca de Alfaro, Kousha Etessami, Salvatore La Torre, P.
Madhusudan, Amir Pnueli, Moshe Vardi, Thomas Wilke, and Mihalis Yannakakis for helpful
discussions. We also thank Freddy Mang for comments on a draft of this manuscript.
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- 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: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. Journal
of the ACM. 2002;49(5):672-713. doi:10.1145/585265.585270
apa: Alur, R., Henzinger, T. A., & Kupferman, O. (2002). Alternating-time temporal
logic. Journal of the ACM. ACM. https://doi.org/10.1145/585265.585270
chicago: Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time
Temporal Logic.” Journal of the ACM. ACM, 2002. https://doi.org/10.1145/585265.585270.
ieee: R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,”
Journal of the ACM, vol. 49, no. 5. ACM, pp. 672–713, 2002.
ista: Alur R, Henzinger TA, Kupferman O. 2002. Alternating-time temporal logic.
Journal of the ACM. 49(5), 672–713.
mla: Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” Journal of the ACM,
vol. 49, no. 5, ACM, 2002, pp. 672–713, doi:10.1145/585265.585270.
short: R. Alur, T.A. Henzinger, O. Kupferman, Journal of the ACM 49 (2002) 672–713.
date_created: 2018-12-11T12:09:40Z
date_published: 2002-09-01T00:00:00Z
date_updated: 2023-06-02T10:07:22Z
day: '01'
doi: 10.1145/585265.585270
extern: '1'
intvolume: ' 49'
issue: '5'
language:
- iso: eng
month: '09'
oa_version: None
page: 672 - 713
publication: Journal of the ACM
publication_identifier:
issn:
- 0004-5411
publication_status: published
publisher: ACM
publist_id: '110'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating-time temporal logic
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 49
year: '2002'
...
---
_id: '4471'
abstract:
- lang: eng
text: The sequential synthesis problem, which is closely related to Church’s solvability
problem, asks, given a specification in the form of a binary relation between
input and output streams, for the construction of a finite-state stream transducer
that converts inputs to appropriate outputs. For efficiency reasons, practical
sequential hardware is often designed to operate without prior initialization.
Such hardware designs can be modeled by uninitialized state machines, which are
required to satisfy their specification if started from any state. In this paper
we solve the sequential synthesis problem for uninitialized systems, that is,
we construct uninitialized finite-state stream transducers. We consider specifications
given by LTL formulas, deterministic, nondeterministic, universal, and alternating
Büchi automata. We solve this uninitialized synthesis problem by reducing it to
the well-understood initialized synthesis problem. While our solution is straightforward,
it leads, for some specification formalisms, to upper bounds that are exponentially
worse than the complexity of the corresponding initialized problems. However,
we prove lower bounds to show that our simple solutions are optimal for all considered
specification formalisms. We also study the problem of deciding whether a given
specification is uninitialized, that is, if its uninitialized and initialized
synthesis problems coincide. We show that this problem has, for each specification
formalism, the same complexity as the equivalence problem.
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
the DARPA contract NAG2-1214, and the NSF grant CCR-9988172.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Sriram
full_name: Krishnan, Sriram
last_name: Krishnan
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'Henzinger TA, Krishnan S, Kupferman O, Mang F. Synthesis of uninitialized
systems. In: Proceedings of the 29th International Colloquium on Automata,
Languages and Programming. Vol 2380. Springer; 2002:644-656. doi:10.1007/3-540-45465-9_55'
apa: 'Henzinger, T. A., Krishnan, S., Kupferman, O., & Mang, F. (2002). Synthesis
of uninitialized systems. In Proceedings of the 29th International Colloquium
on Automata, Languages and Programming (Vol. 2380, pp. 644–656). Malaga, Spain:
Springer. https://doi.org/10.1007/3-540-45465-9_55'
chicago: Henzinger, Thomas A, Sriram Krishnan, Orna Kupferman, and Freddy Mang.
“Synthesis of Uninitialized Systems.” In Proceedings of the 29th International
Colloquium on Automata, Languages and Programming, 2380:644–56. Springer,
2002. https://doi.org/10.1007/3-540-45465-9_55.
ieee: T. A. Henzinger, S. Krishnan, O. Kupferman, and F. Mang, “Synthesis of uninitialized
systems,” in Proceedings of the 29th International Colloquium on Automata,
Languages and Programming, Malaga, Spain, 2002, vol. 2380, pp. 644–656.
ista: 'Henzinger TA, Krishnan S, Kupferman O, Mang F. 2002. Synthesis of uninitialized
systems. Proceedings of the 29th International Colloquium on Automata, Languages
and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2380,
644–656.'
mla: Henzinger, Thomas A., et al. “Synthesis of Uninitialized Systems.” Proceedings
of the 29th International Colloquium on Automata, Languages and Programming,
vol. 2380, Springer, 2002, pp. 644–56, doi:10.1007/3-540-45465-9_55.
short: T.A. Henzinger, S. Krishnan, O. Kupferman, F. Mang, in:, Proceedings of the
29th International Colloquium on Automata, Languages and Programming, Springer,
2002, pp. 644–656.
conference:
end_date: 2002-07-13
location: Malaga, Spain
name: 'ICALP: Automata, Languages and Programming'
start_date: 2002-07-08
date_created: 2018-12-11T12:09:01Z
date_published: 2002-06-26T00:00:00Z
date_updated: 2023-06-05T08:05:13Z
day: '26'
doi: 10.1007/3-540-45465-9_55
extern: '1'
intvolume: ' 2380'
language:
- iso: eng
month: '06'
oa_version: None
page: 644 - 656
publication: Proceedings of the 29th International Colloquium on Automata, Languages
and Programming
publication_identifier:
isbn:
- '9783540438649'
publication_status: published
publisher: Springer
publist_id: '257'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of uninitialized systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2380
year: '2002'
...
---
_id: '4474'
abstract:
- lang: eng
text: 'The simulation preorder for labeled transition systems is defined locally,
and operationally, as a game that relates states with their immediate successor
states. Simulation enjoys many appealing properties. First, simulation has a denotational
characterization: system S simulates system I iff every computation tree embedded
in the unrolling of I can be embedded also in the unrolling of S. Second, simulation
has a logical characterization: S simulates I iff every universal branching-time
formula satisfied by S is satisfied also by I. It follows that simulation is a
suitable notion of implementation, and it is the coarsest abstraction of a system
that preserves universal branching-time properties. Third, based on its local
definition, simulation between finite-state systems can be checked in polynomial
time. Finally, simulation implies trace containment, which cannot be defined locally
and requires polynomial space for verification. Hence simulation is widely used
both in manual and in automatic verification. Liveness assumptions about transition
systems are typically modeled using fairness constraints. Existing notions of
simulation for fair transition systems, however, are not local, and as a result,
many appealing properties of the simulation preorder are lost. We propose a new
view of fair simulation by extending the local definition of simulation to account
for fairness: system View the MathML sourcefairly simulates system View the MathML
source iff in the simulation game, there is a strategy that matches with each
fair computation of View the MathML source a fair computation of View the MathML
source. Our definition enjoys a denotational characterization and has a logical
characterization: View the MathML source fairly simulates View the MathML source
iff every fair computation tree (whose infinite paths are fair) embedded in the
unrolling of View the MathML source can be embedded also in the unrolling of View
the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by
View the MathML source is satisfied also by View the MathML source (∀AFMC is the
universal fragment of the alternation-free μ-calculus). The locality of the definition
leads us to a polynomial-time algorithm for checking fair simulation for finite-state
systems with weak and strong fairness constraints. Finally, fair simulation implies
fair trace containment and is therefore useful as an efficiently computable local
criterion for proving linear-time abstraction hierarchies of fair systems.'
acknowledgement: We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers
for their comments on this paper.
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: Henzinger TA, Kupferman O, Rajamani S. Fair simulation. Information and
Computation. 2002;173(1):64-81. doi:10.1006/inco.2001.3085
apa: Henzinger, T. A., Kupferman, O., & Rajamani, S. (2002). Fair simulation.
Information and Computation. Elsevier. https://doi.org/10.1006/inco.2001.3085
chicago: Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.”
Information and Computation. Elsevier, 2002. https://doi.org/10.1006/inco.2001.3085.
ieee: T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” Information
and Computation, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.
ista: Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information
and Computation. 173(1), 64–81.
mla: Henzinger, Thomas A., et al. “Fair Simulation.” Information and Computation,
vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:10.1006/inco.2001.3085.
short: T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173
(2002) 64–81.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-02-25T00:00:00Z
date_updated: 2023-06-05T07:53:27Z
day: '25'
doi: 10.1006/inco.2001.3085
extern: '1'
intvolume: ' 173'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub
month: '02'
oa: 1
oa_version: Published Version
page: 64 - 81
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '255'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fair simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 173
year: '2002'
...
---
_id: '4563'
abstract:
- lang: eng
text: We present a formal methodology and tool for uncovering errors in the interaction
of software modules. Our methodology consists of a suite of languages for defining
software interfaces, and algorithms for checking interface compatibility. We focus
on interfaces that explain the method-call dependencies between software modules.
Such an interface makes assumptions about the environment in the form of call
and availability constraints. A call constraint restricts the accessibility of
local methods to certain external methods. An availability constraint restricts
the accessibility of local methods to certain states of the module. For example,
the interface for a file server with local methods open and read may assert that
a file cannot be read without having been opened. Checking interface compatibility
requires the solution of games, and in the presence of availability constraints,
of pushdown games. Based on this methodology, we have implemented a tool that
has uncovered incompatibilities in TinyOS, a small operating system for sensor
nodes in adhoc networks.
acknowledgement: This research was supported in part by the AFOSR grant F49620-00-1-0327,
the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the NSF grants CCR-9988172,
CCR-0085949, CCR-0132780, the SRC grant 99-TJ-683, and the Polish KBN grant 7-T11C-027-20.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'Chakrabarti A, De Alfaro L, Henzinger TA, Jurdziński M, Mang F. Interface
compatibility checking for software modules. In: Proceedings of the 14th International
Conference on Computer Aided Verification. Vol 2404. Springer; 2002:428-441.
doi:10.1007/3-540-45657-0_35'
apa: 'Chakrabarti, A., De Alfaro, L., Henzinger, T. A., Jurdziński, M., & Mang,
F. (2002). Interface compatibility checking for software modules. In Proceedings
of the 14th International Conference on Computer Aided Verification (Vol.
2404, pp. 428–441). Copenhagen, Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_35'
chicago: Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, Marcin Jurdziński,
and Freddy Mang. “Interface Compatibility Checking for Software Modules.” In Proceedings
of the 14th International Conference on Computer Aided Verification, 2404:428–41.
Springer, 2002. https://doi.org/10.1007/3-540-45657-0_35.
ieee: A. Chakrabarti, L. De Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang,
“Interface compatibility checking for software modules,” in Proceedings of
the 14th International Conference on Computer Aided Verification, Copenhagen,
Denmark, 2002, vol. 2404, pp. 428–441.
ista: 'Chakrabarti A, De Alfaro L, Henzinger TA, Jurdziński M, Mang F. 2002. Interface
compatibility checking for software modules. Proceedings of the 14th International
Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 2404, 428–441.'
mla: Chakrabarti, Arindam, et al. “Interface Compatibility Checking for Software
Modules.” Proceedings of the 14th International Conference on Computer Aided
Verification, vol. 2404, Springer, 2002, pp. 428–41, doi:10.1007/3-540-45657-0_35.
short: A. Chakrabarti, L. De Alfaro, T.A. Henzinger, M. Jurdziński, F. Mang, in:,
Proceedings of the 14th International Conference on Computer Aided Verification,
Springer, 2002, pp. 428–441.
conference:
end_date: 2002-07-31
location: Copenhagen, Denmark
name: 'CAV: Computer Aided Verification'
start_date: 2002-07-27
date_created: 2018-12-11T12:09:30Z
date_published: 2002-06-19T00:00:00Z
date_updated: 2023-06-05T07:38:10Z
day: '19'
doi: 10.1007/3-540-45657-0_35
extern: '1'
intvolume: ' 2404'
language:
- iso: eng
month: '06'
oa_version: None
page: 428 - 441
publication: Proceedings of the 14th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- ' 9783540439974'
publication_status: published
publisher: Springer
publist_id: '147'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interface compatibility checking for software modules
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2404
year: '2002'
...
---
_id: '4472'
abstract:
- lang: eng
text: 'We present a methodology and tool for verifying and certifying systems code.
The verification is based on the lazy-abstraction paradigm for intertwining the
following three logical steps: construct a predicate abstraction from the code,
model check the abstraction, and automatically refine the abstraction based on
counterexample analysis. The certification is based on the proof-carrying code
paradigm. Lazy abstraction enables the automatic construction of small proof certificates.
The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software
verification Tool. We describe our experience applying Blast to Linux and Windows
device drivers. Given the C code for a driver and for a temporal-safety monitor,
Blast automatically generates an easily checkable correctness certificate if the
driver satisfies the specification, and an error trace otherwise.'
acknowledgement: This work was supported in part by the NSF ITR grants CCR-0085949,
CCR-0081588, the NSF Career grant CCR-9875171, the DARPA PCES grant F33615-00-C-1693,
the MARCO GSRC grant 98-DT-660, the SRC contract 99-TJ-683, a Microsoft fellowship,
and gifts from AT&T Research and Microsoft Research.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: George
full_name: Necula, George
last_name: Necula
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Grégoire
full_name: Sutre, Grégoire
last_name: Sutre
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Westley
full_name: Weimer, Westley
last_name: Weimer
citation:
ama: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. Temporal safety
proofs for systems code. In: Proceedings of the 14th International Conference
on Computer Aided Verification. Vol 2404. Springer; 2002:526-538. doi:10.1007/3-540-45657-0_45'
apa: 'Henzinger, T. A., Necula, G., Jhala, R., Sutre, G., Majumdar, R., & Weimer,
W. (2002). Temporal safety proofs for systems code. In Proceedings of the 14th
International Conference on Computer Aided Verification (Vol. 2404, pp. 526–538).
Copenhagen, Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_45'
chicago: Henzinger, Thomas A, George Necula, Ranjit Jhala, Grégoire Sutre, Ritankar
Majumdar, and Westley Weimer. “Temporal Safety Proofs for Systems Code.” In Proceedings
of the 14th International Conference on Computer Aided Verification, 2404:526–38.
Springer, 2002. https://doi.org/10.1007/3-540-45657-0_45.
ieee: T. A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, and W. Weimer,
“Temporal safety proofs for systems code,” in Proceedings of the 14th International
Conference on Computer Aided Verification, Copenhagen, Denmark, 2002, vol.
2404, pp. 526–538.
ista: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. 2002. Temporal
safety proofs for systems code. Proceedings of the 14th International Conference
on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404,
526–538.'
mla: Henzinger, Thomas A., et al. “Temporal Safety Proofs for Systems Code.” Proceedings
of the 14th International Conference on Computer Aided Verification, vol.
2404, Springer, 2002, pp. 526–38, doi:10.1007/3-540-45657-0_45.
short: T.A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, W. Weimer, in:,
Proceedings of the 14th International Conference on Computer Aided Verification,
Springer, 2002, pp. 526–538.
conference:
end_date: 2002-07-31
location: Copenhagen, Denmark
name: 'CAV: Computer Aided Verification'
start_date: 2002-07-27
date_created: 2018-12-11T12:09:01Z
date_published: 2002-06-19T00:00:00Z
date_updated: 2023-06-05T08:11:32Z
day: '19'
doi: 10.1007/3-540-45657-0_45
extern: '1'
intvolume: ' 2404'
language:
- iso: eng
month: '06'
oa_version: None
page: 526 - 538
publication: Proceedings of the 14th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540439974'
publication_status: published
publisher: Springer
publist_id: '258'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal safety proofs for systems code
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2404
year: '2002'
...
---
_id: '4470'
abstract:
- lang: eng
text: Giotto is a platform-independent language for specifying software for high-performance
control applications. In this paper we present a new approach to the compilation
of Giotto. Following this approach, the Giotto compiler generates code for a virtual
machine, called the E machine, which can be ported to different platforms. The
Giotto compiler also checks if the generated E code is time safe for a given platform,
that is, if the platform offers sufficient performance to ensure that the E code
is executed in a timely fashion that conforms with the Giotto semantics. Time-safety
checking requires a schedulability analysis. We show that while for arbitrary
E code, the analysis is exponential, for E code generated from typical Giotto
programs, the analysis is polynomial. This supports our claim that Giotto identifies
a useful fragment of embedded programs.
acknowledgement: Supported in part by the DARPA SEC grant F33615-C-98-3614, MARCO
GSRC grant 98-DT-660, AFOSR MURI grant F49620-00-1-0327, NSF grant CCR-9988172,
and a Microsoft Research Fellowship.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. Time-safety checking for embedded
programs. In: Proceedings of the 2nd International Conference on Embedded Software.
Vol 2491. ACM; 2002:76-92. doi:10.1007/3-540-45828-X_7'
apa: 'Henzinger, T. A., Kirsch, C., Majumdar, R., & Matic, S. (2002). Time-safety
checking for embedded programs. In Proceedings of the 2nd International Conference
on Embedded Software (Vol. 2491, pp. 76–92). Grenoble, France: ACM. https://doi.org/10.1007/3-540-45828-X_7'
chicago: Henzinger, Thomas A, Christoph Kirsch, Ritankar Majumdar, and Slobodan
Matic. “Time-Safety Checking for Embedded Programs.” In Proceedings of the
2nd International Conference on Embedded Software, 2491:76–92. ACM, 2002.
https://doi.org/10.1007/3-540-45828-X_7.
ieee: T. A. Henzinger, C. Kirsch, R. Majumdar, and S. Matic, “Time-safety checking
for embedded programs,” in Proceedings of the 2nd International Conference
on Embedded Software, Grenoble, France, 2002, vol. 2491, pp. 76–92.
ista: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. 2002. Time-safety checking for
embedded programs. Proceedings of the 2nd International Conference on Embedded
Software. EMSOFT: Embedded Software , LNCS, vol. 2491, 76–92.'
mla: Henzinger, Thomas A., et al. “Time-Safety Checking for Embedded Programs.”
Proceedings of the 2nd International Conference on Embedded Software, vol.
2491, ACM, 2002, pp. 76–92, doi:10.1007/3-540-45828-X_7.
short: T.A. Henzinger, C. Kirsch, R. Majumdar, S. Matic, in:, Proceedings of the
2nd International Conference on Embedded Software, ACM, 2002, pp. 76–92.
conference:
end_date: 2002-10-09
location: Grenoble, France
name: 'EMSOFT: Embedded Software '
start_date: 2002-10-07
date_created: 2018-12-11T12:09:01Z
date_published: 2002-09-25T00:00:00Z
date_updated: 2023-06-05T08:50:59Z
day: '25'
doi: 10.1007/3-540-45828-X_7
extern: '1'
intvolume: ' 2491'
language:
- iso: eng
month: '09'
oa_version: None
page: 76 - 92
publication: Proceedings of the 2nd International Conference on Embedded Software
publication_identifier:
isbn:
- '9783540443070'
publication_status: published
publisher: ACM
publist_id: '259'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Time-safety checking for embedded programs
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2491
year: '2002'
...
---
_id: '4444'
abstract:
- lang: eng
text: The Embedded Machine is a virtual machine that mediates in real time the interaction
between software processes and physical processes. It separates the compilation
of embedded programs into two phases. The first, platform-independent compiler
phase generates E code (code executed by the Embedded Machine), which supervises
the timing ---not the scheduling--- of application tasks relative to external
events, such as clock ticks and sensor interrupts. E~code is portable and exhibits,
given an input behavior, predictable (i.e., deterministic) timing and output behavior.
The second, platform-dependent compiler phase checks the time safety of the E
code, that is, whether platform performance (determined by the hardware) and platform
utilization (determined by the scheduler of the operating system) enable its timely
execution. We have used the Embedded Machine to compile and execute high-performance
control applications written in Giotto, such as the flight control system of an
autonomous model helicopter.
acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614,
the MARCO GSRC grant 98-DT- 660, the AFOSR MURI grant F49620-00-1-0327, and the
NSF ITR grant CCR-0085949.
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
citation:
ama: 'Henzinger TA, Kirsch C. The embedded machine: predictable, portable real-time
code. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language
Design and Implementation. ACM; 2002:315-326. doi:10.1145/512529.512567'
apa: 'Henzinger, T. A., & Kirsch, C. (2002). The embedded machine: predictable,
portable real-time code. In Proceedings of the ACM SIGPLAN 2002 conference
on Programming language design and implementation (pp. 315–326). Berlin, Germany:
ACM. https://doi.org/10.1145/512529.512567'
chicago: 'Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable,
Portable Real-Time Code.” In Proceedings of the ACM SIGPLAN 2002 Conference
on Programming Language Design and Implementation, 315–26. ACM, 2002. https://doi.org/10.1145/512529.512567.'
ieee: 'T. A. Henzinger and C. Kirsch, “The embedded machine: predictable, portable
real-time code,” in Proceedings of the ACM SIGPLAN 2002 conference on Programming
language design and implementation, Berlin, Germany, 2002, pp. 315–326.'
ista: 'Henzinger TA, Kirsch C. 2002. The embedded machine: predictable, portable
real-time code. Proceedings of the ACM SIGPLAN 2002 conference on Programming
language design and implementation. PLDI: Programming Languages Design and Implementation,
315–326.'
mla: 'Henzinger, Thomas A., and Christoph Kirsch. “The Embedded Machine: Predictable,
Portable Real-Time Code.” Proceedings of the ACM SIGPLAN 2002 Conference on
Programming Language Design and Implementation, ACM, 2002, pp. 315–26, doi:10.1145/512529.512567.'
short: T.A. Henzinger, C. Kirsch, in:, Proceedings of the ACM SIGPLAN 2002 Conference
on Programming Language Design and Implementation, ACM, 2002, pp. 315–326.
conference:
end_date: 2002-06-19
location: Berlin, Germany
name: 'PLDI: Programming Languages Design and Implementation'
start_date: 2002-06-17
date_created: 2018-12-11T12:08:53Z
date_published: 2002-06-01T00:00:00Z
date_updated: 2023-06-05T09:02:23Z
day: '01'
doi: 10.1145/512529.512567
extern: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: 315 - 326
publication: Proceedings of the ACM SIGPLAN 2002 conference on Programming language
design and implementation
publication_identifier:
isbn:
- '9781581134636'
publication_status: published
publisher: ACM
publist_id: '284'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'The embedded machine: predictable, portable real-time code'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2002'
...
---
_id: '4476'
abstract:
- lang: eng
text: 'One approach to model checking software is based on the abstract-check-refine
paradigm: build an abstract model, then check the desired property, and if the
check fails, refine the model and start over. We introduce the concept of lazy
abstraction to integrate and optimize the three phases of the abstract-check-refine
loop. Lazy abstraction continuously builds and refines a single abstract model
on demand, driven by the model checker, so that different parts of the model may
exhibit different degrees of precision, namely just enough to verify the desired
property. We present an algorithm for model checking safety properties using lazy
abstraction and describe an implementation of the algorithm applied to C programs.
We also provide sufficient conditions for the termination of the method.'
acknowledgement: "We thank Wes Weimer and Jeff Foster for many useful discussions.
\r\n"
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Grégoire
full_name: Sutre, Grégoire
last_name: Sutre
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: Proceedings
of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
ACM; 2002:58-70. doi:10.1145/503272.503279'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Sutre, G. (2002). Lazy abstraction.
In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming
languages (pp. 58–70). Portland, OR, USA: ACM. https://doi.org/10.1145/503272.503279'
chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre.
“Lazy Abstraction.” In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, 58–70. ACM, 2002. https://doi.org/10.1145/503272.503279.
ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy abstraction,”
in Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming
languages, Portland, OR, USA, 2002, pp. 58–70.
ista: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. 2002. Lazy abstraction. Proceedings
of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages.
POPL: Principles of Programming Languages, 58–70.'
mla: Henzinger, Thomas A., et al. “Lazy Abstraction.” Proceedings of the 29th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM,
2002, pp. 58–70, doi:10.1145/503272.503279.
short: T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the
29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM,
2002, pp. 58–70.
conference:
end_date: 2002-01-18
location: Portland, OR, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2002-01-16
date_created: 2018-12-11T12:09:03Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-06-05T07:45:53Z
day: '01'
doi: 10.1145/503272.503279
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 58 - 70
publication: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of
programming languages
publication_identifier:
isbn:
- '9781581134506'
publication_status: published
publisher: ACM
publist_id: '254'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Lazy abstraction
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2002'
...
---
_id: '4473'
abstract:
- lang: eng
text: 'The simulation preorder on state transition systems is widely accepted as
a useful notion of refinement, both in its own right and as an efficiently checkable
sufficient condition for trace containment. For composite systems, due to the
exponential explosion of the state space, there is a need for decomposing a simulation
check of the form P ≤s Q, denoting "P is simulated by Q," into simpler
simulation checks on the components of P and Q. We present an assume-guarantee
rule that enables such a decomposition. To the best of our knowledge, this is
the first assume-guarantee rule that applies to a refinement relation different
from trace containment. Our rule is circular, and its soundness proof requires
induction on trace trees. The proof is constructive: given simulation relations
that witness the simulation preorder between corresponding components of P and
Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also
extend our assume-guarantee rule to account for fairness constraints on transition
systems.'
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
- first_name: Serdar
full_name: Tasiran, Serdar
last_name: Tasiran
citation:
ama: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for
checking simulation. ACM Transactions on Programming Languages and Systems
(TOPLAS). 2002;24(1):51-64. doi:10.1145/509705.509707
apa: Henzinger, T. A., Qadeer, S., Rajamani, S., & Tasiran, S. (2002). An assume-guarantee
rule for checking simulation. ACM Transactions on Programming Languages and
Systems (TOPLAS). ACM. https://doi.org/10.1145/509705.509707
chicago: Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran.
“An Assume-Guarantee Rule for Checking Simulation.” ACM Transactions on Programming
Languages and Systems (TOPLAS). ACM, 2002. https://doi.org/10.1145/509705.509707.
ieee: T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee
rule for checking simulation,” ACM Transactions on Programming Languages and
Systems (TOPLAS), vol. 24, no. 1. ACM, pp. 51–64, 2002.
ista: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 2002. An assume-guarantee rule
for checking simulation. ACM Transactions on Programming Languages and Systems
(TOPLAS). 24(1), 51–64.
mla: Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.”
ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 24,
no. 1, ACM, 2002, pp. 51–64, doi:10.1145/509705.509707.
short: T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming
Languages and Systems (TOPLAS) 24 (2002) 51–64.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-06-05T07:59:47Z
day: '01'
doi: 10.1145/509705.509707
extern: '1'
intvolume: ' 24'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 51 - 64
publication: ACM Transactions on Programming Languages and Systems (TOPLAS)
publication_identifier:
issn:
- 0164-0925
publication_status: published
publisher: ACM
publist_id: '256'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An assume-guarantee rule for checking simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 24
year: '2002'
...
---
_id: '4423'
abstract:
- lang: eng
text: Automation control systems typically incorporate legacy code and components
that were originally designed to operate independently. Furthermore, they operate
under stringent safety and timing constraints. Current design strategies deal
with these requirements and characteristics with ad hoc approaches. In particular,
when designing control laws, implementation constraints are often ignored or cursorily
estimated. Indeed, costly redesigns are needed after a prototype of the control
system is built due to missed timing constraints and subtle transient errors.
In this paper, we use the concepts of platform-based design, and the Giotto programming
language, to develop a methodology for the design of automation control systems
that builds in modularity and correct-by-construction procedures. We illustrate
our strategy by describing the (successful) application of the methodology to
the design of a time-based control system for a rotorcraft Uninhabited Aerial
Vehicle (UAV).
acknowledgement: "Research supported in part by DARPA under contract no.F33615-98-C-3614,
Software Enabled Control, administered by\r\nAFRL, Dayton OH."
article_processing_charge: No
author:
- first_name: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
- first_name: Judith
full_name: Liebman, Judith
last_name: Liebman
- first_name: Cedric
full_name: Ma, Cedric
last_name: Ma
- first_name: T John
full_name: Koo, T John
last_name: Koo
- 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: Alberto
full_name: Sangiovanni Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
- first_name: Shankar
full_name: Sastry, Shankar
last_name: Sastry
citation:
ama: 'Horowitz B, Liebman J, Ma C, et al. Embedded software design and system integration
for rotorcraft UAV using platforms. In: Proceedings of the 15th Triennial World
Congress of the International Federation of Automatic Control. Vol 15. Elsevier;
2002. doi:10.3182/20020721-6-ES-1901.01628'
apa: 'Horowitz, B., Liebman, J., Ma, C., Koo, T. J., Henzinger, T. A., Sangiovanni
Vincentelli, A., & Sastry, S. (2002). Embedded software design and system
integration for rotorcraft UAV using platforms. In Proceedings of the 15th
Triennial World Congress of the International Federation of Automatic Control
(Vol. 15). Barcelona, Spain: Elsevier. https://doi.org/10.3182/20020721-6-ES-1901.01628'
chicago: Horowitz, Benjamin, Judith Liebman, Cedric Ma, T John Koo, Thomas A Henzinger,
Alberto Sangiovanni Vincentelli, and Shankar Sastry. “Embedded Software Design
and System Integration for Rotorcraft UAV Using Platforms.” In Proceedings
of the 15th Triennial World Congress of the International Federation of Automatic
Control, Vol. 15. Elsevier, 2002. https://doi.org/10.3182/20020721-6-ES-1901.01628.
ieee: B. Horowitz et al., “Embedded software design and system integration
for rotorcraft UAV using platforms,” in Proceedings of the 15th Triennial World
Congress of the International Federation of Automatic Control, Barcelona,
Spain, 2002, vol. 15, no. 1.
ista: 'Horowitz B, Liebman J, Ma C, Koo TJ, Henzinger TA, Sangiovanni Vincentelli
A, Sastry S. 2002. Embedded software design and system integration for rotorcraft
UAV using platforms. Proceedings of the 15th Triennial World Congress of the International
Federation of Automatic Control. IFAC: World Congress on Automatic Control vol.
15.'
mla: Horowitz, Benjamin, et al. “Embedded Software Design and System Integration
for Rotorcraft UAV Using Platforms.” Proceedings of the 15th Triennial World
Congress of the International Federation of Automatic Control, vol. 15, no.
1, Elsevier, 2002, doi:10.3182/20020721-6-ES-1901.01628.
short: B. Horowitz, J. Liebman, C. Ma, T.J. Koo, T.A. Henzinger, A. Sangiovanni
Vincentelli, S. Sastry, in:, Proceedings of the 15th Triennial World Congress
of the International Federation of Automatic Control, Elsevier, 2002.
conference:
end_date: 2002-07-26
location: Barcelona, Spain
name: 'IFAC: World Congress on Automatic Control'
start_date: 2002-07-21
date_created: 2018-12-11T12:08:47Z
date_published: 2002-07-01T00:00:00Z
date_updated: 2023-06-05T09:55:10Z
day: '01'
doi: 10.3182/20020721-6-ES-1901.01628
extern: '1'
intvolume: ' 15'
issue: '1'
language:
- iso: eng
month: '07'
oa_version: None
publication: Proceedings of the 15th Triennial World Congress of the International
Federation of Automatic Control
publication_identifier:
issn:
- 1474-6670
publication_status: published
publisher: Elsevier
publist_id: '306'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Embedded software design and system integration for rotorcraft UAV using platforms
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 15
year: '2002'
...
---
_id: '4421'
abstract:
- lang: eng
text: We demonstrate the feasibility and benefits of Giotto-based control software
development by reimplementing the autopilot system of an autonomously flying model
helicopter. Giotto offers a clean separation between the platform-independent
concerns of software functionality and I/O timing, and the platform-dependent
concerns of software scheduling and execution. Functionality code such as code
computing control laws can be generated automatically from Simulink models or,
as in the case of this project, inherited from a legacy system. I/O timing code
is generated automatically from Giotto models that specify real-time requirements
such as task frequencies and actuator update rates. We extend Simulink to support
the design of Giotto models, and from these models, the automatic generation of
Giotto code that supervises the interaction of the functionality code with the
physical environment. The Giotto compiler performs a schedulability analysis on
the Giotto code, and generates timing code for the helicopter platform. The Giotto
methodology guarantees the stringent hard real-time requirements of the autopilot
system, and at the same time supports the automation of the software development
process in a way that produces a transparent software architecture with predictable
behavior and reusable components.
acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614,
the MARCO GSRC grant 98-DT-660, and the AFOSR MURI grant F49620-00-1-0327.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Marco
full_name: Sanvido, Marco
last_name: Sanvido
- 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: Wolfgang
full_name: Pree, Wolfgang
last_name: Pree
citation:
ama: 'Kirsch C, Sanvido M, Henzinger TA, Pree W. A Giotto-based helicopter control
system. In: Proceedings of the 2nd International Conference on Embedded Software.
Vol 2491. ACM; 2002:46-60. doi:10.1007/3-540-45828-X_5'
apa: 'Kirsch, C., Sanvido, M., Henzinger, T. A., & Pree, W. (2002). A Giotto-based
helicopter control system. In Proceedings of the 2nd International Conference
on Embedded Software (Vol. 2491, pp. 46–60). Grenoble, France: ACM. https://doi.org/10.1007/3-540-45828-X_5'
chicago: Kirsch, Christoph, Marco Sanvido, Thomas A Henzinger, and Wolfgang Pree.
“A Giotto-Based Helicopter Control System.” In Proceedings of the 2nd International
Conference on Embedded Software, 2491:46–60. ACM, 2002. https://doi.org/10.1007/3-540-45828-X_5.
ieee: C. Kirsch, M. Sanvido, T. A. Henzinger, and W. Pree, “A Giotto-based helicopter
control system,” in Proceedings of the 2nd International Conference on Embedded
Software, Grenoble, France, 2002, vol. 2491, pp. 46–60.
ista: 'Kirsch C, Sanvido M, Henzinger TA, Pree W. 2002. A Giotto-based helicopter
control system. Proceedings of the 2nd International Conference on Embedded Software.
EMSOFT: Embedded Software , LNCS, vol. 2491, 46–60.'
mla: Kirsch, Christoph, et al. “A Giotto-Based Helicopter Control System.” Proceedings
of the 2nd International Conference on Embedded Software, vol. 2491, ACM,
2002, pp. 46–60, doi:10.1007/3-540-45828-X_5.
short: C. Kirsch, M. Sanvido, T.A. Henzinger, W. Pree, in:, Proceedings of the 2nd
International Conference on Embedded Software, ACM, 2002, pp. 46–60.
conference:
end_date: 2002-10-09
location: Grenoble, France
name: 'EMSOFT: Embedded Software '
start_date: 2002-10-07
date_created: 2018-12-11T12:08:46Z
date_published: 2002-09-25T00:00:00Z
date_updated: 2023-06-05T13:07:20Z
day: '25'
doi: 10.1007/3-540-45828-X_5
extern: '1'
intvolume: ' 2491'
language:
- iso: eng
month: '09'
oa_version: None
page: 46 - 60
publication: Proceedings of the 2nd International Conference on Embedded Software
publication_identifier:
isbn:
- '9783540443070'
publication_status: published
publisher: ACM
publist_id: '310'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A Giotto-based helicopter control system
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2491
year: '2002'
...
---
_id: '4422'
abstract:
- lang: eng
text: "Behavioral properties of open systems can be formalized as objectives in
two-player games. Turn-based games model asynchronous interaction between the
players (the system and its environment) by interleaving their moves. Concurrent
games model synchronous interaction: the players always move simultaneously. Infinitary
winning criteria are considered: Büchi, co-Büchi, and more general parity conditions.
A generalization of determinacy for parity games to concurrent parity games demands
probabilistic (mixed) strategies: either player 1 has a mixed strategy to win
with probability 1 (almost-sure winning), or player 2 has a mixed strategy to
win with positive probability.\r\nThis work provides efficient reductions of concurrent
probabilistic Büchi and co-Büchi games to turn-based games with Büchi condition
and parity winning condition with three priorities, respectively. From a theoretical
point of view, the latter reduction shows that one can trade the probabilistic
nature of almost-sure winning for a more general parity (fairness) condition.
The reductions improve understanding of concurrent games and provide an alternative
simple proof of determinacy of concurrent Büchi and co-Büchi games. From a practical
point of view, the reductions turn solvers of turn-based games into solvers of
concurrent probabilistic games. Thus improvements in the well-studied algorithms
for the former carry over immediately to the latter. In particular, a recent improvement
in the complexity of solving turn-based parity games yields an improvement in
time complexity of solving concurrent probabilistic co-Büchi games from cubic
to quadratic."
acknowledgement: This research was supported in part by the Polish KBN grant 7-T11C-027-20,
the AFOSR MURI grant F49620-00-1-0327, and the NSF Theory grant CCR-9988172.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Jurdziński M, Kupferman O, Henzinger TA. Trading probability for fairness.
In: Proceedings of the 16th International Workshop on Computer Science Logic.
Vol 2471. Springer; 2002:292-305. doi:10.1007/3-540-45793-3_20'
apa: 'Jurdziński, M., Kupferman, O., & Henzinger, T. A. (2002). Trading probability
for fairness. In Proceedings of the 16th International Workshop on Computer
Science Logic (Vol. 2471, pp. 292–305). Edinburgh, Scotland: Springer. https://doi.org/10.1007/3-540-45793-3_20'
chicago: Jurdziński, Marcin, Orna Kupferman, and Thomas A Henzinger. “Trading Probability
for Fairness.” In Proceedings of the 16th International Workshop on Computer
Science Logic, 2471:292–305. Springer, 2002. https://doi.org/10.1007/3-540-45793-3_20.
ieee: M. Jurdziński, O. Kupferman, and T. A. Henzinger, “Trading probability for
fairness,” in Proceedings of the 16th International Workshop on Computer Science
Logic, Edinburgh, Scotland, 2002, vol. 2471, pp. 292–305.
ista: 'Jurdziński M, Kupferman O, Henzinger TA. 2002. Trading probability for fairness.
Proceedings of the 16th International Workshop on Computer Science Logic. CSL:
Computer Science Logic, LNCS, vol. 2471, 292–305.'
mla: Jurdziński, Marcin, et al. “Trading Probability for Fairness.” Proceedings
of the 16th International Workshop on Computer Science Logic, vol. 2471, Springer,
2002, pp. 292–305, doi:10.1007/3-540-45793-3_20.
short: M. Jurdziński, O. Kupferman, T.A. Henzinger, in:, Proceedings of the 16th
International Workshop on Computer Science Logic, Springer, 2002, pp. 292–305.
conference:
location: Edinburgh, Scotland
name: 'CSL: Computer Science Logic'
date_created: 2018-12-11T12:08:46Z
date_published: 2002-09-09T00:00:00Z
date_updated: 2023-06-05T10:02:54Z
day: '09'
doi: 10.1007/3-540-45793-3_20
extern: '1'
intvolume: ' 2471'
language:
- iso: eng
month: '09'
oa_version: None
page: 292 - 305
publication: Proceedings of the 16th International Workshop on Computer Science Logic
publication_identifier:
isbn:
- '9783540442400'
publication_status: published
publisher: Springer
publist_id: '308'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Trading probability for fairness
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2471
year: '2002'
...
---
_id: '4413'
abstract:
- lang: eng
text: 'An essential problem in component-based design is how to compose components
designed in isolation. Several approaches have been proposed for specifying component
interfaces that capture behavioral aspects such as interaction protocols, and
for verifying interface compatibility. Likewise, several approaches have been
developed for synthesizing converters between incompatible protocols. In this
paper, we introduce the notion of adaptability as the property that two interfaces
have when they can be made compatible by communicating through a converter that
meets specified requirements. We show that verifying adaptability and synthesizing
an appropriate converter are two faces of the same coin: adaptability can be formalized
and solved using a game-theoretic framework, and then the converter can be synthesized
as a strategy that always wins the game. Finally we show that this framework can
be related to the rectification problem in trace theory.'
acknowledgement: "The authors would like to thank Jerry Burch of the Cadence Berkeley
Labs for many insightful discussions and suggestions.\r\n"
article_processing_charge: No
author:
- first_name: Roberto
full_name: Passerone, Roberto
last_name: Passerone
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Alberto
full_name: Sangiovanni Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: 'Passerone R, De Alfaro L, Henzinger TA, Sangiovanni Vincentelli A. Convertibility
verification and converter synthesis: Two faces of the same coin. In: Proceedings
of the 11th IEEE/ACM International Conference on Computer-Aided Design. IEEE;
2002:132-139. doi:10.1145/774572.774592'
apa: 'Passerone, R., De Alfaro, L., Henzinger, T. A., & Sangiovanni Vincentelli,
A. (2002). Convertibility verification and converter synthesis: Two faces of the
same coin. In Proceedings of the 11th IEEE/ACM international conference on
Computer-aided design (pp. 132–139). San Jose, CA, USA: IEEE. https://doi.org/10.1145/774572.774592'
chicago: 'Passerone, Roberto, Luca De Alfaro, Thomas A Henzinger, and Alberto Sangiovanni
Vincentelli. “Convertibility Verification and Converter Synthesis: Two Faces of
the Same Coin.” In Proceedings of the 11th IEEE/ACM International Conference
on Computer-Aided Design, 132–39. IEEE, 2002. https://doi.org/10.1145/774572.774592.'
ieee: 'R. Passerone, L. De Alfaro, T. A. Henzinger, and A. Sangiovanni Vincentelli,
“Convertibility verification and converter synthesis: Two faces of the same coin,”
in Proceedings of the 11th IEEE/ACM international conference on Computer-aided
design, San Jose, CA, USA, 2002, pp. 132–139.'
ista: 'Passerone R, De Alfaro L, Henzinger TA, Sangiovanni Vincentelli A. 2002.
Convertibility verification and converter synthesis: Two faces of the same coin.
Proceedings of the 11th IEEE/ACM international conference on Computer-aided design.
ICCAD: Computer-Aided Design, 132–139.'
mla: 'Passerone, Roberto, et al. “Convertibility Verification and Converter Synthesis:
Two Faces of the Same Coin.” Proceedings of the 11th IEEE/ACM International
Conference on Computer-Aided Design, IEEE, 2002, pp. 132–39, doi:10.1145/774572.774592.'
short: R. Passerone, L. De Alfaro, T.A. Henzinger, A. Sangiovanni Vincentelli, in:,
Proceedings of the 11th IEEE/ACM International Conference on Computer-Aided Design,
IEEE, 2002, pp. 132–139.
conference:
end_date: 2002-11-14
location: San Jose, CA, USA
name: 'ICCAD: Computer-Aided Design'
start_date: 2002-11-10
date_created: 2018-12-11T12:08:44Z
date_published: 2002-11-01T00:00:00Z
date_updated: 2023-06-05T14:21:46Z
day: '01'
doi: 10.1145/774572.774592
extern: '1'
language:
- iso: eng
month: '11'
oa_version: None
page: 132 - 139
publication: Proceedings of the 11th IEEE/ACM international conference on Computer-aided
design
publication_identifier:
isbn:
- '9780780376076'
publication_status: published
publisher: IEEE
publist_id: '318'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Convertibility verification and converter synthesis: Two faces of the same
coin'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2002'
...
---
_id: '4262'
abstract:
- lang: eng
text: Natural populations are structured spatially into local populations and genetically
into diverse ‘genetic backgrounds’ defined by different combinations of selected
alleles. If selection maintains genetic backgrounds at constant frequency then
neutral diversity is enhanced. By contrast, if background frequencies fluctuate
then diversity is reduced. Provided that the population size of each background
is large enough, these effects can be described by the structured coalescent process.
Almost all the extant results based on the coalescent deal with a single selected
locus. Yet we know that very large numbers of genes are under selection and that
any substantial effects are likely to be due to the cumulative effects of many
loci. Here, we set up a general framework for the extension of the coalescent
to multilocus scenarios and we use it to study the simplest model, where strong
balancing selection acting on a set of n loci maintains 2n backgrounds at constant
frequencies and at linkage equilibrium. Analytical results show that the expected
linked neutral diversity increases exponentially with the number of selected loci
and can become extremely large. However, simulation results reveal that the structured
coalescent approach breaks down when the number of backgrounds approaches the
population size, because of stochastic fluctuations in background frequencies.
A new method is needed to extend the structured coalescent to cases with large
numbers of backgrounds.
acknowledgement: "We thank B. Charlesworth, D. Charlesworth and F. Depaulis for valuable
discussion and criticism. We are also\r\ngrateful to an anonymous reviewer, who
pointed out an imprecision in the original manuscript. This work was\r\nsupported
by the BBSRC."
article_processing_charge: No
article_type: original
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Arcadio
full_name: Navarro, Arcadio
last_name: Navarro
citation:
ama: 'Barton NH, Navarro A. Extending the coalescent to multilocus systems: the
case of balancing selection. Genetical Research. 2002;79(2):129-139. doi:10.1017/S0016672301005493'
apa: 'Barton, N. H., & Navarro, A. (2002). Extending the coalescent to multilocus
systems: the case of balancing selection. Genetical Research. Cambridge
University Press. https://doi.org/10.1017/S0016672301005493'
chicago: 'Barton, Nicholas H, and Arcadio Navarro. “Extending the Coalescent to
Multilocus Systems: The Case of Balancing Selection.” Genetical Research.
Cambridge University Press, 2002. https://doi.org/10.1017/S0016672301005493.'
ieee: 'N. H. Barton and A. Navarro, “Extending the coalescent to multilocus systems:
the case of balancing selection,” Genetical Research, vol. 79, no. 2. Cambridge
University Press, pp. 129–139, 2002.'
ista: 'Barton NH, Navarro A. 2002. Extending the coalescent to multilocus systems:
the case of balancing selection. Genetical Research. 79(2), 129–139.'
mla: 'Barton, Nicholas H., and Arcadio Navarro. “Extending the Coalescent to Multilocus
Systems: The Case of Balancing Selection.” Genetical Research, vol. 79,
no. 2, Cambridge University Press, 2002, pp. 129–39, doi:10.1017/S0016672301005493.'
short: N.H. Barton, A. Navarro, Genetical Research 79 (2002) 129–139.
date_created: 2018-12-11T12:07:55Z
date_published: 2002-05-23T00:00:00Z
date_updated: 2023-06-06T11:23:19Z
day: '23'
doi: 10.1017/S0016672301005493
extern: '1'
external_id:
pmid:
- '12073551'
intvolume: ' 79'
issue: '2'
language:
- iso: eng
month: '05'
oa_version: None
page: 129 - 139
pmid: 1
publication: Genetical Research
publication_identifier:
issn:
- 0016-6723
publication_status: published
publisher: Cambridge University Press
publist_id: '1832'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Extending the coalescent to multilocus systems: the case of balancing selection'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 79
year: '2002'
...
---
_id: '4260'
abstract:
- lang: eng
text: 'We calculate the fixation probability of a beneficial allele that arises
as the result of a unique mutation in an asexual population that is subject to
recurrent deleterious mutation at rate U. Our analysis is an extension of previous
works, which make a biologically restrictive assumption that selection against
deleterious alleles is stronger than that on the beneficial allele of interest.
We show that when selection against deleterious alleles is weak, beneficial alleles
that confer a selective advantage that is small relative to U have greatly reduced
probabilities of fixation. We discuss the consequences of this effect for the
distribution of effects of alleles fixed during adaptation. We show that a selective
sweep will increase the fixation probabilities of other beneficial mutations arising
during some short interval afterward. We use the calculated fixation probabilities
to estimate the expected rate of fitness improvement in an asexual population
when beneficial alleles arise continually at some low rate proportional to U.
We estimate the rate of mutation that is optimal in the sense that it maximizes
this rate of fitness improvement. Again, this analysis relaxes the assumption
made previously that selection against deleterious alleles is stronger than on
beneficial alleles. '
acknowledgement: "We thank Brian Charlesworth, Arcadi Navarro, Allen Orr, Sally Otto,
Mario Pineda-Krch, Rosie Redfield, Olivier Tenaillon, and two anonymous reviewers
for discussions and/or helpful comments on the\r\nmanuscript. T.J. is supported
by Wellcome Trust International Prize Travelling Research Fellowship no. 061530.
N.B. is supported by the Biotechnology and Biological Sciences Research Council
and by the Natural Environment Research Council."
article_processing_charge: No
article_type: original
author:
- first_name: Toby
full_name: Johnson, Toby
last_name: Johnson
- 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: Johnson T, Barton NH. The effect of deleterious alleles on adaptation in asexual
populations. Genetics. 2002;162(1):395-411. doi:10.1093/genetics/162.1.395
apa: Johnson, T., & Barton, N. H. (2002). The effect of deleterious alleles
on adaptation in asexual populations. Genetics. Genetics Society of America.
https://doi.org/10.1093/genetics/162.1.395
chicago: Johnson, Toby, and Nicholas H Barton. “The Effect of Deleterious Alleles
on Adaptation in Asexual Populations.” Genetics. Genetics Society of America,
2002. https://doi.org/10.1093/genetics/162.1.395.
ieee: T. Johnson and N. H. Barton, “The effect of deleterious alleles on adaptation
in asexual populations,” Genetics, vol. 162, no. 1. Genetics Society of
America, pp. 395–411, 2002.
ista: Johnson T, Barton NH. 2002. The effect of deleterious alleles on adaptation
in asexual populations. Genetics. 162(1), 395–411.
mla: Johnson, Toby, and Nicholas H. Barton. “The Effect of Deleterious Alleles on
Adaptation in Asexual Populations.” Genetics, vol. 162, no. 1, Genetics
Society of America, 2002, pp. 395–411, doi:10.1093/genetics/162.1.395.
short: T. Johnson, N.H. Barton, Genetics 162 (2002) 395–411.
date_created: 2018-12-11T12:07:54Z
date_published: 2002-09-01T00:00:00Z
date_updated: 2023-06-06T11:45:48Z
day: '01'
doi: 10.1093/genetics/162.1.395
extern: '1'
external_id:
pmid:
- '12242249'
intvolume: ' 162'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC1462245/
month: '09'
oa: 1
oa_version: None
page: 395 - 411
pmid: 1
publication: Genetics
publication_identifier:
issn:
- 0016-6731
publication_status: published
publisher: Genetics Society of America
publist_id: '1833'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The effect of deleterious alleles on adaptation in asexual populations
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 162
year: '2002'
...