---
_id: '6972'
abstract:
- lang: eng
  text: 'We give fault-tolerant algorithms for establishing synchrony in distributed
    systems in which each of thennodes has its own clock. Our algorithms operate in
    a very strong fault model: we require self-stabilisation, i.e.,the initial state
    of the system may be arbitrary, and there can be up to f<n/3 ongoing Byzantine
    faults, i.e.,nodes that deviate from the protocol in an arbitrary manner. Furthermore,
    we assume that the local clocks ofthe nodes may progress at different speeds (clock
    drift) and communication has bounded delay. In this model,we study the pulse synchronisation
    problem, where the task is to guarantee that eventually all correct nodesgenerate
    well-separated local pulse events (i.e., unlabelled logical clock ticks) in a
    synchronised manner.Compared to prior work, we achieveexponentialimprovements
    in stabilisation time and the number ofcommunicated bits, and give the first sublinear-time
    algorithm for the problem:•In the deterministic setting, the state-of-the-art
    solutions stabilise in timeΘ(f)and have each nodebroadcastΘ(flogf)bits per time
    unit. We exponentially reduce the number of bits broadcasted pertime unit toΘ(logf)while
    retaining the same stabilisation time.•In the randomised setting, the state-of-the-art
    solutions stabilise in timeΘ(f)and have each nodebroadcastO(1)bits per time unit.
    We exponentially reduce the stabilisation time to polylogfwhileeach node broadcasts
    polylogfbits per time unit.These results are obtained by means of a recursive
    approach reducing the above task ofself-stabilisingpulse synchronisation in thebounded-delaymodel
    tonon-self-stabilisingbinary consensus in thesynchro-nousmodel. In general, our
    approach introduces at most logarithmic overheads in terms of stabilisation timeand
    broadcasted bits over the underlying consensus routine.'
article_number: '32'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Christoph
  full_name: Lenzen, Christoph
  last_name: Lenzen
- first_name: Joel
  full_name: Rybicki, Joel
  id: 334EFD2E-F248-11E8-B48F-1D18A9856A87
  last_name: Rybicki
  orcid: 0000-0002-6432-6646
citation:
  ama: Lenzen C, Rybicki J. Self-stabilising Byzantine clock synchronisation is almost
    as easy as consensus. <i>Journal of the ACM</i>. 2019;66(5). doi:<a href="https://doi.org/10.1145/3339471">10.1145/3339471</a>
  apa: Lenzen, C., &#38; Rybicki, J. (2019). Self-stabilising Byzantine clock synchronisation
    is almost as easy as consensus. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/3339471">https://doi.org/10.1145/3339471</a>
  chicago: Lenzen, Christoph, and Joel Rybicki. “Self-Stabilising Byzantine Clock
    Synchronisation Is Almost as Easy as Consensus.” <i>Journal of the ACM</i>. ACM,
    2019. <a href="https://doi.org/10.1145/3339471">https://doi.org/10.1145/3339471</a>.
  ieee: C. Lenzen and J. Rybicki, “Self-stabilising Byzantine clock synchronisation
    is almost as easy as consensus,” <i>Journal of the ACM</i>, vol. 66, no. 5. ACM,
    2019.
  ista: Lenzen C, Rybicki J. 2019. Self-stabilising Byzantine clock synchronisation
    is almost as easy as consensus. Journal of the ACM. 66(5), 32.
  mla: Lenzen, Christoph, and Joel Rybicki. “Self-Stabilising Byzantine Clock Synchronisation
    Is Almost as Easy as Consensus.” <i>Journal of the ACM</i>, vol. 66, no. 5, 32,
    ACM, 2019, doi:<a href="https://doi.org/10.1145/3339471">10.1145/3339471</a>.
  short: C. Lenzen, J. Rybicki, Journal of the ACM 66 (2019).
date_created: 2019-10-24T17:12:48Z
date_published: 2019-09-01T00:00:00Z
date_updated: 2023-08-30T07:07:23Z
day: '01'
ddc:
- '000'
department:
- _id: DaAl
doi: 10.1145/3339471
ec_funded: 1
external_id:
  arxiv:
  - '1705.06173'
  isi:
  - '000496514100001'
file:
- access_level: open_access
  checksum: 7e5d95c478e0e393f4927fcf7e48194e
  content_type: application/pdf
  creator: dernst
  date_created: 2019-10-25T12:58:38Z
  date_updated: 2020-07-14T12:47:46Z
  file_id: '6975'
  file_name: 2019_JACM_Lenzen.pdf
  file_size: 2183085
  relation: main_file
file_date_updated: 2020-07-14T12:47:46Z
has_accepted_license: '1'
intvolume: '        66'
isi: 1
issue: '5'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '754411'
  name: ISTplus - Postdoctoral Fellowships
