---
_id: '4373'
abstract:
- lang: eng
text: This paper attempts to improve our understanding of timed languages and their
relation to timed automata. We start by giving a constructive proof of the folk
theorem stating that timed languages specified by the past fragment of mitl, can
be accepted by deterministic timed automata. On the other hand we provide a proof
that certain languages expressed in the future fragment of mitl are not deterministic,
and analyze the reason for this asymmetry.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. Real time temporal logic: Past, present, future.
In: Third International Conference on Formal Modeling and Analysis of Timed
Systems. Vol 3829. Springer; 2006:2-16. doi:10.1007/11603009_2'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). Real time temporal logic:
Past, present, future. In Third International Conference on Formal Modeling
and Analysis of Timed Systems (Vol. 3829, pp. 2–16). Uppsala, Sweden: Springer.
https://doi.org/10.1007/11603009_2'
chicago: 'Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Real Time Temporal Logic:
Past, Present, Future.” In Third International Conference on Formal Modeling
and Analysis of Timed Systems, 3829:2–16. Springer, 2006. https://doi.org/10.1007/11603009_2.'
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “Real time temporal logic: Past, present,
future,” in Third International Conference on Formal Modeling and Analysis
of Timed Systems, Uppsala, Sweden, 2006, vol. 3829, pp. 2–16.'
ista: 'Maler O, Nickovic D, Pnueli A. 2006. Real time temporal logic: Past, present,
future. Third International Conference on Formal Modeling and Analysis of Timed
Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 3829,
2–16.'
mla: 'Maler, Oded, et al. “Real Time Temporal Logic: Past, Present, Future.” Third
International Conference on Formal Modeling and Analysis of Timed Systems,
vol. 3829, Springer, 2006, pp. 2–16, doi:10.1007/11603009_2.'
short: O. Maler, D. Nickovic, A. Pnueli, in:, Third International Conference on
Formal Modeling and Analysis of Timed Systems, Springer, 2006, pp. 2–16.
conference:
end_date: 2005-09-28
location: Uppsala, Sweden
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2005-09-26
date_created: 2018-12-11T12:08:31Z
date_published: 2006-01-23T00:00:00Z
date_updated: 2025-07-01T12:31:15Z
day: '23'
doi: 10.1007/11603009_2
extern: '1'
intvolume: ' 3829'
language:
- iso: eng
month: '01'
oa_version: None
page: 2 - 16
publication: Third International Conference on Formal Modeling and Analysis of Timed
Systems
publication_status: published
publisher: Springer
publist_id: '1084'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Real time temporal logic: Past, present, future'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 3829
year: '2006'
...
---
_id: '4374'
abstract:
- lang: eng
text: We show how to transform formulae written in the real-time temporal logic
MITL into timed automata that recognize their satisfying models. This compositional
construction is much simpler than previously known and can be easily implemented.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. From MITL to timed automata. In: 4th International
Conference on Formal Modeling and Analysis of Timed Systems. Vol 4202. Springer;
2006:274-289. doi:10.1007/11867340_20'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2006). From MITL to timed automata.
In 4th International Conference on Formal Modeling and Analysis of Timed Systems
(Vol. 4202, pp. 274–289). Paris, France: Springer. https://doi.org/10.1007/11867340_20'
chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “From MITL to Timed Automata.”
In 4th International Conference on Formal Modeling and Analysis of Timed Systems,
4202:274–89. Springer, 2006. https://doi.org/10.1007/11867340_20.
ieee: O. Maler, D. Nickovic, and A. Pnueli, “From MITL to timed automata,” in 4th
International Conference on Formal Modeling and Analysis of Timed Systems,
Paris, France, 2006, vol. 4202, pp. 274–289.
ista: 'Maler O, Nickovic D, Pnueli A. 2006. From MITL to timed automata. 4th International
Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling
and Analysis of Timed Systems, LNCS, vol. 4202, 274–289.'
mla: Maler, Oded, et al. “From MITL to Timed Automata.” 4th International Conference
on Formal Modeling and Analysis of Timed Systems, vol. 4202, Springer, 2006,
pp. 274–89, doi:10.1007/11867340_20.
short: O. Maler, D. Nickovic, A. Pnueli, in:, 4th International Conference on Formal
Modeling and Analysis of Timed Systems, Springer, 2006, pp. 274–289.
conference:
end_date: 2006-09-27
location: Paris, France
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2006-09-25
date_created: 2018-12-11T12:08:31Z
date_published: 2006-10-19T00:00:00Z
date_updated: 2025-07-01T12:35:07Z
day: '19'
doi: 10.1007/11867340_20
extern: '1'
intvolume: ' 4202'
language:
- iso: eng
month: '10'
oa_version: None
page: 274 - 289
publication: 4th International Conference on Formal Modeling and Analysis of Timed
Systems
publication_status: published
publisher: Springer
publist_id: '1085'
status: public
title: From MITL to timed automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4202
year: '2006'
...
---
_id: '4401'
abstract:
- lang: eng
text: We propose a general framework of secrecy and preservation of secrecy for
labeled transition systems. Our definition of secrecy is parameterized by the
distinguishing power of the observer, the properties to be kept secret, and the
executions of interest, and captures a multitude of definitions in the literature.
We define a notion of secrecy preserving refinement between systems by strengthening
the classical trace-based refinement so that the implementation leaks a secret
only when the specification also leaks it. We show that secrecy is in general
not definable in μ-calculus, and thus not expressible in specification logics
supported by standard model-checkers. However, we develop a simulation-based proof
technique for establishing secrecy preserving refinement. This result shows how
existing refinement checkers can be used to show correctness of an implementation
with respect to a specification.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Steve
full_name: Zdancewic, Steve
last_name: Zdancewic
citation:
ama: 'Alur R, Cerny P, Zdancewic S. Preserving secrecy under refinement. In: 33rd
International Colloquium on Automata, Languages and Programming. Vol 4052.
Springer; 2006:107-118. doi:10.1007/11787006_10'
apa: Alur, R., Cerny, P., & Zdancewic, S. (2006). Preserving secrecy under refinement.
In 33rd International Colloquium on Automata, Languages and Programming
(Vol. 4052, pp. 107–118). Springer. https://doi.org/10.1007/11787006_10
chicago: Alur, Rajeev, Pavol Cerny, and Steve Zdancewic. “Preserving Secrecy under
Refinement.” In 33rd International Colloquium on Automata, Languages and Programming,
4052:107–18. Springer, 2006. https://doi.org/10.1007/11787006_10.
ieee: R. Alur, P. Cerny, and S. Zdancewic, “Preserving secrecy under refinement,”
in 33rd International Colloquium on Automata, Languages and Programming,
2006, vol. 4052, pp. 107–118.
ista: 'Alur R, Cerny P, Zdancewic S. 2006. Preserving secrecy under refinement.
33rd International Colloquium on Automata, Languages and Programming. ICALP: Automata,
Languages and Programming, LNCS, vol. 4052, 107–118.'
mla: Alur, Rajeev, et al. “Preserving Secrecy under Refinement.” 33rd International
Colloquium on Automata, Languages and Programming, vol. 4052, Springer, 2006,
pp. 107–18, doi:10.1007/11787006_10.
short: R. Alur, P. Cerny, S. Zdancewic, in:, 33rd International Colloquium on Automata,
Languages and Programming, Springer, 2006, pp. 107–118.
conference:
name: 'ICALP: Automata, Languages and Programming'
date_created: 2018-12-11T12:08:40Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2025-07-01T12:27:36Z
day: '01'
doi: 10.1007/11787006_10
extern: '1'
intvolume: ' 4052'
language:
- iso: eng
month: '01'
oa_version: None
page: 107 - 118
publication: 33rd International Colloquium on Automata, Languages and Programming
publication_status: published
publisher: Springer
publist_id: '1054'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Preserving secrecy under refinement
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4052
year: '2006'
...
---
_id: '4406'
abstract:
- lang: eng
text: We propose and evaluate a new algorithm for checking the universality of nondeterministic
finite automata. In contrast to the standard algorithm, which uses the subset
construction to explicitly determinize the automaton, we keep the determinization
step implicit. Our algorithm computes the least fixed point of a monotone function
on the lattice of antichains of state sets. We evaluate the performance of our
algorithm experimentally using the random automaton model recently proposed by
Tabakov and Vardi. We show that on the difficult instances of this probabilistic
model, the antichain algorithm outperforms the standard one by several orders
of magnitude. We also show how variations of the antichain method can be used
for solving the language-inclusion problem for nondeterministic finite automata,
and the emptiness problem for alternating finite automata.
acknowledgement: This research was supported in part by the NSF grants CCR-0234690
and CCR-0225610, and the Belgian FNRS grant 2.4530.02 of the FRFC project “Centre
Fédéré en Vérification.”
alternative_title:
- LNCS
author:
- first_name: Martin
full_name: De Wulf, Martin
last_name: De Wulf
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jean
full_name: Raskin, Jean-François
last_name: Raskin
citation:
ama: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. Antichains: A new algorithm for
checking universality of finite automata. In: Vol 4144. Springer; 2006:17-30.
doi:10.1007/11817963_5'
apa: 'De Wulf, M., Doyen, L., Henzinger, T. A., & Raskin, J. (2006). Antichains:
A new algorithm for checking universality of finite automata (Vol. 4144, pp. 17–30).
Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/11817963_5'
chicago: 'De Wulf, Martin, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Antichains:
A New Algorithm for Checking Universality of Finite Automata,” 4144:17–30. Springer,
2006. https://doi.org/10.1007/11817963_5.'
ieee: 'M. De Wulf, L. Doyen, T. A. Henzinger, and J. Raskin, “Antichains: A new
algorithm for checking universality of finite automata,” presented at the CAV:
Computer Aided Verification, 2006, vol. 4144, pp. 17–30.'
ista: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. 2006. Antichains: A new algorithm
for checking universality of finite automata. CAV: Computer Aided Verification,
LNCS, vol. 4144, 17–30.'
mla: 'De Wulf, Martin, et al. Antichains: A New Algorithm for Checking Universality
of Finite Automata. Vol. 4144, Springer, 2006, pp. 17–30, doi:10.1007/11817963_5.'
short: M. De Wulf, L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2006, pp.
17–30.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:41Z
date_published: 2006-08-08T00:00:00Z
date_updated: 2021-01-12T07:56:45Z
day: '08'
doi: 10.1007/11817963_5
extern: 1
intvolume: ' 4144'
month: '08'
page: 17 - 30
publication_status: published
publisher: Springer
publist_id: '326'
quality_controlled: 0
status: public
title: 'Antichains: A new algorithm for checking universality of finite automata'
type: conference
volume: 4144
year: '2006'
...
---
_id: '4431'
abstract:
- lang: eng
text: 'We summarize some current trends in embedded systems design and point out
some of their characteristics, such as the chasm between analytical and computational
models, and the gap between safety-critical and best-effort engineering practices.
We call for a coherent scientific foundation for embedded systems design, and
we discuss a few key demands on such a foundation: the need for encompassing several
manifestations of heterogeneity, and the need for constructivity in design. We
believe that the development of a satisfactory Embedded Systems Design Science
provides a timely challenge and opportunity for reinvigorating computer science.'
acknowledgement: Supported in part by the ARTIST2 European Network of Excellence on
Embedded Systems Design, by the NSF ITR Center on Hybrid and Embedded Software Systems
(CHESS), and by the SNSF NCCR on Mobile Information and Communication Systems (MICS).
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Joseph
full_name: Sifakis, Joseph
last_name: Sifakis
citation:
ama: 'Henzinger TA, Sifakis J. The embedded systems design challenge. In: Vol 4085.
Springer; 2006:1-15. doi:10.1007/11813040_1'
apa: 'Henzinger, T. A., & Sifakis, J. (2006). The embedded systems design challenge
(Vol. 4085, pp. 1–15). Presented at the FM: Formal Methods, Springer. https://doi.org/10.1007/11813040_1'
chicago: Henzinger, Thomas A, and Joseph Sifakis. “The Embedded Systems Design Challenge,”
4085:1–15. Springer, 2006. https://doi.org/10.1007/11813040_1.
ieee: 'T. A. Henzinger and J. Sifakis, “The embedded systems design challenge,”
presented at the FM: Formal Methods, 2006, vol. 4085, pp. 1–15.'
ista: 'Henzinger TA, Sifakis J. 2006. The embedded systems design challenge. FM:
Formal Methods, LNCS, vol. 4085, 1–15.'
mla: Henzinger, Thomas A., and Joseph Sifakis. The Embedded Systems Design Challenge.
Vol. 4085, Springer, 2006, pp. 1–15, doi:10.1007/11813040_1.
short: T.A. Henzinger, J. Sifakis, in:, Springer, 2006, pp. 1–15.
conference:
name: 'FM: Formal Methods'
date_created: 2018-12-11T12:08:49Z
date_published: 2006-08-10T00:00:00Z
date_updated: 2021-01-12T07:56:55Z
day: '10'
doi: 10.1007/11813040_1
extern: 1
intvolume: ' 4085'
month: '08'
page: 1 - 15
publication_status: published
publisher: Springer
publist_id: '301'
quality_controlled: 0
status: public
title: The embedded systems design challenge
type: conference
volume: 4085
year: '2006'
...
---
_id: '4432'
abstract:
- lang: eng
text: We add freeze quantifiers to the game logic ATL in order to specify real-time
objectives for games played on timed structures. We define the semantics of the
resulting logic TATL by restricting the players to physically meaningful strategies,
which do not prevent time from diverging. We show that TATL can be model checked
over timed automaton games. We also specify timed optimization problems for physically
meaningful strategies, and we show that for timed automaton games, the optimal
answers can be approximated to within any degree of precision.
acknowledgement: This research was supported in part by the NSF grants CCR-0208875,
CCR-0225610, and CCR-0234690.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vinayak
full_name: Prabhu, Vinayak S
last_name: Prabhu
citation:
ama: 'Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: Vol 4202.
Springer; 2006:1-17. doi:10.1007/11867340_1'
apa: 'Henzinger, T. A., & Prabhu, V. (2006). Timed alternating-time temporal
logic (Vol. 4202, pp. 1–17). Presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, Springer. https://doi.org/10.1007/11867340_1'
chicago: Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal
Logic,” 4202:1–17. Springer, 2006. https://doi.org/10.1007/11867340_1.
ieee: 'T. A. Henzinger and V. Prabhu, “Timed alternating-time temporal logic,” presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, vol. 4202,
pp. 1–17.'
ista: 'Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.'
mla: Henzinger, Thomas A., and Vinayak Prabhu. Timed Alternating-Time Temporal
Logic. Vol. 4202, Springer, 2006, pp. 1–17, doi:10.1007/11867340_1.
short: T.A. Henzinger, V. Prabhu, in:, Springer, 2006, pp. 1–17.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:49Z
date_published: 2006-09-19T00:00:00Z
date_updated: 2021-01-12T07:56:56Z
day: '19'
doi: 10.1007/11867340_1
extern: 1
intvolume: ' 4202'
month: '09'
page: 1 - 17
publication_status: published
publisher: Springer
publist_id: '296'
quality_controlled: 0
status: public
title: Timed alternating-time temporal logic
type: conference
volume: 4202
year: '2006'
...
---
_id: '4436'
abstract:
- lang: eng
text: We present an assume-guarantee interface algebra for real-time components.
In our formalism a component implements a set of task sequences that share a resource.
A component interface consists of an arrival rate function and a latency for each
task sequence, and a capacity function for the shared resource. The interface
specifies that the component guarantees certain task latencies depending on assumptions
about task arrival rates and allocated resource capacities. Our algebra defines
compatibility and refinement relations on interfaces. Interface compatibility
can be checked on partial designs, even when some component interfaces are yet
unknown. In this case interface composition computes as new assumptions the weakest
constraints on the unknown components that are necessary to satisfy the specified
guarantees. Interface refinement is defined in a way that ensures that compatible
interfaces can be refined and implemented independently. Our algebra thus formalizes
an interface-based design methodology that supports both the incremental addition
of new components and the independent stepwise refinement of existing components.
We demonstrate the flexibility and efficiency of the framework through simulation
experiments.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Matic S. An interface algebra for real-time components. In:
IEEE; 2006:253-266. doi:10.1109/RTAS.2006.11'
apa: 'Henzinger, T. A., & Matic, S. (2006). An interface algebra for real-time
components (pp. 253–266). Presented at the RTAS: Real-time and Embedded Technology
and Applications Symposium, IEEE. https://doi.org/10.1109/RTAS.2006.11'
chicago: Henzinger, Thomas A, and Slobodan Matic. “An Interface Algebra for Real-Time
Components,” 253–66. IEEE, 2006. https://doi.org/10.1109/RTAS.2006.11.
ieee: 'T. A. Henzinger and S. Matic, “An interface algebra for real-time components,”
presented at the RTAS: Real-time and Embedded Technology and Applications Symposium,
2006, pp. 253–266.'
ista: 'Henzinger TA, Matic S. 2006. An interface algebra for real-time components.
RTAS: Real-time and Embedded Technology and Applications Symposium, 253–266.'
mla: Henzinger, Thomas A., and Slobodan Matic. An Interface Algebra for Real-Time
Components. IEEE, 2006, pp. 253–66, doi:10.1109/RTAS.2006.11.
short: T.A. Henzinger, S. Matic, in:, IEEE, 2006, pp. 253–266.
conference:
name: 'RTAS: Real-time and Embedded Technology and Applications Symposium'
date_created: 2018-12-11T12:08:50Z
date_published: 2006-04-24T00:00:00Z
date_updated: 2021-01-12T07:56:57Z
day: '24'
doi: 10.1109/RTAS.2006.11
extern: 1
month: '04'
page: 253 - 266
publication_status: published
publisher: IEEE
publist_id: '294'
quality_controlled: 0
status: public
title: An interface algebra for real-time components
type: conference
year: '2006'
...
---
_id: '4437'
abstract:
- lang: eng
text: The synthesis of reactive systems requires the solution of two-player games
on graphs with ω-regular objectives. When the objective is specified by a linear
temporal logic formula or nondeterministic Büchi automaton, then previous algorithms
for solving the game require the construction of an equivalent deterministic automaton.
However, determinization for automata on infinite words is extremely complicated,
and current implementations fail to produce deterministic automata even for relatively
small inputs. We show how to construct, from a given nondeterministic Büchi automaton,
an equivalent nondeterministic parity automaton that is good for solving games
with objective . The main insight is that a nondeterministic automaton is good
for solving games if it fairly simulates the equivalent deterministic automaton.
In this way, we omit the determinization step in game solving and reactive synthesis.
The fact that our automata are nondeterministic makes them surprisingly simple,
amenable to symbolic implementation, and allows an incremental search for winning
strategies.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Henzinger TA, Piterman N. Solving games without determinization. In: Vol 4207.
Springer; 2006:395-410. doi:10.1007/11874683_26'
apa: 'Henzinger, T. A., & Piterman, N. (2006). Solving games without determinization
(Vol. 4207, pp. 395–410). Presented at the CSL: Computer Science Logic, Springer.
https://doi.org/10.1007/11874683_26'
chicago: Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization,”
4207:395–410. Springer, 2006. https://doi.org/10.1007/11874683_26.
ieee: 'T. A. Henzinger and N. Piterman, “Solving games without determinization,”
presented at the CSL: Computer Science Logic, 2006, vol. 4207, pp. 395–410.'
ista: 'Henzinger TA, Piterman N. 2006. Solving games without determinization. CSL:
Computer Science Logic, LNCS, vol. 4207, 395–410.'
mla: Henzinger, Thomas A., and Nir Piterman. Solving Games without Determinization.
Vol. 4207, Springer, 2006, pp. 395–410, doi:10.1007/11874683_26.
short: T.A. Henzinger, N. Piterman, in:, Springer, 2006, pp. 395–410.
conference:
name: 'CSL: Computer Science Logic'
date_created: 2018-12-11T12:08:51Z
date_published: 2006-09-20T00:00:00Z
date_updated: 2021-01-12T07:56:58Z
day: '20'
doi: 10.1007/11874683_26
extern: 1
intvolume: ' 4207'
month: '09'
page: 395 - 410
publication_status: published
publisher: Springer
publist_id: '295'
quality_controlled: 0
status: public
title: Solving games without determinization
type: conference
volume: 4207
year: '2006'
...
---
_id: '4451'
abstract:
- lang: eng
text: One source of complexity in the μ-calculus is its ability to specify an unbounded
number of switches between universal (AX) and existential (EX) branching modes.
We therefore study the problems of satisfiability, validity, model checking, and
implication for the universal and existential fragments of the μ-calculus, in
which only one branching mode is allowed. The universal fragment is rich enough
to express most specifications of interest, and therefore improved algorithms
are of practical importance. We show that while the satisfiability and validity
problems become indeed simpler for the existential and universal fragments, this
is, unfortunately, not the case for model checking and implication. We also show
the corresponding results for the alternation-free fragment of the μ-calculus,
where no alternations between least and greatest fixed points are allowed. Our
results imply that efforts to find a polynomial-time model-checking algorithm
for the μ-calculus can be replaced by efforts to find such an algorithm for the
universal or existential fragment.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments
of the mu-calculus. Theoretical Computer Science. 2006;354(2):173-186.
doi:10.1016/j.tcs.2005.11.015
apa: Henzinger, T. A., Kupferman, O., & Majumdar, R. (2006). On the universal
and existential fragments of the mu-calculus. Theoretical Computer Science.
Elsevier. https://doi.org/10.1016/j.tcs.2005.11.015
chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science.
Elsevier, 2006. https://doi.org/10.1016/j.tcs.2005.11.015.
ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
fragments of the mu-calculus,” Theoretical Computer Science, vol. 354,
no. 2. Elsevier, pp. 173–186, 2006.
ista: Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential
fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186.
mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of
the Mu-Calculus.” Theoretical Computer Science, vol. 354, no. 2, Elsevier,
2006, pp. 173–86, doi:10.1016/j.tcs.2005.11.015.
short: T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354
(2006) 173–186.
date_created: 2018-12-11T12:08:55Z
date_published: 2006-03-28T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '28'
doi: 10.1016/j.tcs.2005.11.015
extern: 1
intvolume: ' 354'
issue: '2'
month: '03'
page: 173 - 186
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '276'
quality_controlled: 0
status: public
title: On the universal and existential fragments of the mu-calculus
type: journal_article
volume: 354
year: '2006'
...
---
_id: '4523'
abstract:
- lang: eng
text: We consider the problem if a given program satisfies a specified safety property.
Interesting programs have infinite state spaces, with inputs ranging over infinite
domains, and for these programs the property checking problem is undecidable.
Two broad approaches to property checking are testing and verification. Testing
tries to find inputs and executions which demonstrate violations of the property.
Verification tries to construct a formal proof which shows that all executions
of the program satisfy the property. Testing works best when errors are easy to
find, but it is often difficult to achieve sufficient coverage for correct programs.
On the other hand, verification methods are most successful when proofs are easy
to find, but they are often inefficient at discovering errors. We propose a new
algorithm, Synergy, which combines testing and verification. Synergy unifies several
ideas from the literature, including counterexample-guided model checking, directed
testing, and partition refinement.This paper presents a description of the Synergy
algorithm, its theoretical properties, a comparison with related algorithms, and
a prototype implementation called Yogi.
author:
- first_name: Bhargav
full_name: Gulavani, Bhargav S
last_name: Gulavani
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Yamini
full_name: Kannan, Yamini
last_name: Kannan
- first_name: Aditya
full_name: Nori, Aditya V
last_name: Nori
- first_name: Sriram
full_name: Rajamani, Sriram K
last_name: Rajamani
citation:
ama: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm
for property checking. In: ACM; 2006:117-127. doi:10.1145/1181775.1181790'
apa: 'Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., & Rajamani, S. (2006).
Synergy: A new algorithm for property checking (pp. 117–127). Presented at the
FSE: Foundations of Software Engineering, ACM. https://doi.org/10.1145/1181775.1181790'
chicago: 'Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and
Sriram Rajamani. “Synergy: A New Algorithm for Property Checking,” 117–27. ACM,
2006. https://doi.org/10.1145/1181775.1181790.'
ieee: 'B. Gulavani, T. A. Henzinger, Y. Kannan, A. Nori, and S. Rajamani, “Synergy:
A new algorithm for property checking,” presented at the FSE: Foundations of Software
Engineering, 2006, pp. 117–127.'
ista: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. 2006. Synergy: A
new algorithm for property checking. FSE: Foundations of Software Engineering,
117–127.'
mla: 'Gulavani, Bhargav, et al. Synergy: A New Algorithm for Property Checking.
ACM, 2006, pp. 117–27, doi:10.1145/1181775.1181790.'
short: B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, ACM, 2006,
pp. 117–127.
conference:
name: 'FSE: Foundations of Software Engineering'
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '01'
doi: 10.1145/1181775.1181790
extern: 1
month: '01'
page: 117 - 127
publication_status: published
publisher: ACM
publist_id: '206'
quality_controlled: 0
status: public
title: 'Synergy: A new algorithm for property checking'
type: conference
year: '2006'
...
---
_id: '4526'
abstract:
- lang: eng
text: 'We designed and implemented a new programming language called Hierarchical
Timing Language (HTL) for hard realtime systems. Critical timing constraints are
specified within the language,and ensured by the compiler. Programs in HTL are
extensible in two dimensions without changing their timing behavior: new program
modules can be added, and individual program tasks can be refined. The mechanism
supporting time invariance under parallel composition is that different program
modules communicate at specified instances of time. Time invariance under refinement
is achieved by conservative scheduling of the top level. HTL is a coordination
language, in that individual tasks can be implemented in "foreign" languages.
As a case study, we present a distributed HTL implementation of an automotive
steer-by-wire controller.'
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Daniel
full_name: Iercan, Daniel
last_name: Iercan
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Alberto
full_name: Sangiovanni-Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. A hierarchical
coordination language for interacting real-time tasks. In: ACM; 2006:132-141.
doi:10.1145/1176887.1176907'
apa: 'Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., & Sangiovanni Vincentelli,
A. (2006). A hierarchical coordination language for interacting real-time tasks
(pp. 132–141). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1176887.1176907'
chicago: Ghosal, Arkadeb, Thomas A Henzinger, Daniel Iercan, Christoph Kirsch, and
Alberto Sangiovanni Vincentelli. “A Hierarchical Coordination Language for Interacting
Real-Time Tasks,” 132–41. ACM, 2006. https://doi.org/10.1145/1176887.1176907.
ieee: 'A. Ghosal, T. A. Henzinger, D. Iercan, C. Kirsch, and A. Sangiovanni Vincentelli,
“A hierarchical coordination language for interacting real-time tasks,” presented
at the EMSOFT: Embedded Software , 2006, pp. 132–141.'
ista: 'Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. 2006.
A hierarchical coordination language for interacting real-time tasks. EMSOFT:
Embedded Software , 132–141.'
mla: Ghosal, Arkadeb, et al. A Hierarchical Coordination Language for Interacting
Real-Time Tasks. ACM, 2006, pp. 132–41, doi:10.1145/1176887.1176907.
short: A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, A. Sangiovanni Vincentelli,
in:, ACM, 2006, pp. 132–141.
conference:
name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '01'
doi: 10.1145/1176887.1176907
extern: 1
month: '01'
page: 132 - 141
publication_status: published
publisher: ACM
publist_id: '201'
quality_controlled: 0
status: public
title: A hierarchical coordination language for interacting real-time tasks
type: conference
year: '2006'
...
---
_id: '4528'
abstract:
- lang: eng
text: Computational modeling of biological systems is becoming increasingly common
as scientists attempt to understand biological phenomena in their full complexity.
Here we distinguish between two types of biological models mathematical and computational
- according to their different representations of biological phenomena and their
diverse potential. We call the approach of constructing computational models of
biological systems executable biology, as it focuses on the design of executable
computer algorithms that mimic biological phenomena. We give an overview of the
main modeling efforts in this direction, and discuss some of the new challenges
that executable biology poses for computer science and biology. We argue that
for executable biology to reach its full potential as a mainstream biological
technique, formal and algorithmic approaches must be integrated into biological
research, driving biology towards a more precise engineering discipline.
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Fisher J, Henzinger TA. Executable biology. In: IEEE; 2006:1675-1682. doi:10.1109/WSC.2006.322942'
apa: 'Fisher, J., & Henzinger, T. A. (2006). Executable biology (pp. 1675–1682).
Presented at the WSC: Winter Simulation Conference, IEEE. https://doi.org/10.1109/WSC.2006.322942'
chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Biology,” 1675–82.
IEEE, 2006. https://doi.org/10.1109/WSC.2006.322942.
ieee: 'J. Fisher and T. A. Henzinger, “Executable biology,” presented at the WSC:
Winter Simulation Conference, 2006, pp. 1675–1682.'
ista: 'Fisher J, Henzinger TA. 2006. Executable biology. WSC: Winter Simulation
Conference, 1675–1682.'
mla: Fisher, Jasmin, and Thomas A. Henzinger. Executable Biology. IEEE, 2006,
pp. 1675–82, doi:10.1109/WSC.2006.322942.
short: J. Fisher, T.A. Henzinger, in:, IEEE, 2006, pp. 1675–1682.
conference:
name: 'WSC: Winter Simulation Conference'
date_created: 2018-12-11T12:09:19Z
date_published: 2006-12-03T00:00:00Z
date_updated: 2021-01-12T07:59:28Z
day: '03'
doi: 10.1109/WSC.2006.322942
extern: 1
month: '12'
page: 1675 - 1682
publication_status: published
publisher: IEEE
publist_id: '197'
quality_controlled: 0
status: public
title: Executable biology
type: conference
year: '2006'
...
---
_id: '4538'
abstract:
- lang: eng
text: A stochastic graph game is played by two players on a game graph with probabilistic
transitions. We consider stochastic graph games with ω-regular winning conditions
specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy
improvement algorithm for stochastic parity games; this is the first non-brute-force
algorithm for solving these games. From the strategy improvement algorithm we
obtain a randomized subexponential-time algorithm to solve such games.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Strategy improvement and randomized subexponential
algorithms for stochastic parity games. In: Vol 3884. Springer; 2006:512-523.
doi:10.1007/11672142_42'
apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Strategy improvement and randomized
subexponential algorithms for stochastic parity games (Vol. 3884, pp. 512–523).
Presented at the STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_42'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games,” 3884:512–23.
Springer, 2006. https://doi.org/10.1007/11672142_42.
ieee: 'K. Chatterjee and T. A. Henzinger, “Strategy improvement and randomized subexponential
algorithms for stochastic parity games,” presented at the STACS: Theoretical Aspects
of Computer Science, 2006, vol. 3884, pp. 512–523.'
ista: 'Chatterjee K, Henzinger TA. 2006. Strategy improvement and randomized subexponential
algorithms for stochastic parity games. STACS: Theoretical Aspects of Computer
Science, LNCS, vol. 3884, 512–523.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games. Vol. 3884,
Springer, 2006, pp. 512–23, doi:10.1007/11672142_42.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 512–523.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '14'
doi: 10.1007/11672142_42
extern: 1
intvolume: ' 3884'
month: '02'
page: 512 - 523
publication_status: published
publisher: Springer
publist_id: '184'
quality_controlled: 0
status: public
title: Strategy improvement and randomized subexponential algorithms for stochastic
parity games
type: conference
volume: 3884
year: '2006'
...
---
_id: '4539'
abstract:
- lang: eng
text: Games on graphs with ω-regular objectives provide a model for the control
and synthesis of reactive systems. Every ω-regular objective can be decomposed
into a safety part and a liveness part. The liveness part ensures that something
good happens “eventually.” Two main strengths of the classical, infinite-limit
formulation of liveness are robustness (independence from the granularity of transitions)
and simplicity (abstraction of complicated time bounds). However, the classical
liveness formulation suffers from the drawback that the time until something good
happens may be unbounded. A stronger formulation of liveness, so-called finitary
liveness, overcomes this drawback, while still retaining robustness and simplicity.
Finitary liveness requires that there exists an unknown, fixed bound b such that
something good happens within b transitions. While for one-shot liveness (reachability)
objectives, classical and finitary liveness coincide, for repeated liveness (Büchi)
objectives, the finitary formulation is strictly stronger. In this work we study
games with finitary parity and Streett (fairness) objectives. We prove the determinacy
of these games, present algorithms for solving these games, and characterize the
memory requirements of winning strategies. Our algorithms can be used, for example,
for synthesizing controllers that do not let the response time of a system increase
without bound.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
and the NSF ITR grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Finitary winning in omega-regular games. In: Vol
3920. Springer; 2006:257-271. doi:10.1007/11691372_17'
apa: 'Chatterjee, K., & Henzinger, T. A. (2006). Finitary winning in omega-regular
games (Vol. 3920, pp. 257–271). Presented at the TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, Springer. https://doi.org/10.1007/11691372_17'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Finitary Winning in Omega-Regular
Games,” 3920:257–71. Springer, 2006. https://doi.org/10.1007/11691372_17.
ieee: 'K. Chatterjee and T. A. Henzinger, “Finitary winning in omega-regular games,”
presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, 2006, vol. 3920, pp. 257–271.'
ista: 'Chatterjee K, Henzinger TA. 2006. Finitary winning in omega-regular games.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 3920, 257–271.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Finitary Winning in Omega-Regular
Games. Vol. 3920, Springer, 2006, pp. 257–71, doi:10.1007/11691372_17.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 257–271.
conference:
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-03-15T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '15'
doi: 10.1007/11691372_17
extern: 1
intvolume: ' 3920'
month: '03'
page: 257 - 271
publication_status: published
publisher: Springer
publist_id: '183'
quality_controlled: 0
status: public
title: Finitary winning in omega-regular games
type: conference
volume: 3920
year: '2006'
...
---
_id: '4549'
abstract:
- lang: eng
text: We present a compositional theory of system verification, where specifications
assign real-numbered costs to systems. These costs can express a wide variety
of quantitative system properties, such as resource consumption, price, or a measure
of how well a system satisfies its specification. The theory supports the composition
of systems and specifications, and the hiding of variables. Boolean refinement
relations are replaced by real-numbered distances between descriptions of a system
at different levels of detail. We show that the classical Boolean rules for compositional
reasoning have quantitative counterparts in our setting. While our general theory
allows costs to be specified by arbitrary cost functions, we also consider a class
of linear cost functions, which give rise to an instance of our framework where
all operations are computable in polynomial time.
acknowledgement: Supported in part by the NSF grants CCR-0234690, CCR-0208875, and
CCR-0225610; by the NSF grant CCR-0132780 and ARP grant SC20051123.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Marco
full_name: Faella, Marco
last_name: Faella
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: 'Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M.
Compositional quantitative reasoning. In: IEEE; 2006:179-188. doi:10.1109/QEST.2006.11'
apa: 'Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R.,
& Stoelinga, M. (2006). Compositional quantitative reasoning (pp. 179–188).
Presented at the QEST: Quantitative Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.11'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Thomas A Henzinger,
Ritankar Majumdar, and Mariëlle Stoelinga. “Compositional Quantitative Reasoning,”
179–88. IEEE, 2006. https://doi.org/10.1109/QEST.2006.11.
ieee: 'K. Chatterjee, L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and
M. Stoelinga, “Compositional quantitative reasoning,” presented at the QEST: Quantitative
Evaluation of Systems, 2006, pp. 179–188.'
ista: 'Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga
M. 2006. Compositional quantitative reasoning. QEST: Quantitative Evaluation of
Systems, 179–188.'
mla: Chatterjee, Krishnendu, et al. Compositional Quantitative Reasoning.
IEEE, 2006, pp. 179–88, doi:10.1109/QEST.2006.11.
short: K. Chatterjee, L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga,
in:, IEEE, 2006, pp. 179–188.
conference:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-09-01T00:00:00Z
date_updated: 2021-01-12T07:59:37Z
day: '01'
doi: 10.1109/QEST.2006.11
extern: 1
month: '09'
page: 179 - 188
publication_status: published
publisher: IEEE
publist_id: '163'
quality_controlled: 0
status: public
title: Compositional quantitative reasoning
type: conference
year: '2006'
...
---
_id: '4550'
abstract:
- lang: eng
text: 'In 2-player non-zero-sum games, Nash equilibria capture the options for rational
behavior if each player attempts to maximize her payoff. In contrast to classical
game theory, we consider lexicographic objectives: first, each player tries to
maximize her own payoff, and then, the player tries to minimize the opponent''s
payoff. Such objectives arise naturally in the verification of systems with multiple
components. There, instead of proving that each component satisfies its specification
no matter how the other components behave, it sometimes suffices to prove that
each component satisfies its specification provided that the other components
satisfy their specifications. We say that a Nash equilibrium is secure if it is
an equilibrium with respect to the lexicographic objectives of both players. We
prove that in graph games with Borel winning conditions, which include the games
that arise in verification, there may be several Nash equilibria, but there is
always a unique maximal payoff profile of a secure equilibrium. We show how this
equilibrium can be computed in the case of ω-regular winning conditions, and we
characterize the memory requirements of strategies that achieve the equilibrium.'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
citation:
ama: Chatterjee K, Henzinger TA, Jurdziński M. Games with secure equilibria. Theoretical
Computer Science. 2006;365(1-2):67-82. doi:10.1016/j.tcs.2006.07.032
apa: Chatterjee, K., Henzinger, T. A., & Jurdziński, M. (2006). Games with secure
equilibria. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2006.07.032
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Games
with Secure Equilibria.” Theoretical Computer Science. Elsevier, 2006.
https://doi.org/10.1016/j.tcs.2006.07.032.
ieee: K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Games with secure equilibria,”
Theoretical Computer Science, vol. 365, no. 1–2. Elsevier, pp. 67–82, 2006.
ista: Chatterjee K, Henzinger TA, Jurdziński M. 2006. Games with secure equilibria.
Theoretical Computer Science. 365(1–2), 67–82.
mla: Chatterjee, Krishnendu, et al. “Games with Secure Equilibria.” Theoretical
Computer Science, vol. 365, no. 1–2, Elsevier, 2006, pp. 67–82, doi:10.1016/j.tcs.2006.07.032.
short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science
365 (2006) 67–82.
date_created: 2018-12-11T12:09:26Z
date_published: 2006-08-07T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '07'
doi: 10.1016/j.tcs.2006.07.032
extern: 1
intvolume: ' 365'
issue: 1-2
month: '08'
page: 67 - 82
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '164'
quality_controlled: 0
status: public
title: Games with secure equilibria
type: journal_article
volume: 365
year: '2006'
...
---
_id: '4551'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple discounted reward
objectives. Such MDPs occur in design problems where one wishes to simultaneously
optimize several criteria, for example, latency and power. The possible trade-offs
between the different objectives are characterized by the Pareto curve. We show
that every Pareto-optimal point can be achieved by a memoryless strategy; however,
unlike in the single-objective case, the memoryless strategy may require randomization.
Moreover, we show that the Pareto curve can be approximated in polynomial time
in the size of the MDP. Additionally, we study the problem if a given value vector
is realizable by any strategy, and show that it can be decided in polynomial time;
but the question whether it is realizable by a deterministic memoryless strategy
is NP-complete. These results provide efficient algorithms for design exploration
in MDP models with multiple objectives.\nThis research was supported in part by
the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690,
and CCR-0427202. "
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Majumdar R, Henzinger TA. Markov decision processes with multiple
objectives. In: Vol 3884. Springer; 2006:325-336. doi:10.1007/11672142_26'
apa: 'Chatterjee, K., Majumdar, R., & Henzinger, T. A. (2006). Markov decision
processes with multiple objectives (Vol. 3884, pp. 325–336). Presented at the
STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_26'
chicago: Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov
Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. https://doi.org/10.1007/11672142_26.
ieee: 'K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Markov decision processes
with multiple objectives,” presented at the STACS: Theoretical Aspects of Computer
Science, 2006, vol. 3884, pp. 325–336.'
ista: 'Chatterjee K, Majumdar R, Henzinger TA. 2006. Markov decision processes with
multiple objectives. STACS: Theoretical Aspects of Computer Science, LNCS, vol.
3884, 325–336.'
mla: Chatterjee, Krishnendu, et al. Markov Decision Processes with Multiple Objectives.
Vol. 3884, Springer, 2006, pp. 325–36, doi:10.1007/11672142_26.
short: K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '14'
doi: 10.1007/11672142_26
extern: 1
intvolume: ' 3884'
month: '02'
page: 325 - 336
publication_status: published
publisher: Springer
publist_id: '161'
quality_controlled: 0
status: public
title: Markov decision processes with multiple objectives
type: conference
volume: 3884
year: '2006'
...
---
_id: '4552'
abstract:
- lang: eng
text: 'A concurrent reachability game is a two-player game played on a graph: at
each state, the players simultaneously and independently select moves; the two
moves determine jointly a probability distribution over the successor states.
The objective for player 1 consists in reaching a set of target states; the objective
for player 2 is to prevent this, so that the game is zero-sum. Our contributions
are two-fold. First, we present a simple proof of the fact that in concurrent
reachability games, for all epsilon > 0, memoryless epsilon-optimal strategies
exist. A memoryless strategy is independent of the history of plays, and an epsilon-optimal
strategy achieves the objective with probability within epsilon of the value of
the game. In contrast to previous proofs of this fact, which rely on the limit
behavior of discounted games using advanced Puisieux series analysis, our proof
is elementary and combinatorial. Second, we present a strategy-improvement (a.k.a.
policy-iteration) algorithm for concurrent games with reachability objectives.'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent
reachability games. In: IEEE; 2006:291-300. doi:10.1109/QEST.2006.48'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2006). Strategy improvement
for concurrent reachability games (pp. 291–300). Presented at the QEST: Quantitative
Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.48'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy
Improvement for Concurrent Reachability Games,” 291–300. IEEE, 2006. https://doi.org/10.1109/QEST.2006.48.
ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for
concurrent reachability games,” presented at the QEST: Quantitative Evaluation
of Systems, 2006, pp. 291–300.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2006. Strategy improvement for concurrent
reachability games. QEST: Quantitative Evaluation of Systems, 291–300.'
mla: Chatterjee, Krishnendu, et al. Strategy Improvement for Concurrent Reachability
Games. IEEE, 2006, pp. 291–300, doi:10.1109/QEST.2006.48.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2006, pp. 291–300.
conference:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '01'
doi: 10.1109/QEST.2006.48
extern: 1
month: '01'
page: 291 - 300
publication_status: published
publisher: IEEE
publist_id: '162'
quality_controlled: 0
status: public
title: Strategy improvement for concurrent reachability games
type: conference
year: '2006'
...
---
_id: '4574'
abstract:
- lang: eng
text: Many software model checkers are based on predicate abstraction. If the verification
goal depends on pointer structures, the approach does not work well, because it
is difficult to find adequate predicate abstractions for the heap. In contrast,
shape analysis, which uses graph-based heap abstractions, can provide a compact
representation of recursive data structures. We integrate shape analysis into
the software model checker Blast. Because shape analysis is expensive, we do not
apply it globally. Instead, we ensure that, like predicates, shape graphs are
computed and stored locally, only where necessary for proving the verification
goal. To achieve this, we extend lazy abstraction refinement, which so far has
been used only for predicate abstractions, to three-valued logical structures.
This approach does not only increase the precision of model checking, but it also
increases the efficiency of shape analysis. We implemented the technique by extending
Blast with calls to Tvla.
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Grégory
full_name: Théoduloz, Grégory
last_name: Théoduloz
citation:
ama: 'Beyer D, Henzinger TA, Théoduloz G. Lazy shape analysis. In: Vol 4144. Springer;
2006:532-546. doi:10.1007/11817963_48'
apa: 'Beyer, D., Henzinger, T. A., & Théoduloz, G. (2006). Lazy shape analysis
(Vol. 4144, pp. 532–546). Presented at the CAV: Computer Aided Verification, Springer.
https://doi.org/10.1007/11817963_48'
chicago: Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Lazy Shape Analysis,”
4144:532–46. Springer, 2006. https://doi.org/10.1007/11817963_48.
ieee: 'D. Beyer, T. A. Henzinger, and G. Théoduloz, “Lazy shape analysis,” presented
at the CAV: Computer Aided Verification, 2006, vol. 4144, pp. 532–546.'
ista: 'Beyer D, Henzinger TA, Théoduloz G. 2006. Lazy shape analysis. CAV: Computer
Aided Verification, LNCS, vol. 4144, 532–546.'
mla: Beyer, Dirk, et al. Lazy Shape Analysis. Vol. 4144, Springer, 2006,
pp. 532–46, doi:10.1007/11817963_48.
short: D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Springer, 2006, pp. 532–546.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:09:33Z
date_published: 2006-08-08T00:00:00Z
date_updated: 2021-01-12T07:59:49Z
day: '08'
doi: 10.1007/11817963_48
extern: 1
intvolume: ' 4144'
month: '08'
page: 532 - 546
publication_status: published
publisher: Springer
publist_id: '133'
quality_controlled: 0
status: public
title: Lazy shape analysis
type: conference
volume: 4144
year: '2006'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '854'
abstract:
- lang: eng
text: Phylogenetic relationships between the extinct woolly mammoth (Mammuthus primigenius),
and the Asian (Elephas maximus) and African savanna (Loxodonta africana) elephants
remain unresolved. Here, we report the sequence of the complete mitochondrial
genome (16,842 base pairs) of a woolly mammoth extracted from permafrost-preserved
remains from the Pleistocene epoch - the oldest mitochondrial genome sequence
determined to date. We demonstrate that well-preserved mitochondrial genome fragments,
as long as ∼1,600-1700 base pairs, can be retrieved from pre-Holocene remains
of an extinct species. Phylogenetic reconstruction of the Elephantinae clade suggests
that M. primigenius and E. maximus are sister species that diverged soon after
their common ancestor split from the L. africana lineage. Low nucleotide diversity
found between independently determined mitochondrial genomic sequences of woolly
mammoths separated geographically and in time suggests that north-eastern Siberia
was occupied by a relatively homogeneous population of M. primigenius throughout
the late Pleistocene.
acknowledgement: "FAK is supported by the NSF Graduate Research Fellowship.\r\nWe
thank the Natural History Museum, North-Eastern Research Center, Far Eastern Branch
of the Russian Academy of Sciences for photographic material ofM. primigenius leg,
V. A. Nikishina for artwork and technical support, Y.B. Yurov, G. Dvoryanchikov,
N. Riazanskaya and T. Kolesnikova for technical support, K. Mehren and C. Gray for
elephant specimens, and V. Y. Solovyev for help with artwork of animal images."
article_processing_charge: No
article_type: original
author:
- first_name: Evgeny
full_name: Rogaev, Evgeny
last_name: Rogaev
- first_name: Yuri
full_name: Moliaka, Yuri
last_name: Moliaka
- first_name: Boris
full_name: Malyarchuk, Boris
last_name: Malyarchuk
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Miroslava
full_name: Derenko, Miroslava
last_name: Derenko
- first_name: Ilya
full_name: Chumakov, Ilya
last_name: Chumakov
- first_name: Anastasia
full_name: Grigorenko, Anastasia
last_name: Grigorenko
citation:
ama: Rogaev E, Moliaka Y, Malyarchuk B, et al. Complete mitochondrial genome and
phylogeny of pleistocene mammoth Mammuthus primigenius. PLoS Biology. 2006;4(3):0403-0410.
doi:10.1371/journal.pbio.0040073
apa: Rogaev, E., Moliaka, Y., Malyarchuk, B., Kondrashov, F., Derenko, M., Chumakov,
I., & Grigorenko, A. (2006). Complete mitochondrial genome and phylogeny of
pleistocene mammoth Mammuthus primigenius. PLoS Biology. Public Library
of Science. https://doi.org/10.1371/journal.pbio.0040073
chicago: Rogaev, Evgeny, Yuri Moliaka, Boris Malyarchuk, Fyodor Kondrashov, Miroslava
Derenko, Ilya Chumakov, and Anastasia Grigorenko. “Complete Mitochondrial Genome
and Phylogeny of Pleistocene Mammoth Mammuthus Primigenius.” PLoS Biology.
Public Library of Science, 2006. https://doi.org/10.1371/journal.pbio.0040073.
ieee: E. Rogaev et al., “Complete mitochondrial genome and phylogeny of pleistocene
mammoth Mammuthus primigenius,” PLoS Biology, vol. 4, no. 3. Public Library
of Science, pp. 0403–0410, 2006.
ista: Rogaev E, Moliaka Y, Malyarchuk B, Kondrashov F, Derenko M, Chumakov I, Grigorenko
A. 2006. Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus
primigenius. PLoS Biology. 4(3), 0403–0410.
mla: Rogaev, Evgeny, et al. “Complete Mitochondrial Genome and Phylogeny of Pleistocene
Mammoth Mammuthus Primigenius.” PLoS Biology, vol. 4, no. 3, Public Library
of Science, 2006, pp. 0403–10, doi:10.1371/journal.pbio.0040073.
short: E. Rogaev, Y. Moliaka, B. Malyarchuk, F. Kondrashov, M. Derenko, I. Chumakov,
A. Grigorenko, PLoS Biology 4 (2006) 0403–0410.
date_created: 2018-12-11T11:48:51Z
date_published: 2006-02-07T00:00:00Z
date_updated: 2026-05-08T10:07:52Z
day: '07'
ddc:
- '570'
doi: 10.1371/journal.pbio.0040073
extern: '1'
external_id:
pmid:
- '16448217'
intvolume: ' 4'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1371/journal.pbio.0040073
month: '02'
oa: 1
oa_version: Published Version
page: 0403 - 0410
pmid: 1
publication: PLoS Biology
publication_identifier:
eissn:
- 1545-7885
issn:
- 1544-9173
publication_status: published
publisher: Public Library of Science
publist_id: '6794'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus
primigenius
tmp:
image: /images/cc_0.png
legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
name: Creative Commons Public Domain Dedication (CC0 1.0)
short: CC0 (1.0)
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 4
year: '2006'
...