[{"oa_version":"Published Version","day":"01","citation":{"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>.","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>.","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>","ista":"Lenzen C, Rybicki J. 2019. Self-stabilising Byzantine clock synchronisation is almost as easy as consensus. Journal of the ACM. 66(5), 32.","short":"C. Lenzen, J. Rybicki, Journal of the ACM 66 (2019).","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.","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>"},"month":"09","file_date_updated":"2020-07-14T12:47:46Z","ddc":["000"],"has_accepted_license":"1","article_processing_charge":"Yes","volume":66,"file":[{"date_created":"2019-10-25T12:58:38Z","file_id":"6975","date_updated":"2020-07-14T12:47:46Z","checksum":"7e5d95c478e0e393f4927fcf7e48194e","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":2183085,"creator":"dernst","file_name":"2019_JACM_Lenzen.pdf"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"arxiv":1,"issue":"5","abstract":[{"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.","lang":"eng"}],"doi":"10.1145/3339471","author":[{"last_name":"Lenzen","full_name":"Lenzen, Christoph","first_name":"Christoph"},{"last_name":"Rybicki","full_name":"Rybicki, Joel","first_name":"Joel","id":"334EFD2E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6432-6646"}],"title":"Self-stabilising Byzantine clock synchronisation is almost as easy as consensus","_id":"6972","publication_status":"published","status":"public","ec_funded":1,"publication_identifier":{"issn":["0004-5411"]},"project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships"}],"external_id":{"arxiv":["1705.06173"],"isi":["000496514100001"]},"date_published":"2019-09-01T00:00:00Z","scopus_import":"1","date_created":"2019-10-24T17:12:48Z","department":[{"_id":"DaAl"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","isi":1,"language":[{"iso":"eng"}],"type":"journal_article","quality_controlled":"1","intvolume":"        66","publisher":"ACM","year":"2019","oa":1,"article_type":"original","article_number":"32","publication":"Journal of the ACM","date_updated":"2023-08-30T07:07:23Z"},{"abstract":[{"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.","lang":"eng"}],"issue":"3","doi":"10.1145/3314024","title":"Shellability is NP-complete","author":[{"first_name":"Xavier","last_name":"Goaoc","full_name":"Goaoc, Xavier"},{"full_name":"Patak, Pavel","last_name":"Patak","id":"B593B804-1035-11EA-B4F1-947645A5BB83","first_name":"Pavel"},{"first_name":"Zuzana","id":"48B57058-F248-11E8-B48F-1D18A9856A87","last_name":"Patakova","full_name":"Patakova, Zuzana","orcid":"0000-0002-3975-1683"},{"last_name":"Tancer","full_name":"Tancer, Martin","first_name":"Martin"},{"orcid":"0000-0002-1494-0568","last_name":"Wagner","full_name":"Wagner, Uli","first_name":"Uli","id":"36690CA2-F248-11E8-B48F-1D18A9856A87"}],"_id":"7108","publication_status":"published","status":"public","publication_identifier":{"issn":["0004-5411"]},"oa_version":"Preprint","citation":{"ista":"Goaoc X, Patak P, Patakova Z, Tancer M, Wagner U. 2019. Shellability is NP-complete. Journal of the ACM. 66(3), 21.","short":"X. Goaoc, P. Patak, Z. Patakova, M. Tancer, U. Wagner, Journal of the ACM 66 (2019).","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>","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.","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>.","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>."},"day":"01","month":"06","article_processing_charge":"No","volume":66,"arxiv":1,"year":"2019","oa":1,"related_material":{"record":[{"id":"184","relation":"earlier_version","status":"public"}]},"article_number":"21","article_type":"original","publication":"Journal of the ACM","date_updated":"2023-09-06T11:10:58Z","date_published":"2019-06-01T00:00:00Z","external_id":{"isi":["000495406300007"],"arxiv":["1711.08436"]},"date_created":"2019-11-26T10:13:59Z","scopus_import":"1","department":[{"_id":"UlWa"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","isi":1,"type":"journal_article","language":[{"iso":"eng"}],"quality_controlled":"1","publisher":"ACM","intvolume":"        66","main_file_link":[{"open_access":"1","url":"https://arxiv.org/pdf/1711.08436.pdf"}]},{"citation":{"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>.","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>.","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>","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.","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>","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.","short":"T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019)."},"day":"01","month":"05","oa_version":"None","article_processing_charge":"No","volume":66,"title":"From real-time logic to timed automata","author":[{"first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"first_name":"Dejan","last_name":"Ničković","full_name":"Ničković, Dejan"},{"last_name":"Pnueli","full_name":"Pnueli, Amir","first_name":"Amir"}],"_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."}],"issue":"3","doi":"10.1145/3286976","publication_identifier":{"issn":["0004-5411"]},"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"status":"public","publication_status":"published","department":[{"_id":"ToHe"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_published":"2019-05-01T00:00:00Z","external_id":{"isi":["000495406300005"]},"date_created":"2019-11-26T10:22:32Z","scopus_import":"1","publisher":"ACM","intvolume":"        66","isi":1,"quality_controlled":"1","language":[{"iso":"eng"}],"type":"journal_article","year":"2019","publication":"Journal of the ACM","date_updated":"2023-09-06T11:11:56Z","article_number":"19","article_type":"original"},{"page":"1-40","article_type":"original","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"11855"}]},"date_updated":"2023-02-21T16:30:41Z","publication":"Journal of the ACM","year":"2018","oa":1,"type":"journal_article","quality_controlled":"1","language":[{"iso":"eng"}],"publisher":"Association for Computing Machinery","intvolume":"        65","main_file_link":[{"url":"https://arxiv.org/abs/1512.08148","open_access":"1"}],"date_created":"2022-08-08T12:33:17Z","scopus_import":"1","external_id":{"arxiv":["1512.08148"]},"extern":"1","date_published":"2018-12-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","status":"public","publication_identifier":{"eissn":["1557-735X"],"issn":["0004-5411"]},"doi":"10.1145/3218657","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."}],"issue":"6","_id":"11768","title":"Decremental single-source shortest paths on undirected graphs in near-linear total update time","author":[{"orcid":"0000-0002-5008-6530","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","full_name":"Henzinger, Monika H"},{"full_name":"Krinninger, Sebastian","last_name":"Krinninger","first_name":"Sebastian"},{"full_name":"Nanongkai, Danupon","last_name":"Nanongkai","first_name":"Danupon"}],"volume":65,"article_processing_charge":"No","arxiv":1,"oa_version":"Preprint","month":"12","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>","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.","short":"M.H. Henzinger, S. Krinninger, D. Nanongkai, Journal of the ACM 65 (2018) 1–40.","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.","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>.","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>."},"day":"01"},{"volume":49,"article_processing_charge":"No","oa_version":"None","day":"01","citation":{"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>.","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>.","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>","ista":"Alur R, Henzinger TA, Kupferman O. 2002. Alternating-time temporal logic. Journal of the ACM. 49(5), 672–713.","short":"R. Alur, T.A. Henzinger, O. Kupferman, Journal of the ACM 49 (2002) 672–713.","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.","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>"},"month":"09","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.","publication_status":"published","status":"public","publication_identifier":{"issn":["0004-5411"]},"issue":"5","abstract":[{"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.","lang":"eng"}],"doi":"10.1145/585265.585270","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"}],"title":"Alternating-time temporal logic","_id":"4595","language":[{"iso":"eng"}],"quality_controlled":"1","type":"journal_article","intvolume":"        49","publisher":"ACM","extern":"1","date_published":"2002-09-01T00:00:00Z","scopus_import":"1","date_created":"2018-12-11T12:09:40Z","publist_id":"110","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_type":"original","page":"672 - 713","publication":"Journal of the ACM","date_updated":"2023-06-02T10:07:22Z","year":"2002"},{"publisher":"ACM","intvolume":"        47","quality_controlled":"1","type":"journal_article","language":[{"iso":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"2118","date_published":"2000-09-01T00:00:00Z","extern":"1","date_created":"2018-12-11T12:06:25Z","scopus_import":"1","publication":"Journal of the ACM","date_updated":"2023-04-21T08:58:30Z","page":"883 - 904","article_type":"original","year":"2000","article_processing_charge":"No","volume":47,"citation":{"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>.","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.","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>","short":"S. Cheng, T. Dey, H. Edelsbrunner, M. Facello, S. Teng, Journal of the ACM 47 (2000) 883–904.","ista":"Cheng S, Dey T, Edelsbrunner H, Facello M, Teng S. 2000. Sliver exudation. Journal of the ACM. 47(5), 883–904.","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>"},"day":"01","month":"09","oa_version":"None","publication_identifier":{"issn":["0004-5411"]},"publication_status":"published","status":"public","acknowledgement":"NSF under grant DMS 98-73945, NSF under grant CCR 96-19542 and ARO under grant DAAG-55-98-1-0177.","title":"Sliver exudation","author":[{"last_name":"Cheng","full_name":"Cheng, Siu","first_name":"Siu"},{"full_name":"Dey, Tamal","last_name":"Dey","first_name":"Tamal"},{"orcid":"0000-0002-9823-6833","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","first_name":"Herbert","full_name":"Edelsbrunner, Herbert","last_name":"Edelsbrunner"},{"last_name":"Facello","full_name":"Facello, Michael","first_name":"Michael"},{"first_name":"Shang","last_name":"Teng","full_name":"Teng, Shang"}],"_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."}],"issue":"5","doi":"10.1145/355483.355487"},{"article_type":"original","page":"502-516","publication_status":"published","status":"public","date_updated":"2022-09-12T10:50:08Z","publication":"Journal of the ACM","publication_identifier":{"issn":["0004-5411"],"eissn":["1557-735X"]},"doi":"10.1145/320211.320215","issue":"4","year":"1999","abstract":[{"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.","lang":"eng"}],"_id":"11769","author":[{"orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","full_name":"Henzinger, Monika H","last_name":"Henzinger"},{"full_name":"King, Valerie","last_name":"King","first_name":"Valerie"}],"title":"Randomized fully dynamic graph algorithms with polylogarithmic time per operation","language":[{"iso":"eng"}],"type":"journal_article","quality_controlled":"1","article_processing_charge":"No","volume":46,"intvolume":"        46","publisher":"Association for Computing Machinery","scopus_import":"1","date_created":"2022-08-08T12:50:25Z","oa_version":"None","extern":"1","date_published":"1999-07-01T00:00:00Z","month":"07","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","citation":{"short":"M.H. Henzinger, V. King, Journal of the ACM 46 (1999) 502–516.","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>","ista":"Henzinger MH, King V. 1999. Randomized fully dynamic graph algorithms with polylogarithmic time per operation. Journal of the ACM. 46(4), 502–516.","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>","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.","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>.","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>."}},{"date_published":"1997-01-01T00:00:00Z","extern":"1","conference":{"end_date":"1997-10-22","location":"Washington, DC, United States","start_date":"1997-10-19","name":"FOCS: Foundations of Computer Science"},"scopus_import":"1","oa_version":"None","date_created":"2018-12-11T12:09:44Z","day":"01","citation":{"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.","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>","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.","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>","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.","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>.","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>."},"month":"01","publist_id":"100","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"conference","language":[{"iso":"eng"}],"quality_controlled":"1","article_processing_charge":"No","publisher":"Association for Computing Machinery (ACM)","year":"1997","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"}],"doi":"10.1145/585265.585270","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"title":"Alternating-time temporal logic","_id":"4609","publication_status":"published","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.","status":"public","page":"100 - 109","publication":"Proceedings of the 38th Annual Symposium on Foundations of Computer Science","publication_identifier":{"issn":["0004-5411"]},"date_updated":"2022-09-05T07:32:05Z"},{"article_processing_charge":"No","volume":43,"oa_version":"None","citation":{"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>","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.","short":"R. Alur, T. Feder, T.A. Henzinger, Journal of the ACM 43 (1996) 116–146.","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>","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>.","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>."},"day":"01","month":"01","acknowledgement":"We wish to thank an anonymous referee for pointing out the PSPACE-fragment of Section 4.5. ","publication_status":"published","status":"public","publication_identifier":{"issn":["0004-5411"]},"abstract":[{"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.","lang":"eng"}],"issue":"1","doi":"10.1145/227595.227602","title":"The benefits of relaxing punctuality","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"first_name":"Tomás","last_name":"Feder","full_name":"Feder, Tomás"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"_id":"4610","type":"journal_article","language":[{"iso":"eng"}],"quality_controlled":"1","publisher":"ACM","intvolume":"        43","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/227595.227602"}],"extern":"1","date_published":"1996-01-01T00:00:00Z","date_created":"2018-12-11T12:09:44Z","scopus_import":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"95","page":"116 - 146","article_type":"original","publication":"Journal of the ACM","date_updated":"2022-07-04T12:38:01Z","year":"1996"},{"title":"A really temporal logic","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"_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."}],"issue":"1","doi":"10.1145/174644.174651","publication_identifier":{"issn":["0004-5411"]},"status":"public","publication_status":"published","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","citation":{"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.","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>","short":"R. Alur, T.A. Henzinger, Journal of the ACM 41 (1994) 181–204.","ista":"Alur R, Henzinger TA. 1994. A really temporal logic. Journal of the ACM. 41(1), 181–204.","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>","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>.","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>."},"day":"01","month":"01","oa_version":"None","volume":41,"article_processing_charge":"No","year":"1994","publication":"Journal of the ACM","date_updated":"2022-06-02T08:23:46Z","page":"181 - 204","article_type":"original","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"118","date_published":"1994-01-01T00:00:00Z","extern":"1","date_created":"2018-12-11T12:09:38Z","scopus_import":"1","publisher":"ACM","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/174644.174651"}],"intvolume":"        41","type":"journal_article","language":[{"iso":"eng"}],"quality_controlled":"1"},{"date_created":"2018-12-11T12:06:37Z","scopus_import":"1","extern":"1","date_published":"1992-01-01T00:00:00Z","publist_id":"2078","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","quality_controlled":"1","language":[{"iso":"eng"}],"type":"journal_article","publisher":"ACM","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/147508.147511"}],"intvolume":"        39","year":"1992","page":"1 - 54","article_type":"original","date_updated":"2022-03-16T08:32:17Z","publication":"Journal of the ACM","oa_version":"None","month":"01","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>","short":"B. Chazelle, H. Edelsbrunner, Journal of the ACM 39 (1992) 1–54.","ista":"Chazelle B, Edelsbrunner H. 1992. An optimal algorithm for intersecting line segments in the plane. Journal of the ACM. 39(1), 1–54.","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.","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>.","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>."},"day":"01","article_processing_charge":"No","volume":39,"doi":"10.1145/147508.147511","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."}],"issue":"1","_id":"4046","title":"An optimal algorithm for intersecting line segments in the plane","author":[{"last_name":"Chazelle","full_name":"Chazelle, Bernard","first_name":"Bernard"},{"orcid":"0000-0002-9823-6833","first_name":"Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","last_name":"Edelsbrunner","full_name":"Edelsbrunner, Herbert"}],"publication_status":"published","status":"public","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.","publication_identifier":{"issn":["0004-5411"],"eissn":["1557-735X"]}}]