publication: Journal of the ACM
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: Self-stabilising Byzantine clock synchronisation is almost as easy as consensus
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 66
year: '2019'
...
---
_id: '7108'
abstract:
- lang: eng
  text: We prove that for every d ≥ 2, deciding if a pure, d-dimensional, simplicial
    complex is shellable is NP-hard, hence NP-complete. This resolves a question raised,
    e.g., by Danaraj and Klee in 1978. Our reduction also yields that for every d
    ≥ 2 and k ≥ 0, deciding if a pure, d-dimensional, simplicial complex is k-decomposable
    is NP-hard. For d ≥ 3, both problems remain NP-hard when restricted to contractible
    pure d-dimensional complexes. Another simple corollary of our result is that it
    is NP-hard to decide whether a given poset is CL-shellable.
article_number: '21'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Xavier
  full_name: Goaoc, Xavier
  last_name: Goaoc
- first_name: Pavel
  full_name: Patak, Pavel
  id: B593B804-1035-11EA-B4F1-947645A5BB83
  last_name: Patak
- first_name: Zuzana
  full_name: Patakova, Zuzana
  id: 48B57058-F248-11E8-B48F-1D18A9856A87
  last_name: Patakova
  orcid: 0000-0002-3975-1683
- first_name: Martin
  full_name: Tancer, Martin
  last_name: Tancer
- first_name: Uli
  full_name: Wagner, Uli
  id: 36690CA2-F248-11E8-B48F-1D18A9856A87
  last_name: Wagner
  orcid: 0000-0002-1494-0568
citation:
  ama: Goaoc X, Patak P, Patakova Z, Tancer M, Wagner U. Shellability is NP-complete.
    <i>Journal of the ACM</i>. 2019;66(3). doi:<a href="https://doi.org/10.1145/3314024">10.1145/3314024</a>
  apa: Goaoc, X., Patak, P., Patakova, Z., Tancer, M., &#38; Wagner, U. (2019). Shellability
    is NP-complete. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/3314024">https://doi.org/10.1145/3314024</a>
  chicago: Goaoc, Xavier, Pavel Patak, Zuzana Patakova, Martin Tancer, and Uli Wagner.
    “Shellability Is NP-Complete.” <i>Journal of the ACM</i>. ACM, 2019. <a href="https://doi.org/10.1145/3314024">https://doi.org/10.1145/3314024</a>.
  ieee: X. Goaoc, P. Patak, Z. Patakova, M. Tancer, and U. Wagner, “Shellability is
    NP-complete,” <i>Journal of the ACM</i>, vol. 66, no. 3. ACM, 2019.
  ista: Goaoc X, Patak P, Patakova Z, Tancer M, Wagner U. 2019. Shellability is NP-complete.
    Journal of the ACM. 66(3), 21.
  mla: Goaoc, Xavier, et al. “Shellability Is NP-Complete.” <i>Journal of the ACM</i>,
    vol. 66, no. 3, 21, ACM, 2019, doi:<a href="https://doi.org/10.1145/3314024">10.1145/3314024</a>.
  short: X. Goaoc, P. Patak, Z. Patakova, M. Tancer, U. Wagner, Journal of the ACM
    66 (2019).
date_created: 2019-11-26T10:13:59Z
date_published: 2019-06-01T00:00:00Z
date_updated: 2023-09-06T11:10:58Z
day: '01'
department:
- _id: UlWa
doi: 10.1145/3314024
external_id:
  arxiv:
  - '1711.08436'
  isi:
  - '000495406300007'
intvolume: '        66'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/pdf/1711.08436.pdf
month: '06'
oa: 1
oa_version: Preprint
publication: Journal of the ACM
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
  record:
  - id: '184'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Shellability is NP-complete
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 66
year: '2019'
...
---
_id: '7109'
abstract:
- lang: eng
  text: We show how to construct temporal testers for the logic MITL, a prominent
    linear-time logic for real-time systems. A temporal tester is a transducer that
    inputs a signal holding the Boolean value of atomic propositions and outputs the
    truth value of a formula along time. Here we consider testers over continuous-time
    Boolean signals that use clock variables to enforce duration constraints, as in
    timed automata. We first rewrite the MITL formula into a “simple” formula using
    a limited set of temporal modalities. We then build testers for these specific
    modalities and show how to compose testers for simple formulae into complex ones.
    Temporal testers can be turned into acceptors, yielding a compositional translation
    from MITL to timed automata. This construction is much simpler than previously
    known and remains asymptotically optimal. It supports both past and future operators
    and can easily be extended.
article_number: '19'
article_processing_charge: No
article_type: original
author:
- first_name: Thomas
  full_name: Ferrere, Thomas
  id: 40960E6E-F248-11E8-B48F-1D18A9856A87
  last_name: Ferrere
  orcid: 0000-0001-5199-3143
- first_name: Oded
  full_name: Maler, Oded
  last_name: Maler
- first_name: Dejan
  full_name: Ničković, Dejan
  last_name: Ničković
- first_name: Amir
  full_name: Pnueli, Amir
  last_name: Pnueli
