---
_id: '11756'
abstract:
- lang: eng
text: We give two fully dynamic algorithms that maintain a (1 + ε)-approximation
of the weight M of a minimum spanning forest (MSF) of an n-node graph G with edges
weights in [1, W ], for any ε > 0. (1) Our deterministic algorithm takes O (W
2 log W /ε3) worst-case update time, which is O (1) if both W and ε are constants.
(2) Our randomized (Monte-Carlo style) algorithm works with high probability and
runs in worst-case O (log W /ε4) update time if W = O ((m∗)1/6/log2/3 n), where
m∗ is the minimum number of edges in the graph throughout all the updates. It
works even against an adaptive adversary. We complement our algorithmic results
with two cell-probe lower bounds for dynamically maintaining an approximation
of the weight of an MSF of a graph.
article_number: '104805'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Pan
full_name: Peng, Pan
last_name: Peng
citation:
ama: Henzinger MH, Peng P. Constant-time dynamic weight approximation for minimum
spanning forest. Information and Computation. 2021;281(12). doi:10.1016/j.ic.2021.104805
apa: Henzinger, M. H., & Peng, P. (2021). Constant-time dynamic weight approximation
for minimum spanning forest. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2021.104805
chicago: Henzinger, Monika H, and Pan Peng. “Constant-Time Dynamic Weight Approximation
for Minimum Spanning Forest.” Information and Computation. Elsevier, 2021.
https://doi.org/10.1016/j.ic.2021.104805.
ieee: M. H. Henzinger and P. Peng, “Constant-time dynamic weight approximation for
minimum spanning forest,” Information and Computation, vol. 281, no. 12.
Elsevier, 2021.
ista: Henzinger MH, Peng P. 2021. Constant-time dynamic weight approximation for
minimum spanning forest. Information and Computation. 281(12), 104805.
mla: Henzinger, Monika H., and Pan Peng. “Constant-Time Dynamic Weight Approximation
for Minimum Spanning Forest.” Information and Computation, vol. 281, no.
12, 104805, Elsevier, 2021, doi:10.1016/j.ic.2021.104805.
short: M.H. Henzinger, P. Peng, Information and Computation 281 (2021).
date_created: 2022-08-08T10:58:29Z
date_published: 2021-12-01T00:00:00Z
date_updated: 2022-09-12T09:29:29Z
day: '01'
doi: 10.1016/j.ic.2021.104805
extern: '1'
external_id:
arxiv:
- '2011.00977'
intvolume: ' 281'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2011.00977
month: '12'
oa: 1
oa_version: Preprint
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Constant-time dynamic weight approximation for minimum spanning forest
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 281
year: '2021'
...
---
_id: '11757'
abstract:
- lang: eng
text: We develop a dynamic version of the primal-dual method for optimization problems,
and apply it to obtain the following results. (1) For the dynamic set-cover problem,
we maintain an O ( f 2)-approximately optimal solution in O ( f · log(m + n))
amortized update time, where f is the maximum “frequency” of an element, n is
the number of sets, and m is the maximum number of elements in the universe at
any point in time. (2) For the dynamic b-matching problem, we maintain an O (1)-approximately
optimal solution in O (log3 n) amortized update time, where n is the number of
nodes in the graph.
article_processing_charge: No
article_type: original
author:
- first_name: Sayan
full_name: Bhattacharya, Sayan
last_name: Bhattacharya
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Giuseppe
full_name: Italiano, Giuseppe
last_name: Italiano
citation:
ama: Bhattacharya S, Henzinger MH, Italiano G. Dynamic algorithms via the primal-dual
method. Information and Computation. 2018;261(08):219-239. doi:10.1016/j.ic.2018.02.005
apa: Bhattacharya, S., Henzinger, M. H., & Italiano, G. (2018). Dynamic algorithms
via the primal-dual method. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2018.02.005
chicago: Bhattacharya, Sayan, Monika H Henzinger, and Giuseppe Italiano. “Dynamic
Algorithms via the Primal-Dual Method.” Information and Computation. Elsevier,
2018. https://doi.org/10.1016/j.ic.2018.02.005.
ieee: S. Bhattacharya, M. H. Henzinger, and G. Italiano, “Dynamic algorithms via
the primal-dual method,” Information and Computation, vol. 261, no. 08.
Elsevier, pp. 219–239, 2018.
ista: Bhattacharya S, Henzinger MH, Italiano G. 2018. Dynamic algorithms via the
primal-dual method. Information and Computation. 261(08), 219–239.
mla: Bhattacharya, Sayan, et al. “Dynamic Algorithms via the Primal-Dual Method.”
Information and Computation, vol. 261, no. 08, Elsevier, 2018, pp. 219–39,
doi:10.1016/j.ic.2018.02.005.
short: S. Bhattacharya, M.H. Henzinger, G. Italiano, Information and Computation
261 (2018) 219–239.
date_created: 2022-08-08T11:20:03Z
date_published: 2018-08-01T00:00:00Z
date_updated: 2023-02-10T07:27:39Z
day: '01'
doi: 10.1016/j.ic.2018.02.005
extern: '1'
intvolume: ' 261'
issue: '08'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.ic.2018.02.005
month: '08'
oa: 1
oa_version: Published Version
page: 219-239
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Dynamic algorithms via the primal-dual method
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 261
year: '2018'
...
---
_id: '11758'
article_processing_charge: No
article_type: letter_note
author:
- first_name: Luca
full_name: Aceto, Luca
last_name: Aceto
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Jiří
full_name: Sgall, Jiří
last_name: Sgall
citation:
ama: Aceto L, Henzinger MH, Sgall J. 38th International Colloquium on Automata,
Languages and Programming. Information and Computation. 2013;222(1):1.
doi:10.1016/j.ic.2012.11.002
apa: Aceto, L., Henzinger, M. H., & Sgall, J. (2013). 38th International Colloquium
on Automata, Languages and Programming. Information and Computation. Elsevier.
https://doi.org/10.1016/j.ic.2012.11.002
chicago: Aceto, Luca, Monika H Henzinger, and Jiří Sgall. “38th International Colloquium
on Automata, Languages and Programming.” Information and Computation. Elsevier,
2013. https://doi.org/10.1016/j.ic.2012.11.002.
ieee: L. Aceto, M. H. Henzinger, and J. Sgall, “38th International Colloquium on
Automata, Languages and Programming,” Information and Computation, vol.
222, no. 1. Elsevier, p. 1, 2013.
ista: Aceto L, Henzinger MH, Sgall J. 2013. 38th International Colloquium on Automata,
Languages and Programming. Information and Computation. 222(1), 1.
mla: Aceto, Luca, et al. “38th International Colloquium on Automata, Languages and
Programming.” Information and Computation, vol. 222, no. 1, Elsevier, 2013,
p. 1, doi:10.1016/j.ic.2012.11.002.
short: L. Aceto, M.H. Henzinger, J. Sgall, Information and Computation 222 (2013)
1.
date_created: 2022-08-08T11:25:34Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2023-02-23T10:09:19Z
day: '01'
doi: 10.1016/j.ic.2012.11.002
extern: '1'
intvolume: ' 222'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: '1'
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: 38th International Colloquium on Automata, Languages and Programming
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 222
year: '2013'
...
---
_id: '4474'
abstract:
- lang: eng
text: 'The simulation preorder for labeled transition systems is defined locally,
and operationally, as a game that relates states with their immediate successor
states. Simulation enjoys many appealing properties. First, simulation has a denotational
characterization: system S simulates system I iff every computation tree embedded
in the unrolling of I can be embedded also in the unrolling of S. Second, simulation
has a logical characterization: S simulates I iff every universal branching-time
formula satisfied by S is satisfied also by I. It follows that simulation is a
suitable notion of implementation, and it is the coarsest abstraction of a system
that preserves universal branching-time properties. Third, based on its local
definition, simulation between finite-state systems can be checked in polynomial
time. Finally, simulation implies trace containment, which cannot be defined locally
and requires polynomial space for verification. Hence simulation is widely used
both in manual and in automatic verification. Liveness assumptions about transition
systems are typically modeled using fairness constraints. Existing notions of
simulation for fair transition systems, however, are not local, and as a result,
many appealing properties of the simulation preorder are lost. We propose a new
view of fair simulation by extending the local definition of simulation to account
for fairness: system View the MathML sourcefairly simulates system View the MathML
source iff in the simulation game, there is a strategy that matches with each
fair computation of View the MathML source a fair computation of View the MathML
source. Our definition enjoys a denotational characterization and has a logical
characterization: View the MathML source fairly simulates View the MathML source
iff every fair computation tree (whose infinite paths are fair) embedded in the
unrolling of View the MathML source can be embedded also in the unrolling of View
the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by
View the MathML source is satisfied also by View the MathML source (∀AFMC is the
universal fragment of the alternation-free μ-calculus). The locality of the definition
leads us to a polynomial-time algorithm for checking fair simulation for finite-state
systems with weak and strong fairness constraints. Finally, fair simulation implies
fair trace containment and is therefore useful as an efficiently computable local
criterion for proving linear-time abstraction hierarchies of fair systems.'
acknowledgement: We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers
for their comments on this paper.
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: Henzinger TA, Kupferman O, Rajamani S. Fair simulation. Information and
Computation. 2002;173(1):64-81. doi:10.1006/inco.2001.3085
apa: Henzinger, T. A., Kupferman, O., & Rajamani, S. (2002). Fair simulation.
Information and Computation. Elsevier. https://doi.org/10.1006/inco.2001.3085
chicago: Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.”
Information and Computation. Elsevier, 2002. https://doi.org/10.1006/inco.2001.3085.
ieee: T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” Information
and Computation, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.
ista: Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information
and Computation. 173(1), 64–81.
mla: Henzinger, Thomas A., et al. “Fair Simulation.” Information and Computation,
vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:10.1006/inco.2001.3085.
short: T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173
(2002) 64–81.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-02-25T00:00:00Z
date_updated: 2023-06-05T07:53:27Z
day: '25'
doi: 10.1006/inco.2001.3085
extern: '1'
intvolume: ' 173'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub
month: '02'
oa: 1
oa_version: Published Version
page: 64 - 81
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '255'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fair simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 173
year: '2002'
...
---
_id: '4501'
abstract:
- lang: eng
text: 'We extend the specification language of temporal logic, the corresponding
verification framework, and the underlying computational model to deal with real-;time
properties of reactive systems. The abstract notion of timed transition systems
generalizes traditional transition systems conservatively: qualitative fairness
requirements are replaced (and superseded) by quantitative lower-bound and upper-bound
timing constraints on transitions. This framework can model real-time systems
that communicate either through shared variables or by message passing and real-time
issues such as timeouts, process priorities (interrupts), and process scheduling.
We exhibit two styles for the specification of real-time systems. While the first
approach uses time-bounded versions of the temporal operators, the second approach
allows explicit references to time through a special clock variable. Corresponding
to the two styles of specification, we present and compare two different proof
methodologies for the verification of timing requirements that are expressed in
these styles. For the bounded-operator style, we provide a set of proof rules
for establishing bounded-invariance and bounded-responce properties of timed transition
systems. This approach generalizes the standard temporal proof rules for verifying
invariance and response properties conservatively. For the explicit-clock style,
we exploit the observation that every time-bounded property is a safety property
and use the standard temporal proof rules for establishing safety properties.'
acknowledgement: 'This research was supported in part by an IBM graduate fellowship,
by the National Science Foundation under Grants CCR-9223226 and CCR-9200794. by
the Defense Advanced Research Projects Agency under Contract N00039-84-C-0211. by
the United States Air Force OMee of Scientific Research under Contracts F49620-93-141139
and F4962043-1-0056. and by the European Community ESPRIT Basic Research Action
Project 6021 (REACT). A preliminary version of Part 1 of this paper appeared in
the proceedings of the 1991 REX Workshop on Real Time Theory In Prate [HMP92a I
a preliminary version of Part II appeared in the proceedings of the 1991 ACM Symposium
on Principles of Programming Languages RIMP911. '
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for timed transition
systems. Information and Computation. 1994;112(2):273-337. doi:10.1006/inco.1994.1060
apa: Henzinger, T. A., Manna, Z., & Pnueli, A. (1994). Temporal proof methodologies
for timed transition systems. Information and Computation. Elsevier. https://doi.org/10.1006/inco.1994.1060
chicago: Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies
for Timed Transition Systems.” Information and Computation. Elsevier, 1994.
https://doi.org/10.1006/inco.1994.1060.
ieee: T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for
timed transition systems,” Information and Computation, vol. 112, no. 2.
Elsevier, pp. 273–337, 1994.
ista: Henzinger TA, Manna Z, Pnueli A. 1994. Temporal proof methodologies for timed
transition systems. Information and Computation. 112(2), 273–337.
mla: Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Timed Transition
Systems.” Information and Computation, vol. 112, no. 2, Elsevier, 1994,
pp. 273–337, doi:10.1006/inco.1994.1060.
short: T.A. Henzinger, Z. Manna, A. Pnueli, Information and Computation 112 (1994)
273–337.
date_created: 2018-12-11T12:09:10Z
date_published: 1994-08-01T00:00:00Z
date_updated: 2022-06-02T09:24:58Z
day: '01'
doi: 10.1006/inco.1994.1060
extern: '1'
intvolume: ' 112'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0890540184710601?via%3Dihub
month: '08'
oa: 1
oa_version: None
page: 273 - 337
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '227'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal proof methodologies for timed transition systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 112
year: '1994'
...
---
_id: '4503'
abstract:
- lang: eng
text: 'We describe finite-state programs over real-numbered time in a guarded-command
language with real-valued clocks or, equivalently, as finite automata with real-valued
clocks. Model checking answers the question which states of a real-time program
satisfy a branching-time specification (given in an extension of CTL with clock
variables). We develop an algorithm that computes this set of states symbolically
as a fixpoint of a functional on state predicates, without constructing the state
space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered
time. Unfortunately, many standard program properties, such as response for all
nonzeno execution sequences (during which time diverges), cannot be characterized
by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable
to the expressiveness of timed CTL. Fortunately, this result does not impair the
symbolic verification of "implementable" real-time programs-those whose
safety constraints are machine-closed with respect to diverging time and whose
fairness constraints are restricted to finite upper bounds on clock values. All
timed CTL properties of such programs are shown to be computable as finitely approximable
fixpoints in a simple decidable theory.'
acknowledgement: We thank Peter Kopke for a careful reading.
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Xavier
full_name: Nicollin, Xavier
last_name: Nicollin
- first_name: Joseph
full_name: Sifakis, Joseph
last_name: Sifakis
- first_name: Sergio
full_name: Yovine, Sergio
last_name: Yovine
citation:
ama: Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for
real-time systems. Information and Computation. 1994;111(2):193-244. doi:10.1006/inco.1994.1045
apa: Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic
model checking for real-time systems. Information and Computation. Elsevier.
https://doi.org/10.1006/inco.1994.1045
chicago: Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.
“Symbolic Model Checking for Real-Time Systems.” Information and Computation.
Elsevier, 1994. https://doi.org/10.1006/inco.1994.1045.
ieee: T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking
for real-time systems,” Information and Computation, vol. 111, no. 2. Elsevier,
pp. 193–244, 1994.
ista: Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1994. Symbolic model checking
for real-time systems. Information and Computation. 111(2), 193–244.
mla: Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.”
Information and Computation, vol. 111, no. 2, Elsevier, 1994, pp. 193–244,
doi:10.1006/inco.1994.1045.
short: T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Information and Computation
111 (1994) 193–244.
date_created: 2018-12-11T12:09:11Z
date_published: 1994-06-01T00:00:00Z
date_updated: 2022-06-02T09:02:02Z
day: '01'
doi: 10.1006/inco.1994.1045
extern: '1'
intvolume: ' 111'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/S0890540184710455?via%3Dihub
month: '06'
oa_version: None
page: 193 - 244
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '226'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for real-time systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 111
year: '1994'
...