[{"_id":"14820","title":"Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ec_funded":1,"department":[{"_id":"KrCh"},{"_id":"KrPi"}],"fulldoi":"https://doi.org/10.1016/j.tcs.2023.114353","supplementarymaterial":"no","publication_identifier":{"issn":["0304-3975"]},"day":"21","corr_author":"1","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)"},"file":[{"access_level":"open_access","date_updated":"2024-07-16T12:02:25Z","relation":"main_file","success":1,"date_created":"2024-07-16T12:02:25Z","file_id":"17263","content_type":"application/pdf","checksum":"efd5b7e738bf845312ba53889a3e13e4","creator":"dernst","file_name":"2024_TheorComputerScience_Schmid.pdf","file_size":603570}],"researchdata_availability":"no","keyword":["General Computer Science","Theoretical Computer Science"],"oa":1,"doi":"10.1016/j.tcs.2023.114353","project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"volume":989,"has_accepted_license":"1","article_type":"original","external_id":{"isi":["001168211400001"]},"das_tickbox":"0","article_processing_charge":"Yes (via OA deal)","type":"journal_article","abstract":[{"lang":"eng","text":"We consider a natural problem dealing with weighted packet selection across a rechargeable link, which e.g., finds applications in cryptocurrency networks. The capacity of a link (u, v) is determined by how many nodes u and v allocate for this link. Specifically, the input is a finite ordered sequence of packets that arrive in both directions along a link. Given (u, v) and a packet of weight x going from u to v, node u can either accept or reject the packet. If u accepts the packet, the capacity on link (u, v) decreases by x. Correspondingly, v's capacity on \r\n increases by x. If a node rejects the packet, this will entail a cost affinely linear in the weight of the packet. A link is “rechargeable” in the sense that the total capacity of the link has to remain constant, but the allocation of capacity at the ends of the link can depend arbitrarily on the nodes' decisions. The goal is to minimise the sum of the capacity injected into the link and the cost of rejecting packets. We show that the problem is NP-hard, but can be approximated efficiently with a ratio of (1+E) . (1+3)  for some arbitrary E>0."}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"19985"}]},"language":[{"iso":"eng"}],"status":"public","quality_controlled":"1","date_updated":"2026-10-16T08:09:27Z","scopus_import":"1","author":[{"full_name":"Schmid, Stefan","last_name":"Schmid","first_name":"Stefan"},{"first_name":"Jakub","last_name":"Svoboda","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267"},{"id":"2D82B818-F248-11E8-B48F-1D18A9856A87","full_name":"Yeo, Michelle X","first_name":"Michelle X","last_name":"Yeo","orcid":"0009-0001-3676-4809"}],"isi":1,"article_number":"114353","acknowledgement":"We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful discussions about different variants of the problem. This work is supported by the European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025, the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant 470029389 (FlexNets), 2021-2024.","intvolume":"       989","file_date_updated":"2024-07-16T12:02:25Z","date_created":"2024-01-16T13:40:41Z","publication":"Theoretical Computer Science","year":"2024","publication_status":"published","citation":{"short":"S. Schmid, J. Svoboda, M.X. Yeo, Theoretical Computer Science 989 (2024).","mla":"Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” <i>Theoretical Computer Science</i>, vol. 989, 114353, Elsevier, 2024, doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">10.1016/j.tcs.2023.114353</a>.","chicago":"Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” <i>Theoretical Computer Science</i>. Elsevier, 2024. <a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">https://doi.org/10.1016/j.tcs.2023.114353</a>.","apa":"Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2024). Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">https://doi.org/10.1016/j.tcs.2023.114353</a>","ista":"Schmid S, Svoboda J, Yeo MX. 2024. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. Theoretical Computer Science. 989, 114353.","ieee":"S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation,” <i>Theoretical Computer Science</i>, vol. 989. Elsevier, 2024.","ama":"Schmid S, Svoboda J, Yeo MX. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. <i>Theoretical Computer Science</i>. 2024;989. doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">10.1016/j.tcs.2023.114353</a>"},"oa_version":"Published Version","ddc":["000"],"month":"03","publisher":"Elsevier","license":"https://creativecommons.org/licenses/by/4.0/","date_published":"2024-03-21T00:00:00Z"},{"status":"public","quality_controlled":"1","type":"journal_article","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Approximate agreement is one of the few variants of consensus that can be solved in a wait-free manner in asynchronous systems where processes communicate by reading and writing to shared memory. In this work, we consider a natural generalisation of approximate agreement on arbitrary undirected connected graphs. Each process is given a node of the graph as input and, if non-faulty, must output a node such that\r\n– all the outputs are within distance 1 of one another, and\r\n– each output value lies on a shortest path between two input values.\r\nFrom prior work, it is known that there is no wait-free algorithm among  processes for this problem on any cycle of length , by reduction from 2-set agreement (Castañeda et al., 2018).\r\n\r\nIn this work, we investigate the solvability of this task on general graphs. We give a new, direct proof of the impossibility of approximate agreement on cycles of length , via a generalisation of Sperner's Lemma to convex polygons. We also extend the reduction from 2-set agreement to a larger class of graphs, showing that approximate agreement on these graphs is unsolvable. On the positive side, we present a wait-free algorithm for a different class of graphs, which properly contains the class of chordal graphs."}],"author":[{"orcid":"0000-0003-3650-940X","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","full_name":"Alistarh, Dan-Adrian","first_name":"Dan-Adrian","last_name":"Alistarh"},{"first_name":"Faith","last_name":"Ellen","full_name":"Ellen, Faith"},{"orcid":"0000-0002-6432-6646","id":"334EFD2E-F248-11E8-B48F-1D18A9856A87","full_name":"Rybicki, Joel","first_name":"Joel","last_name":"Rybicki"}],"scopus_import":"1","date_updated":"2025-04-14T07:49:16Z","publication_status":"published","date_created":"2023-02-19T23:00:55Z","year":"2023","publication":"Theoretical Computer Science","intvolume":"       948","isi":1,"acknowledgement":"This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 805223 ScaleML) and under the Marie Skłodowska-Curie grant agreement No. 840605 and from the Natural Sciences and Engineering Research Council of Canada grant RGPIN-2020-04178. Part of this work was done while Faith Ellen was visiting IST Austria.","article_number":"113733","file_date_updated":"2023-02-20T07:30:20Z","publisher":"Elsevier","ddc":["000"],"month":"02","date_published":"2023-02-28T00:00:00Z","oa_version":"Published Version","citation":{"ista":"Alistarh D-A, Ellen F, Rybicki J. 2023. Wait-free approximate agreement on graphs. Theoretical Computer Science. 948(2), 113733.","ieee":"D.-A. Alistarh, F. Ellen, and J. Rybicki, “Wait-free approximate agreement on graphs,” <i>Theoretical Computer Science</i>, vol. 948, no. 2. Elsevier, 2023.","ama":"Alistarh D-A, Ellen F, Rybicki J. Wait-free approximate agreement on graphs. <i>Theoretical Computer Science</i>. 2023;948(2). doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.113733\">10.1016/j.tcs.2023.113733</a>","mla":"Alistarh, Dan-Adrian, et al. “Wait-Free Approximate Agreement on Graphs.” <i>Theoretical Computer Science</i>, vol. 948, no. 2, 113733, Elsevier, 2023, doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.113733\">10.1016/j.tcs.2023.113733</a>.","chicago":"Alistarh, Dan-Adrian, Faith Ellen, and Joel Rybicki. “Wait-Free Approximate Agreement on Graphs.” <i>Theoretical Computer Science</i>. Elsevier, 2023. <a href=\"https://doi.org/10.1016/j.tcs.2023.113733\">https://doi.org/10.1016/j.tcs.2023.113733</a>.","apa":"Alistarh, D.-A., Ellen, F., &#38; Rybicki, J. (2023). Wait-free approximate agreement on graphs. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2023.113733\">https://doi.org/10.1016/j.tcs.2023.113733</a>","short":"D.-A. Alistarh, F. Ellen, J. Rybicki, Theoretical Computer Science 948 (2023)."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","ec_funded":1,"_id":"12566","title":"Wait-free approximate agreement on graphs","day":"28","publication_identifier":{"issn":["0304-3975"]},"department":[{"_id":"DaAl"}],"fulldoi":"https://doi.org/10.1016/j.tcs.2023.113733","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)"},"file":[{"access_level":"open_access","success":1,"relation":"main_file","date_updated":"2023-02-20T07:30:20Z","content_type":"application/pdf","date_created":"2023-02-20T07:30:20Z","file_id":"12570","file_size":602333,"file_name":"2023_TheoreticalCompScience_Alistarh.pdf","checksum":"b27c5290f2f1500c403494364ee39c9f","creator":"dernst"}],"oa":1,"doi":"10.1016/j.tcs.2023.113733","project":[{"grant_number":"805223","name":"Elastic Coordination for Scalable Machine Learning","call_identifier":"H2020","_id":"268A44D6-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","name":"Coordination in constrained and natural distributed systems","grant_number":"840605","_id":"26A5D39A-B435-11E9-9278-68D0E5697425"}],"issue":"2","corr_author":"1","external_id":{"isi":["000934262700001"]},"article_type":"original","article_processing_charge":"Yes (via OA deal)","volume":948,"has_accepted_license":"1"},{"doi":"10.1016/j.tcs.2023.114129","oa":1,"corr_author":"1","article_processing_charge":"No","external_id":{"arxiv":["2212.08424"],"isi":["001076934000001"]},"article_type":"original","volume":977,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2212.08424 "}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Weakly weighted generalised quasi-metric spaces and semilattices","_id":"14362","day":"25","arxiv":1,"publication_identifier":{"issn":["0304-3975"]},"fulldoi":"https://doi.org/10.1016/j.tcs.2023.114129","department":[{"_id":"HeEd"}],"publication_status":"published","date_created":"2023-09-24T22:01:11Z","year":"2023","publication":"Theoretical Computer Science","intvolume":"       977","article_number":"114129","isi":1,"date_published":"2023-10-25T00:00:00Z","publisher":"Elsevier","month":"10","oa_version":"Preprint","citation":{"ieee":"I. Castellano, A. Giordano Bruno, and N. Zava, “Weakly weighted generalised quasi-metric spaces and semilattices,” <i>Theoretical Computer Science</i>, vol. 977. Elsevier, 2023.","ista":"Castellano I, Giordano Bruno A, Zava N. 2023. Weakly weighted generalised quasi-metric spaces and semilattices. Theoretical Computer Science. 977, 114129.","ama":"Castellano I, Giordano Bruno A, Zava N. Weakly weighted generalised quasi-metric spaces and semilattices. <i>Theoretical Computer Science</i>. 2023;977. doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.114129\">10.1016/j.tcs.2023.114129</a>","short":"I. Castellano, A. Giordano Bruno, N. Zava, Theoretical Computer Science 977 (2023).","mla":"Castellano, Ilaria, et al. “Weakly Weighted Generalised Quasi-Metric Spaces and Semilattices.” <i>Theoretical Computer Science</i>, vol. 977, 114129, Elsevier, 2023, doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.114129\">10.1016/j.tcs.2023.114129</a>.","chicago":"Castellano, Ilaria, Anna Giordano Bruno, and Nicolò Zava. “Weakly Weighted Generalised Quasi-Metric Spaces and Semilattices.” <i>Theoretical Computer Science</i>. Elsevier, 2023. <a href=\"https://doi.org/10.1016/j.tcs.2023.114129\">https://doi.org/10.1016/j.tcs.2023.114129</a>.","apa":"Castellano, I., Giordano Bruno, A., &#38; Zava, N. (2023). Weakly weighted generalised quasi-metric spaces and semilattices. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2023.114129\">https://doi.org/10.1016/j.tcs.2023.114129</a>"},"quality_controlled":"1","status":"public","language":[{"iso":"eng"}],"abstract":[{"text":"Motivated by recent applications to entropy theory in dynamical systems, we generalise notions introduced by Matthews and define weakly weighted and componentwise weakly weighted (generalised) quasi-metrics. We then systematise and extend to full generality the correspondences between these objects and other structures arising in theoretical computer science and dynamics. In particular, we study the correspondences with weak partial metrics and, if the underlying space is a semilattice, with invariant (generalised) quasi-metrics satisfying the descending path condition, and with strictly monotone semi(-co-)valuations.\r\nWe conclude discussing, for endomorphisms of generalised quasi-metric semilattices, a generalisation of both the known intrinsic semilattice entropy and the semigroup entropy.","lang":"eng"}],"type":"journal_article","author":[{"full_name":"Castellano, Ilaria","first_name":"Ilaria","last_name":"Castellano"},{"first_name":"Anna","last_name":"Giordano Bruno","full_name":"Giordano Bruno, Anna"},{"last_name":"Zava","first_name":"Nicolò","full_name":"Zava, Nicolò","id":"c8b3499c-7a77-11eb-b046-aa368cbbf2ad","orcid":"0000-0001-8686-1888"}],"scopus_import":"1","date_updated":"2024-10-09T21:07:00Z"},{"author":[{"first_name":"Tatjana","last_name":"Petrov","full_name":"Petrov, Tatjana"},{"full_name":"Igler, Claudia","id":"46613666-F248-11E8-B48F-1D18A9856A87","last_name":"Igler","first_name":"Claudia"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali","first_name":"Ali","last_name":"Sezgin"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"orcid":"0000-0001-6220-2052","full_name":"Guet, Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","first_name":"Calin C"}],"scopus_import":"1","date_updated":"2025-04-15T06:25:56Z","quality_controlled":"1","status":"public","type":"journal_article","language":[{"iso":"eng"}],"abstract":[{"text":"Gene expression is regulated by the set of transcription factors (TFs) that bind to the promoter. The ensuing regulating function is often represented as a combinational logic circuit, where output (gene expression) is determined by current input values (promoter bound TFs) only. However, the simultaneous arrival of TFs is a strong assumption, since transcription and translation of genes introduce intrinsic time delays and there is no global synchronisation among the arrival times of different molecular species at their targets. We present an experimentally implementable genetic circuit with two inputs and one output, which in the presence of small delays in input arrival, exhibits qualitatively distinct population-level phenotypes, over timescales that are longer than typical cell doubling times. From a dynamical systems point of view, these phenotypes represent long-lived transients: although they converge to the same value eventually, they do so after a very long time span. The key feature of this toy model genetic circuit is that, despite having only two inputs and one output, it is regulated by twenty-three distinct DNA-TF configurations, two of which are more stable than others (DNA looped states), one promoting and another blocking the expression of the output gene. Small delays in input arrival time result in a majority of cells in the population quickly reaching the stable state associated with the first input, while exiting of this stable state occurs at a slow timescale. In order to mechanistically model the behaviour of this genetic circuit, we used a rule-based modelling language, and implemented a grid-search to find parameter combinations giving rise to long-lived transients. Our analysis shows that in the absence of feedback, there exist path-dependent gene regulatory mechanisms based on the long timescale of transients. The behaviour of this toy model circuit suggests that gene regulatory networks can exploit event timing to create phenotypes, and it opens the possibility that they could use event timing to memorise events, without regulatory feedback. The model reveals the importance of (i) mechanistically modelling the transitions between the different DNA-TF states, and (ii) employing transient analysis thereof.","lang":"eng"}],"publisher":"Elsevier","month":"06","ddc":["004"],"date_published":"2021-06-04T00:00:00Z","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","oa_version":"Published Version","citation":{"ama":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. Long lived transients in gene regulation. <i>Theoretical Computer Science</i>. 2021;893:1-16. doi:<a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">10.1016/j.tcs.2021.05.023</a>","ieee":"T. Petrov, C. Igler, A. Sezgin, T. A. Henzinger, and C. C. Guet, “Long lived transients in gene regulation,” <i>Theoretical Computer Science</i>, vol. 893. Elsevier, pp. 1–16, 2021.","ista":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. 2021. Long lived transients in gene regulation. Theoretical Computer Science. 893, 1–16.","short":"T. Petrov, C. Igler, A. Sezgin, T.A. Henzinger, C.C. Guet, Theoretical Computer Science 893 (2021) 1–16.","apa":"Petrov, T., Igler, C., Sezgin, A., Henzinger, T. A., &#38; Guet, C. C. (2021). Long lived transients in gene regulation. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">https://doi.org/10.1016/j.tcs.2021.05.023</a>","mla":"Petrov, Tatjana, et al. “Long Lived Transients in Gene Regulation.” <i>Theoretical Computer Science</i>, vol. 893, Elsevier, 2021, pp. 1–16, doi:<a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">10.1016/j.tcs.2021.05.023</a>.","chicago":"Petrov, Tatjana, Claudia Igler, Ali Sezgin, Thomas A Henzinger, and Calin C Guet. “Long Lived Transients in Gene Regulation.” <i>Theoretical Computer Science</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.tcs.2021.05.023\">https://doi.org/10.1016/j.tcs.2021.05.023</a>."},"publication_status":"published","year":"2021","date_created":"2021-07-11T22:01:18Z","publication":"Theoretical Computer Science","intvolume":"       893","acknowledgement":"Tatjana Petrov’s research was supported in part by SNSF Advanced Postdoctoral Mobility Fellowship grant number P300P2 161067, the Ministry of Science, Research and the Arts of the state of Baden-Wurttemberg, and the DFG Centre of Excellence 2117 ‘Centre for the Advanced Study of Collective Behaviour’ (ID: 422037984). Claudia Igler is the recipient of a DOC Fellowship of the Austrian Academy of Sciences. Thomas A. Henzinger’s research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","isi":1,"file_date_updated":"2022-05-12T12:13:27Z","day":"04","page":"1-16","publication_identifier":{"issn":["0304-3975"]},"department":[{"_id":"ToHe"},{"_id":"CaGu"}],"fulldoi":"https://doi.org/10.1016/j.tcs.2021.05.023","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"9647","title":"Long lived transients in gene regulation","article_type":"original","external_id":{"isi":["000710180500002"]},"article_processing_charge":"No","has_accepted_license":"1","volume":893,"file":[{"file_name":"2021_TheoreticalComputerScience_Petrov.pdf","file_size":2566504,"checksum":"d3aef34cfb13e53bba4cf44d01680793","creator":"dernst","content_type":"application/pdf","file_id":"11364","date_created":"2022-05-12T12:13:27Z","success":1,"date_updated":"2022-05-12T12:13:27Z","relation":"main_file","access_level":"open_access"}],"tmp":{"short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"project":[{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"doi":"10.1016/j.tcs.2021.05.023","oa":1,"corr_author":"1"},{"scopus_import":"1","date_updated":"2024-10-09T21:00:45Z","author":[{"last_name":"Chatterjee","first_name":"Bapi","full_name":"Chatterjee, Bapi","id":"3C41A08A-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2742-4028"},{"full_name":"Walulya, Ivan","last_name":"Walulya","first_name":"Ivan"},{"full_name":"Tsigas, Philippas","first_name":"Philippas","last_name":"Tsigas"}],"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"The Nearest neighbour search (NNS) is a fundamental problem in many application domains dealing with multidimensional data. In a concurrent setting, where dynamic modifications are allowed, a linearizable implementation of the NNS is highly desirable.This paper introduces the LockFree-kD-tree (LFkD-tree ): a lock-free concurrent kD-tree, which implements an abstract data type (ADT) that provides the operations Add, Remove, Contains, and NNS. Our implementation is linearizable. The operations in the LFkD-tree use single-word read and compare-and-swap (Image 1 ) atomic primitives, which are readily supported on available multi-core processors. We experimentally evaluate the LFkD-tree using several benchmarks comprising real-world and synthetic datasets. The experiments show that the presented design is scalable and achieves significant speed-up compared to the implementations of an existing sequential kD-tree and a recently proposed multidimensional indexing structure, PH-tree."}],"type":"journal_article","quality_controlled":"1","status":"public","citation":{"ieee":"B. Chatterjee, I. Walulya, and P. Tsigas, “Concurrent linearizable nearest neighbour search in LockFree-kD-tree,” <i>Theoretical Computer Science</i>, vol. 886. Elsevier, pp. 27–48, 2021.","ista":"Chatterjee B, Walulya I, Tsigas P. 2021. Concurrent linearizable nearest neighbour search in LockFree-kD-tree. Theoretical Computer Science. 886, 27–48.","ama":"Chatterjee B, Walulya I, Tsigas P. Concurrent linearizable nearest neighbour search in LockFree-kD-tree. <i>Theoretical Computer Science</i>. 2021;886:27-48. doi:<a href=\"https://doi.org/10.1016/j.tcs.2021.06.041\">10.1016/j.tcs.2021.06.041</a>","mla":"Chatterjee, Bapi, et al. “Concurrent Linearizable Nearest Neighbour Search in LockFree-KD-Tree.” <i>Theoretical Computer Science</i>, vol. 886, Elsevier, 2021, pp. 27–48, doi:<a href=\"https://doi.org/10.1016/j.tcs.2021.06.041\">10.1016/j.tcs.2021.06.041</a>.","chicago":"Chatterjee, Bapi, Ivan Walulya, and Philippas Tsigas. “Concurrent Linearizable Nearest Neighbour Search in LockFree-KD-Tree.” <i>Theoretical Computer Science</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.tcs.2021.06.041\">https://doi.org/10.1016/j.tcs.2021.06.041</a>.","apa":"Chatterjee, B., Walulya, I., &#38; Tsigas, P. (2021). Concurrent linearizable nearest neighbour search in LockFree-kD-tree. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2021.06.041\">https://doi.org/10.1016/j.tcs.2021.06.041</a>","short":"B. Chatterjee, I. Walulya, P. Tsigas, Theoretical Computer Science 886 (2021) 27–48."},"oa_version":"Submitted Version","date_published":"2021-09-13T00:00:00Z","publisher":"Elsevier","month":"09","intvolume":"       886","isi":1,"publication_status":"published","publication":"Theoretical Computer Science","year":"2021","date_created":"2021-08-08T22:01:31Z","fulldoi":"https://doi.org/10.1016/j.tcs.2021.06.041","department":[{"_id":"DaAl"}],"day":"13","page":"27-48","publication_identifier":{"issn":["0304-3975"]},"title":"Concurrent linearizable nearest neighbour search in LockFree-kD-tree","_id":"9827","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","volume":886,"main_file_link":[{"url":"https://publications.lib.chalmers.se/records/fulltext/232185/232185.pdf","open_access":"1"}],"article_processing_charge":"No","external_id":{"isi":["000694718900004"]},"article_type":"original","corr_author":"1","oa":1,"doi":"10.1016/j.tcs.2021.06.041","keyword":["Concurrent data structure","kD-tree","Nearest neighbor search","Similarity search","Lock-free","Linearizability"]},{"type":"journal_article","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"1341","relation":"earlier_version"}]},"abstract":[{"lang":"eng","text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability."}],"quality_controlled":"1","status":"public","scopus_import":"1","date_updated":"2026-04-16T09:35:15Z","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"intvolume":"       807","isi":1,"file_date_updated":"2020-10-09T06:31:22Z","publication_status":"published","date_created":"2019-08-04T21:59:20Z","publication":"Theoretical Computer Science","year":"2020","citation":{"ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. <i>Theoretical Computer Science</i>. 2020;807:42-55. doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">10.1016/j.tcs.2019.06.031</a>","ista":"Avni G, Henzinger TA, Kupferman O. 2020. Dynamic resource allocation games. Theoretical Computer Science. 807, 42–55.","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” <i>Theoretical Computer Science</i>, vol. 807. Elsevier, pp. 42–55, 2020.","apa":"Avni, G., Henzinger, T. A., &#38; Kupferman, O. (2020). Dynamic resource allocation games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">https://doi.org/10.1016/j.tcs.2019.06.031</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games.” <i>Theoretical Computer Science</i>. Elsevier, 2020. <a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">https://doi.org/10.1016/j.tcs.2019.06.031</a>.","mla":"Avni, Guy, et al. “Dynamic Resource Allocation Games.” <i>Theoretical Computer Science</i>, vol. 807, Elsevier, 2020, pp. 42–55, doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">10.1016/j.tcs.2019.06.031</a>.","short":"G. Avni, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 807 (2020) 42–55."},"oa_version":"Submitted Version","publisher":"Elsevier","month":"02","ddc":["000"],"date_published":"2020-02-06T00:00:00Z","_id":"6761","title":"Dynamic resource allocation games","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","department":[{"_id":"ToHe"}],"fulldoi":"https://doi.org/10.1016/j.tcs.2019.06.031","day":"06","page":"42-55","publication_identifier":{"issn":["0304-3975"]},"file":[{"access_level":"open_access","success":1,"date_updated":"2020-10-09T06:31:22Z","relation":"main_file","content_type":"application/pdf","date_created":"2020-10-09T06:31:22Z","file_id":"8639","file_name":"2020_TheoreticalCS_Avni.pdf","file_size":1413001,"checksum":"e86635417f45eb2cd75778f91382f737","creator":"dernst"}],"project":[{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425"}],"doi":"10.1016/j.tcs.2019.06.031","oa":1,"volume":807,"has_accepted_license":"1","external_id":{"isi":["000512219400004"]},"article_type":"original","article_processing_charge":"No"},{"main_file_link":[{"url":"https://arxiv.org/abs/1902.02304","open_access":"1"}],"volume":779,"article_type":"original","external_id":{"arxiv":["1902.02304"]},"article_processing_charge":"No","oa":1,"doi":"10.1016/j.tcs.2019.01.043","fulldoi":"https://doi.org/10.1016/j.tcs.2019.01.043","day":"02","publication_identifier":{"issn":["0304-3975"]},"arxiv":1,"page":"72-87","_id":"11898","title":"New amortized cell-probe lower bounds for dynamic problems","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"S. Bhattacharya, M. Henzinger, S. Neumann, Theoretical Computer Science 779 (2019) 72–87.","mla":"Bhattacharya, Sayan, et al. “New Amortized Cell-Probe Lower Bounds for Dynamic Problems.” <i>Theoretical Computer Science</i>, vol. 779, Elsevier, 2019, pp. 72–87, doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.01.043\">10.1016/j.tcs.2019.01.043</a>.","chicago":"Bhattacharya, Sayan, Monika Henzinger, and Stefan Neumann. “New Amortized Cell-Probe Lower Bounds for Dynamic Problems.” <i>Theoretical Computer Science</i>. Elsevier, 2019. <a href=\"https://doi.org/10.1016/j.tcs.2019.01.043\">https://doi.org/10.1016/j.tcs.2019.01.043</a>.","apa":"Bhattacharya, S., Henzinger, M., &#38; Neumann, S. (2019). New amortized cell-probe lower bounds for dynamic problems. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2019.01.043\">https://doi.org/10.1016/j.tcs.2019.01.043</a>","ieee":"S. Bhattacharya, M. Henzinger, and S. Neumann, “New amortized cell-probe lower bounds for dynamic problems,” <i>Theoretical Computer Science</i>, vol. 779. Elsevier, pp. 72–87, 2019.","ista":"Bhattacharya S, Henzinger M, Neumann S. 2019. New amortized cell-probe lower bounds for dynamic problems. Theoretical Computer Science. 779, 72–87.","ama":"Bhattacharya S, Henzinger M, Neumann S. New amortized cell-probe lower bounds for dynamic problems. <i>Theoretical Computer Science</i>. 2019;779:72-87. doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.01.043\">10.1016/j.tcs.2019.01.043</a>"},"oa_version":"Preprint","month":"08","extern":"1","publisher":"Elsevier","date_published":"2019-08-02T00:00:00Z","intvolume":"       779","publication":"Theoretical Computer Science","date_created":"2022-08-17T09:02:15Z","year":"2019","publication_status":"published","date_updated":"2024-11-06T12:23:49Z","scopus_import":"1","author":[{"full_name":"Bhattacharya, Sayan","first_name":"Sayan","last_name":"Bhattacharya"},{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Neumann, Stefan","first_name":"Stefan","last_name":"Neumann"}],"type":"journal_article","abstract":[{"lang":"eng","text":"We build upon the recent papers by Weinstein and Yu (FOCS'16), Larsen (FOCS'12), and Clifford et al. (FOCS'15) to present a general framework that gives amortized lower bounds on the update and query times of dynamic data structures. Using our framework, we present two concrete results.\r\n(1) For the dynamic polynomial evaluation problem, where the polynomial is defined over a finite field of size n1+Ω(1) and has degree n, any dynamic data structure must either have an amortized update time of Ω((lgn/lglgn)2) or an amortized query time of Ω((lgn/lglgn)2).\r\n(2) For the dynamic online matrix vector multiplication problem, where we get an n×n matrix whose entires are drawn from a finite field of size nΘ(1), any dynamic data structure must either have an amortized update time of Ω((lgn/lglgn)2) or an amortized query time of Ω(n⋅(lgn/lglgn)2).\r\nFor these two problems, the previous works by Larsen (FOCS'12) and Clifford et al. (FOCS'15) gave the same lower bounds, but only for worst case update and query times. Our bounds match the highest unconditional lower bounds known till date for any dynamic problem in the cell-probe model."}],"language":[{"iso":"eng"}],"status":"public","quality_controlled":"1"},{"doi":"10.1016/j.tcs.2015.01.033","oa":1,"article_processing_charge":"No","article_type":"original","volume":573,"main_file_link":[{"url":"https://doi.org/10.1016/j.tcs.2015.01.033","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Truthful unit-demand auctions with budgets revisited","_id":"11901","page":"1-15","day":"30","publication_identifier":{"issn":["0304-3975"]},"fulldoi":"https://doi.org/10.1016/j.tcs.2015.01.033","publication_status":"published","year":"2015","publication":"Theoretical Computer Science","date_created":"2022-08-17T09:06:53Z","intvolume":"       573","date_published":"2015-03-30T00:00:00Z","publisher":"Elsevier","extern":"1","month":"03","citation":{"short":"M. Henzinger, V. Loitzenbauer, Theoretical Computer Science 573 (2015) 1–15.","chicago":"Henzinger, Monika, and Veronika Loitzenbauer. “Truthful Unit-Demand Auctions with Budgets Revisited.” <i>Theoretical Computer Science</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.033\">https://doi.org/10.1016/j.tcs.2015.01.033</a>.","mla":"Henzinger, Monika, and Veronika Loitzenbauer. “Truthful Unit-Demand Auctions with Budgets Revisited.” <i>Theoretical Computer Science</i>, vol. 573, Elsevier, 2015, pp. 1–15, doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.033\">10.1016/j.tcs.2015.01.033</a>.","apa":"Henzinger, M., &#38; Loitzenbauer, V. (2015). Truthful unit-demand auctions with budgets revisited. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.033\">https://doi.org/10.1016/j.tcs.2015.01.033</a>","ieee":"M. Henzinger and V. Loitzenbauer, “Truthful unit-demand auctions with budgets revisited,” <i>Theoretical Computer Science</i>, vol. 573. Elsevier, pp. 1–15, 2015.","ista":"Henzinger M, Loitzenbauer V. 2015. Truthful unit-demand auctions with budgets revisited. Theoretical Computer Science. 573, 1–15.","ama":"Henzinger M, Loitzenbauer V. Truthful unit-demand auctions with budgets revisited. <i>Theoretical Computer Science</i>. 2015;573:1-15. doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.033\">10.1016/j.tcs.2015.01.033</a>"},"oa_version":"None","quality_controlled":"1","status":"public","language":[{"iso":"eng"}],"abstract":[{"text":"We consider auctions of indivisible items to unit-demand bidders with budgets. This setting was suggested as an expressive model for single sponsored search auctions. Prior work presented mechanisms that compute bidder-optimal outcomes and are truthful for a restricted set of inputs, i.e., inputs in so-called general position. This condition is easily violated. We provide the first mechanism that is truthful in expectation for all inputs and achieves for each bidder no worse utility than the bidder-optimal outcome. Additionally we give a complete characterization for which inputs mechanisms that compute bidder-optimal outcomes are truthful.","lang":"eng"}],"type":"journal_article","author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530"},{"last_name":"Loitzenbauer","first_name":"Veronika","full_name":"Loitzenbauer, Veronika"}],"scopus_import":"1","date_updated":"2024-11-06T12:24:01Z"},{"date_published":"2015-04-18T00:00:00Z","month":"04","extern":"1","publisher":"Elsevier","oa_version":"None","citation":{"ama":"Biswas R, Bhowmick P. From prima quadraginta octant to lattice sphere through primitive integer operations. <i>Theoretical Computer Science</i>. 2015;624(4):56-72. doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.11.018\">10.1016/j.tcs.2015.11.018</a>","ieee":"R. Biswas and P. Bhowmick, “From prima quadraginta octant to lattice sphere through primitive integer operations,” <i>Theoretical Computer Science</i>, vol. 624, no. 4. Elsevier, pp. 56–72, 2015.","ista":"Biswas R, Bhowmick P. 2015. From prima quadraginta octant to lattice sphere through primitive integer operations. Theoretical Computer Science. 624(4), 56–72.","apa":"Biswas, R., &#38; Bhowmick, P. (2015). From prima quadraginta octant to lattice sphere through primitive integer operations. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2015.11.018\">https://doi.org/10.1016/j.tcs.2015.11.018</a>","chicago":"Biswas, Ranita, and Partha Bhowmick. “From Prima Quadraginta Octant to Lattice Sphere through Primitive Integer Operations.” <i>Theoretical Computer Science</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.tcs.2015.11.018\">https://doi.org/10.1016/j.tcs.2015.11.018</a>.","mla":"Biswas, Ranita, and Partha Bhowmick. “From Prima Quadraginta Octant to Lattice Sphere through Primitive Integer Operations.” <i>Theoretical Computer Science</i>, vol. 624, no. 4, Elsevier, 2015, pp. 56–72, doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.11.018\">10.1016/j.tcs.2015.11.018</a>.","short":"R. Biswas, P. Bhowmick, Theoretical Computer Science 624 (2015) 56–72."},"volume":624,"publication":"Theoretical Computer Science","date_created":"2019-01-08T20:44:06Z","year":"2015","doi":"10.1016/j.tcs.2015.11.018","publication_status":"published","issue":"4","intvolume":"       624","day":"18","page":"56-72","author":[{"first_name":"Ranita","last_name":"Biswas","id":"3C2B033E-F248-11E8-B48F-1D18A9856A87","full_name":"Biswas, Ranita","orcid":"0000-0002-5372-7890"},{"full_name":"Bhowmick, Partha","last_name":"Bhowmick","first_name":"Partha"}],"publication_identifier":{"issn":["0304-3975"]},"date_updated":"2021-01-12T08:03:36Z","fulldoi":"https://doi.org/10.1016/j.tcs.2015.11.018","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","quality_controlled":"1","abstract":[{"text":"We present here the first integer-based algorithm for constructing a well-defined lattice sphere specified by integer radius and integer center. The algorithm evolves from a unique correspondence between the lattice points comprising the sphere and the distribution of sum of three square numbers in integer intervals. We characterize these intervals to derive a useful set of recurrences, which, in turn, aids in efficient computation. Each point of the lattice sphere is determined by resorting to only a few primitive operations in the integer domain. The symmetry of its quadraginta octants provides an added advantage by confining the computation to its prima quadraginta octant. Detailed theoretical analysis and experimental results have been furnished to demonstrate its simplicity and elegance.","lang":"eng"}],"language":[{"iso":"eng"}],"title":"From prima quadraginta octant to lattice sphere through primitive integer operations","type":"journal_article","_id":"5804"},{"volume":605,"citation":{"ama":"Biswas R, Bhowmick P. On different topological classes of spherical geodesic paths and circles inZ3. <i>Theoretical Computer Science</i>. 2015;605(11):146-163. doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.09.003\">10.1016/j.tcs.2015.09.003</a>","ieee":"R. Biswas and P. Bhowmick, “On different topological classes of spherical geodesic paths and circles inZ3,” <i>Theoretical Computer Science</i>, vol. 605, no. 11. Elsevier, pp. 146–163, 2015.","ista":"Biswas R, Bhowmick P. 2015. On different topological classes of spherical geodesic paths and circles inZ3. Theoretical Computer Science. 605(11), 146–163.","apa":"Biswas, R., &#38; Bhowmick, P. (2015). On different topological classes of spherical geodesic paths and circles inZ3. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2015.09.003\">https://doi.org/10.1016/j.tcs.2015.09.003</a>","mla":"Biswas, Ranita, and Partha Bhowmick. “On Different Topological Classes of Spherical Geodesic Paths and Circles InZ3.” <i>Theoretical Computer Science</i>, vol. 605, no. 11, Elsevier, 2015, pp. 146–63, doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.09.003\">10.1016/j.tcs.2015.09.003</a>.","chicago":"Biswas, Ranita, and Partha Bhowmick. “On Different Topological Classes of Spherical Geodesic Paths and Circles InZ3.” <i>Theoretical Computer Science</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.tcs.2015.09.003\">https://doi.org/10.1016/j.tcs.2015.09.003</a>.","short":"R. Biswas, P. Bhowmick, Theoretical Computer Science 605 (2015) 146–163."},"oa_version":"None","extern":"1","month":"11","publisher":"Elsevier","date_published":"2015-11-09T00:00:00Z","intvolume":"       605","issue":"11","date_created":"2019-01-08T20:44:52Z","publication":"Theoretical Computer Science","year":"2015","publication_status":"published","doi":"10.1016/j.tcs.2015.09.003","date_updated":"2021-01-12T08:03:37Z","fulldoi":"https://doi.org/10.1016/j.tcs.2015.09.003","author":[{"last_name":"Biswas","first_name":"Ranita","full_name":"Biswas, Ranita","id":"3C2B033E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-5372-7890"},{"first_name":"Partha","last_name":"Bhowmick","full_name":"Bhowmick, Partha"}],"day":"09","publication_identifier":{"issn":["0304-3975"]},"page":"146-163","type":"journal_article","_id":"5807","title":"On different topological classes of spherical geodesic paths and circles inZ3","language":[{"iso":"eng"}],"status":"public","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different classes and representations of Muller games lead to problems of varying computational complexity. One such class are parity games; these are of particular significance in computational complexity, as they remain one of the few combinatorial problems known to be in NP ∩ co-NP but not known to be in P. We show that winning regions for a Muller game can be determined from the alternating structure of its traps. To every Muller game we then associate a natural number that we call its trap depth; this parameter measures how complicated the trap structure is. We present algorithms for parity games that run in polynomial time for graphs of bounded trap depth, and in general run in time exponential in the trap depth. "}],"type":"journal_article","status":"public","quality_controlled":"1","scopus_import":"1","publist_id":"4703","date_updated":"2026-04-16T10:08:15Z","author":[{"first_name":"Andrey","last_name":"Grinshpun","full_name":"Grinshpun, Andrey"},{"first_name":"Pakawat","last_name":"Phalitnonkiat","full_name":"Phalitnonkiat, Pakawat"},{"id":"2EC51194-F248-11E8-B48F-1D18A9856A87","full_name":"Rubin, Sasha","first_name":"Sasha","last_name":"Rubin"},{"last_name":"Tarfulea","first_name":"Andrei","full_name":"Tarfulea, Andrei"}],"intvolume":"       521","isi":1,"publication_status":"published","year":"2014","date_created":"2018-12-11T11:56:33Z","publication":"Theoretical Computer Science","citation":{"ama":"Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. Alternating traps in Muller and parity games. <i>Theoretical Computer Science</i>. 2014;521:73-91. doi:<a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">10.1016/j.tcs.2013.11.032</a>","ieee":"A. Grinshpun, P. Phalitnonkiat, S. Rubin, and A. Tarfulea, “Alternating traps in Muller and parity games,” <i>Theoretical Computer Science</i>, vol. 521. Elsevier, pp. 73–91, 2014.","ista":"Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. 2014. Alternating traps in Muller and parity games. Theoretical Computer Science. 521, 73–91.","apa":"Grinshpun, A., Phalitnonkiat, P., Rubin, S., &#38; Tarfulea, A. (2014). Alternating traps in Muller and parity games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">https://doi.org/10.1016/j.tcs.2013.11.032</a>","chicago":"Grinshpun, Andrey, Pakawat Phalitnonkiat, Sasha Rubin, and Andrei Tarfulea. “Alternating Traps in Muller and Parity Games.” <i>Theoretical Computer Science</i>. Elsevier, 2014. <a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">https://doi.org/10.1016/j.tcs.2013.11.032</a>.","mla":"Grinshpun, Andrey, et al. “Alternating Traps in Muller and Parity Games.” <i>Theoretical Computer Science</i>, vol. 521, Elsevier, 2014, pp. 73–91, doi:<a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">10.1016/j.tcs.2013.11.032</a>.","short":"A. Grinshpun, P. Phalitnonkiat, S. Rubin, A. Tarfulea, Theoretical Computer Science 521 (2014) 73–91."},"oa_version":"Submitted Version","date_published":"2014-02-13T00:00:00Z","publisher":"Elsevier","month":"02","title":"Alternating traps in Muller and parity games","_id":"2246","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","fulldoi":"https://doi.org/10.1016/j.tcs.2013.11.032","department":[{"_id":"KrCh"}],"publication_identifier":{"issn":["0304-3975"]},"page":"73 - 91","arxiv":1,"day":"13","corr_author":"1","doi":"10.1016/j.tcs.2013.11.032","oa":1,"volume":521,"main_file_link":[{"url":"http://arxiv.org/abs/1303.3777","open_access":"1"}],"article_processing_charge":"No","external_id":{"isi":["000331433100007"],"arxiv":["1303.3777"]}},{"article_processing_charge":"No","article_type":"original","volume":478,"doi":"10.1016/j.tcs.2013.01.030","issue":"3","day":"25","page":"22-32","publication_identifier":{"issn":["0304-3975"]},"fulldoi":"https://doi.org/10.1016/j.tcs.2013.01.030","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Bidder optimal assignments for general utilities","_id":"11902","date_published":"2013-03-25T00:00:00Z","publisher":"Elsevier","month":"03","extern":"1","oa_version":"None","citation":{"ieee":"P. Dütting, M. Henzinger, and I. Weber, “Bidder optimal assignments for general utilities,” <i>Theoretical Computer Science</i>, vol. 478, no. 3. Elsevier, pp. 22–32, 2013.","ista":"Dütting P, Henzinger M, Weber I. 2013. Bidder optimal assignments for general utilities. Theoretical Computer Science. 478(3), 22–32.","ama":"Dütting P, Henzinger M, Weber I. Bidder optimal assignments for general utilities. <i>Theoretical Computer Science</i>. 2013;478(3):22-32. doi:<a href=\"https://doi.org/10.1016/j.tcs.2013.01.030\">10.1016/j.tcs.2013.01.030</a>","chicago":"Dütting, Paul, Monika Henzinger, and Ingmar Weber. “Bidder Optimal Assignments for General Utilities.” <i>Theoretical Computer Science</i>. Elsevier, 2013. <a href=\"https://doi.org/10.1016/j.tcs.2013.01.030\">https://doi.org/10.1016/j.tcs.2013.01.030</a>.","mla":"Dütting, Paul, et al. “Bidder Optimal Assignments for General Utilities.” <i>Theoretical Computer Science</i>, vol. 478, no. 3, Elsevier, 2013, pp. 22–32, doi:<a href=\"https://doi.org/10.1016/j.tcs.2013.01.030\">10.1016/j.tcs.2013.01.030</a>.","apa":"Dütting, P., Henzinger, M., &#38; Weber, I. (2013). Bidder optimal assignments for general utilities. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2013.01.030\">https://doi.org/10.1016/j.tcs.2013.01.030</a>","short":"P. Dütting, M. Henzinger, I. Weber, Theoretical Computer Science 478 (2013) 22–32."},"publication_status":"published","year":"2013","date_created":"2022-08-17T11:11:04Z","publication":"Theoretical Computer Science","intvolume":"       478","author":[{"full_name":"Dütting, Paul","last_name":"Dütting","first_name":"Paul"},{"last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530"},{"full_name":"Weber, Ingmar","first_name":"Ingmar","last_name":"Weber"}],"scopus_import":"1","date_updated":"2024-11-06T12:24:12Z","quality_controlled":"1","status":"public","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"11799","relation":"earlier_version"}]},"abstract":[{"text":"We study the problem of matching bidders to items where each bidder i has general, strictly monotonic utility functions ui,j(pj) expressing his utility of being matched to item j at price pj. For this setting we prove that a bidder optimal outcome always exists, even when the utility functions are non-linear and non-continuous. We give sufficient conditions under\r\nwhich every mechanism that finds a bidder optimal outcome is incentive compatible. We also give a mechanism that finds a bidder optimal outcome if the conditions for incentive compatibility are satisfied. The running time of this mechanism is exponential in the number of items, but polynomial in the number of bidders.","lang":"eng"}],"type":"journal_article"},{"publication_status":"published","doi":"10.1016/j.tcs.2006.07.032","publication":"Theoretical Computer Science","year":"2006","date_created":"2018-12-11T12:09:26Z","intvolume":"       365","issue":"1-2","article_processing_charge":"No","date_published":"2006-08-07T00:00:00Z","publisher":"Elsevier","month":"08","article_type":"original","extern":"1","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Games with secure equilibria,” <i>Theoretical Computer Science</i>, vol. 365, no. 1–2. Elsevier, pp. 67–82, 2006.","ista":"Chatterjee K, Henzinger TA, Jurdziński M. 2006. Games with secure equilibria. Theoretical Computer Science. 365(1–2), 67–82.","ama":"Chatterjee K, Henzinger TA, Jurdziński M. Games with secure equilibria. <i>Theoretical Computer Science</i>. 2006;365(1-2):67-82. doi:<a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">10.1016/j.tcs.2006.07.032</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Games with Secure Equilibria.” <i>Theoretical Computer Science</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">https://doi.org/10.1016/j.tcs.2006.07.032</a>.","mla":"Chatterjee, Krishnendu, et al. “Games with Secure Equilibria.” <i>Theoretical Computer Science</i>, vol. 365, no. 1–2, Elsevier, 2006, pp. 67–82, doi:<a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">10.1016/j.tcs.2006.07.032</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Jurdziński, M. (2006). Games with secure equilibria. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">https://doi.org/10.1016/j.tcs.2006.07.032</a>","short":"K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science 365 (2006) 67–82."},"oa_version":"None","volume":365,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","status":"public","language":[{"iso":"eng"}],"title":"Games with secure equilibria","abstract":[{"lang":"eng","text":"In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent's payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it sometimes suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of ω-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium."}],"_id":"4550","type":"journal_article","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Jurdziński, Marcin","first_name":"Marcin","last_name":"Jurdziński"}],"publication_identifier":{"eissn":["1879-2294"],"issn":["0304-3975"]},"page":"67 - 82","day":"07","fulldoi":"https://doi.org/10.1016/j.tcs.2006.07.032","publist_id":"164","date_updated":"2026-08-21T10:28:39Z"},{"issue":"2","doi":"10.1016/j.tcs.2005.11.015","volume":354,"article_processing_charge":"No","article_type":"original","title":"On the universal and existential fragments of the mu-calculus","_id":"4451","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.1016/j.tcs.2005.11.015","day":"28","publication_identifier":{"issn":["0304-3975"],"eissn":["1879-2294"]},"page":"173 - 186","intvolume":"       354","publication_status":"published","date_created":"2018-12-11T12:08:55Z","year":"2006","publication":"Theoretical Computer Science","citation":{"ista":"Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186.","ieee":"T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential fragments of the mu-calculus,” <i>Theoretical Computer Science</i>, vol. 354, no. 2. Elsevier, pp. 173–186, 2006.","ama":"Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments of the mu-calculus. <i>Theoretical Computer Science</i>. 2006;354(2):173-186. doi:<a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">10.1016/j.tcs.2005.11.015</a>","chicago":"Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal and Existential Fragments of the Mu-Calculus.” <i>Theoretical Computer Science</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">https://doi.org/10.1016/j.tcs.2005.11.015</a>.","mla":"Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of the Mu-Calculus.” <i>Theoretical Computer Science</i>, vol. 354, no. 2, Elsevier, 2006, pp. 173–86, doi:<a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">10.1016/j.tcs.2005.11.015</a>.","apa":"Henzinger, T. A., Kupferman, O., &#38; Majumdar, R. (2006). On the universal and existential fragments of the mu-calculus. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">https://doi.org/10.1016/j.tcs.2005.11.015</a>","short":"T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354 (2006) 173–186."},"oa_version":"None","date_published":"2006-03-28T00:00:00Z","publisher":"Elsevier","month":"03","extern":"1","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternation-free fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment."}],"type":"journal_article","status":"public","OA_type":"closed access","publist_id":"276","date_updated":"2026-08-21T10:58:07Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"}]},{"issue":"1","doi":"10.1016/j.tcs.2005.07.033","volume":345,"article_processing_charge":"No","article_type":"original","title":"Model checking discounted temporal properties","_id":"4625","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.1016/j.tcs.2005.07.033","page":"139 - 170","publication_identifier":{"issn":["0304-3975"],"eissn":["1879-2294"]},"day":"21","intvolume":"       345","publication_status":"published","publication":"Theoretical Computer Science","date_created":"2018-12-11T12:09:49Z","year":"2005","citation":{"ieee":"L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “Model checking discounted temporal properties,” <i>Theoretical Computer Science</i>, vol. 345, no. 1. Elsevier, pp. 139–170, 2005.","ista":"De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2005. Model checking discounted temporal properties. Theoretical Computer Science. 345(1), 139–170.","ama":"De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Model checking discounted temporal properties. <i>Theoretical Computer Science</i>. 2005;345(1):139-170. doi:<a href=\"https://doi.org/10.1016/j.tcs.2005.07.033\">10.1016/j.tcs.2005.07.033</a>","mla":"De Alfaro, Luca, et al. “Model Checking Discounted Temporal Properties.” <i>Theoretical Computer Science</i>, vol. 345, no. 1, Elsevier, 2005, pp. 139–70, doi:<a href=\"https://doi.org/10.1016/j.tcs.2005.07.033\">10.1016/j.tcs.2005.07.033</a>.","chicago":"De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and Mariëlle Stoelinga. “Model Checking Discounted Temporal Properties.” <i>Theoretical Computer Science</i>. Elsevier, 2005. <a href=\"https://doi.org/10.1016/j.tcs.2005.07.033\">https://doi.org/10.1016/j.tcs.2005.07.033</a>.","apa":"De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., &#38; Stoelinga, M. (2005). Model checking discounted temporal properties. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2005.07.033\">https://doi.org/10.1016/j.tcs.2005.07.033</a>","short":"L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, Theoretical Computer Science 345 (2005) 139–170."},"oa_version":"None","date_published":"2005-11-21T00:00:00Z","publisher":"Elsevier","extern":"1","month":"11","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators ⋄ and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path.\r\n\r\nWe interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics."}],"type":"journal_article","status":"public","OA_type":"closed access","date_updated":"2026-09-30T14:03:08Z","publist_id":"80","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"first_name":"Marco","last_name":"Faella","full_name":"Faella, Marco"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"full_name":"Stoelinga, Mariëlle","last_name":"Stoelinga","first_name":"Mariëlle"}]},{"page":"151 - 182","day":"01","publication_identifier":{"issn":["0304-3975"]},"fulldoi":"https://doi.org/10.1016/S0304-3975(00)00308-X","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4407","title":"Axioms for real-time logics","article_type":"original","article_processing_charge":"No","volume":274,"doi":"10.1016/S0304-3975(00)00308-X","issue":"1-2","author":[{"last_name":"Raskin","first_name":"Jean","full_name":"Raskin, Jean"},{"full_name":"Schobbens, Pierre","first_name":"Pierre","last_name":"Schobbens"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"date_updated":"2023-06-06T09:10:56Z","publist_id":"324","scopus_import":"1","quality_controlled":"1","status":"public","type":"journal_article","abstract":[{"lang":"eng","text":"This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MetricIntervalTL formulae into EventClockTL formulae, the two logics being equally expressive. Our proof is structured to yield axiomatizations also for interesting fragments of these logics, such as the linear temporal logic of the real numbers (TLR)."}],"language":[{"iso":"eng"}],"month":"03","extern":"1","publisher":"Elsevier","date_published":"2002-03-01T00:00:00Z","oa_version":"None","citation":{"ista":"Raskin J, Schobbens P, Henzinger TA. 2002. Axioms for real-time logics. Theoretical Computer Science. 274(1–2), 151–182.","ieee":"J. Raskin, P. Schobbens, and T. A. Henzinger, “Axioms for real-time logics,” <i>Theoretical Computer Science</i>, vol. 274, no. 1–2. Elsevier, pp. 151–182, 2002.","ama":"Raskin J, Schobbens P, Henzinger TA. Axioms for real-time logics. <i>Theoretical Computer Science</i>. 2002;274(1-2):151-182. doi:<a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">10.1016/S0304-3975(00)00308-X</a>","chicago":"Raskin, Jean, Pierre Schobbens, and Thomas A Henzinger. “Axioms for Real-Time Logics.” <i>Theoretical Computer Science</i>. Elsevier, 2002. <a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">https://doi.org/10.1016/S0304-3975(00)00308-X</a>.","mla":"Raskin, Jean, et al. “Axioms for Real-Time Logics.” <i>Theoretical Computer Science</i>, vol. 274, no. 1–2, Elsevier, 2002, pp. 151–82, doi:<a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">10.1016/S0304-3975(00)00308-X</a>.","apa":"Raskin, J., Schobbens, P., &#38; Henzinger, T. A. (2002). Axioms for real-time logics. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0304-3975(00)00308-X\">https://doi.org/10.1016/S0304-3975(00)00308-X</a>","short":"J. Raskin, P. Schobbens, T.A. Henzinger, Theoretical Computer Science 274 (2002) 151–182."},"year":"2002","date_created":"2018-12-11T12:08:42Z","publication":"Theoretical Computer Science","publication_status":"published","intvolume":"       274"},{"intvolume":"       221","publication_status":"published","date_created":"2018-12-11T12:08:52Z","publication":"Theoretical Computer Science","year":"1999","citation":{"chicago":"Henzinger, Thomas A, and Peter Kopke. “Discrete-Time Control for Rectangular Hybrid Automata.” <i>Theoretical Computer Science</i>. Elsevier, 1999. <a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">https://doi.org/10.1016/S0304-3975(99)00038-9</a>.","mla":"Henzinger, Thomas A., and Peter Kopke. “Discrete-Time Control for Rectangular Hybrid Automata.” <i>Theoretical Computer Science</i>, vol. 221, no. 1–2, Elsevier, 1999, pp. 369–92, doi:<a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">10.1016/S0304-3975(99)00038-9</a>.","apa":"Henzinger, T. A., &#38; Kopke, P. (1999). Discrete-time control for rectangular hybrid automata. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">https://doi.org/10.1016/S0304-3975(99)00038-9</a>","short":"T.A. Henzinger, P. Kopke, Theoretical Computer Science 221 (1999) 369–392.","ista":"Henzinger TA, Kopke P. 1999. Discrete-time control for rectangular hybrid automata. Theoretical Computer Science. 221(1–2), 369–392.","ieee":"T. A. Henzinger and P. Kopke, “Discrete-time control for rectangular hybrid automata,” <i>Theoretical Computer Science</i>, vol. 221, no. 1–2. Elsevier, pp. 369–392, 1999.","ama":"Henzinger TA, Kopke P. Discrete-time control for rectangular hybrid automata. <i>Theoretical Computer Science</i>. 1999;221(1-2):369-392. doi:<a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">10.1016/S0304-3975(99)00038-9</a>"},"oa_version":"None","date_published":"1999-01-01T00:00:00Z","publisher":"Elsevier","extern":"1","month":"01","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Rectangular hybrid automata model digital control programs of analog plant environments. We study rectangular hybrid automata where the plant state evolves continuously in real-numbered time, and the controller samples the plant state and changes the control state discretely, only at the integer points in time. We prove that rectangular hybrid automata have finite bisimilarity quotients when all control transitions happen at integer times, even if the constraints on the derivatives of the variables vary between control states. This is in contrast with the conventional model where control transitions may happen at any real time, and already the reachability problem is undecidable. Based on the finite bisimilarity quotients, we give an exponential algorithm for the symbolic sampling-controller synthesis of rectangular automata. We show our algorithm to be optimal by proving the problem to be EXPTIME-hard. We also show that rectangular automata form a maximal class of systems for which the sampling-controller synthesis problem can be solved algorithmically."}],"type":"journal_article","quality_controlled":"1","status":"public","scopus_import":"1","date_updated":"2022-09-06T08:03:48Z","publist_id":"290","author":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Kopke, Peter","first_name":"Peter","last_name":"Kopke"}],"issue":"1-2","doi":"10.1016/S0304-3975(99)00038-9","volume":221,"article_processing_charge":"No","article_type":"original","title":"Discrete-time control for rectangular hybrid automata","_id":"4442","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","fulldoi":"https://doi.org/10.1016/S0304-3975(99)00038-9","publication_identifier":{"issn":["0304-3975"]},"day":"01","page":"369 - 392"},{"publist_id":"94","date_updated":"2022-06-09T13:40:48Z","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"first_name":"Costas","last_name":"Courcoubetis","full_name":"Courcoubetis, Costas"},{"first_name":"Nicolas","last_name":"Halbwachs","full_name":"Halbwachs, Nicolas"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Ho, Pei","first_name":"Pei","last_name":"Ho"},{"first_name":"Xavier","last_name":"Nicollin","full_name":"Nicollin, Xavier"},{"last_name":"Olivero","first_name":"Alfredo","full_name":"Olivero, Alfredo"},{"last_name":"Sifakis","first_name":"Joseph","full_name":"Sifakis, Joseph"},{"last_name":"Yovine","first_name":"Sergio","full_name":"Yovine, Sergio"}],"abstract":[{"lang":"eng","text":"We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge."}],"language":[{"iso":"eng"}],"type":"journal_article","quality_controlled":"1","status":"public","oa_version":"None","citation":{"ista":"Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho P, Nicollin X, Olivero A, Sifakis J, Yovine S. 1995. The algorithmic analysis of hybrid systems. Theoretical Computer Science. 138(1), 3–34.","ieee":"R. Alur <i>et al.</i>, “The algorithmic analysis of hybrid systems,” <i>Theoretical Computer Science</i>, vol. 138, no. 1. Elsevier, pp. 3–34, 1995.","ama":"Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems. <i>Theoretical Computer Science</i>. 1995;138(1):3-34. doi:<a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">10.1016/0304-3975(94)00202-T</a>","mla":"Alur, Rajeev, et al. “The Algorithmic Analysis of Hybrid Systems.” <i>Theoretical Computer Science</i>, vol. 138, no. 1, Elsevier, 1995, pp. 3–34, doi:<a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">10.1016/0304-3975(94)00202-T</a>.","chicago":"Alur, Rajeev, Costas Courcoubetis, Nicolas Halbwachs, Thomas A Henzinger, Pei Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The Algorithmic Analysis of Hybrid Systems.” <i>Theoretical Computer Science</i>. Elsevier, 1995. <a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">https://doi.org/10.1016/0304-3975(94)00202-T</a>.","apa":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P., Nicollin, X., … Yovine, S. (1995). The algorithmic analysis of hybrid systems. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">https://doi.org/10.1016/0304-3975(94)00202-T</a>","short":"R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine, Theoretical Computer Science 138 (1995) 3–34."},"date_published":"1995-02-06T00:00:00Z","extern":"1","month":"02","publisher":"Elsevier","intvolume":"       138","publication":"Theoretical Computer Science","year":"1995","date_created":"2018-12-11T12:09:45Z","publication_status":"published","fulldoi":"https://doi.org/10.1016/0304-3975(94)00202-T","day":"06","page":"3 - 34","publication_identifier":{"issn":["0304-3975"]},"title":"The algorithmic analysis of hybrid systems","_id":"4613","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/030439759400202T?via%3Dihub"}],"volume":138,"article_processing_charge":"No","article_type":"original","issue":"1","doi":"10.1016/0304-3975(94)00202-T"},{"status":"public","quality_controlled":"1","type":"journal_article","abstract":[{"text":"Arrangements of curves in the plane are fundamental to many problems in computational and combinatorial geometry (e.g. motion planning, algebraic cell decomposition, etc.). In this paper we study various topological and combinatorial properties of such arrangements under some mild assumptions on the shape of the curves, and develop basic tools for the construction, manipulation, and analysis of these arrangements. Our main results include a generalization of the zone theorem of Edelsbrunner (1986) and Chazelle (1985) to arrangements of curves (in which we show that the combinatorial complexity of the zone of a curve is nearly linear in the number of curves) and an application of that theorem to obtain a nearly quadratic incremental algorithm for the construction of such arrangements.","lang":"eng"}],"language":[{"iso":"eng"}],"author":[{"orcid":"0000-0002-9823-6833","last_name":"Edelsbrunner","first_name":"Herbert","full_name":"Edelsbrunner, Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Guibas, Leonidas","last_name":"Guibas","first_name":"Leonidas"},{"full_name":"Pach, János","last_name":"Pach","first_name":"János"},{"full_name":"Pollack, Richard","last_name":"Pollack","first_name":"Richard"},{"first_name":"Raimund","last_name":"Seidel","full_name":"Seidel, Raimund"},{"last_name":"Sharir","first_name":"Micha","full_name":"Sharir, Micha"}],"publist_id":"2079","date_updated":"2022-03-16T09:04:37Z","scopus_import":"1","date_created":"2018-12-11T12:06:37Z","publication":"Theoretical Computer Science","year":"1992","publication_status":"published","acknowledgement":"Work on this paper by the first author has been supported by the National Science Foundation under grant CCR-8714565. Work by the third and sixth authors has been supported by Office of Naval Research Grant NOOOl4-82-K-0381, by National Science Foundation Grant No. NSF-DCR-83-20085, by grants from the Digital Equipment Corporation, and the IBM Corporation. Work by the sixth author has also been supported by a research grant from the NCRD- the Israeli National Council for Research and Development. Work by the fourth author has been supported by National Science Foundation Grant DMS-8501947. ","intvolume":"        92","extern":"1","month":"01","publisher":"Elsevier","date_published":"1992-01-20T00:00:00Z","citation":{"short":"H. Edelsbrunner, L. Guibas, J. Pach, R. Pollack, R. Seidel, M. Sharir, Theoretical Computer Science 92 (1992) 319–336.","mla":"Edelsbrunner, Herbert, et al. “Arrangements of Curves in the Plane - Topology, Combinatorics, and Algorithms.” <i>Theoretical Computer Science</i>, vol. 92, no. 2, Elsevier, 1992, pp. 319–36, doi:<a href=\"https://doi.org/10.1016/0304-3975(92)90319-B\">10.1016/0304-3975(92)90319-B</a>.","chicago":"Edelsbrunner, Herbert, Leonidas Guibas, János Pach, Richard Pollack, Raimund Seidel, and Micha Sharir. “Arrangements of Curves in the Plane - Topology, Combinatorics, and Algorithms.” <i>Theoretical Computer Science</i>. Elsevier, 1992. <a href=\"https://doi.org/10.1016/0304-3975(92)90319-B\">https://doi.org/10.1016/0304-3975(92)90319-B</a>.","apa":"Edelsbrunner, H., Guibas, L., Pach, J., Pollack, R., Seidel, R., &#38; Sharir, M. (1992). Arrangements of curves in the plane - topology, combinatorics, and algorithms. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/0304-3975(92)90319-B\">https://doi.org/10.1016/0304-3975(92)90319-B</a>","ieee":"H. Edelsbrunner, L. Guibas, J. Pach, R. Pollack, R. Seidel, and M. Sharir, “Arrangements of curves in the plane - topology, combinatorics, and algorithms,” <i>Theoretical Computer Science</i>, vol. 92, no. 2. Elsevier, pp. 319–336, 1992.","ista":"Edelsbrunner H, Guibas L, Pach J, Pollack R, Seidel R, Sharir M. 1992. Arrangements of curves in the plane - topology, combinatorics, and algorithms. Theoretical Computer Science. 92(2), 319–336.","ama":"Edelsbrunner H, Guibas L, Pach J, Pollack R, Seidel R, Sharir M. Arrangements of curves in the plane - topology, combinatorics, and algorithms. <i>Theoretical Computer Science</i>. 1992;92(2):319-336. doi:<a href=\"https://doi.org/10.1016/0304-3975(92)90319-B\">10.1016/0304-3975(92)90319-B</a>"},"oa_version":"Published Version","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4047","title":"Arrangements of curves in the plane - topology, combinatorics, and algorithms","publication_identifier":{"issn":["0304-3975"]},"day":"20","page":"319 - 336","fulldoi":"https://doi.org/10.1016/0304-3975(92)90319-B","oa":1,"doi":"10.1016/0304-3975(92)90319-B","issue":"2","article_type":"original","article_processing_charge":"No","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/030439759290319B?via%3Dihub","open_access":"1"}],"volume":92},{"fulldoi":"https://doi.org/10.1016/0304-3975(91)90261-Y","publication_identifier":{"issn":["0304-3975"],"eissn":["1879-2294"]},"day":"22","page":"77 - 105","_id":"4052","title":"A singly exponential stratification scheme for real semi-algebraic varieties and its applications","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","volume":84,"main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/030439759190261Y?via%3Dihub"}],"article_type":"original","article_processing_charge":"No","issue":"1","oa":1,"doi":"10.1016/0304-3975(91)90261-Y","scopus_import":"1","date_updated":"2022-03-02T10:23:58Z","publist_id":"2073","author":[{"full_name":"Chazelle, Bernard","last_name":"Chazelle","first_name":"Bernard"},{"first_name":"Herbert","last_name":"Edelsbrunner","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","full_name":"Edelsbrunner, Herbert","orcid":"0000-0002-9823-6833"},{"last_name":"Guibas","first_name":"Leonidas","full_name":"Guibas, Leonidas"},{"full_name":"Sharir, Micha","first_name":"Micha","last_name":"Sharir"}],"type":"journal_article","language":[{"iso":"eng"}],"abstract":[{"text":"This paper describes an effective procedure for stratifying a real semi-algebraic set into cells of constant description size. The attractive feature of our method is that the number of cells produced is singly exponential in the number of input variables. This compares favorably with the doubly exponential size of Collins' decomposition. Unlike Collins' construction, however, our scheme does not produce a cell complex but only a smooth stratification. Nevertheless, we are able to apply our results in interesting ways to problems of point location and geometric optimization.","lang":"eng"}],"quality_controlled":"1","status":"public","citation":{"ama":"Chazelle B, Edelsbrunner H, Guibas L, Sharir M. A singly exponential stratification scheme for real semi-algebraic varieties and its applications. <i>Theoretical Computer Science</i>. 1991;84(1):77-105. doi:<a href=\"https://doi.org/10.1016/0304-3975(91)90261-Y\">10.1016/0304-3975(91)90261-Y</a>","ista":"Chazelle B, Edelsbrunner H, Guibas L, Sharir M. 1991. A singly exponential stratification scheme for real semi-algebraic varieties and its applications. Theoretical Computer Science. 84(1), 77–105.","ieee":"B. Chazelle, H. Edelsbrunner, L. Guibas, and M. Sharir, “A singly exponential stratification scheme for real semi-algebraic varieties and its applications,” <i>Theoretical Computer Science</i>, vol. 84, no. 1. Elsevier, pp. 77–105, 1991.","apa":"Chazelle, B., Edelsbrunner, H., Guibas, L., &#38; Sharir, M. (1991). A singly exponential stratification scheme for real semi-algebraic varieties and its applications. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/0304-3975(91)90261-Y\">https://doi.org/10.1016/0304-3975(91)90261-Y</a>","mla":"Chazelle, Bernard, et al. “A Singly Exponential Stratification Scheme for Real Semi-Algebraic Varieties and Its Applications.” <i>Theoretical Computer Science</i>, vol. 84, no. 1, Elsevier, 1991, pp. 77–105, doi:<a href=\"https://doi.org/10.1016/0304-3975(91)90261-Y\">10.1016/0304-3975(91)90261-Y</a>.","chicago":"Chazelle, Bernard, Herbert Edelsbrunner, Leonidas Guibas, and Micha Sharir. “A Singly Exponential Stratification Scheme for Real Semi-Algebraic Varieties and Its Applications.” <i>Theoretical Computer Science</i>. Elsevier, 1991. <a href=\"https://doi.org/10.1016/0304-3975(91)90261-Y\">https://doi.org/10.1016/0304-3975(91)90261-Y</a>.","short":"B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, Theoretical Computer Science 84 (1991) 77–105."},"oa_version":"Published Version","publisher":"Elsevier","extern":"1","month":"07","date_published":"1991-07-22T00:00:00Z","intvolume":"        84","acknowledgement":"The authors wish to thank DEC/Systems Research Center and DEC/Paris Research Laboratory, where part of this research was conducted. For individual support, Bernard Chazelle acknowledges the National Science Foundation for supporting this research in part under Grant CCR-8700917. Herbert Edelsbrunner acknowledges the support of the National Science Foundation under Grant CCR-8714565. Micha Sharir acknowledges the Office of Naval Research under Grant N00014-87-K-0129, the National Science Foundation under Grant No. NSF-DCR-83-20085, grants from the Digital Equipment Corporation and the IBM Corporation, and a research grant from the US-Israeli Binational Science Foundation.","publication_status":"published","publication":"Theoretical Computer Science","year":"1991","date_created":"2018-12-11T12:06:39Z"}]