citation:
  ama: Ferrere T, Maler O, Ničković D, Pnueli A. From real-time logic to timed automata.
    <i>Journal of the ACM</i>. 2019;66(3). doi:<a href="https://doi.org/10.1145/3286976">10.1145/3286976</a>
  apa: Ferrere, T., Maler, O., Ničković, D., &#38; Pnueli, A. (2019). From real-time
    logic to timed automata. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/3286976">https://doi.org/10.1145/3286976</a>
  chicago: Ferrere, Thomas, Oded Maler, Dejan Ničković, and Amir Pnueli. “From Real-Time
    Logic to Timed Automata.” <i>Journal of the ACM</i>. ACM, 2019. <a href="https://doi.org/10.1145/3286976">https://doi.org/10.1145/3286976</a>.
  ieee: T. Ferrere, O. Maler, D. Ničković, and A. Pnueli, “From real-time logic to
    timed automata,” <i>Journal of the ACM</i>, vol. 66, no. 3. ACM, 2019.
  ista: Ferrere T, Maler O, Ničković D, Pnueli A. 2019. From real-time logic to timed
    automata. Journal of the ACM. 66(3), 19.
  mla: Ferrere, Thomas, et al. “From Real-Time Logic to Timed Automata.” <i>Journal
    of the ACM</i>, vol. 66, no. 3, 19, ACM, 2019, doi:<a href="https://doi.org/10.1145/3286976">10.1145/3286976</a>.
  short: T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019).
date_created: 2019-11-26T10:22:32Z
date_published: 2019-05-01T00:00:00Z
date_updated: 2023-09-06T11:11:56Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3286976
external_id:
  isi:
  - '000495406300005'
intvolume: '        66'
isi: 1
issue: '3'
language:
- iso: eng
month: '05'
oa_version: None
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Journal of the ACM
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: From real-time logic to timed automata
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 66
year: '2019'
...
---
_id: '11768'
abstract:
- lang: eng
  text: "In the decremental single-source shortest paths (SSSP) problem, we want to
    maintain the distances between a given source node s and every other node in an
    n-node m-edge graph G undergoing edge deletions. While its static counterpart
    can be solved in near-linear time, this decremental problem is much more challenging
    even in the undirected unweighted case. In this case, the classic O(mn) total
    update time of Even and Shiloach [16] has been the fastest known algorithm for
    three decades. At the cost of a (1+ϵ)-approximation factor, the running time was
    recently improved to n2+o(1) by Bernstein and Roditty [9]. In this article, we
    bring the running time down to near-linear: We give a (1+ϵ)-approximation algorithm
    with m1+o(1) expected total update time, thus obtaining near-linear time. Moreover,
    we obtain m1+o(1) log W time for the weighted case, where the edge weights are
    integers from 1 to W. The only prior work on weighted graphs in o(mn) time is
    the mn0.9 + o(1)-time algorithm by Henzinger et al. [18, 19], which works for
    directed graphs with quasi-polynomial edge weights. The expected running time
    bound of our algorithm holds against an oblivious adversary.\r\n\r\nIn contrast
    to the previous results, which rely on maintaining a sparse emulator, our algorithm
    relies on maintaining a so-called sparse (h, ϵ)-hop set introduced by Cohen [12]
    in the PRAM literature. An (h, ϵ)-hop set of a graph G=(V, E) is a set F of weighted
    edges such that the distance between any pair of nodes in G can be (1+ϵ)-approximated
    by their h-hop distance (given by a path containing at most h edges) on G′=(V,
    E ∪ F). Our algorithm can maintain an (no(1), ϵ)-hop set of near-linear size in
    near-linear time under edge deletions. It is the first of its kind to the best
    of our knowledge. To maintain approximate distances using this hop set, we extend
    the monotone Even-Shiloach tree of Henzinger et al. [20] and combine it with the
    bounded-hop SSSP technique of Bernstein [4, 5] and Mądry [27]. These two new tools
    might be of independent interest."
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: Sebastian
  full_name: Krinninger, Sebastian
  last_name: Krinninger
- first_name: Danupon
  full_name: Nanongkai, Danupon
  last_name: Nanongkai
citation:
  ama: Henzinger MH, Krinninger S, Nanongkai D. Decremental single-source shortest
    paths on undirected graphs in near-linear total update time. <i>Journal of the
    ACM</i>. 2018;65(6):1-40. doi:<a href="https://doi.org/10.1145/3218657">10.1145/3218657</a>
  apa: Henzinger, M. H., Krinninger, S., &#38; Nanongkai, D. (2018). Decremental single-source
    shortest paths on undirected graphs in near-linear total update time. <i>Journal
    of the ACM</i>. Association for Computing Machinery. <a href="https://doi.org/10.1145/3218657">https://doi.org/10.1145/3218657</a>
  chicago: Henzinger, Monika H, Sebastian Krinninger, and Danupon Nanongkai. “Decremental
    Single-Source Shortest Paths on Undirected Graphs in near-Linear Total Update
    Time.” <i>Journal of the ACM</i>. Association for Computing Machinery, 2018. <a
    href="https://doi.org/10.1145/3218657">https://doi.org/10.1145/3218657</a>.
  ieee: M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Decremental single-source
    shortest paths on undirected graphs in near-linear total update time,” <i>Journal
    of the ACM</i>, vol. 65, no. 6. Association for Computing Machinery, pp. 1–40,
    2018.
  ista: Henzinger MH, Krinninger S, Nanongkai D. 2018. Decremental single-source shortest
    paths on undirected graphs in near-linear total update time. Journal of the ACM.
    65(6), 1–40.
  mla: Henzinger, Monika H., et al. “Decremental Single-Source Shortest Paths on Undirected
    Graphs in near-Linear Total Update Time.” <i>Journal of the ACM</i>, vol. 65,
    no. 6, Association for Computing Machinery, 2018, pp. 1–40, doi:<a href="https://doi.org/10.1145/3218657">10.1145/3218657</a>.
  short: M.H. Henzinger, S. Krinninger, D. Nanongkai, Journal of the ACM 65 (2018)
    1–40.
