---
_id: '4289'
abstract:
- lang: eng
text: A worldwide survey of polymorphic molecular markers shows that the human population
is genetically homogeneous, in close agreement with evidence from quite different
genes and traits.
article_processing_charge: No
article_type: letter_note
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: 'Barton NH. Population genetics: A new apportionment of human diversity. Current
Biology. 1997;7(12):757-758. doi:10.1016/S0960-9822(06)00397-6'
apa: 'Barton, N. H. (1997). Population genetics: A new apportionment of human diversity.
Current Biology. Cell Press. https://doi.org/10.1016/S0960-9822(06)00397-6'
chicago: 'Barton, Nicholas H. “Population Genetics: A New Apportionment of Human
Diversity.” Current Biology. Cell Press, 1997. https://doi.org/10.1016/S0960-9822(06)00397-6.'
ieee: 'N. H. Barton, “Population genetics: A new apportionment of human diversity,”
Current Biology, vol. 7, no. 12. Cell Press, pp. 757–758, 1997.'
ista: 'Barton NH. 1997. Population genetics: A new apportionment of human diversity.
Current Biology. 7(12), 757–758.'
mla: 'Barton, Nicholas H. “Population Genetics: A New Apportionment of Human Diversity.”
Current Biology, vol. 7, no. 12, Cell Press, 1997, pp. 757–58, doi:10.1016/S0960-9822(06)00397-6.'
short: N.H. Barton, Current Biology 7 (1997) 757–758.
date_created: 2018-12-11T12:08:04Z
date_published: 1997-12-01T00:00:00Z
date_updated: 2022-08-17T13:07:08Z
day: '01'
doi: 10.1016/S0960-9822(06)00397-6
extern: '1'
intvolume: ' 7'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0960982206003976?via%3Dihub
month: '12'
oa: 1
oa_version: Published Version
page: 757 - 758
publication: Current Biology
publication_identifier:
issn:
- 0960-9822
publication_status: published
publisher: Cell Press
publist_id: '1788'
quality_controlled: '1'
status: public
title: 'Population genetics: A new apportionment of human diversity'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 7
year: '1997'
...
---
_id: '4290'
article_processing_charge: No
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Barton NH. Natural hybridization and evolution. Genetical Research.
1997;70(2):178-180.
apa: Barton, N. H. (1997). Natural hybridization and evolution. Genetical Research.
Cambridge University Press.
chicago: Barton, Nicholas H. “Natural Hybridization and Evolution.” Genetical
Research. Cambridge University Press, 1997.
ieee: N. H. Barton, “Natural hybridization and evolution,” Genetical Research,
vol. 70, no. 2. Cambridge University Press, pp. 178–180, 1997.
ista: Barton NH. 1997. Natural hybridization and evolution. Genetical Research.
70(2), 178–180.
mla: Barton, Nicholas H. “Natural Hybridization and Evolution.” Genetical Research,
vol. 70, no. 2, Cambridge University Press, 1997, pp. 178–80.
short: N.H. Barton, Genetical Research 70 (1997) 178–180.
date_created: 2018-12-11T12:08:04Z
date_published: 1997-10-01T00:00:00Z
date_updated: 2022-08-17T14:10:20Z
day: '01'
extern: '1'
intvolume: ' 70'
issue: '2'
language:
- iso: eng
month: '10'
oa_version: None
page: 178 - 180
publication: Genetical Research
publication_identifier:
issn:
- 0016-6723
publication_status: published
publisher: Cambridge University Press
publist_id: '1789'
status: public
title: Natural hybridization and evolution
type: review
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 70
year: '1997'
...
---
_id: '4291'
article_processing_charge: No
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: 'Barton NH. The ecological detective: Confronting models with data. Genetical
Research. 1997;70(2):180-181.'
apa: 'Barton, N. H. (1997). The ecological detective: Confronting models with data.
Genetical Research. Cambridge University Press.'
chicago: 'Barton, Nicholas H. “The Ecological Detective: Confronting Models with
Data.” Genetical Research. Cambridge University Press, 1997.'
ieee: 'N. H. Barton, “The ecological detective: Confronting models with data,” Genetical
Research, vol. 70, no. 2. Cambridge University Press, pp. 180–181, 1997.'
ista: 'Barton NH. 1997. The ecological detective: Confronting models with data.
Genetical Research. 70(2), 180–181.'
mla: 'Barton, Nicholas H. “The Ecological Detective: Confronting Models with Data.”
Genetical Research, vol. 70, no. 2, Cambridge University Press, 1997, pp.
180–81.'
short: N.H. Barton, Genetical Research 70 (1997) 180–181.
date_created: 2018-12-11T12:08:04Z
date_published: 1997-10-01T00:00:00Z
date_updated: 2022-08-18T09:36:25Z
day: '01'
extern: '1'
intvolume: ' 70'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://www.cambridge.org/core/journals/genetics-research/article/ecological-detective-confronting-models-with-data-by-ray-hilborn-and-marc-mangel-princeton-university-press-1997-315xvii-pages-price-3000-cloth-1695-paper-isbn-0-691-03496-6-0-691-03497-4-pbk/AA6FCD668DFFAEF537C2674ECCFC8966
month: '10'
oa_version: None
page: 180 - 181
publication: Genetical Research
publication_identifier:
issn:
- 0016-6723
publication_status: published
publisher: Cambridge University Press
publist_id: '1790'
quality_controlled: '1'
status: public
title: 'The ecological detective: Confronting models with data'
type: review
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 70
year: '1997'
...
---
_id: '4293'
abstract:
- lang: eng
text: Natural populations differ from the simplest models in ways which can significantly
affect their evolution. Real populations are rarely all of the same size; the
rates of migration into and out of populations vary in space and time; some populations
go extinct, and new ones are established, while all populations fluctuate in size.
Furthermore, the genetic properties of real species are not like those assumed
in simple models. Alleles are exposed to a wide variety of selection mutation
rarely creates novel genotypes with each mutation event, generations overlap,
and environments vary from place to place. Evolution in a metapopulation can be
substantially different from the predictions of single-population models and,
indeed, very different from the simplest models of subdivided species.
article_processing_charge: No
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: Michael
full_name: Whitlock, Michael
last_name: Whitlock
citation:
ama: 'Barton NH, Whitlock M. The evolution of metapopulations. In: Hanski I, Gilpin
ME, eds. Metapopulation Biology. Academic Press; 1997:183-210. doi:10.1016/B978-012323445-2/50012-2'
apa: Barton, N. H., & Whitlock, M. (1997). The evolution of metapopulations.
In I. Hanski & M. E. Gilpin (Eds.), Metapopulation Biology (pp. 183–210).
Academic Press. https://doi.org/10.1016/B978-012323445-2/50012-2
chicago: Barton, Nicholas H, and Michael Whitlock. “The Evolution of Metapopulations.”
In Metapopulation Biology, edited by Illka Hanski and Michael E. Gilpin,
183–210. Academic Press, 1997. https://doi.org/10.1016/B978-012323445-2/50012-2.
ieee: N. H. Barton and M. Whitlock, “The evolution of metapopulations,” in Metapopulation
Biology, I. Hanski and M. E. Gilpin, Eds. Academic Press, 1997, pp. 183–210.
ista: 'Barton NH, Whitlock M. 1997.The evolution of metapopulations. In: Metapopulation
Biology. , 183–210.'
mla: Barton, Nicholas H., and Michael Whitlock. “The Evolution of Metapopulations.”
Metapopulation Biology, edited by Illka Hanski and Michael E. Gilpin, Academic
Press, 1997, pp. 183–210, doi:10.1016/B978-012323445-2/50012-2.
short: N.H. Barton, M. Whitlock, in:, I. Hanski, M.E. Gilpin (Eds.), Metapopulation
Biology, Academic Press, 1997, pp. 183–210.
date_created: 2018-12-11T12:08:05Z
date_published: 1997-03-12T00:00:00Z
date_updated: 2022-08-17T12:47:42Z
day: '12'
doi: 10.1016/B978-012323445-2/50012-2
editor:
- first_name: Illka
full_name: Hanski, Illka
last_name: Hanski
- first_name: Michael E.
full_name: Gilpin, Michael E.
last_name: Gilpin
extern: '1'
language:
- iso: eng
month: '03'
oa_version: None
page: 183 - 210
publication: Metapopulation Biology
publication_identifier:
isbn:
- '9780123234452'
publication_status: published
publisher: Academic Press
publist_id: '1782'
quality_controlled: '1'
status: public
title: The evolution of metapopulations
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1997'
...
---
_id: '4438'
abstract:
- lang: eng
text: "In temporal-logic model checking, we verify the correctness of a program
with respect to a desired behavior by checking whether a structure that models
the program satisfies a temporal-logic formula that specifies the behavior. The
model-checking problem for the branching-time temporal logic CTL can be solved
in linear running time, and model-checking tools for CTL are used successfully
in industrial applications. The development of programs that must meet rigid real-time
constraints has brought with it a need for real-time temporal logics that enable
quantitative reference to time. Early research on real-time temporal logics uses
the discrete domain of the integers to model time. Present research on real-time
temporal logics focuses on continuous time and uses the dense domain of the reals
to model time. There, model checking becomes significantly more complicated. For
example, the model-checking problem for TCTL, a continuous-time extension of the
logic CTL, is PSPACE-complete.\r\nIn this paper we suggest a reduction from TCTL
model checking to CTL model checking. The contribution of such a reduction is
twofold. Theoretically, while it has long been known that model-checking methods
for untimed temporal logics can be extended quite easily to handle discrete time,
it was not clear whether and how untimed methods can handle the reset quantifier
of TCTL, which resets a realvalued clock. Practically, our reduction enables anyone
who has a tool for CTL model checking to use it for TCTL model checking. The TCTL
model-checking algorithm that follows from our reduction is in PSPACE, matching
the known bound for this problem. In addition, it enjoys the wide distribution
of CTL model-checking tools and the extensive and fruitful research efforts and
heuristics that have been put into these tools."
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the SRC contract 95-DC-324.036.
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: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Henzinger TA, Kupferman O. From quantity to quality. In: Proceedings of
the 5th International Workshop on Hybrid and Real-Time Systems. Vol 1201.
Springer; 1997:48-62. doi:10.1007/BFb0014712'
apa: 'Henzinger, T. A., & Kupferman, O. (1997). From quantity to quality. In
Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems
(Vol. 1201, pp. 48–62). Grenoble, France: Springer. https://doi.org/10.1007/BFb0014712'
chicago: Henzinger, Thomas A, and Orna Kupferman. “From Quantity to Quality.” In
Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems,
1201:48–62. Springer, 1997. https://doi.org/10.1007/BFb0014712.
ieee: T. A. Henzinger and O. Kupferman, “From quantity to quality,” in Proceedings
of the 5th International Workshop on Hybrid and Real-Time Systems, Grenoble,
France, 1997, vol. 1201, pp. 48–62.
ista: 'Henzinger TA, Kupferman O. 1997. From quantity to quality. Proceedings of
the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid and
Real-Time Systems, LNCS, vol. 1201, 48–62.'
mla: Henzinger, Thomas A., and Orna Kupferman. “From Quantity to Quality.” Proceedings
of the 5th International Workshop on Hybrid and Real-Time Systems, vol. 1201,
Springer, 1997, pp. 48–62, doi:10.1007/BFb0014712.
short: T.A. Henzinger, O. Kupferman, in:, Proceedings of the 5th International Workshop
on Hybrid and Real-Time Systems, Springer, 1997, pp. 48–62.
conference:
end_date: 1997-03-28
location: Grenoble, France
name: 'HART: Hybrid and Real-Time Systems'
start_date: 1997-03-26
date_created: 2018-12-11T12:08:51Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T12:29:48Z
day: '01'
doi: 10.1007/BFb0014712
extern: '1'
intvolume: ' 1201'
language:
- iso: eng
month: '01'
oa_version: None
page: 48 - 62
publication: Proceedings of the 5th International Workshop on Hybrid and Real-Time
Systems
publication_identifier:
isbn:
- '9783540626008'
publication_status: published
publisher: Springer
publist_id: '291'
quality_controlled: '1'
scopus_import: '1'
status: public
title: From quantity to quality
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1201
year: '1997'
...
---
_id: '4441'
abstract:
- lang: eng
text: Rectangular hybrid automata model digital control programs of analog plant
environments. We study rectangular hybrid automata where the plant state evolves
continuously in real-numbered time, and the controller samples the plant state
and changes the control state discretely, only at the integer points in time.
We prove that rectangular hybrid automata have finite bisimilarity quotients when
all control transitions happen at integer times, even if the constraints on the
derivatives of the variables vary between control states. This is sharply in contrast
with the conventional model where control transitions may happen at any real time,
and already the reachability problem is undecidable. Based on the finite bisimilarity
quotients, we give an exponential algorithm for the symbolic sampling-controller
synthesis of rectangular automata. We show our algorithm to be optimal by proving
the problem to be EXPTIME-hard. We also show that rectangular automata form a
maximal class of systems for which the sampling-controller synthesis problem can
be solved algorithmically.
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI contract DAAH-04-96-1-0341, by the ARO
contract DAAL03-91-C-0027 through the MSI at Cornell University, by the ARPA grant
NAG2-892, and by the SRC contract 95-DC-324.036.
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: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: 'Henzinger TA, Kopke P. Discrete-time control for rectangular hybrid automata.
In: Proceedings of the 24th International Colloquium on Automata, Languages
and Programming. Vol 1256. Springer; 1997:582-593. doi:10.1007/3-540-63165-8_213'
apa: 'Henzinger, T. A., & Kopke, P. (1997). Discrete-time control for rectangular
hybrid automata. In Proceedings of the 24th International Colloquium on Automata,
Languages and Programming (Vol. 1256, pp. 582–593). Bologna, Italy: Springer.
https://doi.org/10.1007/3-540-63165-8_213'
chicago: Henzinger, Thomas A, and Peter Kopke. “Discrete-Time Control for Rectangular
Hybrid Automata.” In Proceedings of the 24th International Colloquium on Automata,
Languages and Programming, 1256:582–93. Springer, 1997. https://doi.org/10.1007/3-540-63165-8_213.
ieee: T. A. Henzinger and P. Kopke, “Discrete-time control for rectangular hybrid
automata,” in Proceedings of the 24th International Colloquium on Automata,
Languages and Programming, Bologna, Italy, 1997, vol. 1256, pp. 582–593.
ista: 'Henzinger TA, Kopke P. 1997. Discrete-time control for rectangular hybrid
automata. Proceedings of the 24th International Colloquium on Automata, Languages
and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 1256,
582–593.'
mla: Henzinger, Thomas A., and Peter Kopke. “Discrete-Time Control for Rectangular
Hybrid Automata.” Proceedings of the 24th International Colloquium on Automata,
Languages and Programming, vol. 1256, Springer, 1997, pp. 582–93, doi:10.1007/3-540-63165-8_213.
short: T.A. Henzinger, P. Kopke, in:, Proceedings of the 24th International Colloquium
on Automata, Languages and Programming, Springer, 1997, pp. 582–593.
conference:
end_date: 1997-07-11
location: Bologna, Italy
name: 'ICALP: Automata, Languages and Programming'
start_date: 1997-07-07
date_created: 2018-12-11T12:08:52Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T12:04:15Z
day: '01'
doi: 10.1007/3-540-63165-8_213
extern: '1'
intvolume: ' 1256'
language:
- iso: eng
month: '01'
oa_version: None
page: 582 - 593
publication: Proceedings of the 24th International Colloquium on Automata, Languages
and Programming
publication_identifier:
isbn:
- '9783540631651'
publication_status: published
publisher: Springer
publist_id: '289'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discrete-time control for rectangular hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1256
year: '1997'
...
---
_id: '4493'
abstract:
- lang: eng
text: A hybrid system is a dynamical system whose behavior exhibits both discrete
and continuous change. A hybrid automaton is a mathematical model for hybrid systems,
which combines, in a single formalism, automaton transitions for capturing discrete
change with differential equations for capturing continuous change. HyTech is
a symbolic model checker for linear hybrid automata, a subclass of hybrid automata
that can be analyzed automatically by computing with polyhedral state sets. A
key feature of HyTech is its ability to perform parametric analysis, i.e., to
determine the values of design parameters for which a linear hybrid automaton
satisfies a temporal-logic requirement.
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
the NSF CAREER award CCR-501708, NSF grant CCR-9504469, AFOSR contract F49620-93-1-0056,
ARO MURI grant DAAH-04-96-1-0341, ARPA grant AG2-892, and SRC contract 95-DC-324.036.
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: Pei
full_name: Ho, Pei
last_name: Ho
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Henzinger TA, Ho P, Wong Toi H. HyTech: A model checker for hybrid systems.
Software Tools For Technology Transfer. 1997;1(1-2):110-122. doi:10.1007/s100090050008'
apa: 'Henzinger, T. A., Ho, P., & Wong Toi, H. (1997). HyTech: A model checker
for hybrid systems. Software Tools For Technology Transfer. Springer. https://doi.org/10.1007/s100090050008'
chicago: 'Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: A Model Checker
for Hybrid Systems.” Software Tools For Technology Transfer. Springer,
1997. https://doi.org/10.1007/s100090050008.'
ieee: 'T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: A model checker for hybrid
systems,” Software Tools For Technology Transfer, vol. 1, no. 1–2. Springer,
pp. 110–122, 1997.'
ista: 'Henzinger TA, Ho P, Wong Toi H. 1997. HyTech: A model checker for hybrid
systems. Software Tools For Technology Transfer. 1(1–2), 110–122.'
mla: 'Henzinger, Thomas A., et al. “HyTech: A Model Checker for Hybrid Systems.”
Software Tools For Technology Transfer, vol. 1, no. 1–2, Springer, 1997,
pp. 110–22, doi:10.1007/s100090050008.'
short: T.A. Henzinger, P. Ho, H. Wong Toi, Software Tools For Technology Transfer
1 (1997) 110–122.
date_created: 2018-12-11T12:09:08Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T11:14:15Z
day: '01'
doi: 10.1007/s100090050008
extern: '1'
intvolume: ' 1'
issue: 1-2
language:
- iso: eng
month: '01'
oa_version: None
page: 110 - 122
publication: Software Tools For Technology Transfer
publication_identifier:
issn:
- 1433-2779
publication_status: published
publisher: Springer
publist_id: '236'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'HyTech: A model checker for hybrid systems'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1
year: '1997'
...
---
_id: '4494'
abstract:
- lang: eng
text: A hybrid system consists of a collection of digital programs that interact
with each other and with an analog environment. Examples of hybrid systems include
medical equipment, manufacturing controllers, automotive controllers, and robots.
The formal analysis of the mixed digital-analog nature of these systems requires
a model that incorporates the discrete behavior of computer programs with the
continuous behavior of environment variables, such as temperature and pressure.
Hybrid automata capture both types of behavior by combining finite automata with
differential inclusions (i.e. differential inequalities). HyTech is a symbolic
model checker for linear hybrid automata, an expressive, yet automatically analyzable,
subclass of hybrid automata. A key feature of HyTech is its ability to perform
parametric analysis, i.e. to determine the values of design parameters for which
a linear hybrid automaton satisfies a temporal requirement.
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the SRC contract 95-DC-324.036.
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: Pei
full_name: Ho, Pei
last_name: Ho
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Henzinger TA, Ho P, Wong Toi H. HyTech: A model checker for hybrid systems.
In: Vol 1254. Springer; 1997:460-463. doi:10.1007/3-540-63166-6_48'
apa: 'Henzinger, T. A., Ho, P., & Wong Toi, H. (1997). HyTech: A model checker
for hybrid systems (Vol. 1254, pp. 460–463). Presented at the CAV: Computer Aided
Verification, Haifa, Israel: Springer. https://doi.org/10.1007/3-540-63166-6_48'
chicago: 'Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: A Model Checker
for Hybrid Systems,” 1254:460–63. Springer, 1997. https://doi.org/10.1007/3-540-63166-6_48.'
ieee: 'T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: A model checker for hybrid
systems,” presented at the CAV: Computer Aided Verification, Haifa, Israel, 1997,
vol. 1254, pp. 460–463.'
ista: 'Henzinger TA, Ho P, Wong Toi H. 1997. HyTech: A model checker for hybrid
systems. CAV: Computer Aided Verification, LNCS, vol. 1254, 460–463.'
mla: 'Henzinger, Thomas A., et al. HyTech: A Model Checker for Hybrid Systems.
Vol. 1254, Springer, 1997, pp. 460–63, doi:10.1007/3-540-63166-6_48.'
short: T.A. Henzinger, P. Ho, H. Wong Toi, in:, Springer, 1997, pp. 460–463.
conference:
end_date: 1997-06-25
location: Haifa, Israel
name: 'CAV: Computer Aided Verification'
start_date: 1997-06-22
date_created: 2018-12-11T12:09:08Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T11:06:13Z
day: '01'
doi: 10.1007/3-540-63166-6_48
extern: '1'
intvolume: ' 1254'
language:
- iso: eng
month: '01'
oa_version: None
page: 460 - 463
publication_identifier:
isbn:
- '9783540631668'
publication_status: published
publisher: Springer
publist_id: '235'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'HyTech: A model checker for hybrid systems'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1254
year: '1997'
...
---
_id: '4496'
abstract:
- lang: eng
text: 'The simulation preorder for labeled transition systems is defined locally
as a game that relates states with their immediate successor states. 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 extend the local definition of simulation to account for fairness: system S
fairly simulates system I iff in the simulation game, there is a strategy that
matches with each fair computation of I a fair computation of S. Our definition
enjoys a fully abstract semantics and has a logical characterization: S fairly
simulates I iff every fair computation tree embedded in the unrolling of I can
be embedded also in the unrolling of S or, equivalently, iff every Fair-AFMC formula
satisfied by I is satisfied also by S (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 efficientlycomputable local criterion for proving linear-time abstraction
hierarchies.'
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the SRC contract 95-DC-324.036.
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: 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. In: Proceedings
of the 8th International Conference on Concurrency Theory. Vol 1243. Springer;
1997:273-287. doi:10.1007/3-540-63141-0_19'
apa: 'Henzinger, T. A., Kupferman, O., & Rajamani, S. (1997). Fair simulation.
In Proceedings of the 8th International Conference on Concurrency Theory
(Vol. 1243, pp. 273–287). Warsaw, Poland: Springer. https://doi.org/10.1007/3-540-63141-0_19'
chicago: Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.”
In Proceedings of the 8th International Conference on Concurrency Theory,
1243:273–87. Springer, 1997. https://doi.org/10.1007/3-540-63141-0_19.
ieee: T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” in Proceedings
of the 8th International Conference on Concurrency Theory, Warsaw, Poland,
1997, vol. 1243, pp. 273–287.
ista: 'Henzinger TA, Kupferman O, Rajamani S. 1997. Fair simulation. Proceedings
of the 8th International Conference on Concurrency Theory. CONCUR: Concurrency
Theory, LNCS, vol. 1243, 273–287.'
mla: Henzinger, Thomas A., et al. “Fair Simulation.” Proceedings of the 8th International
Conference on Concurrency Theory, vol. 1243, Springer, 1997, pp. 273–87, doi:10.1007/3-540-63141-0_19.
short: T.A. Henzinger, O. Kupferman, S. Rajamani, in:, Proceedings of the 8th International
Conference on Concurrency Theory, Springer, 1997, pp. 273–287.
conference:
end_date: 1997-07-04
location: Warsaw, Poland
name: 'CONCUR: Concurrency Theory'
start_date: 1997-07-01
date_created: 2018-12-11T12:09:09Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T09:09:13Z
day: '01'
doi: 10.1007/3-540-63141-0_19
extern: '1'
intvolume: ' 1243'
language:
- iso: eng
month: '01'
oa_version: None
page: 273 - 287
publication: Proceedings of the 8th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540631415'
publication_status: published
publisher: Springer
publist_id: '234'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fair simulation
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1243
year: '1997'
...
---
_id: '4520'
abstract:
- lang: eng
text: 'We define robust timed automata, which are timed automata that accept all
trajectories robustly: if a robust timed automaton accepts a trajectory, then
it must accept neighboring trajectories also; and if a robust timed automaton
rejects a trajectory, then it must reject neighboring trajectories also. We show
that the emptiness problem for robust timed automata is still decidable, by modifying
the region construction for timed automata. We then show that, like timed automata,
robust timed automata cannot be determinized. This result is somewhat unexpected,
given that in temporal logic, the removal of realtime equality constraints is
known to lead to a decidable theory that is closed under all boolean operations.'
acknowledgement: The first and third author were supported in part by grants from
ARPA and ONR. The second author was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the SRC contract 95-DC-324.036. The third author was also
supported by the NSF.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Vineet
full_name: Gupta, Vineet
last_name: Gupta
- 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: Radha
full_name: Jagadeesan, Radha
last_name: Jagadeesan
citation:
ama: 'Gupta V, Henzinger TA, Jagadeesan R. Robust timed automata. In: Proceedings
of the 5th International Workshop on Hybrid and Real-Time Systems. Vol 1201.
Springer; 1997:331-345. doi:10.1007/BFb0014736'
apa: 'Gupta, V., Henzinger, T. A., & Jagadeesan, R. (1997). Robust timed automata.
In Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems
(Vol. 1201, pp. 331–345). Grenoble, France: Springer. https://doi.org/10.1007/BFb0014736'
chicago: Gupta, Vineet, Thomas A Henzinger, and Radha Jagadeesan. “Robust Timed
Automata.” In Proceedings of the 5th International Workshop on Hybrid and Real-Time
Systems, 1201:331–45. Springer, 1997. https://doi.org/10.1007/BFb0014736.
ieee: V. Gupta, T. A. Henzinger, and R. Jagadeesan, “Robust timed automata,” in
Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems,
Grenoble, France, 1997, vol. 1201, pp. 331–345.
ista: 'Gupta V, Henzinger TA, Jagadeesan R. 1997. Robust timed automata. Proceedings
of the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid
and Real-Time Systems, LNCS, vol. 1201, 331–345.'
mla: Gupta, Vineet, et al. “Robust Timed Automata.” Proceedings of the 5th International
Workshop on Hybrid and Real-Time Systems, vol. 1201, Springer, 1997, pp. 331–45,
doi:10.1007/BFb0014736.
short: V. Gupta, T.A. Henzinger, R. Jagadeesan, in:, Proceedings of the 5th International
Workshop on Hybrid and Real-Time Systems, Springer, 1997, pp. 331–345.
conference:
end_date: 1997-03-28
location: Grenoble, France
name: 'HART: Hybrid and Real-Time Systems'
start_date: 1997-03-26
date_created: 2018-12-11T12:09:17Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T09:04:39Z
day: '01'
doi: 10.1007/BFb0014736
extern: '1'
intvolume: ' 1201'
language:
- iso: eng
month: '01'
oa_version: None
page: 331 - 345
publication: Proceedings of the 5th International Workshop on Hybrid and Real-Time
Systems
publication_identifier:
isbn:
- '9783540626008'
publication_status: published
publisher: Springer
publist_id: '207'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Robust timed automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1201
year: '1997'
...
---
_id: '4583'
abstract:
- lang: eng
text: In a trace-based world, the modular specification, verification, and control
of live systems require each module to be receptive; that is, each module must
be able to meet its liveness assumptions no matter how the other modules behave.
In a real-time world, liveness is automatically present in the form of diverging
time. The receptiveness condition, then, translates to the requirement that a
module must be able to let time diverge no matter how the environment behaves.
We study the receptiveness condition for real-time systems by extending the model
of reactive modules to timed and hybrid modules. We define the receptiveness of
such a module as the existence of a winning strategy in a game of the module against
its environment. By solving the game on region graphs, we present an (optimal)
Exptime algorithm for checking the receptiveness of prepositional timed modules.
By giving a fixpoint characterization of the game, we present a symbolic procedure
for checking the receptiveness of linear hybrid modules. Finally, we present an
assume-guarantee principle for reasoning about timed and hybrid modules, and a
method for synthesizing receptive controllers of timed and hybrid modules.
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the SRC contract 95-DC-324.036.
alternative_title:
- LNCS
article_processing_charge: No
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
citation:
ama: 'Alur R, Henzinger TA. Modularity for timed and hybrid systems. In: 8th
International Conference on Concurrency Theory. Vol 1243. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 1997:74-88. doi:10.1007/3-540-63141-0_6'
apa: 'Alur, R., & Henzinger, T. A. (1997). Modularity for timed and hybrid systems.
In 8th International Conference on Concurrency Theory (Vol. 1243, pp. 74–88).
Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-63141-0_6'
chicago: Alur, Rajeev, and Thomas A Henzinger. “Modularity for Timed and Hybrid
Systems.” In 8th International Conference on Concurrency Theory, 1243:74–88.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997. https://doi.org/10.1007/3-540-63141-0_6.
ieee: R. Alur and T. A. Henzinger, “Modularity for timed and hybrid systems,” in
8th International Conference on Concurrency Theory, Warsaw, Poland, 1997,
vol. 1243, pp. 74–88.
ista: 'Alur R, Henzinger TA. 1997. Modularity for timed and hybrid systems. 8th
International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS,
vol. 1243, 74–88.'
mla: Alur, Rajeev, and Thomas A. Henzinger. “Modularity for Timed and Hybrid Systems.”
8th International Conference on Concurrency Theory, vol. 1243, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 1997, pp. 74–88, doi:10.1007/3-540-63141-0_6.
short: R. Alur, T.A. Henzinger, in:, 8th International Conference on Concurrency
Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997, pp. 74–88.
conference:
end_date: 1997-07-04
location: Warsaw, Poland
name: 'CONCUR: Concurrency Theory'
start_date: 1997-07-01
date_created: 2018-12-11T12:09:36Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T08:47:55Z
day: '01'
doi: 10.1007/3-540-63141-0_6
extern: '1'
intvolume: ' 1243'
language:
- iso: eng
month: '01'
oa_version: None
page: 74 - 88
publication: 8th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540691884'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '124'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Modularity for timed and hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1243
year: '1997'
...
---
_id: '4584'
abstract:
- lang: eng
text: This paper introduces, gently but rigorously, the clock approach to real-time
programming. We present with mathematical precision, assuming no prerequisites
other than familiarity with logical and programming notations, the concepts that
are necessary for understanding, writing, and executing clock programs. In keeping
with an expository style, all references are clustered in bibliographic remarks
at the end of each section. The first appendix presents proof rules for verifying
temporal properties of clock programs. The second appendix points to selected
literature on formal methods and tools for programming with clocks. In particular,
the timed automaton, which is a finite-state machine equipped with clocks, has
become a standard paradigm for real-time model checking; it underlies the tools
HyTech, Kronos, and Uppaal, which are discussed elsewhere in this volume.
acknowledgement: The authors thank Rance Cleaveland, Limor Fix, David Karr, Peter
Kopke, Fred Schneider, and Bernhard Steffen for helpful comments.
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
citation:
ama: Alur R, Henzinger TA. Real-time system = discrete system + clock variables.
Software Tools For Technology Transfer. 1997;1(1-2):86-109. doi:10.1007/s100090050007
apa: Alur, R., & Henzinger, T. A. (1997). Real-time system = discrete system
+ clock variables. Software Tools For Technology Transfer. Springer. https://doi.org/10.1007/s100090050007
chicago: Alur, Rajeev, and Thomas A Henzinger. “Real-Time System = Discrete System
+ Clock Variables.” Software Tools For Technology Transfer. Springer, 1997.
https://doi.org/10.1007/s100090050007.
ieee: R. Alur and T. A. Henzinger, “Real-time system = discrete system + clock variables,”
Software Tools For Technology Transfer, vol. 1, no. 1–2. Springer, pp.
86–109, 1997.
ista: Alur R, Henzinger TA. 1997. Real-time system = discrete system + clock variables.
Software Tools For Technology Transfer. 1(1–2), 86–109.
mla: Alur, Rajeev, and Thomas A. Henzinger. “Real-Time System = Discrete System
+ Clock Variables.” Software Tools For Technology Transfer, vol. 1, no.
1–2, Springer, 1997, pp. 86–109, doi:10.1007/s100090050007.
short: R. Alur, T.A. Henzinger, Software Tools For Technology Transfer 1 (1997)
86–109.
date_created: 2018-12-11T12:09:36Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-17T08:27:20Z
day: '01'
doi: 10.1007/s100090050007
extern: '1'
intvolume: ' 1'
issue: 1-2
language:
- iso: eng
month: '01'
oa_version: None
page: 86 - 109
publication: Software Tools For Technology Transfer
publication_identifier:
issn:
- 1433-2779
publication_status: published
publisher: Springer
publist_id: '123'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Real-time system = discrete system + clock variables
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1
year: '1997'
...
---
_id: '4605'
abstract:
- lang: eng
text: A hybrid system is a dynamical system whose behavior exhibits both discrete
and continuous change. A hybrid automaton is a mathematical model for hybrid systems,
which combines, in a single formalism, automaton transitions for capturing discrete
change with differential equations for capturing continuous change. In this survey,
we demonstrate symbolic algorithms for the verification of and controller synthesis
for linear hybrid automata, a subclass of hybrid automata that can be analyzed
automatically
article_processing_charge: No
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: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Alur R, Henzinger TA, Wong Toi H. Symbolic analysis of hybrid systems. In:
Proceedings of the 36th IEEE Conference on Decision and Control. IEEE;
1997:702-707. doi:10.1109/CDC.1997.650717
'
apa: 'Alur, R., Henzinger, T. A., & Wong Toi, H. (1997). Symbolic analysis of
hybrid systems. In Proceedings of the 36th IEEE Conference on Decision and
Control (pp. 702–707). San Diego, CA, USA: IEEE. https://doi.org/10.1109/CDC.1997.650717 '
chicago: Alur, Rajeev, Thomas A Henzinger, and Howard Wong Toi. “Symbolic Analysis
of Hybrid Systems.” In Proceedings of the 36th IEEE Conference on Decision
and Control, 702–7. IEEE, 1997. https://doi.org/10.1109/CDC.1997.650717 .
ieee: R. Alur, T. A. Henzinger, and H. Wong Toi, “Symbolic analysis of hybrid systems,”
in Proceedings of the 36th IEEE Conference on Decision and Control, San
Diego, CA, USA, 1997, pp. 702–707.
ista: 'Alur R, Henzinger TA, Wong Toi H. 1997. Symbolic analysis of hybrid systems.
Proceedings of the 36th IEEE Conference on Decision and Control. CDC: Decision
and Control, 702–707.'
mla: Alur, Rajeev, et al. “Symbolic Analysis of Hybrid Systems.” Proceedings
of the 36th IEEE Conference on Decision and Control, IEEE, 1997, pp. 702–07,
doi:10.1109/CDC.1997.650717
.
short: R. Alur, T.A. Henzinger, H. Wong Toi, in:, Proceedings of the 36th IEEE Conference
on Decision and Control, IEEE, 1997, pp. 702–707.
conference:
end_date: 1997-12-12
location: San Diego, CA, USA
name: 'CDC: Decision and Control'
start_date: 1997-12-12
date_created: 2018-12-11T12:09:43Z
date_published: 1997-12-01T00:00:00Z
date_updated: 2022-08-17T08:08:36Z
day: '01'
doi: '10.1109/CDC.1997.650717 '
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 702 - 707
publication: Proceedings of the 36th IEEE Conference on Decision and Control
publication_identifier:
isbn:
- '0780341872'
publication_status: published
publisher: IEEE
publist_id: '101'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic analysis of hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1997'
...
---
_id: '4607'
abstract:
- lang: eng
text: We present a verification algorithm for duration properties of real-time systems.
While simple real-time properties constrain the total elapsed time between events,
duration properties constrain the accumulated satisfaction time of state predicates.
We formalize the concept of durations by introducing duration measures for timed
automata. A duration measure assigns to each finite run of a timed automaton a
real number —the duration of the run— which may be the accumulated satisfaction
time of a state predicate along the run. Given a timed automaton with a duration
measure, an initial and a final state, and an arithmetic constraint, the duration-bounded
reachability problem asks if there is a run of the automaton from the initial
state to the final state such that the duration of the run satisfies the constraint.
Our main result is an (optimal) PSPACE decision procedure for the duration-bounded
reachability problem.
acknowledgement: "A preliminary version of this paper appeared in the Proceedings
of the Fifth International Conference on Computer-Aided Verification (CAV 93), Springer-Verlag
LNCS 818, pp. 181–193, 1993. We thank Sergio Yovine for a careful reading of the
manuscript. This reaserch was partially supported by the BRA ESPRIT project REACT,
by the ONR YIP\r\naward N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by
the NSF grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056,
and by the ARPA grant NAG2-892."
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Costas
full_name: Courcoubetis, Costas
last_name: Courcoubetis
- 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: Alur R, Courcoubetis C, Henzinger TA. Computing accumulated delays in real-time
systems. Formal Methods in System Design. 1997;11(2):137-156. doi:10.1023/A:1008626013578
apa: Alur, R., Courcoubetis, C., & Henzinger, T. A. (1997). Computing accumulated
delays in real-time systems. Formal Methods in System Design. Springer.
https://doi.org/10.1023/A:1008626013578
chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated
Delays in Real-Time Systems.” Formal Methods in System Design. Springer,
1997. https://doi.org/10.1023/A:1008626013578.
ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays
in real-time systems,” Formal Methods in System Design, vol. 11, no. 2.
Springer, pp. 137–156, 1997.
ista: Alur R, Courcoubetis C, Henzinger TA. 1997. Computing accumulated delays in
real-time systems. Formal Methods in System Design. 11(2), 137–156.
mla: Alur, Rajeev, et al. “Computing Accumulated Delays in Real-Time Systems.” Formal
Methods in System Design, vol. 11, no. 2, Springer, 1997, pp. 137–56, doi:10.1023/A:1008626013578.
short: R. Alur, C. Courcoubetis, T.A. Henzinger, Formal Methods in System Design
11 (1997) 137–156.
date_created: 2018-12-11T12:09:43Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-16T13:43:41Z
day: '01'
doi: 10.1023/A:1008626013578
extern: '1'
intvolume: ' 11'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 137 - 156
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '98'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing accumulated delays in real-time systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 11
year: '1997'
...
---
_id: '4608'
abstract:
- lang: eng
text: 'State space explosion is a fundamental obstacle in formal verification of
designs and protocols. Several techniques for combating this problem have emerged
in the past few years, among which two are significant: partial-order reductions
and symbolic state space search. In asynchronous systems, interleavings of independent
concurrent events are equivalent, and only a representative interleaving needs
to be explored to verify local properties. Partial-order methods exploit this
redundancy and visit only a subset of the reachable states. Symbolic techniques,
on the other hand, capture the transition relation of a system and the set of
reachable states as boolean functions. In many cases, these functions can be represented
compactly using binary decision diagrams (BDDs). Traditionally, the two techniques
have been practiced by two different schools—partial-order methods with enumerative
depth-first search for the analysis of asynchronous network protocols, and symbolic
breadth-first search for the analysis of synchronous hardware designs. We combine
both approaches and develop a method for using partial-order reduction techniques
in symbolic BDD-based invariant checking. We present theoretical results to prove
the correctness of the method, and experimental results to demonstrate its efficacy.'
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the Semiconductor Research Corporation contracts DC-324.036
and DC-324.005.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Robert
full_name: Brayton, Robert
last_name: Brayton
- 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
citation:
ama: 'Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction
in symbolic state-space exploration. In: 9th International Conference on Computer
Aided Verification. Vol 1254. Springer; 1997:340-351. doi:10.1007/3-540-63166-6_34'
apa: 'Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., & Rajamani, S. (1997).
Partial-order reduction in symbolic state-space exploration. In 9th International
Conference on Computer Aided Verification (Vol. 1254, pp. 340–351). Haifa,
Israel: Springer. https://doi.org/10.1007/3-540-63166-6_34'
chicago: Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram
Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” In 9th
International Conference on Computer Aided Verification, 1254:340–51. Springer,
1997. https://doi.org/10.1007/3-540-63166-6_34.
ieee: R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order
reduction in symbolic state-space exploration,” in 9th International Conference
on Computer Aided Verification, Haifa, Israel, 1997, vol. 1254, pp. 340–351.
ista: 'Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 1997. Partial-order
reduction in symbolic state-space exploration. 9th International Conference on
Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1254,
340–351.'
mla: Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.”
9th International Conference on Computer Aided Verification, vol. 1254,
Springer, 1997, pp. 340–51, doi:10.1007/3-540-63166-6_34.
short: R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, in:, 9th International
Conference on Computer Aided Verification, Springer, 1997, pp. 340–351.
conference:
end_date: 1997-06-25
location: Haifa, Israel
name: 'CAV: Computer Aided Verification'
start_date: 1997-06-22
date_created: 2018-12-11T12:09:44Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-16T14:09:54Z
day: '01'
doi: 10.1007/3-540-63166-6_34
extern: '1'
intvolume: ' 1254'
language:
- iso: eng
month: '01'
oa_version: None
page: 340 - 351
publication: 9th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540631668'
publication_status: published
publisher: Springer
publist_id: '99'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Partial-order reduction in symbolic state-space exploration
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1254
year: '1997'
...
---
_id: '4609'
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 system
moves; 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. Also the problems of receptiveness, realizability, and
controllability can be formulated as model-checking problems for alternating-time
formulas'
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
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. In: Proceedings
of the 38th Annual Symposium on Foundations of Computer Science. Association
for Computing Machinery (ACM); 1997:100-109. doi:10.1145/585265.585270'
apa: 'Alur, R., Henzinger, T. A., & Kupferman, O. (1997). Alternating-time temporal
logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer
Science (pp. 100–109). Washington, DC, United States: Association for Computing
Machinery (ACM). https://doi.org/10.1145/585265.585270'
chicago: Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time
Temporal Logic.” In Proceedings of the 38th Annual Symposium on Foundations
of Computer Science, 100–109. Association for Computing Machinery (ACM), 1997.
https://doi.org/10.1145/585265.585270.
ieee: R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,”
in Proceedings of the 38th Annual Symposium on Foundations of Computer Science,
Washington, DC, United States, 1997, pp. 100–109.
ista: 'Alur R, Henzinger TA, Kupferman O. 1997. Alternating-time temporal logic.
Proceedings of the 38th Annual Symposium on Foundations of Computer Science. FOCS:
Foundations of Computer Science, 100–109.'
mla: Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” Proceedings of the
38th Annual Symposium on Foundations of Computer Science, Association for
Computing Machinery (ACM), 1997, pp. 100–09, doi:10.1145/585265.585270.
short: R. Alur, T.A. Henzinger, O. Kupferman, in:, Proceedings of the 38th Annual
Symposium on Foundations of Computer Science, Association for Computing Machinery
(ACM), 1997, pp. 100–109.
conference:
end_date: 1997-10-22
location: Washington, DC, United States
name: 'FOCS: Foundations of Computer Science'
start_date: 1997-10-19
date_created: 2018-12-11T12:09:44Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-09-05T07:32:05Z
day: '01'
doi: 10.1145/585265.585270
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 100 - 109
publication: Proceedings of the 38th Annual Symposium on Foundations of Computer Science
publication_identifier:
issn:
- 0004-5411
publication_status: published
publisher: Association for Computing Machinery (ACM)
publist_id: '100'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating-time temporal logic
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1997'
...