---
_id: '4275'
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. Differentiation. In: Encyclopedia of Biodiversity. Academic
Press; 2000:85-94. doi:10.1016/B0-12-226865-2/00070-5'
apa: Barton, N. H. (2000). Differentiation. In Encyclopedia of Biodiversity
(pp. 85–94). Academic Press. https://doi.org/10.1016/B0-12-226865-2/00070-5
chicago: Barton, Nicholas H. “Differentiation.” In Encyclopedia of Biodiversity,
85–94. Academic Press, 2000. https://doi.org/10.1016/B0-12-226865-2/00070-5.
ieee: N. H. Barton, “Differentiation,” in Encyclopedia of Biodiversity, Academic
Press, 2000, pp. 85–94.
ista: 'Barton NH. 2000.Differentiation. In: Encyclopedia of Biodiversity. , 85–94.'
mla: Barton, Nicholas H. “Differentiation.” Encyclopedia of Biodiversity,
Academic Press, 2000, pp. 85–94, doi:10.1016/B0-12-226865-2/00070-5.
short: N.H. Barton, in:, Encyclopedia of Biodiversity, Academic Press, 2000, pp.
85–94.
date_created: 2018-12-11T12:07:59Z
date_published: 2000-10-01T00:00:00Z
date_updated: 2023-04-19T09:39:55Z
day: '01'
doi: 10.1016/B0-12-226865-2/00070-5
extern: '1'
language:
- iso: eng
month: '10'
oa_version: None
page: 85 - 94
publication: Encyclopedia of Biodiversity
publication_identifier:
isbn:
- '9780122268656'
publication_status: published
publisher: Academic Press
publist_id: '1816'
status: public
title: Differentiation
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...
---
_id: '4276'
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. Population genetics of multiple loci. Genetics Research.
2000;75(3):371-373. doi:10.1017/S0016672300239220
apa: Barton, N. H. (2000). Population genetics of multiple loci. Genetics Research.
Cambridge University Press. https://doi.org/10.1017/S0016672300239220
chicago: Barton, Nicholas H. “Population Genetics of Multiple Loci.” Genetics
Research. Cambridge University Press, 2000. https://doi.org/10.1017/S0016672300239220.
ieee: N. H. Barton, “Population genetics of multiple loci,” Genetics Research,
vol. 75, no. 3. Cambridge University Press, pp. 371–373, 2000.
ista: Barton NH. 2000. Population genetics of multiple loci. Genetics Research.
75(3), 371–373.
mla: Barton, Nicholas H. “Population Genetics of Multiple Loci.” Genetics Research,
vol. 75, no. 3, Cambridge University Press, 2000, pp. 371–73, doi:10.1017/S0016672300239220.
short: N.H. Barton, Genetics Research 75 (2000) 371–373.
date_created: 2018-12-11T12:07:59Z
date_published: 2000-06-01T00:00:00Z
date_updated: 2023-04-18T15:01:01Z
day: '01'
doi: 10.1017/S0016672300239220
extern: '1'
intvolume: ' 75'
issue: '3'
language:
- iso: eng
main_file_link:
- url: https://www.cambridge.org/core/journals/genetics-research/article/population-genetics-of-multiple-loci-by-f-b-christiansen-wiley-series-in-mathematical-and-computational-biology-ed-s-levin-john-wiley-sons-1999-isbn-0-471-979791-365-pages-price-80-hardback/9F9E954479B9FB87B0A07250AD6AAD9C
month: '06'
oa_version: None
page: 371 - 373
publication: Genetics Research
publication_identifier:
issn:
- 0016-6723
publication_status: published
publisher: Cambridge University Press
publist_id: '1814'
quality_controlled: '1'
status: public
title: Population genetics of multiple loci
type: review
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 75
year: '2000'
...
---
_id: '4433'
abstract:
- lang: eng
text: "Bisimulations enjoy numerous applications in the analysis of labeled transition
systems. Many of these applications are based on two central observations: first,
bisimilar systems satisfy the same branching-time properties; second, bisimilarity
can be checked efficiently for finite-state systems. The local character of bisimulation,
however, makes it difficult to address liveness concerns. Indeed, the definitions
of fair bisimulation that have been proposed in the literature sacrifice locality,
and with it, also efficient checkability. We put forward a new definition of fair
bisimulation which does not suffer from this drawback.\r\nThe bisimilarity of
two systems can be viewed in terms of a game played between a protagonist and
an adversary. In each step of the infinite bisimulation game, the adversary chooses
one system, makes a move, and the protagonist matches it with a move of the other
system. Consistent with this game-based view, we call two fair transition systems
bisimilar if in the bisimulation game, the infinite path produced in the first
system is fair iff the infinite path produced in the second system is fair.\r\nWe
show that this notion of fair bisimulation enjoys the following properties. First,
fairly bisimilar systems satisfy the same formulas of the logics Fair-AFMC (the
fair alternation-free μ-calculus) and Fair-CTL*. Therefore, fair bisimulations
can serve as property-preserving abstractions for these logics and weaker ones,
such as Fair-CTL and LTL. Indeed, Fair-AFMC provides an exact logical characterization
of fair bisimilarity. Second, it can be checked in time polynomial in the number
of states if two systems are fairly bisimilar. This is in stark contrast to all
trace-based equivalences, which are traditionally used for addressing liveness
but require exponential time for checking."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, the DARPA (MARCO) grant
MDA972-99-1-0001, and the NSF CAREER award CCR-9501708.
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: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Henzinger TA, Rajamani S. Fair bisimulation. In: Proceedings of the 6th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. Vol 1785. Springer; 2000:299-314. doi:10.1007/3-540-46419-0_21'
apa: 'Henzinger, T. A., & Rajamani, S. (2000). Fair bisimulation. In Proceedings
of the 6th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 1785, pp. 299–314). Berlin, Germany: Springer.
https://doi.org/10.1007/3-540-46419-0_21'
chicago: Henzinger, Thomas A, and Sriram Rajamani. “Fair Bisimulation.” In Proceedings
of the 6th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 1785:299–314. Springer, 2000. https://doi.org/10.1007/3-540-46419-0_21.
ieee: T. A. Henzinger and S. Rajamani, “Fair bisimulation,” in Proceedings of
the 6th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Berlin, Germany, 2000, vol. 1785, pp. 299–314.
ista: 'Henzinger TA, Rajamani S. 2000. Fair bisimulation. Proceedings of the 6th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
LNCS, vol. 1785, 299–314.'
mla: Henzinger, Thomas A., and Sriram Rajamani. “Fair Bisimulation.” Proceedings
of the 6th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 1785, Springer, 2000, pp. 299–314, doi:10.1007/3-540-46419-0_21.
short: T.A. Henzinger, S. Rajamani, in:, Proceedings of the 6th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Springer,
2000, pp. 299–314.
conference:
end_date: 2000-04-02
location: Berlin, Germany
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2000-03-25
date_created: 2018-12-11T12:08:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:11:07Z
day: '01'
doi: 10.1007/3-540-46419-0_21
extern: '1'
intvolume: ' 1785'
language:
- iso: eng
month: '01'
oa_version: None
page: 299 - 314
publication: Proceedings of the 6th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems
publication_identifier:
isbn:
- '9783540672821'
publication_status: published
publisher: Springer
publist_id: '297'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fair bisimulation
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1785
year: '2000'
...
---
_id: '4434'
abstract:
- lang: eng
text: 'The algorithmic approach to the analysis of timed and hybrid systems is fundamentally
limited by undecidability, of universality in the timed case (where all continuous
variables are clocks), and of emptiness in the rectangular case (which includes
drifting clocks). Traditional proofs of undecidability encode a single Turing
computation by a single timed trajectory. These proofs have nurtured the hope
that the introduction of “fuzziness” into timed and hybrid models (in the sense
that a system cannot distinguish between trajectories that are sufficiently similar)
may lead to decidability. We show that this is not the case, by sharpening both
fundamental undecidability results. Besides the obvious blow our results deal
to the algorithmic method, they also prove that the standard model of timed and
hybrid systems, while not “robust” in its definition of trajectory acceptance
(which is affected by tiny perturbations in the timing of events), is quite robust
in its mathematical properties: the undecidability barriers are not affected by
reasonable perturbations of the model.'
acknowledgement: 'This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the ARO MURI grant DAAH-04-96-1-0341,
and the NSF CAREER award CCR-9501708. '
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: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: 'Henzinger TA, Raskin J. Robust undecidability of timed and hybrid systems.
In: Proceedings of the 3rd International Workshop on Hybrid Systems. Vol
1790. Springer; 2000:145-159. doi:10.1007/3-540-46430-1_15'
apa: 'Henzinger, T. A., & Raskin, J. (2000). Robust undecidability of timed
and hybrid systems. In Proceedings of the 3rd International Workshop on Hybrid
Systems (Vol. 1790, pp. 145–159). Pittsburgh, PA, USA: Springer. https://doi.org/10.1007/3-540-46430-1_15'
chicago: Henzinger, Thomas A, and Jean Raskin. “Robust Undecidability of Timed and
Hybrid Systems.” In Proceedings of the 3rd International Workshop on Hybrid
Systems, 1790:145–59. Springer, 2000. https://doi.org/10.1007/3-540-46430-1_15.
ieee: T. A. Henzinger and J. Raskin, “Robust undecidability of timed and hybrid
systems,” in Proceedings of the 3rd International Workshop on Hybrid Systems,
Pittsburgh, PA, USA, 2000, vol. 1790, pp. 145–159.
ista: 'Henzinger TA, Raskin J. 2000. Robust undecidability of timed and hybrid systems.
Proceedings of the 3rd International Workshop on Hybrid Systems. HSCC: Hybrid
Systems - Computation and Control, LNCS, vol. 1790, 145–159.'
mla: Henzinger, Thomas A., and Jean Raskin. “Robust Undecidability of Timed and
Hybrid Systems.” Proceedings of the 3rd International Workshop on Hybrid Systems,
vol. 1790, Springer, 2000, pp. 145–59, doi:10.1007/3-540-46430-1_15.
short: T.A. Henzinger, J. Raskin, in:, Proceedings of the 3rd International Workshop
on Hybrid Systems, Springer, 2000, pp. 145–159.
conference:
end_date: 2000-03-25
location: Pittsburgh, PA, USA
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2000-03-23
date_created: 2018-12-11T12:08:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:16:13Z
day: '01'
doi: 10.1007/3-540-46430-1_15
extern: '1'
intvolume: ' 1790'
language:
- iso: eng
month: '01'
oa_version: None
page: 145 - 159
publication: Proceedings of the 3rd International Workshop on Hybrid Systems
publication_identifier:
isbn:
- '9783540672593'
publication_status: published
publisher: Springer
publist_id: '298'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Robust undecidability of timed and hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1790
year: '2000'
...
---
_id: '4435'
abstract:
- lang: eng
text: 'An important case of hybrid systems are the rectangular automata. First,
rectangular dynamics can naturally and arbitrarily closely approximate more general,
nonlinear dynamics. Second, rectangular automata are the most general type of
hybrid systems for which model checking -in particular, Ltl model checking- is
decidable. However, on one hand, the original proofs of decidability did not suggest
practical algorithms and, on the other hand, practical symbolic model-checking
procedures -such as those implemented in HyTech- were not known to terminate on
rectangular automata. We remedy this unsatisfactory situation: we present a symbolic
method for Ltl model checking which can be performed by HyTech and is guaranteed
to terminate on all rectangular automata. We do so by proving that our method
for symbolic Ltl model checking terminates on an infinite-state transition system
if the trace-equivalence relation of the system has finite index, which is the
case for all rectangular automata.'
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660,
the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Henzinger TA, Majumdar R. Symbolic model checking for rectangular hybrid systems.
In: Proceedings of the 6th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems. Vol 1785. Springer; 2000:142-156.
doi:10.1007/3-540-46419-0_11'
apa: 'Henzinger, T. A., & Majumdar, R. (2000). Symbolic model checking for rectangular
hybrid systems. In Proceedings of the 6th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (Vol. 1785, pp.
142–156). Berlin, Germany: Springer. https://doi.org/10.1007/3-540-46419-0_11'
chicago: Henzinger, Thomas A, and Ritankar Majumdar. “Symbolic Model Checking for
Rectangular Hybrid Systems.” In Proceedings of the 6th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 1785:142–56.
Springer, 2000. https://doi.org/10.1007/3-540-46419-0_11.
ieee: T. A. Henzinger and R. Majumdar, “Symbolic model checking for rectangular
hybrid systems,” in Proceedings of the 6th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, Berlin, Germany,
2000, vol. 1785, pp. 142–156.
ista: 'Henzinger TA, Majumdar R. 2000. Symbolic model checking for rectangular hybrid
systems. Proceedings of the 6th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 1785, 142–156.'
mla: Henzinger, Thomas A., and Ritankar Majumdar. “Symbolic Model Checking for Rectangular
Hybrid Systems.” Proceedings of the 6th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, vol. 1785, Springer,
2000, pp. 142–56, doi:10.1007/3-540-46419-0_11.
short: T.A. Henzinger, R. Majumdar, in:, Proceedings of the 6th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Springer,
2000, pp. 142–156.
conference:
end_date: 2000-04-02
location: Berlin, Germany
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2000-03-25
date_created: 2018-12-11T12:08:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:08:09Z
day: '01'
doi: 10.1007/3-540-46419-0_11
extern: '1'
intvolume: ' 1785'
language:
- iso: eng
month: '01'
oa_version: None
page: 142 - 156
publication: Proceedings of the 6th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems
publication_identifier:
isbn:
- '9783540672821'
publication_status: published
publisher: Springer
publist_id: '293'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for rectangular hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1785
year: '2000'
...
---
_id: '4439'
abstract:
- lang: eng
text: "We define five increasingly comprehensive classes of infinite-state systems,
called STS1–5, whose state spaces have finitary structure. For four of these classes,
we provide examples from hybrid systems.\r\nSTS1 These are the systems with finite
bisimilarity quotients. They can be analyzed symbolically by (1) iterating the
predecessor and boolean operations starting from a finite set of observable state
sets, and (2) terminating when no new state sets are generated. This enables model
checking of the μ-calculus.\r\nSTS2 These are the systems with finite similarity
quotients. They can be analyzed symbolically by iterating the predecessor and
positive boolean operations. This enables model checking of the existential and
universal fragments of the μ-calculus.\r\nSTS3 These are the systems with finite
trace-equivalence quotients. They can be analyzed symbolically by iterating the
predecessor operation and a restricted form of positive boolean operations (intersection
is restricted to intersection with observables). This enables model checking of
linear temporal logic.\r\nSTS4 These are the systems with finite distance-equivalence
quotients (two states are equivalent if for every distance d, the same observables
can be reached in d transitions). The systems in this class can be analyzed symbolically
by iterating the predecessor operation and terminating when no new state sets
are generated. This enables model checking of the existential conjunction-free
and universal disjunction-free fragments of the μ-calculus.\r\nSTS5 These are
the systems with finite bounded-reachability quotients (two states are equivalent
if for every distance d, the same observables can be reached in d or fewer transitions).
The systems in this class can be analyzed symbolically by iterating the predecessor
operation and terminating when no new states are encountered. This enables model
checking of reachability properties."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660,
the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Henzinger TA, Majumdar R. A classification of symbolic transition systems.
In: Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer
Science. Vol 1770. Springer; 2000:13-34. doi:10.1007/3-540-46541-3_2'
apa: 'Henzinger, T. A., & Majumdar, R. (2000). A classification of symbolic
transition systems. In Proceedings of the 17th Annual Symposium on Theoretical
Aspects of Computer Science (Vol. 1770, pp. 13–34). Lille, France: Springer.
https://doi.org/10.1007/3-540-46541-3_2'
chicago: Henzinger, Thomas A, and Ritankar Majumdar. “A Classification of Symbolic
Transition Systems.” In Proceedings of the 17th Annual Symposium on Theoretical
Aspects of Computer Science, 1770:13–34. Springer, 2000. https://doi.org/10.1007/3-540-46541-3_2.
ieee: T. A. Henzinger and R. Majumdar, “A classification of symbolic transition
systems,” in Proceedings of the 17th Annual Symposium on Theoretical Aspects
of Computer Science, Lille, France, 2000, vol. 1770, pp. 13–34.
ista: 'Henzinger TA, Majumdar R. 2000. A classification of symbolic transition systems.
Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science.
STACS: Theoretical Aspects of Computer Science, LNCS, vol. 1770, 13–34.'
mla: Henzinger, Thomas A., and Ritankar Majumdar. “A Classification of Symbolic
Transition Systems.” Proceedings of the 17th Annual Symposium on Theoretical
Aspects of Computer Science, vol. 1770, Springer, 2000, pp. 13–34, doi:10.1007/3-540-46541-3_2.
short: T.A. Henzinger, R. Majumdar, in:, Proceedings of the 17th Annual Symposium
on Theoretical Aspects of Computer Science, Springer, 2000, pp. 13–34.
conference:
end_date: 2000-02-19
location: Lille, France
name: 'STACS: Theoretical Aspects of Computer Science'
start_date: 2000-02-17
date_created: 2018-12-11T12:08:51Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:02:39Z
day: '01'
doi: 10.1007/3-540-46541-3_2
extern: '1'
intvolume: ' 1770'
language:
- iso: eng
month: '01'
oa_version: None
page: 13 - 34
publication: Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer
Science
publication_identifier:
isbn:
- '9783540671411'
publication_status: published
publisher: Springer
publist_id: '292'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A classification of symbolic transition systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1770
year: '2000'
...
---
_id: '4481'
abstract:
- lang: eng
text: 'Since hybrid embedded systems are pervasive and often safety-critical, guarantees
about their correct performance are desirable. The hybrid systems model checker
HyTech provides such guarantees and has successfully verified some systems. However,
HyTech severely restricts the continuous dynamics of the system being analyzed
and, therefore, often forces the use of prohibitively expensive discrete and polyhedral
abstractions. We have designed a new algorithm, which is capable of directly verifying
hybrid systems with general continuous dynamics, such as linear and nonlinear
differential equations. The new algorithm conservatively overapproximates the
reachable states of a hybrid automaton by using interval numerical methods. Interval
numerical methods return sets of points that enclose the true result of numerical
computation and, thus, avoid distortions due to the accumulation of round-off
errors. We have implemented the new algorithm in a successor tool to HyTech called
HyperTech. We consider three examples: a thermostat with delay, a two-tank water
system, and an air-traffic collision avoidance protocol. HyperTech enables the
direct, fully automatic analysis of these systems, which is also more accurate
than the use of polyhedral abstractions.'
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the ARO MURI grant DAAH-04-96-1-0341,
and the NSF CAREER award CCR-9501708.
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: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Howard
full_name: Wong Toi, Howard
last_name: Wong Toi
citation:
ama: 'Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. Beyond HyTech: Hybrid systems
analysis using interval numerical methods. In: Proceedings of the 3rd International
Workshop on Hybrid Systems. Vol 1790. Springer; 2000:130-144. doi:10.1007/3-540-46430-1_14'
apa: 'Henzinger, T. A., Horowitz, B., Majumdar, R., & Wong Toi, H. (2000). Beyond
HyTech: Hybrid systems analysis using interval numerical methods. In Proceedings
of the 3rd International Workshop on Hybrid Systems (Vol. 1790, pp. 130–144).
Pittsburgh, PA, USA: Springer. https://doi.org/10.1007/3-540-46430-1_14'
chicago: 'Henzinger, Thomas A, Benjamin Horowitz, Ritankar Majumdar, and Howard
Wong Toi. “Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods.”
In Proceedings of the 3rd International Workshop on Hybrid Systems, 1790:130–44.
Springer, 2000. https://doi.org/10.1007/3-540-46430-1_14.'
ieee: 'T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong Toi, “Beyond HyTech:
Hybrid systems analysis using interval numerical methods,” in Proceedings of
the 3rd International Workshop on Hybrid Systems, Pittsburgh, PA, USA, 2000,
vol. 1790, pp. 130–144.'
ista: 'Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. 2000. Beyond HyTech: Hybrid
systems analysis using interval numerical methods. Proceedings of the 3rd International
Workshop on Hybrid Systems. HSCC: Hybrid Systems - Computation and Control, LNCS,
vol. 1790, 130–144.'
mla: 'Henzinger, Thomas A., et al. “Beyond HyTech: Hybrid Systems Analysis Using
Interval Numerical Methods.” Proceedings of the 3rd International Workshop
on Hybrid Systems, vol. 1790, Springer, 2000, pp. 130–44, doi:10.1007/3-540-46430-1_14.'
short: T.A. Henzinger, B. Horowitz, R. Majumdar, H. Wong Toi, in:, Proceedings of
the 3rd International Workshop on Hybrid Systems, Springer, 2000, pp. 130–144.
conference:
end_date: 2000-03-25
location: Pittsburgh, PA, USA
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2000-03-23
date_created: 2018-12-11T12:09:04Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T12:44:52Z
day: '01'
doi: 10.1007/3-540-46430-1_14
extern: '1'
intvolume: ' 1790'
language:
- iso: eng
month: '01'
oa_version: None
page: 130 - 144
publication: Proceedings of the 3rd International Workshop on Hybrid Systems
publication_identifier:
isbn:
- '9783540672593'
publication_status: published
publisher: Springer
publist_id: '247'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Beyond HyTech: Hybrid systems analysis using interval numerical methods'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1790
year: '2000'
...
---
_id: '4482'
abstract:
- lang: eng
text: "We apply the theory of abstract interpretation to the verification of game
properties for reactive systems. Unlike properties expressed in standard temporal
logics, game properties can distinguish adversarial from collaborative relationships
between the processes of a concurrent program, or the components of a parallel
system. We consider two-player concurrent games –say, component vs. environment–
and specify properties of such games –say, the component has a winning strategy
to obtain a resource, no matter how the environment behaves– in the alternating-time
μ-calculus (Aμ ). A sound abstraction of such a game must at the same time restrict
the behaviors of the component and increase the behaviors of the environment:
if a less powerful component can win against a more powerful environment, then
surely the original component can win against the original environment.\r\nWe
formalize the concrete semantics of a concurrent game in terms of controllable
and uncontrollable predecessor predicates, which suffice for model checking all
Aμ properties by applying boolean operations and iteration. We then define the
abstract semantics of a concurrent game in terms of abstractions for the controllable
and uncontrollable predecessor predicates. This allows us to give general characterizations
for the soundness and completeness of abstract games with respect to Aμ properties.
We also present a simple programming language for multi-process programs, and
show how approximations of the maximal abstraction (w.r.t. Aμ properties) can
be obtained from the program text. We apply the theory to two practical verification
examples, a communication protocol developed at the Berkeley Wireless Research
Center, and a protocol converter. In the wireless protocol, both the use of a
game property for specification and the use of abstraction for automatic verification
were instrumental to uncover a subtle bug."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660,
the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: 'Henzinger TA, Majumdar R, Mang F, Raskin J. Abstract interpretation of game
properties. In: Proceedings of the 7th International Symposium on Static Analysis.
Vol 1824. Springer; 2000:220-239. doi:10.1007/978-3-540-45099-3_12'
apa: 'Henzinger, T. A., Majumdar, R., Mang, F., & Raskin, J. (2000). Abstract
interpretation of game properties. In Proceedings of the 7th International
Symposium on Static Analysis (Vol. 1824, pp. 220–239). Santa Barbara, CA,
USA: Springer. https://doi.org/10.1007/978-3-540-45099-3_12'
chicago: Henzinger, Thomas A, Ritankar Majumdar, Freddy Mang, and Jean Raskin. “Abstract
Interpretation of Game Properties.” In Proceedings of the 7th International
Symposium on Static Analysis, 1824:220–39. Springer, 2000. https://doi.org/10.1007/978-3-540-45099-3_12.
ieee: T. A. Henzinger, R. Majumdar, F. Mang, and J. Raskin, “Abstract interpretation
of game properties,” in Proceedings of the 7th International Symposium on Static
Analysis, Santa Barbara, CA, USA, 2000, vol. 1824, pp. 220–239.
ista: 'Henzinger TA, Majumdar R, Mang F, Raskin J. 2000. Abstract interpretation
of game properties. Proceedings of the 7th International Symposium on Static Analysis.
SAS: Static Analysis Symposium, LNCS, vol. 1824, 220–239.'
mla: Henzinger, Thomas A., et al. “Abstract Interpretation of Game Properties.”
Proceedings of the 7th International Symposium on Static Analysis, vol.
1824, Springer, 2000, pp. 220–39, doi:10.1007/978-3-540-45099-3_12.
short: T.A. Henzinger, R. Majumdar, F. Mang, J. Raskin, in:, Proceedings of the
7th International Symposium on Static Analysis, Springer, 2000, pp. 220–239.
conference:
end_date: 2000-07-06
location: Santa Barbara, CA, USA
name: 'SAS: Static Analysis Symposium'
start_date: 2000-06-29
date_created: 2018-12-11T12:09:04Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T12:49:56Z
day: '01'
doi: 10.1007/978-3-540-45099-3_12
extern: '1'
intvolume: ' 1824'
language:
- iso: eng
month: '01'
oa_version: None
page: 220 - 239
publication: Proceedings of the 7th International Symposium on Static Analysis
publication_identifier:
isbn:
- '9783540676683'
publication_status: published
publisher: Springer
publist_id: '248'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstract interpretation of game properties
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1824
year: '2000'
...
---
_id: '4483'
abstract:
- lang: eng
text: 'Model-checking algorithms can be used to verify, formally and automatically,
if a low-level description of a design conforms with a high-level description.
However, for designs with very large state spaces, prior to the application of
an algorithm, the refinement-checking task needs to be decomposed into subtasks
of manageable complexity. It is natural to decompose the task following the component
structure of the design. However, an individual component often does not satisfy
its requirements unless the component is put into the right context, which constrains
the inputs to the component. Thus, in order to verify each component individually,
we need to make assumptions about its inputs, which are provided by the other
components of the design. This reasoning is circular: component A is verified
under the assumption that context B behaves correctly, and symmetrically, B is
verified assuming the correctness of A. The assume-guarantee paradigm provides
a systematic theory and methodology for ensuring the soundness of the circular
style of postulating and discharging assumptions in component-based reasoning.We
give a tutorial introduction to the assume-guarantee paradigm for decomposing
refinement-checking tasks. To illustrate the method, we step in detail through
the formal verification of a processor pipeline against an instruction set architecture.
In this example, the verification of a three-stage pipeline is broken up into
three subtasks, one for each stage of the pipeline.'
acknowledgement: 'Supported in part by DARPA Information Technology Office, by the
MARC0 Gigascale Silicon Research Center, and by the National Science Foundation. '
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: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Henzinger TA, Qadeer S, Rajamani S. Decomposing refinement proofs using assume-guarantee
reasoning. In: Proceedings of the 2000 International Conference on Computer-Aided
Design. IEEE; 2000:245-252. doi:10.1109/ICCAD.2000.896481'
apa: 'Henzinger, T. A., Qadeer, S., & Rajamani, S. (2000). Decomposing refinement
proofs using assume-guarantee reasoning. In Proceedings of the 2000 International
Conference on Computer-Aided Design (pp. 245–252). San Jose, CA, USA: IEEE.
https://doi.org/10.1109/ICCAD.2000.896481'
chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Decomposing Refinement
Proofs Using Assume-Guarantee Reasoning.” In Proceedings of the 2000 International
Conference on Computer-Aided Design, 245–52. IEEE, 2000. https://doi.org/10.1109/ICCAD.2000.896481.
ieee: T. A. Henzinger, S. Qadeer, and S. Rajamani, “Decomposing refinement proofs
using assume-guarantee reasoning,” in Proceedings of the 2000 International
Conference on Computer-Aided Design, San Jose, CA, USA, 2000, pp. 245–252.
ista: 'Henzinger TA, Qadeer S, Rajamani S. 2000. Decomposing refinement proofs using
assume-guarantee reasoning. Proceedings of the 2000 International Conference on
Computer-Aided Design. ICCAD: Computer-Aided Design, 245–252.'
mla: Henzinger, Thomas A., et al. “Decomposing Refinement Proofs Using Assume-Guarantee
Reasoning.” Proceedings of the 2000 International Conference on Computer-Aided
Design, IEEE, 2000, pp. 245–52, doi:10.1109/ICCAD.2000.896481.
short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 2000 International
Conference on Computer-Aided Design, IEEE, 2000, pp. 245–252.
conference:
end_date: 2000-11-09
location: San Jose, CA, USA
name: 'ICCAD: Computer-Aided Design'
start_date: 2000-11-05
date_created: 2018-12-11T12:09:05Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T12:57:52Z
day: '01'
doi: 10.1109/ICCAD.2000.896481
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 245 - 252
publication: Proceedings of the 2000 International Conference on Computer-Aided Design
publication_identifier:
isbn:
- '0780364457'
publication_status: published
publisher: IEEE
publist_id: '249'
quality_controlled: '1'
status: public
title: Decomposing refinement proofs using assume-guarantee reasoning
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...
---
_id: '4512'
abstract:
- lang: eng
text: "Masaccio is a formal model for hybrid dynamical systems which are built from
atomic discrete components (difference equations) and atomic continuous components
(differential equations) by parallel and serial composition, arbitrarily nested.
Each system component consists of an interface, which determines the possible
ways of using the component, and a set of executions, which define the possible
behaviors of the component in real time.\r\nVersion 1.0 (May 2000).\r\n"
acknowledgement: This research was supported in part by the DARPA grants NAG2-1214
and F33615-C-98-3614, and by the MARCO grant 98-DT-660.
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
citation:
ama: 'Henzinger TA. Masaccio: A formal model for embedded components. In: Proceedings
of the 1st International Conference on Theoretical Computer Science . Vol
1872. Springer; 2000:549-563. doi:10.1007/3-540-44929-9_38'
apa: 'Henzinger, T. A. (2000). Masaccio: A formal model for embedded components.
In Proceedings of the 1st International Conference on Theoretical Computer
Science (Vol. 1872, pp. 549–563). Sendai, Japan: Springer. https://doi.org/10.1007/3-540-44929-9_38'
chicago: 'Henzinger, Thomas A. “Masaccio: A Formal Model for Embedded Components.”
In Proceedings of the 1st International Conference on Theoretical Computer
Science , 1872:549–63. Springer, 2000. https://doi.org/10.1007/3-540-44929-9_38.'
ieee: 'T. A. Henzinger, “Masaccio: A formal model for embedded components,” in Proceedings
of the 1st International Conference on Theoretical Computer Science , Sendai,
Japan, 2000, vol. 1872, pp. 549–563.'
ista: 'Henzinger TA. 2000. Masaccio: A formal model for embedded components. Proceedings
of the 1st International Conference on Theoretical Computer Science . TCS: Theoretical
Computer Science, LNCS, vol. 1872, 549–563.'
mla: 'Henzinger, Thomas A. “Masaccio: A Formal Model for Embedded Components.” Proceedings
of the 1st International Conference on Theoretical Computer Science , vol.
1872, Springer, 2000, pp. 549–63, doi:10.1007/3-540-44929-9_38.'
short: T.A. Henzinger, in:, Proceedings of the 1st International Conference on Theoretical
Computer Science , Springer, 2000, pp. 549–563.
conference:
end_date: 2000-08-19
location: Sendai, Japan
name: 'TCS: Theoretical Computer Science'
start_date: 2000-08-17
date_created: 2018-12-11T12:09:14Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T13:48:08Z
day: '01'
doi: 10.1007/3-540-44929-9_38
extern: '1'
intvolume: ' 1872'
language:
- iso: eng
month: '01'
oa_version: None
page: 549 - 563
publication: 'Proceedings of the 1st International Conference on Theoretical Computer
Science '
publication_identifier:
isbn:
- '9783540678236'
publication_status: published
publisher: Springer
publist_id: '215'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Masaccio: A formal model for embedded components'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1872
year: '2000'
...
---
_id: '4513'
abstract:
- lang: eng
text: 'A hybrid automaton is a formal model for a mixed discrete-continuous system.
We classify hybrid automata according to what questions about their behavior can
be answered algorithmically. The classification reveals structure on mixed discrete-continuous
state spaces that was previously studied on purely discrete state spaces only.
In particular, various classes of hybrid automata induce finitary trace equivalence
(or similarity, or bisimilarity) relations on an uncountable state space, thus
permitting the application of various model-checking techniques that were originally
developed for finitestate systems. '
acknowledgement: 'This research was supported in part by the Office of Naval Research
Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER
award CCR-9501708, by the National Science Foundation grant CR9504469, by the Air
Force Office of Scientific Research contract F49620-93-1-0056, by the Army Research
Office MURI grant DAAH-04-96-1-0341, by the Advanced Research Projects Agency grant
NAG2-892, and by the Semiconductor Research Corporation contract 96-DC-324.036. '
alternative_title:
- 'NATO ASI Series F: Computer and Systems Sciences'
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
citation:
ama: 'Henzinger TA. The theory of hybrid automata. In: Inan M, Kurshan R, eds. Verification
of Digital and Hybrid Systems. Vol 170. Springer; 2000:265-292. doi:10.1007/978-3-642-59615-5'
apa: Henzinger, T. A. (2000). The theory of hybrid automata. In M. Inan & R.
Kurshan (Eds.), Verification of Digital and Hybrid Systems (Vol. 170, pp.
265–292). Springer. https://doi.org/10.1007/978-3-642-59615-5
chicago: Henzinger, Thomas A. “The Theory of Hybrid Automata.” In Verification
of Digital and Hybrid Systems, edited by M. Inan and Robert Kurshan, 170:265–92.
Springer, 2000. https://doi.org/10.1007/978-3-642-59615-5.
ieee: T. A. Henzinger, “The theory of hybrid automata,” in Verification of Digital
and Hybrid Systems, vol. 170, M. Inan and R. Kurshan, Eds. Springer, 2000,
pp. 265–292.
ista: 'Henzinger TA. 2000.The theory of hybrid automata. In: Verification of Digital
and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol. 170,
265–292.'
mla: Henzinger, Thomas A. “The Theory of Hybrid Automata.” Verification of Digital
and Hybrid Systems, edited by M. Inan and Robert Kurshan, vol. 170, Springer,
2000, pp. 265–92, doi:10.1007/978-3-642-59615-5.
short: T.A. Henzinger, in:, M. Inan, R. Kurshan (Eds.), Verification of Digital
and Hybrid Systems, Springer, 2000, pp. 265–292.
date_created: 2018-12-11T12:09:14Z
date_published: 2000-04-28T00:00:00Z
date_updated: 2023-04-18T12:37:17Z
day: '28'
doi: 10.1007/978-3-642-59615-5
editor:
- first_name: M.
full_name: Inan, M.
last_name: Inan
- first_name: Robert
full_name: Kurshan, Robert
last_name: Kurshan
extern: '1'
intvolume: ' 170'
language:
- iso: eng
month: '04'
oa_version: None
page: 265 - 292
publication: Verification of Digital and Hybrid Systems
publication_identifier:
isbn:
- '9783642596155'
publication_status: published
publisher: Springer
publist_id: '216'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The theory of hybrid automata
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 170
year: '2000'
...
---
_id: '4598'
abstract:
- lang: eng
text: A hybrid system is a dynamical system with both discrete and continuous state
changes. For analysis purposes, it is often useful to abstract a system in a way
that preserves the properties being analyzed while hiding the details that are
of no interest. We show that interesting classes of hybrid systems can be abstracted
to purely discrete systems while preserving all properties that are definable
in temporal logic. The classes that permit discrete abstractions fall into two
categories. Either the continuous dynamics must be restricted, as is the case
for timed and rectangular hybrid systems, or the discrete dynamics must be restricted,
as is the case for o-minimal hybrid systems. In this paper, we survey and unify
results from both areas.
acknowledgement: The authors would like to thank the reviewers for their detailed
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
- first_name: Gerardo
full_name: Lafferriere, Gerardo
last_name: Lafferriere
- first_name: George
full_name: Pappas, George
last_name: Pappas
citation:
ama: Alur R, Henzinger TA, Lafferriere G, Pappas G. Discrete abstractions of hybrid
systems. Proceedings of the IEEE. 2000;88(7):971-984. doi:10.1109/5.871304
apa: Alur, R., Henzinger, T. A., Lafferriere, G., & Pappas, G. (2000). Discrete
abstractions of hybrid systems. Proceedings of the IEEE. IEEE. https://doi.org/10.1109/5.871304
chicago: Alur, Rajeev, Thomas A Henzinger, Gerardo Lafferriere, and George Pappas.
“Discrete Abstractions of Hybrid Systems.” Proceedings of the IEEE. IEEE,
2000. https://doi.org/10.1109/5.871304
.
ieee: R. Alur, T. A. Henzinger, G. Lafferriere, and G. Pappas, “Discrete abstractions
of hybrid systems,” Proceedings of the IEEE, vol. 88, no. 7. IEEE, pp.
971–984, 2000.
ista: Alur R, Henzinger TA, Lafferriere G, Pappas G. 2000. Discrete abstractions
of hybrid systems. Proceedings of the IEEE. 88(7), 971–984.
mla: Alur, Rajeev, et al. “Discrete Abstractions of Hybrid Systems.” Proceedings
of the IEEE, vol. 88, no. 7, IEEE, 2000, pp. 971–84, doi:10.1109/5.871304 .
short: R. Alur, T.A. Henzinger, G. Lafferriere, G. Pappas, Proceedings of the IEEE
88 (2000) 971–984.
date_created: 2018-12-11T12:09:41Z
date_published: 2000-07-01T00:00:00Z
date_updated: 2023-04-13T13:32:11Z
day: '01'
doi: '10.1109/5.871304 '
extern: '1'
intvolume: ' 88'
issue: '7'
language:
- iso: eng
month: '07'
oa_version: None
page: 971 - 984
publication: Proceedings of the IEEE
publication_identifier:
issn:
- 0018-9219
publication_status: published
publisher: IEEE
publist_id: '107'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discrete abstractions of hybrid systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 88
year: '2000'
...
---
_id: '4627'
abstract:
- lang: eng
text: 'We consider two-player games, which are played on a finite state space for
an infinite number of rounds. The games are concurrent, that is, in each round,
the two players choose their moves independently and simultaneously; the current
state and the two moves determine a successor state. We consider omega-regular
winning conditions on the resulting infinite state sequence. To model the independent
choice of moves, both players are allowed to use randomization for selecting their
moves. This gives rise to the following qualitative modes of winning, which can
be studied without numerical considerations concerning probabilities: sure-win
(player 1 can ensure winning with certainty), almost-sure-win (player 1 can ensure
winning with probability 1), limit-win (player 1 can ensure winning with probability
arbitrarily close to 1), bounded-win (player 1 can ensure winning with probability
bounded away from 0), positive-win (player 1 can ensure winning with positive
probability), and exist-win (player 1 can ensure that at least one possible outcome
of the game satisfies the winning condition).We provide algorithms for computing
the sets of winning states for each of these winning modes. In particular, we
solve concurrent Rabin-chain games in n0 (m) time, where n is the size of the
game structure and m is the number of pairs in the Rabin-chain condition. While
this complexity is in line with traditional turn-based games, where in each state
only one of the two players has a choice of moves, our algorithms are considerably
more involved than those for turn-based games are. This is because concurrent
games violate two of the most fundamental properties of turn-based games. First,
concurrent games are not determined, but rather exhibit a more general duality
property, which involves multiple modes of winning. Second, winning strategies
for concurrent games may require infinite memory.'
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
citation:
ama: 'De Alfaro L, Henzinger TA. Concurrent omega-regular games. In: Proceedings
of the 15th Annual IEEE Symposium on Logic in Computer Science. IEEE; 2000:141-154.
doi:10.1109/LICS.2000.855763'
apa: 'De Alfaro, L., & Henzinger, T. A. (2000). Concurrent omega-regular games.
In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science
(pp. 141–154). Santa Barbara, CA, USA: IEEE. https://doi.org/10.1109/LICS.2000.855763'
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Concurrent Omega-Regular Games.”
In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science,
141–54. IEEE, 2000. https://doi.org/10.1109/LICS.2000.855763.
ieee: L. De Alfaro and T. A. Henzinger, “Concurrent omega-regular games,” in Proceedings
of the 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara,
CA, USA, 2000, pp. 141–154.
ista: 'De Alfaro L, Henzinger TA. 2000. Concurrent omega-regular games. Proceedings
of the 15th Annual IEEE Symposium on Logic in Computer Science. LICS: Logic in
Computer Science, 141–154.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. “Concurrent Omega-Regular Games.”
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science,
IEEE, 2000, pp. 141–54, doi:10.1109/LICS.2000.855763.
short: L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 15th Annual IEEE Symposium
on Logic in Computer Science, IEEE, 2000, pp. 141–154.
conference:
end_date: 2000-06-28
location: Santa Barbara, CA, USA
name: 'LICS: Logic in Computer Science'
start_date: 2000-06-26
date_created: 2018-12-11T12:09:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T13:24:29Z
day: '01'
doi: 10.1109/LICS.2000.855763
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 141 - 154
publication: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
isbn:
- '0769507255'
publication_status: published
publisher: IEEE
publist_id: '82'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Concurrent omega-regular games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...
---
_id: '4637'
abstract:
- lang: eng
text: "In the synchronous composition of processes, one process may prevent another
process from proceeding unless compositions without a well-defined product behavior
are ruled out. They can be ruled out semantically, by insisting on the existence
of certain fixed points, or syntactically, by equipping processes with types,
which make the dependencies between input and output signals transparent. We classify
various typing mechanisms and study their effects on the control problem.\r\nA
static type enforces fixed, acyclic dependencies between input and output ports.
For example, synchronous hardware without combinational loops can be typed statically.
A dynamic type may vary the dependencies from state to state, while maintaining
acyclicity, as in level-sensitive latches. Then, two dynamically typed processes
can be syntactically compatible, if all pairs of possible dependencies are compatible,
or semantically compatible, if in each state the combined dependencies remain
acyclic. For a given plant process and control objective, there may be a controller
of a static type, or only a controller of a syntactically compatible dynamic type,
or only a controller of a semantically compatible dynamic type. We show this to
be a strict hierarchy of possibilities, and we present algorithms and determine
the complexity of the corresponding control problems.\r\nFurthermore, we consider
versions of the control problem in which the type of the controller (static or
dynamic) is given. We show that the solution of these fixed-type control problems
requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas,
and is therefore harder (nondeterministic exponential time) than more traditional
control questions"
acknowledgement: This research was supported in part by the DARPA grants NAG2-1214
and F33615-C-98-3614, the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660,
and the NSF CAREER award CCR-9501708.
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: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems. In:
Proceedings of the 11th International Conference on Concurrency Theory.
Vol 1877. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2000:458-473. doi:10.1007/3-540-44618-4_33'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). The control of synchronous
systems. In Proceedings of the 11th International Conference on Concurrency
Theory (Vol. 1877, pp. 458–473). University Park, PA, USA: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44618-4_33'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous
Systems.” In Proceedings of the 11th International Conference on Concurrency
Theory, 1877:458–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2000.
https://doi.org/10.1007/3-540-44618-4_33.
ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems,”
in Proceedings of the 11th International Conference on Concurrency Theory,
University Park, PA, USA, 2000, vol. 1877, pp. 458–473.
ista: 'De Alfaro L, Henzinger TA, Mang F. 2000. The control of synchronous systems.
Proceedings of the 11th International Conference on Concurrency Theory. CONCUR:
Concurrency Theory, LNCS, vol. 1877, 458–473.'
mla: De Alfaro, Luca, et al. “The Control of Synchronous Systems.” Proceedings
of the 11th International Conference on Concurrency Theory, vol. 1877, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2000, pp. 458–73, doi:10.1007/3-540-44618-4_33.
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 11th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2000, pp. 458–473.
conference:
end_date: 2000-08-25
location: University Park, PA, USA
name: 'CONCUR: Concurrency Theory'
start_date: 2000-08-22
date_created: 2018-12-11T12:09:53Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T11:00:46Z
day: '01'
doi: 10.1007/3-540-44618-4_33
extern: '1'
intvolume: ' 1877'
language:
- iso: eng
month: '01'
oa_version: None
page: 458 - 473
publication: Proceedings of the 11th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540678977'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '69'
quality_controlled: '1'
status: public
title: The control of synchronous systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1877
year: '2000'
...
---
_id: '4638'
abstract:
- lang: eng
text: "Any formal method or tool is almost certainly more often applied in situations
where the outcome is failure (a counterexample) rather than success (a correctness
proof). We present a method for symbolic model checking that can lead to significant
time and memory savings for model-checking runs that fail, while occurring only
a small overhead for model-checking runs that succeed. Our method discovers an
error as soon as it cannot be prevented, which can be long before it actually
occurs; for example, the violation of an invariant may become unpreventable many
transitions before the invariant is violated.\r\nThe key observation is that “unpreventability”
is a local property of a single module: an error is unpreventable in a module
state if no environment can prevent it. Therefore, unpreventability is inexpensive
to compute for each module, yet can save much work in the state exploration of
the global, compound system. Based on different degrees of information available
about the environment, we define and implement several notions of “unpreventability,”
including the standard notion of uncontrollability from discrete-event control.
We present experimental results for two examples, a distributed database protocol
and a wireless communication protocol."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, the DARPA (MARCO) grant
MDA972-99-1-0001, and the NSF CAREER award CCR-9501708.
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: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'De Alfaro L, Henzinger TA, Mang F. Detecting errors before reaching them.
In: Proceedings of the 12th International Conference on Computer Aided Verification.
Vol 1855. Springer; 2000:186-201. doi:10.1007/10722167_17'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). Detecting errors before
reaching them. In Proceedings of the 12th International Conference on Computer
Aided Verification (Vol. 1855, pp. 186–201). Chicago, IL, USA: Springer. https://doi.org/10.1007/10722167_17'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “Detecting Errors
before Reaching Them.” In Proceedings of the 12th International Conference
on Computer Aided Verification, 1855:186–201. Springer, 2000. https://doi.org/10.1007/10722167_17.
ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “Detecting errors before reaching
them,” in Proceedings of the 12th International Conference on Computer Aided
Verification, Chicago, IL, USA, 2000, vol. 1855, pp. 186–201.
ista: 'De Alfaro L, Henzinger TA, Mang F. 2000. Detecting errors before reaching
them. Proceedings of the 12th International Conference on Computer Aided Verification.
CAV: Computer-Aided Verification, LNCS, vol. 1855, 186–201.'
mla: De Alfaro, Luca, et al. “Detecting Errors before Reaching Them.” Proceedings
of the 12th International Conference on Computer Aided Verification, vol.
1855, Springer, 2000, pp. 186–201, doi:10.1007/10722167_17.
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International
Conference on Computer Aided Verification, Springer, 2000, pp. 186–201.
conference:
end_date: 2000-07-19
location: Chicago, IL, USA
name: 'CAV: Computer-Aided Verification'
start_date: 2000-07-15
date_created: 2018-12-11T12:09:53Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T13:18:06Z
day: '01'
doi: 10.1007/10722167_17
extern: '1'
intvolume: ' 1855'
language:
- iso: eng
month: '01'
oa_version: None
page: 186 - 201
publication: Proceedings of the 12th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540677703'
publication_status: published
publisher: Springer
publist_id: '70'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Detecting errors before reaching them
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1855
year: '2000'
...