date_created: 2022-08-08T12:33:17Z
date_published: 2018-12-01T00:00:00Z
date_updated: 2023-02-21T16:30:41Z
day: '01'
doi: 10.1145/3218657
extern: '1'
external_id:
  arxiv:
  - '1512.08148'
intvolume: '        65'
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1512.08148
month: '12'
oa: 1
oa_version: Preprint
page: 1-40
publication: Journal of the ACM
publication_identifier:
  eissn:
  - 1557-735X
  issn:
  - 0004-5411
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '11855'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Decremental single-source shortest paths on undirected graphs in near-linear
  total update time
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 65
year: '2018'
...
---
_id: '4595'
abstract:
- lang: eng
  text: 'Temporal logic comes in two varieties: linear-time temporal logic assumes
    implicit universal quantification over all paths that are generated by the execution
    of a system; branching-time temporal logic allows explicit existential and universal
    quantification over all paths. We introduce a third, more general variety of temporal
    logic: alternating-time temporal logic offers selective quantification over those
    paths that are possible outcomes of games, such as the game in which the system
    and the environment alternate moves. While linear-time and branching-time logics
    are natural specification languages for closed systems, alternating-time logics
    are natural specification languages for open systems. For example, by preceding
    the temporal operator &quot;eventually&quot; with a selective path quantifier,
    we can specify that in the game between the system and the environment, the system
    has a strategy to reach a certain state. The problems of receptiveness, realizability,
    and controllability can be formulated as model-checking problems for alternating-time
    formulas. Depending on whether or not we admit arbitrary nesting of selective
    path quantifiers and temporal operators, we obtain the two alternating-time temporal
    logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures.
    Every state transition of a concurrent game structure results from a choice of
    moves, one for each player. The players represent individual components and the
    environment of an open system. Concurrent game structures can capture various
    forms of synchronous composition for open systems, and if augmented with fairness
    constraints, also asynchronous composition. Over structures without fairness constraints,
    the model-checking complexity of ATL is linear in the size of the game structure
    and length of the formula, and the symbolic model-checking algorithm for CTL extends
    with few modifications to ATL. Over structures with weak-fairness constraints,
    ATL model checking requires the solution of 1-pair Rabin games, and can be done
    in polynomial time. Over structures with strong-fairness constraints, ATL model
    checking requires the solution of games with Boolean combinations of Büchi conditions,
    and can be done in PSPACE. In the case of ATL*, the model-checking problem is
    closely related to the synthesis problem for linear-time formulas, and requires
    doubly exponential time.'
acknowledgement: We thank Luca de Alfaro, Kousha Etessami, Salvatore La Torre, P.
  Madhusudan, Amir Pnueli, Moshe Vardi, Thomas Wilke, and Mihalis Yannakakis for helpful
  discussions. We also thank Freddy Mang for comments on a draft of this manuscript.
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
citation:
  ama: Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. <i>Journal
    of the ACM</i>. 2002;49(5):672-713. doi:<a href="https://doi.org/10.1145/585265.585270">10.1145/585265.585270</a>
  apa: Alur, R., Henzinger, T. A., &#38; Kupferman, O. (2002). Alternating-time temporal
    logic. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/585265.585270">https://doi.org/10.1145/585265.585270</a>
  chicago: Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time
    Temporal Logic.” <i>Journal of the ACM</i>. ACM, 2002. <a href="https://doi.org/10.1145/585265.585270">https://doi.org/10.1145/585265.585270</a>.
  ieee: R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,”
    <i>Journal of the ACM</i>, vol. 49, no. 5. ACM, pp. 672–713, 2002.
  ista: Alur R, Henzinger TA, Kupferman O. 2002. Alternating-time temporal logic.
    Journal of the ACM. 49(5), 672–713.
  mla: Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” <i>Journal of the ACM</i>,
    vol. 49, no. 5, ACM, 2002, pp. 672–713, doi:<a href="https://doi.org/10.1145/585265.585270">10.1145/585265.585270</a>.
  short: R. Alur, T.A. Henzinger, O. Kupferman, Journal of the ACM 49 (2002) 672–713.
