[{"date_published":"2018-05-01T00:00:00Z","_id":"11890","external_id":{"arxiv":["1412.1318"]},"title":"Deterministic fully dynamic data structures for vertex cover and matching","arxiv":1,"year":"2018","date_created":"2022-08-17T08:21:23Z","type":"journal_article","month":"05","article_type":"original","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","issue":"3","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1412.1318"}],"intvolume":" 47","language":[{"iso":"eng"}],"volume":47,"publication":"SIAM Journal on Computing","scopus_import":"1","oa":1,"publication_identifier":{"eissn":["1095-7111"],"issn":["0097-5397"]},"status":"public","publisher":"Society for Industrial & Applied Mathematics","citation":{"short":"S. Bhattacharya, M. Henzinger, G.F. Italiano, SIAM Journal on Computing 47 (2018) 859–887.","apa":"Bhattacharya, S., Henzinger, M., & Italiano, G. F. (2018). Deterministic fully dynamic data structures for vertex cover and matching. SIAM Journal on Computing. Society for Industrial & Applied Mathematics. https://doi.org/10.1137/140998925","ista":"Bhattacharya S, Henzinger M, Italiano GF. 2018. Deterministic fully dynamic data structures for vertex cover and matching. SIAM Journal on Computing. 47(3), 859–887.","ieee":"S. Bhattacharya, M. Henzinger, and G. F. Italiano, “Deterministic fully dynamic data structures for vertex cover and matching,” SIAM Journal on Computing, vol. 47, no. 3. Society for Industrial & Applied Mathematics, pp. 859–887, 2018.","chicago":"Bhattacharya, Sayan, Monika Henzinger, and Giuseppe F. Italiano. “Deterministic Fully Dynamic Data Structures for Vertex Cover and Matching.” SIAM Journal on Computing. Society for Industrial & Applied Mathematics, 2018. https://doi.org/10.1137/140998925.","mla":"Bhattacharya, Sayan, et al. “Deterministic Fully Dynamic Data Structures for Vertex Cover and Matching.” SIAM Journal on Computing, vol. 47, no. 3, Society for Industrial & Applied Mathematics, 2018, pp. 859–87, doi:10.1137/140998925.","ama":"Bhattacharya S, Henzinger M, Italiano GF. Deterministic fully dynamic data structures for vertex cover and matching. SIAM Journal on Computing. 2018;47(3):859-887. doi:10.1137/140998925"},"related_material":{"record":[{"id":"11875","status":"public","relation":"earlier_version"}]},"author":[{"first_name":"Sayan","full_name":"Bhattacharya, Sayan","last_name":"Bhattacharya"},{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"last_name":"Italiano","first_name":"Giuseppe F.","full_name":"Italiano, Giuseppe F."}],"date_updated":"2024-11-06T12:22:54Z","quality_controlled":"1","oa_version":"Preprint","page":"859-887","abstract":[{"text":"We present the first deterministic data structures for maintaining approximate minimum vertex cover and maximum matching in a fully dynamic graph 𝐺=(𝑉,𝐸), with |𝑉|=𝑛 and |𝐸|=𝑚, in 𝑜(𝑚‾‾√) time per update. In particular, for minimum vertex cover, we provide deterministic data structures for maintaining a (2+𝜖) approximation in 𝑂(log𝑛/𝜖2) amortized time per update. For maximum matching, we show how to maintain a (3+𝜖) approximation in 𝑂(min(𝑛√/𝜖,𝑚1/3/𝜖2) amortized time per update and a (4+𝜖) approximation in 𝑂(𝑚1/3/𝜖2) worst-case time per update. Our data structure for fully dynamic minimum vertex cover is essentially near-optimal and settles an open problem by Onak and Rubinfeld [in 42nd ACM Symposium on Theory of Computing, Cambridge, MA, ACM, 2010, pp. 457--464].","lang":"eng"}],"publication_status":"published","doi":"10.1137/140998925","day":"01","extern":"1"},{"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Partially observable Markov decision processes (POMDPs) are the standard models for planning under uncertainty with both finite and infinite horizon. Besides the well-known discounted-sum objective, indefinite-horizon objective (aka Goal-POMDPs) is another classical objective for POMDPs. In this case, given a set of target states and a positive cost for each transition, the optimization objective is to minimize the expected total cost until a target state is reached. In the literature, RTDP-Bel or heuristic search value iteration (HSVI) have been used for solving Goal-POMDPs. Neither of these algorithms has theoretical convergence guarantees, and HSVI may even fail to terminate its trials. We give the following contributions: (1) We discuss the challenges introduced in Goal-POMDPs and illustrate how they prevent the original HSVI from converging. (2) We present a novel algorithm inspired by HSVI, termed Goal-HSVI, and show that our algorithm has convergence guarantees. (3) We show that Goal-HSVI outperforms RTDP-Bel on a set of well-known examples."}],"page":"4764 - 4770","ddc":["000"],"publication_status":"published","doi":"10.24963/ijcai.2018/662","publist_id":"8030","day":"01","isi":1,"department":[{"_id":"KrCh"}],"conference":{"end_date":"2018-07-19","start_date":"2018-07-13","name":"IJCAI: International Joint Conference on Artificial Intelligence","location":"Stockholm, Sweden"},"scopus_import":"1","publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","acknowledgement":"∗This work has been supported by Vienna Science and Technology Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Starting grant (279307: Graph Games). This research was sponsored by the Army Research Laboratory and was accomplished under Cooperative Agreement Number W911NF-13-2-0045 (ARL Cyber Security CRA). ","oa":1,"status":"public","citation":{"apa":"Horák, K., Bošanský, B., & Chatterjee, K. (2018). Goal-HSVI: Heuristic search value iteration for goal-POMDPs. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (Vol. 2018–July, pp. 4764–4770). Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/662","short":"K. Horák, B. Bošanský, K. Chatterjee, in:, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4764–4770.","ieee":"K. Horák, B. Bošanský, and K. Chatterjee, “Goal-HSVI: Heuristic search value iteration for goal-POMDPs,” in Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018–July, pp. 4764–4770.","ista":"Horák K, Bošanský B, Chatterjee K. 2018. Goal-HSVI: Heuristic search value iteration for goal-POMDPs. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018–July, 4764–4770.","chicago":"Horák, Karel, Branislav Bošanský, and Krishnendu Chatterjee. “Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs.” In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018–July:4764–70. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/662.","mla":"Horák, Karel, et al. “Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs.” Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, vol. 2018–July, IJCAI, 2018, pp. 4764–70, doi:10.24963/ijcai.2018/662.","ama":"Horák K, Bošanský B, Chatterjee K. Goal-HSVI: Heuristic search value iteration for goal-POMDPs. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. Vol 2018-July. IJCAI; 2018:4764-4770. doi:10.24963/ijcai.2018/662"},"publisher":"IJCAI","author":[{"full_name":"Horák, Karel","first_name":"Karel","last_name":"Horák"},{"first_name":"Branislav","full_name":"Bošanský, Branislav","last_name":"Bošanský"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"date_updated":"2026-06-18T18:34:17Z","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"quality_controlled":"1","date_created":"2018-12-11T11:44:13Z","type":"conference","month":"07","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.24963/ijcai.2018/662"}],"language":[{"iso":"eng"}],"volume":"2018-July","date_published":"2018-07-01T00:00:00Z","_id":"25","external_id":{"isi":["000764175404127"]},"title":"Goal-HSVI: Heuristic search value iteration for goal-POMDPs","year":"2018"},{"external_id":{"arxiv":["1712.00434"]},"file_date_updated":"2020-07-14T12:45:51Z","arxiv":1,"title":"On the treewidth of triangulated 3-manifolds","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"year":"2018","date_published":"2018-06-01T00:00:00Z","_id":"285","intvolume":" 99","language":[{"iso":"eng"}],"volume":99,"date_created":"2018-12-11T11:45:37Z","type":"conference","file":[{"content_type":"application/pdf","file_size":642522,"creator":"dernst","date_created":"2018-12-17T15:32:38Z","access_level":"open_access","checksum":"530d084116778135d5bffaa317479cac","relation":"main_file","date_updated":"2020-07-14T12:45:51Z","file_id":"5713","file_name":"2018_LIPIcs_Huszar.pdf"}],"month":"06","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"ama":"Huszár K, Spreer J, Wagner U. On the treewidth of triangulated 3-manifolds. In: Vol 99. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.SoCG.2018.46","mla":"Huszár, Kristóf, et al. On the Treewidth of Triangulated 3-Manifolds. Vol. 99, 46, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.SoCG.2018.46.","chicago":"Huszár, Kristóf, Jonathan Spreer, and Uli Wagner. “On the Treewidth of Triangulated 3-Manifolds,” Vol. 99. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.SoCG.2018.46.","ieee":"K. Huszár, J. Spreer, and U. Wagner, “On the treewidth of triangulated 3-manifolds,” presented at the SoCG: Symposium on Computational Geometry, Budapest, Hungary, 2018, vol. 99.","ista":"Huszár K, Spreer J, Wagner U. 2018. On the treewidth of triangulated 3-manifolds. SoCG: Symposium on Computational Geometry, LIPIcs, vol. 99, 46.","apa":"Huszár, K., Spreer, J., & Wagner, U. (2018). On the treewidth of triangulated 3-manifolds (Vol. 99). Presented at the SoCG: Symposium on Computational Geometry, Budapest, Hungary: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SoCG.2018.46","short":"K. Huszár, J. Spreer, U. Wagner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018."},"related_material":{"record":[{"id":"7093","status":"public","relation":"later_version"}]},"date_updated":"2025-07-10T11:52:21Z","author":[{"orcid":"0000-0002-5445-5057","last_name":"Huszár","id":"33C26278-F248-11E8-B48F-1D18A9856A87","full_name":"Huszár, Kristóf","first_name":"Kristóf"},{"last_name":"Spreer","full_name":"Spreer, Jonathan","first_name":"Jonathan"},{"full_name":"Wagner, Uli","first_name":"Uli","id":"36690CA2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1494-0568","last_name":"Wagner"}],"quality_controlled":"1","alternative_title":["LIPIcs"],"scopus_import":"1","oa":1,"acknowledgement":"Research of the second author was supported by the Einstein Foundation (project “Einstein Visiting Fellow Santos”) and by the Simons Foundation (“Simons Visiting Professors” program).","status":"public","publication_identifier":{"issn":["1868-8969"]},"article_number":"46","doi":"10.4230/LIPIcs.SoCG.2018.46","has_accepted_license":"1","day":"01","publist_id":"7614","department":[{"_id":"UlWa"}],"conference":{"location":"Budapest, Hungary","name":"SoCG: Symposium on Computational Geometry","end_date":"2018-06-14","start_date":"2018-06-11"},"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"In graph theory, as well as in 3-manifold topology, there exist several width-type parameters to describe how "simple" or "thin" a given graph or 3-manifold is. These parameters, such as pathwidth or treewidth for graphs, or the concept of thin position for 3-manifolds, play an important role when studying algorithmic problems; in particular, there is a variety of problems in computational 3-manifold topology - some of them known to be computationally hard in general - that become solvable in polynomial time as soon as the dual graph of the input triangulation has bounded treewidth. In view of these algorithmic results, it is natural to ask whether every 3-manifold admits a triangulation of bounded treewidth. We show that this is not the case, i.e., that there exists an infinite family of closed 3-manifolds not admitting triangulations of bounded pathwidth or treewidth (the latter implies the former, but we present two separate proofs). We derive these results from work of Agol and of Scharlemann and Thompson, by exhibiting explicit connections between the topology of a 3-manifold M on the one hand and width-type parameters of the dual graphs of triangulations of M on the other hand, answering a question that had been raised repeatedly by researchers in computational 3-manifold topology. In particular, we show that if a closed, orientable, irreducible, non-Haken 3-manifold M has a triangulation of treewidth (resp. pathwidth) k then the Heegaard genus of M is at most 48(k+1) (resp. 4(3k+1))."}],"ddc":["516","000"],"publication_status":"published"},{"_id":"297","date_published":"2018-04-12T00:00:00Z","file_date_updated":"2020-07-14T12:45:57Z","external_id":{"isi":["000546326300021"]},"year":"2018","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Strategy representation by decision trees in reactive synthesis","type":"conference","date_created":"2018-12-11T11:45:41Z","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"file_name":"2018_LNCS_Brazdil.pdf","file_id":"5723","date_updated":"2020-07-14T12:45:57Z","relation":"main_file","checksum":"b13874ffb114932ad9cc2586b7469db4","date_created":"2018-12-17T16:29:08Z","access_level":"open_access","creator":"dernst","file_size":1829940,"content_type":"application/pdf"}],"month":"04","volume":10805,"intvolume":" 10805","language":[{"iso":"eng"}],"scopus_import":"1","alternative_title":["LNCS"],"status":"public","oa":1,"author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","first_name":"Viktor"}],"date_updated":"2025-03-31T16:01:11Z","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"H2020","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program"}],"publisher":"Springer","citation":{"mla":"Brázdil, Tomáš, et al. Strategy Representation by Decision Trees in Reactive Synthesis. Vol. 10805, Springer, 2018, pp. 385–407, doi:10.1007/978-3-319-89960-2_21.","ama":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:10.1007/978-3-319-89960-2_21","short":"T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.","apa":"Brázdil, T., Chatterjee, K., Kretinsky, J., & Toman, V. (2018). Strategy representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407). Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89960-2_21","ista":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman. “Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407. Springer, 2018. https://doi.org/10.1007/978-3-319-89960-2_21.","ieee":"T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10805, pp. 385–407."},"quality_controlled":"1","ec_funded":1,"oa_version":"Published Version","publication_status":"published","ddc":["000"],"page":"385 - 407","abstract":[{"text":"Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.","lang":"eng"}],"has_accepted_license":"1","publist_id":"7584","day":"12","doi":"10.1007/978-3-319-89960-2_21","conference":{"name":"TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems","location":"Thessaloniki, Greece","end_date":"2018-04-20","start_date":"2018-04-14"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"isi":1},{"oa":1,"status":"public","scopus_import":"1","alternative_title":["LNCS"],"quality_controlled":"1","ec_funded":1,"citation":{"ieee":"J. F. Alwen, J. Blocki, and K. Z. Pietrzak, “Sustained space complexity,” presented at the Eurocrypt: Advances in Cryptology, Tel Aviv, Israel, 2018, vol. 10821, pp. 99–130.","chicago":"Alwen, Joel F, Jeremiah Blocki, and Krzysztof Z Pietrzak. “Sustained Space Complexity,” 10821:99–130. Springer, 2018. https://doi.org/10.1007/978-3-319-78375-8_4.","ista":"Alwen JF, Blocki J, Pietrzak KZ. 2018. Sustained space complexity. Eurocrypt: Advances in Cryptology, LNCS, vol. 10821, 99–130.","apa":"Alwen, J. F., Blocki, J., & Pietrzak, K. Z. (2018). Sustained space complexity (Vol. 10821, pp. 99–130). Presented at the Eurocrypt: Advances in Cryptology, Tel Aviv, Israel: Springer. https://doi.org/10.1007/978-3-319-78375-8_4","short":"J.F. Alwen, J. Blocki, K.Z. Pietrzak, in:, Springer, 2018, pp. 99–130.","ama":"Alwen JF, Blocki J, Pietrzak KZ. Sustained space complexity. In: Vol 10821. Springer; 2018:99-130. doi:10.1007/978-3-319-78375-8_4","mla":"Alwen, Joel F., et al. Sustained Space Complexity. Vol. 10821, Springer, 2018, pp. 99–130, doi:10.1007/978-3-319-78375-8_4."},"publisher":"Springer","date_updated":"2025-07-10T11:52:24Z","author":[{"full_name":"Alwen, Joel F","first_name":"Joel F","id":"2A8DFA8C-F248-11E8-B48F-1D18A9856A87","last_name":"Alwen"},{"full_name":"Blocki, Jeremiah","first_name":"Jeremiah","last_name":"Blocki"},{"orcid":"0000-0002-9139-1654","last_name":"Pietrzak","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","full_name":"Pietrzak, Krzysztof Z","first_name":"Krzysztof Z"}],"project":[{"call_identifier":"H2020","_id":"258AA5B2-B435-11E9-9278-68D0E5697425","name":"Teaching Old Crypto New Tricks","grant_number":"682815"}],"page":"99 - 130","abstract":[{"text":"Memory-hard functions (MHF) are functions whose evaluation cost is dominated by memory cost. MHFs are egalitarian, in the sense that evaluating them on dedicated hardware (like FPGAs or ASICs) is not much cheaper than on off-the-shelf hardware (like x86 CPUs). MHFs have interesting cryptographic applications, most notably to password hashing and securing blockchains.\r\n\r\nAlwen and Serbinenko [STOC’15] define the cumulative memory complexity (cmc) of a function as the sum (over all time-steps) of the amount of memory required to compute the function. They advocate that a good MHF must have high cmc. Unlike previous notions, cmc takes into account that dedicated hardware might exploit amortization and parallelism. Still, cmc has been critizised as insufficient, as it fails to capture possible time-memory trade-offs; as memory cost doesn’t scale linearly, functions with the same cmc could still have very different actual hardware cost.\r\n\r\nIn this work we address this problem, and introduce the notion of sustained-memory complexity, which requires that any algorithm evaluating the function must use a large amount of memory for many steps. We construct functions (in the parallel random oracle model) whose sustained-memory complexity is almost optimal: our function can be evaluated using n steps and O(n/log(n)) memory, in each step making one query to the (fixed-input length) random oracle, while any algorithm that can make arbitrary many parallel queries to the random oracle, still needs Ω(n/log(n)) memory for Ω(n) steps.\r\n\r\nAs has been done for various notions (including cmc) before, we reduce the task of constructing an MHFs with high sustained-memory complexity to proving pebbling lower bounds on DAGs. Our main technical contribution is the construction is a family of DAGs on n nodes with constant indegree with high “sustained-space complexity”, meaning that any parallel black-pebbling strategy requires Ω(n/log(n)) pebbles for at least Ω(n) steps.\r\n\r\nAlong the way we construct a family of maximally “depth-robust” DAGs with maximum indegree O(logn) , improving upon the construction of Mahmoody et al. [ITCS’13] which had maximum indegree O(log2n⋅","lang":"eng"}],"publication_status":"published","oa_version":"Preprint","department":[{"_id":"KrPi"}],"isi":1,"conference":{"location":"Tel Aviv, Israel","name":"Eurocrypt: Advances in Cryptology","end_date":"2018-05-03","start_date":"2018-04-29"},"doi":"10.1007/978-3-319-78375-8_4","day":"31","publist_id":"7583","date_published":"2018-03-31T00:00:00Z","_id":"298","title":"Sustained space complexity","arxiv":1,"year":"2018","external_id":{"arxiv":["1705.05313"],"isi":["000517098700004"]},"month":"03","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:45:41Z","type":"conference","language":[{"iso":"eng"}],"intvolume":" 10821","volume":10821,"main_file_link":[{"url":"https://arxiv.org/abs/1705.05313","open_access":"1"}]},{"isi":1,"department":[{"_id":"ToHe"}],"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Thessaloniki, Greece","start_date":"2018-04-14","end_date":"2018-04-20"},"doi":"10.1007/978-3-319-89963-3_18","publist_id":"7582","has_accepted_license":"1","day":"14","corr_author":"1","abstract":[{"lang":"eng","text":"We introduce in this paper AMT 2.0 , a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal."}],"page":"303 - 319","ddc":["000"],"publication_status":"published","oa_version":"Published Version","quality_controlled":"1","citation":{"ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2018. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10806, 303–319.","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10806, pp. 303–319.","chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” edited by Dirk Beyer and Marieke Huisman, 10806:303–19. Springer, 2018. https://doi.org/10.1007/978-3-319-89963-3_18.","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M. Huisman (Eds.), Springer, 2018, pp. 303–319.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2018). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In D. Beyer & M. Huisman (Eds.) (Vol. 10806, pp. 303–319). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89963-3_18","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In: Beyer D, Huisman M, eds. Vol 10806. Springer; 2018:303-319. doi:10.1007/978-3-319-89963-3_18","mla":"Nickovic, Dejan, et al. AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic. Edited by Dirk Beyer and Marieke Huisman, vol. 10806, Springer, 2018, pp. 303–19, doi:10.1007/978-3-319-89963-3_18."},"related_material":{"record":[{"relation":"later_version","id":"10861","status":"public"}]},"publisher":"Springer","date_updated":"2024-10-09T20:58:19Z","author":[{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Lebeltel","full_name":"Lebeltel, Olivier","first_name":"Olivier"},{"last_name":"Maler","first_name":"Oded","full_name":"Maler, Oded"},{"first_name":"Thomas","full_name":"Ferrere, Thomas","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143"},{"last_name":"Ulus","first_name":"Dogan","full_name":"Ulus, Dogan"}],"oa":1,"status":"public","alternative_title":["LNCS"],"scopus_import":"1","language":[{"iso":"eng"}],"intvolume":" 10806","volume":10806,"month":"04","file":[{"file_name":"2018_LNCS_Nickovic.pdf","date_updated":"2020-07-14T12:45:58Z","relation":"main_file","file_id":"5928","checksum":"e11db3b9c8e27a1c7d1c738cc5e4d25a","file_size":3267209,"content_type":"application/pdf","access_level":"open_access","creator":"dernst","date_created":"2019-02-06T07:33:05Z"}],"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_created":"2018-12-11T11:45:41Z","type":"conference","title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"year":"2018","editor":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"full_name":"Huisman, Marieke","first_name":"Marieke","last_name":"Huisman"}],"external_id":{"isi":["00445822600018"]},"file_date_updated":"2020-07-14T12:45:58Z","date_published":"2018-04-14T00:00:00Z","_id":"299"},{"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"03","type":"conference","date_created":"2018-12-11T11:45:42Z","volume":10820,"language":[{"iso":"eng"}],"intvolume":" 10820","main_file_link":[{"url":"https://eprint.iacr.org/2018/077","open_access":"1"}],"_id":"300","date_published":"2018-03-31T00:00:00Z","year":"2018","title":"On the bit security of cryptographic primitives","external_id":{"isi":["000517097500001"]},"publication_status":"published","page":"3 - 28","corr_author":"1","abstract":[{"text":"We introduce a formal quantitative notion of “bit security” for a general type of cryptographic games (capturing both decision and search problems), aimed at capturing the intuition that a cryptographic primitive with k-bit security is as hard to break as an ideal cryptographic function requiring a brute force attack on a k-bit key space. Our new definition matches the notion of bit security commonly used by cryptographers and cryptanalysts when studying search (e.g., key recovery) problems, where the use of the traditional definition is well established. However, it produces a quantitatively different metric in the case of decision (indistinguishability) problems, where the use of (a straightforward generalization of) the traditional definition is more problematic and leads to a number of paradoxical situations or mismatches between theoretical/provable security and practical/common sense intuition. Key to our new definition is to consider adversaries that may explicitly declare failure of the attack. We support and justify the new definition by proving a number of technical results, including tight reductions between several standard cryptographic problems, a new hybrid theorem that preserves bit security, and an application to the security analysis of indistinguishability primitives making use of (approximate) floating point numbers. This is the first result showing that (standard precision) 53-bit floating point numbers can be used to achieve 100-bit security in the context of cryptographic primitives with general indistinguishability-based security definitions. Previous results of this type applied only to search problems, or special types of decision problems.","lang":"eng"}],"oa_version":"Submitted Version","conference":{"name":"Eurocrypt: Advances in Cryptology","location":"Tel Aviv, Israel","start_date":"2018-04-29","end_date":"2018-05-03"},"department":[{"_id":"KrPi"}],"isi":1,"day":"31","publist_id":"7581","doi":"10.1007/978-3-319-78381-9_1","status":"public","oa":1,"acknowledgement":"Research supported in part by the Defense Advanced Research Projects Agency (DARPA) and the U.S. Army Research Office under the SafeWare program. Opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views, position or policy of the Government. The second author was also supported by the European Research Council, ERC consolidator grant (682815 - TOCNeT).","scopus_import":"1","alternative_title":["LNCS"],"quality_controlled":"1","ec_funded":1,"project":[{"call_identifier":"H2020","_id":"258AA5B2-B435-11E9-9278-68D0E5697425","name":"Teaching Old Crypto New Tricks","grant_number":"682815"}],"date_updated":"2025-04-14T07:22:06Z","author":[{"last_name":"Micciancio","first_name":"Daniele","full_name":"Micciancio, Daniele"},{"last_name":"Walter","id":"488F98B0-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3186-2482","first_name":"Michael","full_name":"Walter, Michael"}],"publisher":"Springer","citation":{"chicago":"Micciancio, Daniele, and Michael Walter. “On the Bit Security of Cryptographic Primitives,” 10820:3–28. Springer, 2018. https://doi.org/10.1007/978-3-319-78381-9_1.","ieee":"D. Micciancio and M. Walter, “On the bit security of cryptographic primitives,” presented at the Eurocrypt: Advances in Cryptology, Tel Aviv, Israel, 2018, vol. 10820, pp. 3–28.","ista":"Micciancio D, Walter M. 2018. On the bit security of cryptographic primitives. Eurocrypt: Advances in Cryptology, LNCS, vol. 10820, 3–28.","short":"D. Micciancio, M. Walter, in:, Springer, 2018, pp. 3–28.","apa":"Micciancio, D., & Walter, M. (2018). On the bit security of cryptographic primitives (Vol. 10820, pp. 3–28). Presented at the Eurocrypt: Advances in Cryptology, Tel Aviv, Israel: Springer. https://doi.org/10.1007/978-3-319-78381-9_1","ama":"Micciancio D, Walter M. On the bit security of cryptographic primitives. In: Vol 10820. Springer; 2018:3-28. doi:10.1007/978-3-319-78381-9_1","mla":"Micciancio, Daniele, and Michael Walter. On the Bit Security of Cryptographic Primitives. Vol. 10820, Springer, 2018, pp. 3–28, doi:10.1007/978-3-319-78381-9_1."}},{"type":"conference","date_created":"2018-12-11T11:45:42Z","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"05","main_file_link":[{"url":"https://eprint.iacr.org/2018/183.pdf","open_access":"1"}],"volume":10821,"intvolume":" 10821","language":[{"iso":"eng"}],"_id":"302","date_published":"2018-05-29T00:00:00Z","external_id":{"isi":["000517098700015"]},"year":"2018","title":"Simple proofs of sequential work","oa_version":"Submitted Version","publication_status":"published","abstract":[{"lang":"eng","text":"At ITCS 2013, Mahmoody, Moran and Vadhan [MMV13] introduce and construct publicly verifiable proofs of sequential work, which is a protocol for proving that one spent sequential computational work related to some statement. The original motivation for such proofs included non-interactive time-stamping and universally verifiable CPU benchmarks. A more recent application, and our main motivation, are blockchain designs, where proofs of sequential work can be used – in combination with proofs of space – as a more ecological and economical substitute for proofs of work which are currently used to secure Bitcoin and other cryptocurrencies. The construction proposed by [MMV13] is based on a hash function and can be proven secure in the random oracle model, or assuming inherently sequential hash-functions, which is a new standard model assumption introduced in their work. In a proof of sequential work, a prover gets a “statement” χ, a time parameter N and access to a hash-function H, which for the security proof is modelled as a random oracle. Correctness requires that an honest prover can make a verifier accept making only N queries to H, while soundness requires that any prover who makes the verifier accept must have made (almost) N sequential queries to H. Thus a solution constitutes a proof that N time passed since χ was received. Solutions must be publicly verifiable in time at most polylogarithmic in N. The construction of [MMV13] is based on “depth-robust” graphs, and as a consequence has rather poor concrete parameters. But the major drawback is that the prover needs not just N time, but also N space to compute a proof. In this work we propose a proof of sequential work which is much simpler, more efficient and achieves much better concrete bounds. Most importantly, the space required can be as small as log (N) (but we get better soundness using slightly more memory than that). An open problem stated by [MMV13] that our construction does not solve either is achieving a “unique” proof, where even a cheating prover can only generate a single accepting proof. This property would be extremely useful for applications to blockchains."}],"page":"451 - 467","publist_id":"7579","day":"29","doi":"10.1007/978-3-319-78375-8_15","conference":{"end_date":"2018-05-03","start_date":"2018-04-29","location":"Tel Aviv, Israel","name":"Eurocrypt: Advances in Cryptology"},"isi":1,"department":[{"_id":"KrPi"}],"alternative_title":["LNCS"],"scopus_import":"1","status":"public","oa":1,"author":[{"last_name":"Cohen","first_name":"Bram","full_name":"Cohen, Bram"},{"orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","last_name":"Pietrzak","full_name":"Pietrzak, Krzysztof Z","first_name":"Krzysztof Z"}],"project":[{"call_identifier":"H2020","name":"Teaching Old Crypto New Tricks","grant_number":"682815","_id":"258AA5B2-B435-11E9-9278-68D0E5697425"}],"date_updated":"2025-04-14T07:22:06Z","citation":{"apa":"Cohen, B., & Pietrzak, K. Z. (2018). Simple proofs of sequential work (Vol. 10821, pp. 451–467). Presented at the Eurocrypt: Advances in Cryptology, Tel Aviv, Israel: Springer. https://doi.org/10.1007/978-3-319-78375-8_15","short":"B. Cohen, K.Z. Pietrzak, in:, Springer, 2018, pp. 451–467.","ista":"Cohen B, Pietrzak KZ. 2018. Simple proofs of sequential work. Eurocrypt: Advances in Cryptology, LNCS, vol. 10821, 451–467.","ieee":"B. Cohen and K. Z. Pietrzak, “Simple proofs of sequential work,” presented at the Eurocrypt: Advances in Cryptology, Tel Aviv, Israel, 2018, vol. 10821, pp. 451–467.","chicago":"Cohen, Bram, and Krzysztof Z Pietrzak. “Simple Proofs of Sequential Work,” 10821:451–67. Springer, 2018. https://doi.org/10.1007/978-3-319-78375-8_15.","mla":"Cohen, Bram, and Krzysztof Z. Pietrzak. Simple Proofs of Sequential Work. Vol. 10821, Springer, 2018, pp. 451–67, doi:10.1007/978-3-319-78375-8_15.","ama":"Cohen B, Pietrzak KZ. Simple proofs of sequential work. In: Vol 10821. Springer; 2018:451-467. doi:10.1007/978-3-319-78375-8_15"},"publisher":"Springer","quality_controlled":"1","ec_funded":1},{"status":"public","_id":"124","publication":"Geochimica et Cosmochimica Acta","date_published":"2018-02-15T00:00:00Z","year":"2018","quality_controlled":"1","title":"The retention of dust in protoplanetary disks: evidence from agglomeration olivine chondrules from the outer solar system","date_updated":"2021-01-12T06:49:19Z","author":[{"full_name":"Waitukaitis, Scott R","first_name":"Scott R","orcid":"0000-0002-2299-3176","id":"3A1FFC16-F248-11E8-B48F-1D18A9856A87","last_name":"Waitukaitis"},{"first_name":"Devin","full_name":"Schrader, Devin","last_name":"Schrader"},{"last_name":"Nagashima","first_name":"Kazuhide","full_name":"Nagashima, Kazuhide"},{"last_name":"Davidson","first_name":"Jemma","full_name":"Davidson, Jemma"},{"last_name":"Mccoy","first_name":"Timothy","full_name":"Mccoy, Timothy"},{"last_name":"Conolly Jr","first_name":"Harold","full_name":"Conolly Jr, Harold"},{"first_name":"Dante","full_name":"Lauretta, Dante","last_name":"Lauretta"}],"publisher":"Elsevier","citation":{"ama":"Waitukaitis SR, Schrader D, Nagashima K, et al. The retention of dust in protoplanetary disks: evidence from agglomeration olivine chondrules from the outer solar system. Geochimica et Cosmochimica Acta. 2018;223:405-421. doi:10.1016/j.gca.2017.12.014","mla":"Waitukaitis, Scott R., et al. “The Retention of Dust in Protoplanetary Disks: Evidence from Agglomeration Olivine Chondrules from the Outer Solar System.” Geochimica et Cosmochimica Acta, vol. 223, Elsevier, 2018, pp. 405–21, doi:10.1016/j.gca.2017.12.014.","ista":"Waitukaitis SR, Schrader D, Nagashima K, Davidson J, Mccoy T, Conolly Jr H, Lauretta D. 2018. The retention of dust in protoplanetary disks: evidence from agglomeration olivine chondrules from the outer solar system. Geochimica et Cosmochimica Acta. 223, 405–421.","ieee":"S. R. Waitukaitis et al., “The retention of dust in protoplanetary disks: evidence from agglomeration olivine chondrules from the outer solar system,” Geochimica et Cosmochimica Acta, vol. 223. Elsevier, pp. 405–421, 2018.","chicago":"Waitukaitis, Scott R, Devin Schrader, Kazuhide Nagashima, Jemma Davidson, Timothy Mccoy, Harold Conolly Jr, and Dante Lauretta. “The Retention of Dust in Protoplanetary Disks: Evidence from Agglomeration Olivine Chondrules from the Outer Solar System.” Geochimica et Cosmochimica Acta. Elsevier, 2018. https://doi.org/10.1016/j.gca.2017.12.014.","apa":"Waitukaitis, S. R., Schrader, D., Nagashima, K., Davidson, J., Mccoy, T., Conolly Jr, H., & Lauretta, D. (2018). The retention of dust in protoplanetary disks: evidence from agglomeration olivine chondrules from the outer solar system. Geochimica et Cosmochimica Acta. Elsevier. https://doi.org/10.1016/j.gca.2017.12.014","short":"S.R. Waitukaitis, D. Schrader, K. Nagashima, J. Davidson, T. Mccoy, H. Conolly Jr, D. Lauretta, Geochimica et Cosmochimica Acta 223 (2018) 405–421."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","abstract":[{"text":"By investigating the in situ chemical and O-isotope compositions of olivine in lightly sintered dust agglomerates from the early Solar System, we constrain their origins and the retention of dust in the protoplanetary disk. The grain sizes of silicates in these agglomeratic olivine (AO) chondrules indicate that the grain sizes of chondrule precursors in the Renazzo-like carbonaceous (CR) chondrites ranged from <1 to 80 µm. We infer this grain size range to be equivalent to the size range for dust in the early Solar System. AO chondrules may contain, but are not solely composed of, recycled fragments of earlier formed chondrules. They also contain 16O-rich olivine related to amoeboid olivine aggregates and represent the best record of chondrule-precursor materials. AO chondrules contain one or more large grains, sometimes similar to FeO-poor (type I) and/or FeO-rich (type II) chondrules, while others contain a type II chondrule core. These morphologies are consistent with particle agglomeration by electrostatic charging of grains during collision, a process that may explain solid agglomeration in the protoplanetary disk in the micrometer size regime. The petrographic, isotopic, and chemical compositions of AO chondrules are consistent with chondrule formation by large-scale shocks, bow shocks, and current sheets. The petrographic, isotopic, and chemical similarities between AO chondrules in CR chondrites and chondrule-like objects from comet 81P/Wild 2 indicate that comets contain AO chondrules. We infer that these AO chondrules likely formed in the inner Solar System and migrated to the comet forming region at least 3 Ma after the formation of the first Solar System solids. Observations made in this study imply that the protoplanetary disk retained a dusty disk at least ∼3.7 Ma after the formation of the first Solar System solids, longer than half of the dusty accretion disks observed around other stars.","lang":"eng"}],"page":"405 - 421","month":"02","type":"journal_article","oa_version":"None","date_created":"2018-12-11T11:44:45Z","volume":223,"language":[{"iso":"eng"}],"extern":"1","intvolume":" 223","day":"15","publist_id":"7930","doi":"10.1016/j.gca.2017.12.014"},{"date_updated":"2026-05-05T07:24:51Z","author":[{"last_name":"Remez","full_name":"Remez, Roei","first_name":"Roei"},{"last_name":"Shapira","full_name":"Shapira, Niv","first_name":"Niv"},{"last_name":"Roques-Carmes","id":"e2e68fc9-6505-11ef-a541-eb4e72cc3e82","first_name":"Charles","full_name":"Roques-Carmes, Charles"},{"full_name":"Tirole, Romain","first_name":"Romain","last_name":"Tirole"},{"last_name":"Yang","first_name":"Yi","full_name":"Yang, Yi"},{"last_name":"Lereah","full_name":"Lereah, Yossi","first_name":"Yossi"},{"last_name":"Soljačić","first_name":"Marin","full_name":"Soljačić, Marin"},{"last_name":"Kaminer","full_name":"Kaminer, Ido","first_name":"Ido"},{"full_name":"Arie, Ady","first_name":"Ady","last_name":"Arie"}],"publisher":"Optica Publishing Group","citation":{"apa":"Remez, R., Shapira, N., Roques-Carmes, C., Tirole, R., Yang, Y., Lereah, Y., … Arie, A. (2018). Spectral and spatial shaping of Smith-Purcell radiation. In Conference on Lasers and Electro-Optics. San Jose, CA, United States: Optica Publishing Group. https://doi.org/10.1364/cleo_qels.2018.fw4h.3","short":"R. Remez, N. Shapira, C. Roques-Carmes, R. Tirole, Y. Yang, Y. Lereah, M. Soljačić, I. Kaminer, A. Arie, in:, Conference on Lasers and Electro-Optics, Optica Publishing Group, 2018.","chicago":"Remez, Roei, Niv Shapira, Charles Roques-Carmes, Romain Tirole, Yi Yang, Yossi Lereah, Marin Soljačić, Ido Kaminer, and Ady Arie. “Spectral and Spatial Shaping of Smith-Purcell Radiation.” In Conference on Lasers and Electro-Optics. Optica Publishing Group, 2018. https://doi.org/10.1364/cleo_qels.2018.fw4h.3.","ieee":"R. Remez et al., “Spectral and spatial shaping of Smith-Purcell radiation,” in Conference on Lasers and Electro-Optics, San Jose, CA, United States, 2018.","ista":"Remez R, Shapira N, Roques-Carmes C, Tirole R, Yang Y, Lereah Y, Soljačić M, Kaminer I, Arie A. 2018. Spectral and spatial shaping of Smith-Purcell radiation. Conference on Lasers and Electro-Optics. CLEO: Fundamental Science, FW4H.3.","mla":"Remez, Roei, et al. “Spectral and Spatial Shaping of Smith-Purcell Radiation.” Conference on Lasers and Electro-Optics, FW4H.3, Optica Publishing Group, 2018, doi:10.1364/cleo_qels.2018.fw4h.3.","ama":"Remez R, Shapira N, Roques-Carmes C, et al. Spectral and spatial shaping of Smith-Purcell radiation. In: Conference on Lasers and Electro-Optics. Optica Publishing Group; 2018. doi:10.1364/cleo_qels.2018.fw4h.3"},"quality_controlled":"1","scopus_import":"1","publication":"Conference on Lasers and Electro-Optics","publication_identifier":{"eisbn":["9781943580422"],"issnl":["2162-2701"]},"OA_type":"green","status":"public","oa":1,"day":"01","doi":"10.1364/cleo_qels.2018.fw4h.3","article_number":"FW4H.3","conference":{"name":"CLEO: Fundamental Science","location":"San Jose, CA, United States","start_date":"2018-05-13","end_date":"2018-05-18"},"extern":"1","oa_version":"Preprint","publication_status":"published","ddc":["530"],"abstract":[{"lang":"eng","text":"The Smith-Purcell effect is observed when an electron beam passes in the vicinity of a periodic structure. We propose a method to shape the spatial and spectral far-field radiation using complex periodic and aperiodic gratings."}],"external_id":{"arxiv":["1710.03719"]},"year":"2018","title":"Spectral and spatial shaping of Smith-Purcell radiation","arxiv":1,"_id":"21619","date_published":"2018-06-01T00:00:00Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1710.03719","open_access":"1"}],"OA_place":"repository","language":[{"iso":"eng"}],"type":"conference","date_created":"2026-03-30T12:22:48Z","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"06"},{"scopus_import":"1","publication":"Astronomy & Astrophysics","oa":1,"publication_identifier":{"issn":["0004-6361"],"eissn":["1432-0746"]},"status":"public","publisher":"EDP Sciences","citation":{"mla":"Schootemeijer, A., et al. “Clues about the Scarcity of Stripped-Envelope Stars from the Evolutionary State of the SdO+Be Binary System φ Persei.” Astronomy & Astrophysics, vol. 615, A30, EDP Sciences, 2018, doi:10.1051/0004-6361/201731194.","ama":"Schootemeijer A, Götberg YLL, de Mink SE, Gies D, Zapartas E. Clues about the scarcity of stripped-envelope stars from the evolutionary state of the sdO+Be binary system φ Persei. Astronomy & Astrophysics. 2018;615. doi:10.1051/0004-6361/201731194","short":"A. Schootemeijer, Y.L.L. Götberg, S.E. de Mink, D. Gies, E. Zapartas, Astronomy & Astrophysics 615 (2018).","apa":"Schootemeijer, A., Götberg, Y. L. L., de Mink, S. E., Gies, D., & Zapartas, E. (2018). Clues about the scarcity of stripped-envelope stars from the evolutionary state of the sdO+Be binary system φ Persei. Astronomy & Astrophysics. EDP Sciences. https://doi.org/10.1051/0004-6361/201731194","ieee":"A. Schootemeijer, Y. L. L. Götberg, S. E. de Mink, D. Gies, and E. Zapartas, “Clues about the scarcity of stripped-envelope stars from the evolutionary state of the sdO+Be binary system φ Persei,” Astronomy & Astrophysics, vol. 615. EDP Sciences, 2018.","ista":"Schootemeijer A, Götberg YLL, de Mink SE, Gies D, Zapartas E. 2018. Clues about the scarcity of stripped-envelope stars from the evolutionary state of the sdO+Be binary system φ Persei. Astronomy & Astrophysics. 615, A30.","chicago":"Schootemeijer, A., Ylva Louise Linsdotter Götberg, S. E. de Mink, D. Gies, and E. Zapartas. “Clues about the Scarcity of Stripped-Envelope Stars from the Evolutionary State of the SdO+Be Binary System φ Persei.” Astronomy & Astrophysics. EDP Sciences, 2018. https://doi.org/10.1051/0004-6361/201731194."},"date_updated":"2023-08-09T12:22:52Z","author":[{"last_name":"Schootemeijer","full_name":"Schootemeijer, A.","first_name":"A."},{"first_name":"Ylva Louise Linsdotter","full_name":"Götberg, Ylva Louise Linsdotter","last_name":"Götberg","id":"d0648d0c-0f64-11ee-a2e0-dd0faa2e4f7d","orcid":"0000-0002-6960-6911"},{"last_name":"de Mink","first_name":"S. E.","full_name":"de Mink, S. E."},{"last_name":"Gies","first_name":"D.","full_name":"Gies, D."},{"first_name":"E.","full_name":"Zapartas, E.","last_name":"Zapartas"}],"quality_controlled":"1","oa_version":"Published Version","abstract":[{"lang":"eng","text":"Stripped-envelope stars form in binary systems after losing mass through Roche-lobe overflow. They bear astrophysical significance as sources of UV and ionizing radiation in older stellar populations and, if sufficiently massive, as stripped supernova progenitors. Binary evolutionary models predict that they are common, but only a handful of subdwarfs with B-type companions are known. The question is whether a large population of such systems has evaded detection as a result of biases, or whether the model predictions are wrong. We reanalyze the well-studied post-interaction binary φ Persei. Recently, new data have improved the orbital solution of the system, which contains an ~1.2M⊙ stripped-envelope star and a rapidly rotating ~9.6M⊙ Be star. We compare with an extensive grid of evolutionary models using a Bayesian approach and constrain the initial masses of the progenitor to 7.2 ± 0.4M⊙ for the stripped star and 3.8 ± 0.4M⊙ for the Be star. The system must have evolved through near-conservative mass transfer. These findings are consistent with earlier studies. The age we obtain, 57 ± 9 Myr, is in excellent agreement with the age of the α Persei cluster. We note that neither star was initially massive enough to produce a core-collapse supernova, but mass exchange pushed the Be star above the mass threshold. We find that the subdwarf is overluminous for its mass by almost an order of magnitude, compared to the expectations for a helium core burning star. We can only reconcile this if the subdwarf resides in a late phase of helium shell burning, which lasts only 2–3% of the total lifetime as a subdwarf. Assuming continuous star formation implies that up to ~50 less evolved, dimmer subdwarfs exist for each system similar to φ Persei, but have evaded detection so far. Our findings can be interpreted as a strong indication that a substantial population of stripped-envelope stars indeed exists, but has so far evaded detection because of observational biases and lack of large-scale systematic searches."}],"publication_status":"published","keyword":["Space and Planetary Science","Astronomy and Astrophysics"],"doi":"10.1051/0004-6361/201731194","article_number":"A30","day":"06","extern":"1","date_published":"2018-07-06T00:00:00Z","_id":"13473","external_id":{"arxiv":["1803.02379"]},"title":"Clues about the scarcity of stripped-envelope stars from the evolutionary state of the sdO+Be binary system φ Persei","arxiv":1,"year":"2018","date_created":"2023-08-03T10:14:37Z","type":"journal_article","month":"07","article_type":"original","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://doi.org/10.1051/0004-6361/201731194","open_access":"1"}],"intvolume":" 615","language":[{"iso":"eng"}],"volume":615},{"date_published":"2018-07-18T00:00:00Z","_id":"140","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Space-time interpolants","year":"2018","external_id":{"isi":["000491481600025"]},"file_date_updated":"2020-07-14T12:44:50Z","month":"07","file":[{"file_name":"IST-2018-1010-v1+1_space-time_interpolants.pdf","relation":"main_file","date_updated":"2020-07-14T12:44:50Z","file_id":"5310","checksum":"6dca832f575d6b3f0ea9dff56f579142","content_type":"application/pdf","file_size":563710,"access_level":"open_access","date_created":"2018-12-12T10:17:53Z","creator":"system"}],"article_processing_charge":"No","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","date_created":"2018-12-11T11:44:50Z","type":"conference","intvolume":" 10981","language":[{"iso":"eng"}],"volume":10981,"oa":1,"publication_identifier":{"issn":["0302-9743"]},"status":"public","scopus_import":"1","alternative_title":["LNCS"],"quality_controlled":"1","publisher":"Springer","related_material":{"record":[{"relation":"dissertation_contains","id":"6894","status":"public"}]},"citation":{"ista":"Frehse G, Giacobbe M, Henzinger TA. 2018. Space-time interpolants. CAV: Computer Aided Verification, LNCS, vol. 10981, 468–486.","chicago":"Frehse, Goran, Mirco Giacobbe, and Thomas A Henzinger. “Space-Time Interpolants,” 10981:468–86. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_25.","ieee":"G. Frehse, M. Giacobbe, and T. A. Henzinger, “Space-time interpolants,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10981, pp. 468–486.","short":"G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2018, pp. 468–486.","apa":"Frehse, G., Giacobbe, M., & Henzinger, T. A. (2018). Space-time interpolants (Vol. 10981, pp. 468–486). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96145-3_25","ama":"Frehse G, Giacobbe M, Henzinger TA. Space-time interpolants. In: Vol 10981. Springer; 2018:468-486. doi:10.1007/978-3-319-96145-3_25","mla":"Frehse, Goran, et al. Space-Time Interpolants. Vol. 10981, Springer, 2018, pp. 468–86, doi:10.1007/978-3-319-96145-3_25."},"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"author":[{"full_name":"Frehse, Goran","first_name":"Goran","last_name":"Frehse"},{"orcid":"0000-0001-8180-0904","last_name":"Giacobbe","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","full_name":"Giacobbe, Mirco","first_name":"Mirco"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"date_updated":"2026-04-16T09:55:04Z","pubrep_id":"1010","page":"468 - 486","abstract":[{"lang":"eng","text":"Reachability analysis is difficult for hybrid automata with affine differential equations, because the reach set needs to be approximated. Promising abstraction techniques usually employ interval methods or template polyhedra. Interval methods account for dense time and guarantee soundness, and there are interval-based tools that overapproximate affine flowpipes. But interval methods impose bounded and rigid shapes, which make refinement expensive and fixpoint detection difficult. Template polyhedra, on the other hand, can be adapted flexibly and can be unbounded, but sound template refinement for unbounded reachability analysis has been implemented only for systems with piecewise constant dynamics. We capitalize on the advantages of both techniques, combining interval arithmetic and template polyhedra, using the former to abstract time and the latter to abstract space. During a CEGAR loop, whenever a spurious error trajectory is found, we compute additional space constraints and split time intervals, and use these space-time interpolants to eliminate the counterexample. Space-time interpolation offers a lazy, flexible framework for increasing precision while guaranteeing soundness, both for error avoidance and fixpoint detection. To the best of out knowledge, this is the first abstraction refinement scheme for the reachability analysis over unbounded and dense time of affine hybrid systems, which is both sound and automatic. We demonstrate the effectiveness of our algorithm with several benchmark examples, which cannot be handled by other tools."}],"publication_status":"published","ddc":["005"],"oa_version":"Published Version","department":[{"_id":"ToHe"}],"isi":1,"conference":{"name":"CAV: Computer Aided Verification","location":"Oxford, United Kingdom","end_date":"2018-07-17","start_date":"2018-07-14"},"doi":"10.1007/978-3-319-96145-3_25","day":"18","has_accepted_license":"1","publist_id":"7783"},{"conference":{"location":"Oxford, United Kingdom","name":"CAV: Computer Aided Verification","start_date":"2018-07-14","end_date":"2018-07-17"},"department":[{"_id":"KrCh"}],"isi":1,"has_accepted_license":"1","day":"18","publist_id":"7782","doi":"10.1007/978-3-319-96142-2_13","publication_status":"published","ddc":["000"],"page":"178-197","abstract":[{"text":"Given a model and a specification, the fundamental model-checking problem asks for algorithmic verification of whether the model satisfies the specification. We consider graphs and Markov decision processes (MDPs), which are fundamental models for reactive systems. One of the very basic specifications that arise in verification of reactive systems is the strong fairness (aka Streett) objective. Given different types of requests and corresponding grants, the objective requires that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All ω -regular objectives can be expressed as Streett objectives and hence they are canonical in verification. To handle the state-space explosion, symbolic algorithms are required that operate on a succinct implicit representation of the system rather than explicitly accessing the system. While explicit algorithms for graphs and MDPs with Streett objectives have been widely studied, there has been no improvement of the basic symbolic algorithms. The worst-case numbers of symbolic steps required for the basic symbolic algorithms are as follows: quadratic for graphs and cubic for MDPs. In this work we present the first sub-quadratic symbolic algorithm for graphs with Streett objectives, and our algorithm is sub-quadratic even for MDPs. Based on our algorithmic insights we present an implementation of the new symbolic approach and show that it improves the existing approach on several academic benchmark examples.","lang":"eng"}],"oa_version":"Published Version","ec_funded":1,"quality_controlled":"1","date_updated":"2026-04-08T07:00:31Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H"},{"first_name":"Veronika","full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer"},{"last_name":"Oraee","first_name":"Simin","full_name":"Oraee, Simin"},{"orcid":"0000-0001-9036-063X","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","full_name":"Toman, Viktor"}],"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"publisher":"Springer","citation":{"short":"K. Chatterjee, M. Henzinger, V. Loitzenbauer, S. Oraee, V. Toman, in:, Springer, 2018, pp. 178–197.","apa":"Chatterjee, K., Henzinger, M., Loitzenbauer, V., Oraee, S., & Toman, V. (2018). Symbolic algorithms for graphs and Markov decision processes with fairness objectives (Vol. 10982, pp. 178–197). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96142-2_13","ista":"Chatterjee K, Henzinger M, Loitzenbauer V, Oraee S, Toman V. 2018. Symbolic algorithms for graphs and Markov decision processes with fairness objectives. CAV: Computer Aided Verification, LNCS, vol. 10982, 178–197.","ieee":"K. Chatterjee, M. Henzinger, V. Loitzenbauer, S. Oraee, and V. Toman, “Symbolic algorithms for graphs and Markov decision processes with fairness objectives,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10982, pp. 178–197.","chicago":"Chatterjee, Krishnendu, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee, and Viktor Toman. “Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives,” 10982:178–97. Springer, 2018. https://doi.org/10.1007/978-3-319-96142-2_13.","mla":"Chatterjee, Krishnendu, et al. Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives. Vol. 10982, Springer, 2018, pp. 178–97, doi:10.1007/978-3-319-96142-2_13.","ama":"Chatterjee K, Henzinger M, Loitzenbauer V, Oraee S, Toman V. Symbolic algorithms for graphs and Markov decision processes with fairness objectives. In: Vol 10982. Springer; 2018:178-197. doi:10.1007/978-3-319-96142-2_13"},"related_material":{"record":[{"relation":"dissertation_contains","id":"10199","status":"public"}]},"status":"public","acknowledgement":"Acknowledgements. K. C. and M. H. are partially supported by the Vienna Science and Technology Fund (WWTF) grant ICT15-003. K. C. is partially supported by the Austrian Science Fund (FWF): S11407-N23 (RiSE/SHiNE), and an ERC Start Grant (279307: Graph Games). V. T. is partially supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie Grant Agreement No. 665385.","oa":1,"scopus_import":"1","alternative_title":["LNCS"],"volume":10982,"language":[{"iso":"eng"}],"intvolume":" 10982","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","file":[{"content_type":"application/pdf","file_size":675606,"access_level":"open_access","date_created":"2018-12-18T08:52:38Z","creator":"dernst","checksum":"1a6ffa4febe8bb8ac28be3adb3eafebc","relation":"main_file","date_updated":"2020-07-14T12:44:53Z","file_id":"5737","file_name":"2018_LNCS_Chatterjee.pdf"}],"month":"07","type":"conference","date_created":"2018-12-11T11:44:51Z","year":"2018","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Symbolic algorithms for graphs and Markov decision processes with fairness objectives","file_date_updated":"2020-07-14T12:44:53Z","external_id":{"isi":["000491469700013"]},"_id":"141","date_published":"2018-07-18T00:00:00Z"},{"_id":"142","date_published":"2018-07-18T00:00:00Z","year":"2018","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Reachable set over-approximation for nonlinear systems using piecewise barrier tubes","file_date_updated":"2020-07-14T12:44:53Z","external_id":{"isi":["000491481600024"]},"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"07","file":[{"file_name":"2018_LNCS_Kong.pdf","file_id":"5718","relation":"main_file","date_updated":"2020-07-14T12:44:53Z","checksum":"fd95e8026deacef3dc752a733bb9355f","creator":"dernst","date_created":"2018-12-17T15:57:06Z","access_level":"open_access","content_type":"application/pdf","file_size":5591566}],"type":"conference","date_created":"2018-12-11T11:44:51Z","volume":10981,"language":[{"iso":"eng"}],"intvolume":" 10981","status":"public","acknowledgement":"Austrian Science Fund FWF: S11402-N23, S11405-N23, Z211-N32","oa":1,"scopus_import":"1","alternative_title":["LNCS"],"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"author":[{"orcid":"0000-0002-3066-6941","last_name":"Kong","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","full_name":"Kong, Hui","first_name":"Hui"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"date_updated":"2025-04-15T06:25:58Z","publisher":"Springer","citation":{"ama":"Kong H, Bartocci E, Henzinger TA. Reachable set over-approximation for nonlinear systems using piecewise barrier tubes. In: Vol 10981. Springer; 2018:449-467. doi:10.1007/978-3-319-96145-3_24","mla":"Kong, Hui, et al. Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes. Vol. 10981, Springer, 2018, pp. 449–67, doi:10.1007/978-3-319-96145-3_24.","ista":"Kong H, Bartocci E, Henzinger TA. 2018. Reachable set over-approximation for nonlinear systems using piecewise barrier tubes. CAV: Computer Aided Verification, LNCS, vol. 10981, 449–467.","ieee":"H. Kong, E. Bartocci, and T. A. Henzinger, “Reachable set over-approximation for nonlinear systems using piecewise barrier tubes,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10981, pp. 449–467.","chicago":"Kong, Hui, Ezio Bartocci, and Thomas A Henzinger. “Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes,” 10981:449–67. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_24.","apa":"Kong, H., Bartocci, E., & Henzinger, T. A. (2018). Reachable set over-approximation for nonlinear systems using piecewise barrier tubes (Vol. 10981, pp. 449–467). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96145-3_24","short":"H. Kong, E. Bartocci, T.A. Henzinger, in:, Springer, 2018, pp. 449–467."},"publication_status":"published","ddc":["000"],"page":"449 - 467","abstract":[{"text":"We address the problem of analyzing the reachable set of a polynomial nonlinear continuous system by over-approximating the flowpipe of its dynamics. The common approach to tackle this problem is to perform a numerical integration over a given time horizon based on Taylor expansion and interval arithmetic. However, this method results to be very conservative when there is a large difference in speed between trajectories as time progresses. In this paper, we propose to use combinations of barrier functions, which we call piecewise barrier tube (PBT), to over-approximate flowpipe. The basic idea of PBT is that for each segment of a flowpipe, a coarse box which is big enough to contain the segment is constructed using sampled simulation and then in the box we compute by linear programming a set of barrier functions (called barrier tube or BT for short) which work together to form a tube surrounding the flowpipe. The benefit of using PBT is that (1) BT is independent of time and hence can avoid being stretched and deformed by time; and (2) a small number of BTs can form a tight over-approximation for the flowpipe, which means that the computation required to decide whether the BTs intersect the unsafe set can be reduced significantly. We implemented a prototype called PBTS in C++. Experiments on some benchmark systems show that our approach is effective.","lang":"eng"}],"oa_version":"Published Version","conference":{"name":"CAV: Computer Aided Verification","location":"Oxford, United Kingdom","end_date":"2018-07-17","start_date":"2018-07-14"},"department":[{"_id":"ToHe"}],"isi":1,"publist_id":"7781","day":"18","has_accepted_license":"1","doi":"10.1007/978-3-319-96145-3_24"},{"author":[{"first_name":"Thomas","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","orcid":"0000-0001-5199-3143"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ege","full_name":"Saraç, Ege","last_name":"Saraç"}],"date_updated":"2023-09-08T11:49:13Z","publisher":"IEEE","citation":{"ama":"Ferrere T, Henzinger TA, Saraç E. A theory of register monitors. In: Vol Part F138033. IEEE; 2018:394-403. doi:10.1145/3209108.3209194","mla":"Ferrere, Thomas, et al. A Theory of Register Monitors. Vol. Part F138033, IEEE, 2018, pp. 394–403, doi:10.1145/3209108.3209194.","chicago":"Ferrere, Thomas, Thomas A Henzinger, and Ege Saraç. “A Theory of Register Monitors,” Part F138033:394–403. IEEE, 2018. https://doi.org/10.1145/3209108.3209194.","ieee":"T. Ferrere, T. A. Henzinger, and E. Saraç, “A theory of register monitors,” presented at the LICS: Logic in Computer Science, Oxford, UK, 2018, vol. Part F138033, pp. 394–403.","ista":"Ferrere T, Henzinger TA, Saraç E. 2018. A theory of register monitors. LICS: Logic in Computer Science, ACM/IEEE Symposium on Logic in Computer Science, vol. Part F138033, 394–403.","apa":"Ferrere, T., Henzinger, T. A., & Saraç, E. (2018). A theory of register monitors (Vol. Part F138033, pp. 394–403). Presented at the LICS: Logic in Computer Science, Oxford, UK: IEEE. https://doi.org/10.1145/3209108.3209194","short":"T. Ferrere, T.A. Henzinger, E. Saraç, in:, IEEE, 2018, pp. 394–403."},"external_id":{"isi":["000545262800041"]},"quality_controlled":"1","year":"2018","title":"A theory of register monitors","_id":"144","scopus_import":"1","date_published":"2018-07-09T00:00:00Z","alternative_title":["ACM/IEEE Symposium on Logic in Computer Science"],"status":"public","day":"09","publist_id":"7779","doi":"10.1145/3209108.3209194","volume":"Part F138033","conference":{"start_date":"2018-07-09","end_date":"2018-07-12","location":"Oxford, UK","name":"LICS: Logic in Computer Science"},"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"isi":1,"type":"conference","date_created":"2018-12-11T11:44:52Z","oa_version":"None","publication_status":"published","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","page":"394 - 403","month":"07","abstract":[{"lang":"eng","text":"The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these register monitors according to the number k of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every k 1, monitors with k + 1 counters (with instruction set 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety -languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are as expressive as real-time Turing machines."}]},{"date_created":"2018-12-11T11:44:53Z","type":"dissertation","file":[{"relation":"main_file","date_updated":"2020-07-14T12:44:57Z","file_id":"6241","file_name":"2018_thesis_Alt.pdf","content_type":"application/pdf","file_size":5801709,"date_created":"2019-04-08T13:55:20Z","access_level":"open_access","creator":"dernst","checksum":"d4dad55a7513f345706aaaba90cb1bb8"},{"checksum":"d73fcf46300dce74c403f2b491148ab4","creator":"dernst","date_created":"2019-04-08T13:55:20Z","access_level":"closed","content_type":"application/zip","file_size":3802059,"file_name":"2018_thesis_Alt_source.zip","file_id":"6242","relation":"source_file","date_updated":"2020-07-14T12:44:57Z"}],"month":"07","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","OA_place":"publisher","degree_awarded":"PhD","language":[{"iso":"eng"}],"date_published":"2018-07-12T00:00:00Z","_id":"149","file_date_updated":"2020-07-14T12:44:57Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Dyson equation and eigenvalue statistics of random matrices","year":"2018","oa_version":"Published Version","corr_author":"1","abstract":[{"text":"The eigenvalue density of many large random matrices is well approximated by a deterministic measure, the self-consistent density of states. In the present work, we show this behaviour for several classes of random matrices. In fact, we establish that, in each of these classes, the self-consistent density of states approximates the eigenvalue density of the random matrix on all scales slightly above the typical eigenvalue spacing. For large classes of random matrices, the self-consistent density of states exhibits several universal features. We prove that, under suitable assumptions, random Gram matrices and Hermitian random matrices with decaying correlations have a 1/3-Hölder continuous self-consistent density of states ρ on R, which is analytic, where it is positive, and has either a square root edge or a cubic root cusp, where it vanishes. We, thus, extend the validity of the corresponding result for Wigner-type matrices from [4, 5, 7]. We show that ρ is determined as the inverse Stieltjes transform of the normalized trace of the unique solution m(z) to the Dyson equation −m(z) −1 = z − a + S[m(z)] on C N×N with the constraint Im m(z) ≥ 0. Here, z lies in the complex upper half-plane, a is a self-adjoint element of C N×N and S is a positivity-preserving operator on C N×N encoding the first two moments of the random matrix. In order to analyze a possible limit of ρ for N → ∞ and address some applications in free probability theory, we also consider the Dyson equation on infinite dimensional von Neumann algebras. We present two applications to random matrices. We first establish that, under certain assumptions, large random matrices with independent entries have a rotationally symmetric self-consistent density of states which is supported on a centered disk in C. Moreover, it is infinitely often differentiable apart from a jump on the boundary of this disk. Second, we show edge universality at all regular (not necessarily extreme) spectral edges for Hermitian random matrices with decaying correlations.","lang":"eng"}],"supervisor":[{"full_name":"Erdös, László","first_name":"László","id":"4DBD5372-F248-11E8-B48F-1D18A9856A87","last_name":"Erdös","orcid":"0000-0001-5366-9603"}],"page":"456","ddc":["515","519"],"publication_status":"published","doi":"10.15479/AT:ISTA:TH_1040","publist_id":"7772","day":"12","has_accepted_license":"1","department":[{"_id":"LaEr"}],"alternative_title":["ISTA Thesis"],"oa":1,"status":"public","publication_identifier":{"issn":["2663-337X"]},"related_material":{"record":[{"relation":"part_of_dissertation","id":"6240","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"6184"},{"relation":"part_of_dissertation","status":"public","id":"566"},{"relation":"part_of_dissertation","status":"public","id":"6183"},{"status":"public","id":"1010","relation":"part_of_dissertation"},{"id":"550","status":"public","relation":"part_of_dissertation"},{"status":"public","id":"1677","relation":"part_of_dissertation"}]},"publisher":"Institute of Science and Technology Austria","citation":{"ieee":"J. Alt, “Dyson equation and eigenvalue statistics of random matrices,” Institute of Science and Technology Austria, 2018.","ista":"Alt J. 2018. Dyson equation and eigenvalue statistics of random matrices. Institute of Science and Technology Austria.","chicago":"Alt, Johannes. “Dyson Equation and Eigenvalue Statistics of Random Matrices.” Institute of Science and Technology Austria, 2018. https://doi.org/10.15479/AT:ISTA:TH_1040.","short":"J. Alt, Dyson Equation and Eigenvalue Statistics of Random Matrices, Institute of Science and Technology Austria, 2018.","apa":"Alt, J. (2018). Dyson equation and eigenvalue statistics of random matrices. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:TH_1040","ama":"Alt J. Dyson equation and eigenvalue statistics of random matrices. 2018. doi:10.15479/AT:ISTA:TH_1040","mla":"Alt, Johannes. Dyson Equation and Eigenvalue Statistics of Random Matrices. Institute of Science and Technology Austria, 2018, doi:10.15479/AT:ISTA:TH_1040."},"pubrep_id":"1040","date_updated":"2026-04-08T14:11:37Z","project":[{"name":"Random matrices, universality and disordered quantum systems","grant_number":"338804","_id":"258DCDE6-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"author":[{"id":"36D3D8B6-F248-11E8-B48F-1D18A9856A87","last_name":"Alt","full_name":"Alt, Johannes","first_name":"Johannes"}],"ec_funded":1},{"quality_controlled":"1","date_updated":"2024-04-08T07:01:20Z","author":[{"full_name":"Santangelo, Andrea","first_name":"Andrea","last_name":"Santangelo"},{"full_name":"Zane, Silvia","first_name":"Silvia","last_name":"Zane"},{"first_name":"Hua","full_name":"Feng, Hua","last_name":"Feng"},{"last_name":"Xu","first_name":"RenXin","full_name":"Xu, RenXin"},{"first_name":"Victor","full_name":"Doroshenko, Victor","last_name":"Doroshenko"},{"last_name":"Bozzo","first_name":"Enrico","full_name":"Bozzo, Enrico"},{"first_name":"Ilaria","full_name":"Caiazzo, Ilaria","orcid":"0000-0002-4770-5388","id":"8ae5b6e7-2a03-11ee-914d-b58ed7a3b47d","last_name":"Caiazzo"},{"full_name":"Zelati, Francesco Coti","first_name":"Francesco Coti","last_name":"Zelati"},{"first_name":"Paolo","full_name":"Esposito, Paolo","last_name":"Esposito"},{"full_name":"González-Caniulef, Denis","first_name":"Denis","last_name":"González-Caniulef"},{"last_name":"Heyl","first_name":"Jeremy","full_name":"Heyl, Jeremy"},{"last_name":"Huppenkothen","first_name":"Daniela","full_name":"Huppenkothen, Daniela"},{"last_name":"Israel","full_name":"Israel, Gianluca","first_name":"Gianluca"},{"last_name":"Li","first_name":"ZhaoSheng","full_name":"Li, ZhaoSheng"},{"last_name":"Lin","first_name":"Lin","full_name":"Lin, Lin"},{"last_name":"Mignani","first_name":"Roberto","full_name":"Mignani, Roberto"},{"first_name":"Nanda","full_name":"Rea, Nanda","last_name":"Rea"},{"full_name":"Orlandini, Mauro","first_name":"Mauro","last_name":"Orlandini"},{"last_name":"Taverna","full_name":"Taverna, Roberto","first_name":"Roberto"},{"first_name":"Hao","full_name":"Tong, Hao","last_name":"Tong"},{"full_name":"Turolla, Roberto","first_name":"Roberto","last_name":"Turolla"},{"full_name":"Baglio, Cristina","first_name":"Cristina","last_name":"Baglio"},{"first_name":"Federico","full_name":"Bernardini, Federico","last_name":"Bernardini"},{"last_name":"Bucciantini","first_name":"Niccolo’","full_name":"Bucciantini, Niccolo’"},{"full_name":"Feroci, Marco","first_name":"Marco","last_name":"Feroci"},{"last_name":"Fürst","full_name":"Fürst, Felix","first_name":"Felix"},{"last_name":"Göğüş","full_name":"Göğüş, Ersin","first_name":"Ersin"},{"last_name":"Güngör","first_name":"Can","full_name":"Güngör, Can"},{"full_name":"Ji, Long","first_name":"Long","last_name":"Ji"},{"last_name":"Lu","full_name":"Lu, FangJun","first_name":"FangJun"},{"first_name":"Antonios","full_name":"Manousakis, Antonios","last_name":"Manousakis"},{"first_name":"Sandro","full_name":"Mereghetti, Sandro","last_name":"Mereghetti"},{"last_name":"Mikusincova","full_name":"Mikusincova, Romana","first_name":"Romana"},{"full_name":"Paul, Biswajit","first_name":"Biswajit","last_name":"Paul"},{"full_name":"Prescod-Weinstein, Chanda","first_name":"Chanda","last_name":"Prescod-Weinstein"},{"first_name":"George","full_name":"Younes, George","last_name":"Younes"},{"last_name":"Tiengo","first_name":"Andrea","full_name":"Tiengo, Andrea"},{"last_name":"Xu","first_name":"YuPeng","full_name":"Xu, YuPeng"},{"last_name":"Watts","first_name":"Anna","full_name":"Watts, Anna"},{"first_name":"Shu","full_name":"Zhang, Shu","last_name":"Zhang"},{"last_name":"Zhan","full_name":"Zhan, Shuang-Nan","first_name":"Shuang-Nan"}],"publisher":"Springer Nature","citation":{"apa":"Santangelo, A., Zane, S., Feng, H., Xu, R., Doroshenko, V., Bozzo, E., … Zhan, S.-N. (2018). Physics and astrophysics of strong magnetic field systems with eXTP. Science China Physics, Mechanics & Astronomy. Springer Nature. https://doi.org/10.1007/s11433-018-9234-3","short":"A. Santangelo, S. Zane, H. Feng, R. Xu, V. Doroshenko, E. Bozzo, I. Caiazzo, F.C. Zelati, P. Esposito, D. González-Caniulef, J. Heyl, D. Huppenkothen, G. Israel, Z. Li, L. Lin, R. Mignani, N. Rea, M. Orlandini, R. Taverna, H. Tong, R. Turolla, C. Baglio, F. Bernardini, N. Bucciantini, M. Feroci, F. Fürst, E. Göğüş, C. Güngör, L. Ji, F. Lu, A. Manousakis, S. Mereghetti, R. Mikusincova, B. Paul, C. Prescod-Weinstein, G. Younes, A. Tiengo, Y. Xu, A. Watts, S. Zhang, S.-N. Zhan, Science China Physics, Mechanics & Astronomy 62 (2018).","chicago":"Santangelo, Andrea, Silvia Zane, Hua Feng, RenXin Xu, Victor Doroshenko, Enrico Bozzo, Ilaria Caiazzo, et al. “Physics and Astrophysics of Strong Magnetic Field Systems with EXTP.” Science China Physics, Mechanics & Astronomy. Springer Nature, 2018. https://doi.org/10.1007/s11433-018-9234-3.","ista":"Santangelo A, Zane S, Feng H, Xu R, Doroshenko V, Bozzo E, Caiazzo I, Zelati FC, Esposito P, González-Caniulef D, Heyl J, Huppenkothen D, Israel G, Li Z, Lin L, Mignani R, Rea N, Orlandini M, Taverna R, Tong H, Turolla R, Baglio C, Bernardini F, Bucciantini N, Feroci M, Fürst F, Göğüş E, Güngör C, Ji L, Lu F, Manousakis A, Mereghetti S, Mikusincova R, Paul B, Prescod-Weinstein C, Younes G, Tiengo A, Xu Y, Watts A, Zhang S, Zhan S-N. 2018. Physics and astrophysics of strong magnetic field systems with eXTP. Science China Physics, Mechanics & Astronomy. 62(2), 29505.","ieee":"A. Santangelo et al., “Physics and astrophysics of strong magnetic field systems with eXTP,” Science China Physics, Mechanics & Astronomy, vol. 62, no. 2. Springer Nature, 2018.","mla":"Santangelo, Andrea, et al. “Physics and Astrophysics of Strong Magnetic Field Systems with EXTP.” Science China Physics, Mechanics & Astronomy, vol. 62, no. 2, 29505, Springer Nature, 2018, doi:10.1007/s11433-018-9234-3.","ama":"Santangelo A, Zane S, Feng H, et al. Physics and astrophysics of strong magnetic field systems with eXTP. Science China Physics, Mechanics & Astronomy. 2018;62(2). doi:10.1007/s11433-018-9234-3"},"status":"public","publication_identifier":{"eissn":["1869-1927"],"issn":["1674-7348"]},"oa":1,"publication":"Science China Physics, Mechanics & Astronomy","scopus_import":"1","extern":"1","day":"08","article_number":"29505","doi":"10.1007/s11433-018-9234-3","keyword":["General Physics and Astronomy"],"publication_status":"published","abstract":[{"lang":"eng","text":"In this paper we present the science potential of the enhanced X-ray Timing and Polarimetry (eXTP) mission for studies of strongly magnetized objects. We will focus on the physics and astrophysics of strongly magnetized objects, namely magnetars, accreting X-ray pulsars, and rotation powered pulsars. We also discuss the science potential of eXTP for QED studies. Developed by an international Consortium led by the Institute of High Energy Physics of the Chinese Academy of Sciences, the eXTP mission is expected to be launched in the mid 2020s."}],"oa_version":"Preprint","year":"2018","arxiv":1,"title":"Physics and astrophysics of strong magnetic field systems with eXTP","external_id":{"arxiv":["1812.04460"]},"_id":"15233","date_published":"2018-10-08T00:00:00Z","volume":62,"language":[{"iso":"eng"}],"intvolume":" 62","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1812.04460"}],"issue":"2","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","month":"10","article_type":"original","type":"journal_article","date_created":"2024-03-26T10:38:05Z"},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Stability of the 2+2 fermionic system with point interactions","year":"2018","external_id":{"isi":["000439639700001"]},"file_date_updated":"2020-07-14T12:45:01Z","date_published":"2018-09-01T00:00:00Z","_id":"154","language":[{"iso":"eng"}],"intvolume":" 21","volume":21,"issue":"3","article_type":"original","file":[{"file_name":"2018_MathPhysics_Moser.pdf","file_id":"5729","date_updated":"2020-07-14T12:45:01Z","relation":"main_file","checksum":"411c4db5700d7297c9cd8ebc5dd29091","date_created":"2018-12-17T16:49:02Z","access_level":"open_access","creator":"dernst","file_size":496973,"content_type":"application/pdf"}],"month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","date_created":"2018-12-11T11:44:55Z","type":"journal_article","quality_controlled":"1","ec_funded":1,"citation":{"ama":"Moser T, Seiringer R. Stability of the 2+2 fermionic system with point interactions. Mathematical Physics Analysis and Geometry. 2018;21(3). doi:10.1007/s11040-018-9275-3","mla":"Moser, Thomas, and Robert Seiringer. “Stability of the 2+2 Fermionic System with Point Interactions.” Mathematical Physics Analysis and Geometry, vol. 21, no. 3, 19, Springer, 2018, doi:10.1007/s11040-018-9275-3.","ista":"Moser T, Seiringer R. 2018. Stability of the 2+2 fermionic system with point interactions. Mathematical Physics Analysis and Geometry. 21(3), 19.","ieee":"T. Moser and R. Seiringer, “Stability of the 2+2 fermionic system with point interactions,” Mathematical Physics Analysis and Geometry, vol. 21, no. 3. Springer, 2018.","chicago":"Moser, Thomas, and Robert Seiringer. “Stability of the 2+2 Fermionic System with Point Interactions.” Mathematical Physics Analysis and Geometry. Springer, 2018. https://doi.org/10.1007/s11040-018-9275-3.","short":"T. Moser, R. Seiringer, Mathematical Physics Analysis and Geometry 21 (2018).","apa":"Moser, T., & Seiringer, R. (2018). Stability of the 2+2 fermionic system with point interactions. Mathematical Physics Analysis and Geometry. Springer. https://doi.org/10.1007/s11040-018-9275-3"},"related_material":{"record":[{"id":"52","status":"public","relation":"dissertation_contains"}]},"publisher":"Springer","author":[{"full_name":"Moser, Thomas","first_name":"Thomas","last_name":"Moser","id":"2B5FC9A4-F248-11E8-B48F-1D18A9856A87"},{"id":"4AFD0470-F248-11E8-B48F-1D18A9856A87","last_name":"Seiringer","orcid":"0000-0002-6781-0521","full_name":"Seiringer, Robert","first_name":"Robert"}],"project":[{"name":"Analysis of quantum many-body systems","_id":"25C6DC12-B435-11E9-9278-68D0E5697425","grant_number":"694227","call_identifier":"H2020"},{"call_identifier":"FWF","grant_number":"P27533_N27","name":"Structure of the Excitation Spectrum for Many-Body Quantum Systems","_id":"25C878CE-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"3AC91DDA-15DF-11EA-824D-93A3E7B544D1","name":"FWF Open Access Fund"}],"date_updated":"2026-04-08T14:12:30Z","acknowledgement":"Open access funding provided by Austrian Science Fund (FWF).","oa":1,"status":"public","publication_identifier":{"eissn":["1572-9656"],"issn":["1385-0172"]},"publication":"Mathematical Physics Analysis and Geometry","scopus_import":"1","isi":1,"department":[{"_id":"RoSe"}],"article_number":"19","doi":"10.1007/s11040-018-9275-3","publist_id":"7767","day":"01","has_accepted_license":"1","abstract":[{"lang":"eng","text":"We give a lower bound on the ground state energy of a system of two fermions of one species interacting with two fermions of another species via point interactions. We show that there is a critical mass ratio m2 ≈ 0.58 such that the system is stable, i.e., the energy is bounded from below, for m∈[m2,m2−1]. So far it was not known whether this 2 + 2 system exhibits a stable region at all or whether the formation of four-body bound states causes an unbounded spectrum for all mass ratios, similar to the Thomas effect. Our result gives further evidence for the stability of the more general N + M system."}],"ddc":["530"],"publication_status":"published","oa_version":"Published Version"},{"file":[{"date_updated":"2020-10-09T06:22:41Z","relation":"main_file","success":1,"file_id":"8637","file_name":"2018_LNCS_Ferrere.pdf","file_size":485576,"content_type":"application/pdf","date_created":"2020-10-09T06:22:41Z","creator":"dernst","access_level":"open_access","checksum":"a045c213c42c445f1889326f8db82a0a"}],"month":"07","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","date_created":"2018-12-11T11:44:55Z","type":"conference","language":[{"iso":"eng"}],"intvolume":" 10951","volume":10951,"date_published":"2018-07-12T00:00:00Z","_id":"156","title":"The compound interest in relaxing punctuality","year":"2018","external_id":{"isi":["000489765800009"]},"file_date_updated":"2020-10-09T06:22:41Z","page":"147 - 164","abstract":[{"text":"Imprecision in timing can sometimes be beneficial: Metric interval temporal logic (MITL), disabling the expression of punctuality constraints, was shown to translate to timed automata, yielding an elementary decision procedure. We show how this principle extends to other forms of dense-time specification using regular expressions. By providing a clean, automaton-based formal framework for non-punctual languages, we are able to recover and extend several results in timed systems. Metric interval regular expressions (MIRE) are introduced, providing regular expressions with non-singular duration constraints. We obtain that MIRE are expressively complete relative to a class of one-clock timed automata, which can be determinized using additional clocks. Metric interval dynamic logic (MIDL) is then defined using MIRE as temporal modalities. We show that MIDL generalizes known extensions of MITL, while translating to timed automata at comparable cost.","lang":"eng"}],"publication_status":"published","ddc":["000"],"oa_version":"Submitted Version","department":[{"_id":"ToHe"}],"isi":1,"conference":{"name":"FM: Formal Methods","location":"Oxford, UK","end_date":"2018-07-17","start_date":"2018-07-15"},"doi":"10.1007/978-3-319-95582-7_9","publist_id":"7765","has_accepted_license":"1","day":"12","oa":1,"status":"public","scopus_import":"1","alternative_title":["LNCS"],"quality_controlled":"1","citation":{"short":"T. Ferrere, in:, Springer, 2018, pp. 147–164.","apa":"Ferrere, T. (2018). The compound interest in relaxing punctuality (Vol. 10951, pp. 147–164). Presented at the FM: Formal Methods, Oxford, UK: Springer. https://doi.org/10.1007/978-3-319-95582-7_9","ieee":"T. Ferrere, “The compound interest in relaxing punctuality,” presented at the FM: Formal Methods, Oxford, UK, 2018, vol. 10951, pp. 147–164.","chicago":"Ferrere, Thomas. “The Compound Interest in Relaxing Punctuality,” 10951:147–64. Springer, 2018. https://doi.org/10.1007/978-3-319-95582-7_9.","ista":"Ferrere T. 2018. The compound interest in relaxing punctuality. FM: Formal Methods, LNCS, vol. 10951, 147–164.","mla":"Ferrere, Thomas. The Compound Interest in Relaxing Punctuality. Vol. 10951, Springer, 2018, pp. 147–64, doi:10.1007/978-3-319-95582-7_9.","ama":"Ferrere T. The compound interest in relaxing punctuality. In: Vol 10951. Springer; 2018:147-164. doi:10.1007/978-3-319-95582-7_9"},"publisher":"Springer","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","last_name":"Ferrere","first_name":"Thomas","full_name":"Ferrere, Thomas"}],"date_updated":"2025-07-10T11:51:10Z","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}]},{"file":[{"checksum":"c64fff560fe5a7532ec10626ad1c215e","content_type":"application/pdf","file_size":1603844,"access_level":"open_access","creator":"dernst","date_created":"2018-12-17T12:52:12Z","file_name":"2018_LNCS_Kragl.pdf","relation":"main_file","date_updated":"2020-07-14T12:45:04Z","file_id":"5705"}],"month":"07","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_created":"2018-12-11T11:44:57Z","type":"conference","language":[{"iso":"eng"}],"intvolume":" 10981","volume":10981,"date_published":"2018-07-18T00:00:00Z","_id":"160","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Layered Concurrent Programs","year":"2018","external_id":{"isi":["000491481600005"]},"file_date_updated":"2020-07-14T12:45:04Z","abstract":[{"lang":"eng","text":"We present layered concurrent programs, a compact and expressive notation for specifying refinement proofs of concurrent programs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. These programs are expressed in the ordinary syntax of imperative concurrent programs using gated atomic actions, sequencing, choice, and (recursive) procedure calls. Each concurrent program is automatically extracted from the layered program. We reduce refinement to the safety of a sequence of concurrent checker programs, one each to justify the connection between every two consecutive concurrent programs. These checker programs are also automatically extracted from the layered program. Layered concurrent programs have been implemented in the CIVL verifier which has been successfully used for the verification of several complex concurrent programs."}],"page":"79 - 102","ddc":["000"],"publication_status":"published","oa_version":"Published Version","isi":1,"department":[{"_id":"ToHe"}],"conference":{"start_date":"2018-07-14","end_date":"2018-07-17","name":"CAV: Computer Aided Verification","location":"Oxford, UK"},"doi":"10.1007/978-3-319-96145-3_5","day":"18","has_accepted_license":"1","publist_id":"7761","oa":1,"status":"public","alternative_title":["LNCS"],"scopus_import":"1","quality_controlled":"1","publisher":"Springer","citation":{"mla":"Kragl, Bernhard, and Shaz Qadeer. Layered Concurrent Programs. Vol. 10981, Springer, 2018, pp. 79–102, doi:10.1007/978-3-319-96145-3_5.","ama":"Kragl B, Qadeer S. Layered Concurrent Programs. In: Vol 10981. Springer; 2018:79-102. doi:10.1007/978-3-319-96145-3_5","short":"B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102.","apa":"Kragl, B., & Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981, pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer. https://doi.org/10.1007/978-3-319-96145-3_5","ieee":"B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV: Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102.","chicago":"Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_5.","ista":"Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided Verification, LNCS, vol. 10981, 79–102."},"related_material":{"record":[{"relation":"dissertation_contains","id":"8332","status":"public"}]},"author":[{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","last_name":"Kragl","first_name":"Bernhard","full_name":"Kragl, Bernhard"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"}],"date_updated":"2026-04-08T07:23:52Z","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}]}]