date_created: 2018-12-11T12:09:40Z
date_published: 2002-09-01T00:00:00Z
date_updated: 2023-06-02T10:07:22Z
day: '01'
doi: 10.1145/585265.585270
extern: '1'
intvolume: '        49'
issue: '5'
language:
- iso: eng
month: '09'
oa_version: None
page: 672 - 713
publication: Journal of the ACM
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
publist_id: '110'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating-time temporal logic
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 49
year: '2002'
...
---
_id: '4010'
abstract:
- lang: eng
  text: A sliver is a tetrahedron whose four vertices lie close to a plane and whose
    orthogonal projection to that plane is a convex quadrilateral with no short edge.
    Slivers are notoriously common in 3-dimensional Delaunay triangulations even for
    well-spaced point sets. We show that, if the Delaunay triangulation has the ratio
    property introduced in Miller et al. [1995], then there is an assignment of weights
    so the weighted Delaunay triangulation contains no slivers. We also give an algorithm
    to compute such a weight assignment.
acknowledgement: NSF under grant DMS 98-73945, NSF under grant CCR 96-19542 and ARO
  under grant DAAG-55-98-1-0177.
article_processing_charge: No
article_type: original
author:
- first_name: Siu
  full_name: Cheng, Siu
  last_name: Cheng
- first_name: Tamal
  full_name: Dey, Tamal
  last_name: Dey
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
- first_name: Michael
  full_name: Facello, Michael
  last_name: Facello
- first_name: Shang
  full_name: Teng, Shang
  last_name: Teng
citation:
  ama: Cheng S, Dey T, Edelsbrunner H, Facello M, Teng S. Sliver exudation. <i>Journal
    of the ACM</i>. 2000;47(5):883-904. doi:<a href="https://doi.org/10.1145/355483.355487">10.1145/355483.355487</a>
  apa: Cheng, S., Dey, T., Edelsbrunner, H., Facello, M., &#38; Teng, S. (2000). Sliver
    exudation. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/355483.355487">https://doi.org/10.1145/355483.355487</a>
  chicago: Cheng, Siu, Tamal Dey, Herbert Edelsbrunner, Michael Facello, and Shang
    Teng. “Sliver Exudation.” <i>Journal of the ACM</i>. ACM, 2000. <a href="https://doi.org/10.1145/355483.355487">https://doi.org/10.1145/355483.355487</a>.
  ieee: S. Cheng, T. Dey, H. Edelsbrunner, M. Facello, and S. Teng, “Sliver exudation,”
    <i>Journal of the ACM</i>, vol. 47, no. 5. ACM, pp. 883–904, 2000.
  ista: Cheng S, Dey T, Edelsbrunner H, Facello M, Teng S. 2000. Sliver exudation.
    Journal of the ACM. 47(5), 883–904.
  mla: Cheng, Siu, et al. “Sliver Exudation.” <i>Journal of the ACM</i>, vol. 47,
    no. 5, ACM, 2000, pp. 883–904, doi:<a href="https://doi.org/10.1145/355483.355487">10.1145/355483.355487</a>.
  short: S. Cheng, T. Dey, H. Edelsbrunner, M. Facello, S. Teng, Journal of the ACM
    47 (2000) 883–904.
date_created: 2018-12-11T12:06:25Z
date_published: 2000-09-01T00:00:00Z
date_updated: 2023-04-21T08:58:30Z
day: '01'
doi: 10.1145/355483.355487
extern: '1'
intvolume: '        47'
issue: '5'
language:
- iso: eng
month: '09'
oa_version: None
page: 883 - 904
publication: Journal of the ACM
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
publist_id: '2118'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Sliver exudation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 47
year: '2000'
...
---
_id: '11769'
abstract:
- lang: eng
  text: "This paper solves a longstanding open problem in fully dynamic algorithms:
    We present the first fully dynamic algorithms that maintain connectivity, bipartiteness,
    and approximate minimum spanning trees in polylogarithmic time per edge insertion
    or deletion. The algorithms are designed using a new dynamic technique that combines
    a novel graph decomposition with randomization. They are Las-Vegas type randomized
    algorithms which use simple data structures and have a small constant factor.\r\nLet
    n denote the number of nodes in the graph. For a sequence of Ω(m0) operations,
    where m0 is the number of edges in the initial graph, the expected time for p
    updates is O(p log3 n) (througout the paper the logarithms are based 2) for connectivity
    and bipartiteness. The worst-case time for one query is O(log n/log log n). For
    the k-edge witness problem (“Does the removal of k given edges disconnect the
    graph?”) the expected time for p updates is O(p log3 n) and the expected time
    for q queries is O(qk log3 n). Given a graph with k different weights, the minimum
    spanning tree can be maintained during a sequence of p updates in expected time
    O(pk log3 n). This implies an algorithm to maintain a 1 + ε-approximation of the
    minimum spanning tree in expected time O((p log3 n logU)/ε) for p updates, where
    the weights of the edges are between 1 and U."
article_processing_charge: No
article_type: original
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: Valerie
  full_name: King, Valerie
  last_name: King
citation:
  ama: Henzinger MH, King V. Randomized fully dynamic graph algorithms with polylogarithmic
    time per operation. <i>Journal of the ACM</i>. 1999;46(4):502-516. doi:<a href="https://doi.org/10.1145/320211.320215">10.1145/320211.320215</a>
  apa: Henzinger, M. H., &#38; King, V. (1999). Randomized fully dynamic graph algorithms
    with polylogarithmic time per operation. <i>Journal of the ACM</i>. Association
    for Computing Machinery. <a href="https://doi.org/10.1145/320211.320215">https://doi.org/10.1145/320211.320215</a>
  chicago: Henzinger, Monika H, and Valerie King. “Randomized Fully Dynamic Graph
    Algorithms with Polylogarithmic Time per Operation.” <i>Journal of the ACM</i>.
    Association for Computing Machinery, 1999. <a href="https://doi.org/10.1145/320211.320215">https://doi.org/10.1145/320211.320215</a>.
  ieee: M. H. Henzinger and V. King, “Randomized fully dynamic graph algorithms with
    polylogarithmic time per operation,” <i>Journal of the ACM</i>, vol. 46, no. 4.
    Association for Computing Machinery, pp. 502–516, 1999.
  ista: Henzinger MH, King V. 1999. Randomized fully dynamic graph algorithms with
    polylogarithmic time per operation. Journal of the ACM. 46(4), 502–516.
  mla: Henzinger, Monika H., and Valerie King. “Randomized Fully Dynamic Graph Algorithms
    with Polylogarithmic Time per Operation.” <i>Journal of the ACM</i>, vol. 46,
    no. 4, Association for Computing Machinery, 1999, pp. 502–16, doi:<a href="https://doi.org/10.1145/320211.320215">10.1145/320211.320215</a>.
  short: M.H. Henzinger, V. King, Journal of the ACM 46 (1999) 502–516.
date_created: 2022-08-08T12:50:25Z
date_published: 1999-07-01T00:00:00Z
date_updated: 2022-09-12T10:50:08Z
day: '01'
doi: 10.1145/320211.320215
extern: '1'
intvolume: '        46'
issue: '4'
language:
- iso: eng
month: '07'
oa_version: None
page: 502-516
publication: Journal of the ACM
publication_identifier:
  eissn:
  - 1557-735X
  issn:
  - 0004-5411
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Randomized fully dynamic graph algorithms with polylogarithmic time per operation
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 46
year: '1999'
...
---
_id: '4609'
abstract:
- lang: eng
  text: 'Temporal logic comes in two varieties: linear-time temporal logic assumes
    implicit universal quantification over all paths that are generated by system
    moves; branching-time temporal logic allows explicit existential and universal
    quantification over all paths. We introduce a third, more general variety of temporal
    logic: alternating-time temporal logic offers selective quantification over those
    paths that are possible outcomes of games, such as the game in which the system
    and the environment alternate moves. While linear-time and branching-time logics
    are natural specification languages for closed systems, alternating-time logics
    are natural specification languages for open systems. For example, by preceding
    the temporal operator “eventually” with a selective path quantifier, we can specify
    that in the game between the system and the environment, the system has a strategy
    to reach a certain state. Also the problems of receptiveness, realizability, and
    controllability can be formulated as model-checking problems for alternating-time
    formulas'
acknowledgement: We thank Luca de Alfaro, Kousha Etessami, Salvatore La Torre, P.
  Madhusudan, Amir Pnueli, Moshe Vardi, Thomas Wilke, and Mihalis Yannakakis for helpful
  discussions. We also thank Freddy Mang for comments on a draft of this manuscript.
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
citation:
  ama: 'Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. In: <i>Proceedings
    of the 38th Annual Symposium on Foundations of Computer Science</i>. Association
    for Computing Machinery (ACM); 1997:100-109. doi:<a href="https://doi.org/10.1145/585265.585270">10.1145/585265.585270</a>'
  apa: 'Alur, R., Henzinger, T. A., &#38; Kupferman, O. (1997). Alternating-time temporal
    logic. In <i>Proceedings of the 38th Annual Symposium on Foundations of Computer
    Science</i> (pp. 100–109). Washington, DC, United States: Association for Computing
    Machinery (ACM). <a href="https://doi.org/10.1145/585265.585270">https://doi.org/10.1145/585265.585270</a>'
  chicago: Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time
    Temporal Logic.” In <i>Proceedings of the 38th Annual Symposium on Foundations
    of Computer Science</i>, 100–109. Association for Computing Machinery (ACM), 1997.
    <a href="https://doi.org/10.1145/585265.585270">https://doi.org/10.1145/585265.585270</a>.
  ieee: R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,”
    in <i>Proceedings of the 38th Annual Symposium on Foundations of Computer Science</i>,
    Washington, DC, United States, 1997, pp. 100–109.
  ista: 'Alur R, Henzinger TA, Kupferman O. 1997. Alternating-time temporal logic.
    Proceedings of the 38th Annual Symposium on Foundations of Computer Science. FOCS:
    Foundations of Computer Science, 100–109.'
  mla: Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” <i>Proceedings of the
    38th Annual Symposium on Foundations of Computer Science</i>, Association for
    Computing Machinery (ACM), 1997, pp. 100–09, doi:<a href="https://doi.org/10.1145/585265.585270">10.1145/585265.585270</a>.
  short: R. Alur, T.A. Henzinger, O. Kupferman, in:, Proceedings of the 38th Annual
    Symposium on Foundations of Computer Science, Association for Computing Machinery
    (ACM), 1997, pp. 100–109.
conference:
  end_date: 1997-10-22
  location: Washington, DC, United States
  name: 'FOCS: Foundations of Computer Science'
  start_date: 1997-10-19
date_created: 2018-12-11T12:09:44Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-09-05T07:32:05Z
day: '01'
doi: 10.1145/585265.585270
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 100 - 109
publication: Proceedings of the 38th Annual Symposium on Foundations of Computer Science
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: Association for Computing Machinery (ACM)
publist_id: '100'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating-time temporal logic
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1997'
...
---
_id: '4610'
abstract:
- lang: eng
  text: The most natural, compositional, way of modeling real-time systems uses a
    dense domain for time. The satisfiability of timing constraints that are capable
    of expressing punctuality in this model, however, is known to be undecidable.
    We introduce a temporal language that can constrain the time difference between
    events only with finite, yet arbitrary, precision and show the resulting logic
    to be EXPSPACE-complete. This result allows us to develop an algorithm for the
    verification of timing properties of real-time systems with a dense semantics.
acknowledgement: 'We wish to thank an anonymous referee for pointing out the PSPACE-fragment
  of Section 4.5. '
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Tomás
  full_name: Feder, Tomás
  last_name: Feder
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: Alur R, Feder T, Henzinger TA. The benefits of relaxing punctuality. <i>Journal
    of the ACM</i>. 1996;43(1):116-146. doi:<a href="https://doi.org/10.1145/227595.227602">10.1145/227595.227602</a>
  apa: Alur, R., Feder, T., &#38; Henzinger, T. A. (1996). The benefits of relaxing
    punctuality. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/227595.227602">https://doi.org/10.1145/227595.227602</a>
  chicago: Alur, Rajeev, Tomás Feder, and Thomas A Henzinger. “The Benefits of Relaxing
    Punctuality.” <i>Journal of the ACM</i>. ACM, 1996. <a href="https://doi.org/10.1145/227595.227602">https://doi.org/10.1145/227595.227602</a>.
  ieee: R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing punctuality,”
    <i>Journal of the ACM</i>, vol. 43, no. 1. ACM, pp. 116–146, 1996.
  ista: Alur R, Feder T, Henzinger TA. 1996. The benefits of relaxing punctuality.
    Journal of the ACM. 43(1), 116–146.
  mla: Alur, Rajeev, et al. “The Benefits of Relaxing Punctuality.” <i>Journal of
    the ACM</i>, vol. 43, no. 1, ACM, 1996, pp. 116–46, doi:<a href="https://doi.org/10.1145/227595.227602">10.1145/227595.227602</a>.
  short: R. Alur, T. Feder, T.A. Henzinger, Journal of the ACM 43 (1996) 116–146.
date_created: 2018-12-11T12:09:44Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-04T12:38:01Z
day: '01'
doi: 10.1145/227595.227602
extern: '1'
intvolume: '        43'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://dl.acm.org/doi/10.1145/227595.227602
month: '01'
oa_version: None
page: 116 - 146
publication: Journal of the ACM
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
publist_id: '95'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The benefits of relaxing punctuality
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 43
year: '1996'
...
---
_id: '4591'
abstract:
- lang: eng
  text: 'We introduce a temporal logic for the specification of real-time systems.
    Our logic, TPTL, employs a novel quantifier construct for referencing time: the
    freeze quantifier binds a variable to the time of the local temporal context.
    TPTL is both a natural language for specification and a suitable formalism for
    verification. We present a tableau-based decision procedure and a model-checking
    algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.'
acknowledgement: "We thank Zohar Manna, Amir Pnueli, and David Dill for their guidance.
  Moshe Vardi and Joe Halpern gave us very helpful advice for refining our undecidability
  results; in particular, they pointed out to us the completeness of a problem on
  Turing machines.\r\n"
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: Alur R, Henzinger TA. A really temporal logic. <i>Journal of the ACM</i>. 1994;41(1):181-204.
    doi:<a href="https://doi.org/10.1145/174644.174651">10.1145/174644.174651</a>
  apa: Alur, R., &#38; Henzinger, T. A. (1994). A really temporal logic. <i>Journal
    of the ACM</i>. ACM. <a href="https://doi.org/10.1145/174644.174651">https://doi.org/10.1145/174644.174651</a>
  chicago: Alur, Rajeev, and Thomas A Henzinger. “A Really Temporal Logic.” <i>Journal
    of the ACM</i>. ACM, 1994. <a href="https://doi.org/10.1145/174644.174651">https://doi.org/10.1145/174644.174651</a>.
  ieee: R. Alur and T. A. Henzinger, “A really temporal logic,” <i>Journal of the
    ACM</i>, vol. 41, no. 1. ACM, pp. 181–204, 1994.
  ista: Alur R, Henzinger TA. 1994. A really temporal logic. Journal of the ACM. 41(1),
    181–204.
  mla: Alur, Rajeev, and Thomas A. Henzinger. “A Really Temporal Logic.” <i>Journal
    of the ACM</i>, vol. 41, no. 1, ACM, 1994, pp. 181–204, doi:<a href="https://doi.org/10.1145/174644.174651">10.1145/174644.174651</a>.
  short: R. Alur, T.A. Henzinger, Journal of the ACM 41 (1994) 181–204.
date_created: 2018-12-11T12:09:38Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T08:23:46Z
day: '01'
doi: 10.1145/174644.174651
extern: '1'
intvolume: '        41'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://dl.acm.org/doi/10.1145/174644.174651
month: '01'
oa_version: None
page: 181 - 204
publication: Journal of the ACM
publication_identifier:
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
publist_id: '118'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A really temporal logic
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 41
year: '1994'
...
---
_id: '4046'
abstract:
- lang: eng
  text: The main contribution of this work is an O(n log n + k)-time algorithm for
    computing all k intersections among n line segments in the plane. This time complexity
    is easily shown to be optimal. Within the same asymptotic cost, our algorithm
    can also construct the subdivision of the plane defined by the segments and compute
    which segment (if any) lies right above (or below) each intersection and each
    endpoint. The algorithm has been implemented and performs very well. The storage
    requirement is on the order of n + k in the worst case, but it is considerably
    lower in practice. To analyze the complexity of the algorithm, an amortization
    argument based on a new combinatorial theorem on line arrangements is used.
acknowledgement: "B, Chazelle wishes to acknowledge the National Science Foundation
  for supporting this research in part under Grant CCR 87-00917. H, Edelsbrunner is
  pleased to acknowledge the support of Amoco Fnd. Fac. Dev. Comput. Sci. 1-6-44862
  and the NSF under Grant CCR 87-14565. Permission to copy without fee all or part
  of this material is granted provided that the copies are not made or distributed
  for direct commercial advantage, the ACM copyright notice and the title of the publication
  and its date appear, and notice is given that copying is by permission of the Association
  for\r\nComputing Machinery. To copy otherwise, or to republish, requires a fee and/or
  specific permission."
article_processing_charge: No
article_type: original
author:
- first_name: Bernard
  full_name: Chazelle, Bernard
  last_name: Chazelle
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
citation:
  ama: Chazelle B, Edelsbrunner H. An optimal algorithm for intersecting line segments
    in the plane. <i>Journal of the ACM</i>. 1992;39(1):1-54. doi:<a href="https://doi.org/10.1145/147508.147511">10.1145/147508.147511</a>
  apa: Chazelle, B., &#38; Edelsbrunner, H. (1992). An optimal algorithm for intersecting
    line segments in the plane. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/147508.147511">https://doi.org/10.1145/147508.147511</a>
  chicago: Chazelle, Bernard, and Herbert Edelsbrunner. “An Optimal Algorithm for
    Intersecting Line Segments in the Plane.” <i>Journal of the ACM</i>. ACM, 1992.
    <a href="https://doi.org/10.1145/147508.147511">https://doi.org/10.1145/147508.147511</a>.
  ieee: B. Chazelle and H. Edelsbrunner, “An optimal algorithm for intersecting line
    segments in the plane,” <i>Journal of the ACM</i>, vol. 39, no. 1. ACM, pp. 1–54,
    1992.
  ista: Chazelle B, Edelsbrunner H. 1992. An optimal algorithm for intersecting line
    segments in the plane. Journal of the ACM. 39(1), 1–54.
  mla: Chazelle, Bernard, and Herbert Edelsbrunner. “An Optimal Algorithm for Intersecting
    Line Segments in the Plane.” <i>Journal of the ACM</i>, vol. 39, no. 1, ACM, 1992,
    pp. 1–54, doi:<a href="https://doi.org/10.1145/147508.147511">10.1145/147508.147511</a>.
  short: B. Chazelle, H. Edelsbrunner, Journal of the ACM 39 (1992) 1–54.
date_created: 2018-12-11T12:06:37Z
date_published: 1992-01-01T00:00:00Z
date_updated: 2022-03-16T08:32:17Z
day: '01'
doi: 10.1145/147508.147511
extern: '1'
intvolume: '        39'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://dl.acm.org/doi/10.1145/147508.147511
month: '01'
oa_version: None
page: 1 - 54
publication: Journal of the ACM
publication_identifier:
  eissn:
  - 1557-735X
  issn:
  - 0004-5411
publication_status: published
publisher: ACM
publist_id: '2078'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An optimal algorithm for intersecting line segments in the plane
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 39
year: '1992'
...