[{"day":"10","doi":"10.1007/978-3-030-90870-6_33","arxiv":1,"abstract":[{"text":"We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in LexRSM not existing even for simple terminating programs. Our contributions are twofold: First, we introduce a generalization of LexRSMs which allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.","lang":"eng"}],"citation":{"ista":"Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Zikelic D. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.","short":"K. Chatterjee, E.K. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:, 24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639.","mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>24th International Symposium on Formal Methods</i>, vol. 13047, Springer Nature, 2021, pp. 619–39, doi:<a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">10.1007/978-3-030-90870-6_33</a>.","ieee":"K. Chatterjee, E. K. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” in <i>24th International Symposium on Formal Methods</i>, Virtual, 2021, vol. 13047, pp. 619–639.","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” In <i>24th International Symposium on Formal Methods</i>, 13047:619–39. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">https://doi.org/10.1007/978-3-030-90870-6_33</a>.","ama":"Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. In: <i>24th International Symposium on Formal Methods</i>. Vol 13047. Springer Nature; 2021:619-639. doi:<a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">10.1007/978-3-030-90870-6_33</a>","apa":"Chatterjee, K., Goharshady, E. K., Novotný, P., Zárevúcky, J., &#38; Zikelic, D. (2021). On lexicographic proof rules for probabilistic termination. In <i>24th International Symposium on Formal Methods</i> (Vol. 13047, pp. 619–639). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">https://doi.org/10.1007/978-3-030-90870-6_33</a>"},"year":"2021","date_updated":"2025-07-14T09:10:11Z","external_id":{"arxiv":["2108.02188"],"isi":["000758218600033"]},"isi":1,"volume":13047,"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the Czech Science Foundation grant No. GJ19-15134Y, and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","article_processing_charge":"No","department":[{"_id":"KrCh"}],"date_created":"2021-12-05T23:01:45Z","publication_status":"published","intvolume":"     13047","title":"On lexicographic proof rules for probabilistic termination","alternative_title":["LNCS"],"scopus_import":"1","_id":"10414","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Ehsan Kafshdar","last_name":"Goharshady","full_name":"Goharshady, Ehsan Kafshdar"},{"full_name":"Novotný, Petr","last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zárevúcky","first_name":"Jiří","full_name":"Zárevúcky, Jiří"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic"}],"publisher":"Springer Nature","ec_funded":1,"quality_controlled":"1","page":"619-639","publication_identifier":{"isbn":["9-783-0309-0869-0"],"eisbn":["978-3-030-90870-6"],"eissn":["1611-3349"],"issn":["0302-9743"]},"oa":1,"type":"conference","date_published":"2021-11-10T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2108.02188"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"14539"},{"id":"14778","relation":"later_version","status":"public"}]},"status":"public","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"oa_version":"Preprint","month":"11","publication":"24th International Symposium on Formal Methods","conference":{"end_date":"2021-11-26","location":"Virtual","start_date":"2021-11-20","name":"FM: Formal Methods"},"language":[{"iso":"eng"}]},{"isi":1,"external_id":{"isi":["000927876200012"]},"date_updated":"2023-08-17T06:34:41Z","citation":{"ieee":"S. Chakraborty, C. Ganesh, M. Pancholi, and P. Sarkar, “Reverse firewalls for adaptively secure MPC without setup,” in <i>27th International Conference on the Theory and Application of Cryptology and Information Security</i>, Virtual, Singapore, 2021, vol. 13091, pp. 335–364.","chicago":"Chakraborty, Suvradip, Chaya Ganesh, Mahak Pancholi, and Pratik Sarkar. “Reverse Firewalls for Adaptively Secure MPC without Setup.” In <i>27th International Conference on the Theory and Application of Cryptology and Information Security</i>, 13091:335–64. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-92075-3_12\">https://doi.org/10.1007/978-3-030-92075-3_12</a>.","ama":"Chakraborty S, Ganesh C, Pancholi M, Sarkar P. Reverse firewalls for adaptively secure MPC without setup. In: <i>27th International Conference on the Theory and Application of Cryptology and Information Security</i>. Vol 13091. Springer Nature; 2021:335-364. doi:<a href=\"https://doi.org/10.1007/978-3-030-92075-3_12\">10.1007/978-3-030-92075-3_12</a>","apa":"Chakraborty, S., Ganesh, C., Pancholi, M., &#38; Sarkar, P. (2021). Reverse firewalls for adaptively secure MPC without setup. In <i>27th International Conference on the Theory and Application of Cryptology and Information Security</i> (Vol. 13091, pp. 335–364). Virtual, Singapore: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-92075-3_12\">https://doi.org/10.1007/978-3-030-92075-3_12</a>","ista":"Chakraborty S, Ganesh C, Pancholi M, Sarkar P. 2021. Reverse firewalls for adaptively secure MPC without setup. 27th International Conference on the Theory and Application of Cryptology and Information Security. ASIACRYPT: International Conference on Cryptology in Asia, LNCS, vol. 13091, 335–364.","short":"S. Chakraborty, C. Ganesh, M. Pancholi, P. Sarkar, in:, 27th International Conference on the Theory and Application of Cryptology and Information Security, Springer Nature, 2021, pp. 335–364.","mla":"Chakraborty, Suvradip, et al. “Reverse Firewalls for Adaptively Secure MPC without Setup.” <i>27th International Conference on the Theory and Application of Cryptology and Information Security</i>, vol. 13091, Springer Nature, 2021, pp. 335–64, doi:<a href=\"https://doi.org/10.1007/978-3-030-92075-3_12\">10.1007/978-3-030-92075-3_12</a>."},"year":"2021","abstract":[{"text":"We study Multi-party computation (MPC) in the setting of subversion, where the adversary tampers with the machines of honest parties. Our goal is to construct actively secure MPC protocols where parties are corrupted adaptively by an adversary (as in the standard adaptive security setting), and in addition, honest parties’ machines are compromised.\r\nThe idea of reverse firewalls (RF) was introduced at EUROCRYPT’15 by Mironov and Stephens-Davidowitz as an approach to protecting protocols against corruption of honest parties’ devices. Intuitively, an RF for a party   P  is an external entity that sits between   P  and the outside world and whose scope is to sanitize   P ’s incoming and outgoing messages in the face of subversion of their computer. Mironov and Stephens-Davidowitz constructed a protocol for passively-secure two-party computation. At CRYPTO’20, Chakraborty, Dziembowski and Nielsen constructed a protocol for secure computation with firewalls that improved on this result, both by extending it to multi-party computation protocol, and considering active security in the presence of static corruptions. In this paper, we initiate the study of RF for MPC in the adaptive setting. We put forward a definition for adaptively secure MPC in the reverse firewall setting, explore relationships among the security notions, and then construct reverse firewalls for MPC in this stronger setting of adaptive security. We also resolve the open question of Chakraborty, Dziembowski and Nielsen by removing the need for a trusted setup in constructing RF for MPC. Towards this end, we construct reverse firewalls for adaptively secure augmented coin tossing and adaptively secure zero-knowledge protocols and obtain a constant round adaptively secure MPC protocol in the reverse firewall setting without setup. Along the way, we propose a new multi-party adaptively secure coin tossing protocol in the plain model, that is of independent interest.","lang":"eng"}],"doi":"10.1007/978-3-030-92075-3_12","day":"01","volume":13091,"author":[{"full_name":"Chakraborty, Suvradip","last_name":"Chakraborty","first_name":"Suvradip","id":"B9CD0494-D033-11E9-B219-A439E6697425"},{"last_name":"Ganesh","first_name":"Chaya","full_name":"Ganesh, Chaya"},{"last_name":"Pancholi","first_name":"Mahak","full_name":"Pancholi, Mahak"},{"full_name":"Sarkar, Pratik","last_name":"Sarkar","first_name":"Pratik"}],"_id":"10609","scopus_import":"1","title":"Reverse firewalls for adaptively secure MPC without setup","alternative_title":["LNCS"],"intvolume":"     13091","publication_status":"published","article_processing_charge":"No","date_created":"2022-01-09T23:01:27Z","department":[{"_id":"KrPi"}],"page":"335-364","ec_funded":1,"quality_controlled":"1","publisher":"Springer Nature","date_published":"2021-12-01T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"isbn":["978-3-030-92074-6"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["978-3-030-92075-3"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2021/1262"}],"publication":"27th International Conference on the Theory and Application of Cryptology and Information Security","month":"12","oa_version":"Preprint","project":[{"grant_number":"682815","name":"Teaching Old Crypto New Tricks","_id":"258AA5B2-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"language":[{"iso":"eng"}],"conference":{"start_date":"2021-12-06","name":"ASIACRYPT: International Conference on Cryptology in Asia","end_date":"2021-12-10","location":"Virtual, Singapore"}},{"author":[{"full_name":"Bansal, Suguman","first_name":"Suguman","last_name":"Bansal"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Vardi, Moshe Y.","first_name":"Moshe Y.","last_name":"Vardi"}],"scopus_import":"1","_id":"12767","intvolume":"     12651","alternative_title":["LNCS"],"title":"On satisficing in quantitative games","department":[{"_id":"KrCh"}],"date_created":"2023-03-26T22:01:09Z","article_processing_charge":"No","publication_status":"published","file_date_updated":"2023-03-28T11:00:33Z","quality_controlled":"1","ec_funded":1,"page":"20-37","publisher":"Springer Nature","external_id":{"arxiv":["2101.02594"]},"year":"2021","citation":{"apa":"Bansal, S., Chatterjee, K., &#38; Vardi, M. Y. (2021). On satisficing in quantitative games. In <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 12651, pp. 20–37). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-72016-2\">https://doi.org/10.1007/978-3-030-72016-2</a>","ama":"Bansal S, Chatterjee K, Vardi MY. On satisficing in quantitative games. In: <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 12651. Springer Nature; 2021:20-37. doi:<a href=\"https://doi.org/10.1007/978-3-030-72016-2\">10.1007/978-3-030-72016-2</a>","ieee":"S. Bansal, K. Chatterjee, and M. Y. Vardi, “On satisficing in quantitative games,” in <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2021, vol. 12651, pp. 20–37.","chicago":"Bansal, Suguman, Krishnendu Chatterjee, and Moshe Y. Vardi. “On Satisficing in Quantitative Games.” In <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 12651:20–37. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-72016-2\">https://doi.org/10.1007/978-3-030-72016-2</a>.","mla":"Bansal, Suguman, et al. “On Satisficing in Quantitative Games.” <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 12651, Springer Nature, 2021, pp. 20–37, doi:<a href=\"https://doi.org/10.1007/978-3-030-72016-2\">10.1007/978-3-030-72016-2</a>.","short":"S. Bansal, K. Chatterjee, M.Y. Vardi, in:, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2021, pp. 20–37.","ista":"Bansal S, Chatterjee K, Vardi MY. 2021. On satisficing in quantitative games. 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 12651, 20–37."},"date_updated":"2025-07-14T09:09:51Z","abstract":[{"lang":"eng","text":"Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games. Optimization is one form of analysis. We argue that in many cases it may be better to replace the optimization problem with the satisficing problem, where instead of searching for optimal solutions, the goal is to search for solutions that adhere to a given threshold bound.\r\nThis work defines and investigates the satisficing problem on a two-player graph game with the discounted-sum cost model. We show that while the satisficing problem can be solved using numerical methods just like the optimization problem, this approach does not render compelling benefits over optimization. When the discount factor is, however, an integer, we present another approach to satisficing, which is purely based on automata methods. We show that this approach is algorithmically more performant – both theoretically and empirically – and demonstrates the broader applicability of satisficing over optimization."}],"day":"21","arxiv":1,"doi":"10.1007/978-3-030-72016-2","ddc":["000"],"acknowledgement":"We thank anonymous reviewers for valuable inputs. This work is supported in part by NSF grant 2030859 to the CRA for the CIFellows Project, NSF grants IIS-1527668, CCF-1704883, IIS-1830549, the ERC CoG 863818 (ForM-SMArt), and an award from the Maryland Procurement Office.","volume":12651,"has_accepted_license":"1","publication":"27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","month":"03","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"end_date":"2021-04-01","location":"Luxembourg City, Luxembourg","start_date":"2021-03-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","date_published":"2021-03-21T00:00:00Z","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)"},"oa":1,"publication_identifier":{"isbn":["9783030720155"],"issn":["0302-9743"],"eissn":["1611-3349"]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"b020b78b23587ce7610b1aafb4e63438","file_size":747418,"date_created":"2023-03-28T11:00:33Z","content_type":"application/pdf","file_name":"2021_LNCS_Bansal.pdf","date_updated":"2023-03-28T11:00:33Z","success":1,"relation":"main_file","access_level":"open_access","creator":"dernst","file_id":"12777"}]},{"isi":1,"external_id":{"isi":["000698732400016"],"arxiv":["2105.06424"]},"date_updated":"2025-07-14T09:10:15Z","citation":{"ista":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.","short":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, V. Toman, in:, 33rd International Conference on Computer-Aided Verification , Springer Nature, 2021, pp. 341–366.","mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” <i>33rd International Conference on Computer-Aided Verification </i>, vol. 12759, Springer Nature, 2021, pp. 341–66, doi:<a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">10.1007/978-3-030-81685-8_16</a>.","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in <i>33rd International Conference on Computer-Aided Verification </i>, Virtual, 2021, vol. 12759, pp. 341–366.","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In <i>33rd International Conference on Computer-Aided Verification </i>, 12759:341–66. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">https://doi.org/10.1007/978-3-030-81685-8_16</a>.","ama":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: <i>33rd International Conference on Computer-Aided Verification </i>. Vol 12759. Springer Nature; 2021:341-366. doi:<a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">10.1007/978-3-030-81685-8_16</a>","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., &#38; Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In <i>33rd International Conference on Computer-Aided Verification </i> (Vol. 12759, pp. 341–366). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">https://doi.org/10.1007/978-3-030-81685-8_16</a>"},"year":"2021","abstract":[{"text":"Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present   RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover,   RVF-SMC  generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.","lang":"eng"}],"arxiv":1,"doi":"10.1007/978-3-030-81685-8_16","day":"15","ddc":["000"],"volume":"12759 ","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.","author":[{"full_name":"Agarwal, Pratyush","last_name":"Agarwal","first_name":"Pratyush"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Pathak, Shreya","last_name":"Pathak","first_name":"Shreya"},{"first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"_id":"9987","scopus_import":"1","alternative_title":["LNCS"],"title":"Stateless model checking under a reads-value-from equivalence","publication_status":"published","date_created":"2021-09-05T22:01:24Z","article_processing_charge":"Yes","department":[{"_id":"KrCh"}],"file_date_updated":"2022-05-13T07:00:20Z","page":"341-366","quality_controlled":"1","ec_funded":1,"publisher":"Springer Nature","date_published":"2021-07-15T00:00:00Z","type":"conference","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)"},"oa":1,"publication_identifier":{"isbn":["978-3-030-81684-1"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["978-3-030-81685-8"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","related_material":{"record":[{"status":"public","id":"10199","relation":"dissertation_contains"}]},"file":[{"date_updated":"2022-05-13T07:00:20Z","file_name":"2021_LNCS_Agarwal.pdf","content_type":"application/pdf","date_created":"2022-05-13T07:00:20Z","checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","file_size":1516756,"file_id":"11368","creator":"dernst","success":1,"access_level":"open_access","relation":"main_file"}],"publication":"33rd International Conference on Computer-Aided Verification ","has_accepted_license":"1","month":"07","oa_version":"Published Version","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"language":[{"iso":"eng"}],"conference":{"start_date":"2021-07-20","name":"CAV: Computer Aided Verification ","end_date":"2021-07-23","location":"Virtual"}},{"publisher":"Springer Nature","editor":[{"last_name":"Kiayias","first_name":"A","full_name":"Kiayias, A"}],"page":"220-246","quality_controlled":"1","series_title":"LNCS","title":"Witness maps and applications","intvolume":"     12110","publication_status":"published","date_created":"2022-03-18T11:35:51Z","article_processing_charge":"No","author":[{"id":"B9CD0494-D033-11E9-B219-A439E6697425","last_name":"Chakraborty","first_name":"Suvradip","full_name":"Chakraborty, Suvradip"},{"full_name":"Prabhakaran, Manoj","last_name":"Prabhakaran","first_name":"Manoj"},{"full_name":"Wichs, Daniel","last_name":"Wichs","first_name":"Daniel"}],"_id":"10865","scopus_import":"1","volume":12110,"acknowledgement":"We would like to thank the anonymous reviewers of PKC 2019 for their useful comments and suggestions. We thank Omer Paneth for pointing out to us the connection between Unique Witness Maps (UWM) and Witness encryption (WE). The first author would like to acknowledge Pandu Rangan for his involvement during the initial discussion phase of the project.","abstract":[{"lang":"eng","text":"We introduce the notion of Witness Maps as a cryptographic notion of a proof system. A Unique Witness Map (UWM) deterministically maps all witnesses for an   NP  statement to a single representative witness, resulting in a computationally sound, deterministic-prover, non-interactive witness independent proof system. A relaxation of UWM, called Compact Witness Map (CWM), maps all the witnesses to a small number of witnesses, resulting in a “lossy” deterministic-prover, non-interactive proof-system. We also define a Dual Mode Witness Map (DMWM) which adds an “extractable” mode to a CWM.\r\nOur main construction is a DMWM for all   NP  relations, assuming sub-exponentially secure indistinguishability obfuscation (  iO ), along with standard cryptographic assumptions. The DMWM construction relies on a CWM and a new primitive called Cumulative All-Lossy-But-One Trapdoor Functions (C-ALBO-TDF), both of which are in turn instantiated based on   iO  and other primitives. Our instantiation of a CWM is in fact a UWM; in turn, we show that a UWM implies Witness Encryption. Along the way to constructing UWM and C-ALBO-TDF, we also construct, from standard assumptions, Puncturable Digital Signatures and a new primitive called Cumulative Lossy Trapdoor Functions (C-LTDF). The former improves up on a construction of Bellare et al. (Eurocrypt 2016), who relied on sub-exponentially secure   iO  and sub-exponentially secure OWF.\r\nAs an application of our constructions, we show how to use a DMWM to construct the first leakage and tamper-resilient signatures with a deterministic signer, thereby solving a decade old open problem posed by Katz and Vaikunthanathan (Asiacrypt 2009), by Boyle, Segev and Wichs (Eurocrypt 2011), as well as by Faonio and Venturi (Asiacrypt 2016). Our construction achieves the optimal leakage rate of   1−o(1) ."}],"doi":"10.1007/978-3-030-45374-9_8","day":"29","date_updated":"2023-09-05T15:10:02Z","citation":{"chicago":"Chakraborty, Suvradip, Manoj Prabhakaran, and Daniel Wichs. “Witness Maps and Applications.” In <i>Public-Key Cryptography</i>, edited by A Kiayias, 12110:220–46. LNCS. Cham: Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-45374-9_8\">https://doi.org/10.1007/978-3-030-45374-9_8</a>.","ieee":"S. Chakraborty, M. Prabhakaran, and D. Wichs, “Witness maps and applications,” in <i>Public-Key Cryptography</i>, vol. 12110, A. Kiayias, Ed. Cham: Springer Nature, 2020, pp. 220–246.","apa":"Chakraborty, S., Prabhakaran, M., &#38; Wichs, D. (2020). Witness maps and applications. In A. Kiayias (Ed.), <i>Public-Key Cryptography</i> (Vol. 12110, pp. 220–246). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-45374-9_8\">https://doi.org/10.1007/978-3-030-45374-9_8</a>","ama":"Chakraborty S, Prabhakaran M, Wichs D. Witness maps and applications. In: Kiayias A, ed. <i>Public-Key Cryptography</i>. Vol 12110. LNCS. Cham: Springer Nature; 2020:220-246. doi:<a href=\"https://doi.org/10.1007/978-3-030-45374-9_8\">10.1007/978-3-030-45374-9_8</a>","ista":"Chakraborty S, Prabhakaran M, Wichs D. 2020.Witness maps and applications. In: Public-Key Cryptography. vol. 12110, 220–246.","mla":"Chakraborty, Suvradip, et al. “Witness Maps and Applications.” <i>Public-Key Cryptography</i>, edited by A Kiayias, vol. 12110, Springer Nature, 2020, pp. 220–46, doi:<a href=\"https://doi.org/10.1007/978-3-030-45374-9_8\">10.1007/978-3-030-45374-9_8</a>.","short":"S. Chakraborty, M. Prabhakaran, D. Wichs, in:, A. Kiayias (Ed.), Public-Key Cryptography, Springer Nature, Cham, 2020, pp. 220–246."},"year":"2020","language":[{"iso":"eng"}],"month":"04","oa_version":"Preprint","publication":"Public-Key Cryptography","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2020/090"}],"place":"Cham","oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783030453732","9783030453749"]},"date_published":"2020-04-29T00:00:00Z","type":"book_chapter"},{"title":"Everybody’s a target: Scalability in public-key encryption","alternative_title":["LNCS"],"intvolume":"     12107","publication_status":"published","department":[{"_id":"KrPi"}],"article_processing_charge":"No","date_created":"2020-06-15T07:13:37Z","author":[{"id":"D33D2B18-E445-11E9-ABB7-15F4E5697425","orcid":"0000-0002-7553-6606","full_name":"Auerbach, Benedikt","first_name":"Benedikt","last_name":"Auerbach"},{"full_name":"Giacon, Federico","first_name":"Federico","last_name":"Giacon"},{"full_name":"Kiltz, Eike","first_name":"Eike","last_name":"Kiltz"}],"_id":"7966","publisher":"Springer Nature","page":"475-506","ec_funded":1,"quality_controlled":"1","abstract":[{"text":"For 1≤m≤n, we consider a natural m-out-of-n multi-instance scenario for a public-key encryption (PKE) scheme. An adversary, given n independent instances of PKE, wins if he breaks at least m out of the n instances. In this work, we are interested in the scaling factor of PKE schemes, SF, which measures how well the difficulty of breaking m out of the n instances scales in m. That is, a scaling factor SF=ℓ indicates that breaking m out of n instances is at least ℓ times more difficult than breaking one single instance. A PKE scheme with small scaling factor hence provides an ideal target for mass surveillance. In fact, the Logjam attack (CCS 2015) implicitly exploited, among other things, an almost constant scaling factor of ElGamal over finite fields (with shared group parameters).\r\n\r\nFor Hashed ElGamal over elliptic curves, we use the generic group model to argue that the scaling factor depends on the scheme's granularity. In low granularity, meaning each public key contains its independent group parameter, the scheme has optimal scaling factor SF=m; In medium and high granularity, meaning all public keys share the same group parameter, the scheme still has a reasonable scaling factor SF=√m. Our findings underline that instantiating ElGamal over elliptic curves should be preferred to finite fields in a multi-instance scenario.\r\n\r\nAs our main technical contribution, we derive new generic-group lower bounds of Ω(√(mp)) on the difficulty of solving both the m-out-of-n Gap Discrete Logarithm and the m-out-of-n Gap Computational Diffie-Hellman problem over groups of prime order p, extending a recent result by Yun (EUROCRYPT 2015). We establish the lower bound by studying the hardness of a related computational problem which we call the search-by-hypersurface problem.","lang":"eng"}],"doi":"10.1007/978-3-030-45727-3_16","day":"01","isi":1,"external_id":{"isi":["000828688000016"]},"date_updated":"2023-09-05T15:06:40Z","year":"2020","citation":{"ama":"Auerbach B, Giacon F, Kiltz E. Everybody’s a target: Scalability in public-key encryption. In: <i>Advances in Cryptology – EUROCRYPT 2020</i>. Vol 12107. Springer Nature; 2020:475-506. doi:<a href=\"https://doi.org/10.1007/978-3-030-45727-3_16\">10.1007/978-3-030-45727-3_16</a>","apa":"Auerbach, B., Giacon, F., &#38; Kiltz, E. (2020). Everybody’s a target: Scalability in public-key encryption. In <i>Advances in Cryptology – EUROCRYPT 2020</i> (Vol. 12107, pp. 475–506). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-45727-3_16\">https://doi.org/10.1007/978-3-030-45727-3_16</a>","ieee":"B. Auerbach, F. Giacon, and E. Kiltz, “Everybody’s a target: Scalability in public-key encryption,” in <i>Advances in Cryptology – EUROCRYPT 2020</i>, 2020, vol. 12107, pp. 475–506.","chicago":"Auerbach, Benedikt, Federico Giacon, and Eike Kiltz. “Everybody’s a Target: Scalability in Public-Key Encryption.” In <i>Advances in Cryptology – EUROCRYPT 2020</i>, 12107:475–506. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-45727-3_16\">https://doi.org/10.1007/978-3-030-45727-3_16</a>.","mla":"Auerbach, Benedikt, et al. “Everybody’s a Target: Scalability in Public-Key Encryption.” <i>Advances in Cryptology – EUROCRYPT 2020</i>, vol. 12107, Springer Nature, 2020, pp. 475–506, doi:<a href=\"https://doi.org/10.1007/978-3-030-45727-3_16\">10.1007/978-3-030-45727-3_16</a>.","short":"B. Auerbach, F. Giacon, E. Kiltz, in:, Advances in Cryptology – EUROCRYPT 2020, Springer Nature, 2020, pp. 475–506.","ista":"Auerbach B, Giacon F, Kiltz E. 2020. Everybody’s a target: Scalability in public-key encryption. Advances in Cryptology – EUROCRYPT 2020. EUROCRYPT: Theory and Applications of Cryptographic Techniques, LNCS, vol. 12107, 475–506."},"volume":12107,"month":"05","oa_version":"Submitted Version","project":[{"call_identifier":"H2020","_id":"258AA5B2-B435-11E9-9278-68D0E5697425","name":"Teaching Old Crypto New Tricks","grant_number":"682815"}],"publication":"Advances in Cryptology – EUROCRYPT 2020","conference":{"start_date":"2020-05-11","name":"EUROCRYPT: Theory and Applications of Cryptographic Techniques","end_date":"2020-05-15"},"language":[{"iso":"eng"}],"oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783030457266","9783030457273"]},"date_published":"2020-05-01T00:00:00Z","type":"conference","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2019/364"}]},{"ddc":["000"],"acknowledgement":"Bernhard Kragl and Thomas A. Henzinger were supported by\r\nthe Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","volume":12224,"isi":1,"external_id":{"isi":["000695276000014"]},"date_updated":"2023-09-07T13:18:00Z","year":"2020","citation":{"short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Computer Aided Verification, Springer Nature, 2020, pp. 275–298.","mla":"Kragl, Bernhard, et al. “Refinement for Structured Concurrent Programs.” <i>Computer Aided Verification</i>, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:<a href=\"https://doi.org/10.1007/978-3-030-53288-8_14\">10.1007/978-3-030-53288-8_14</a>.","ista":"Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298.","ama":"Kragl B, Qadeer S, Henzinger TA. Refinement for structured concurrent programs. In: <i>Computer Aided Verification</i>. Vol 12224. Springer Nature; 2020:275-298. doi:<a href=\"https://doi.org/10.1007/978-3-030-53288-8_14\">10.1007/978-3-030-53288-8_14</a>","apa":"Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2020). Refinement for structured concurrent programs. In <i>Computer Aided Verification</i> (Vol. 12224, pp. 275–298). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-53288-8_14\">https://doi.org/10.1007/978-3-030-53288-8_14</a>","chicago":"Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured Concurrent Programs.” In <i>Computer Aided Verification</i>, 12224:275–98. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-53288-8_14\">https://doi.org/10.1007/978-3-030-53288-8_14</a>.","ieee":"B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent programs,” in <i>Computer Aided Verification</i>, 2020, vol. 12224, pp. 275–298."},"abstract":[{"lang":"eng","text":"This paper presents a foundation for refining concurrent programs with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the Civl verifier."}],"doi":"10.1007/978-3-030-53288-8_14","day":"14","file_date_updated":"2020-08-06T08:14:54Z","page":"275-298","quality_controlled":"1","publisher":"Springer Nature","author":[{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","first_name":"Bernhard","last_name":"Kragl","orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"8195","scopus_import":"1","alternative_title":["LNCS"],"title":"Refinement for structured concurrent programs","intvolume":"     12224","publication_status":"published","date_created":"2020-08-03T11:45:35Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"id":"8332","relation":"dissertation_contains","status":"public"}]},"file":[{"date_updated":"2020-08-06T08:14:54Z","content_type":"application/pdf","file_name":"2020_LNCS_Kragl.pdf","date_created":"2020-08-06T08:14:54Z","file_size":804237,"file_id":"8201","creator":"dernst","success":1,"access_level":"open_access","relation":"main_file"}],"date_published":"2020-07-14T00:00:00Z","type":"conference","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)"},"oa":1,"publication_identifier":{"isbn":["9783030532871"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783030532888"]},"language":[{"iso":"eng"}],"publication":"Computer Aided Verification","has_accepted_license":"1","month":"07","oa_version":"Published Version","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}]},{"conference":{"name":"RV: Runtime Verification","start_date":"2020-10-06","location":"Los Angeles, CA, United States","end_date":"2020-10-09"},"language":[{"iso":"eng"}],"month":"10","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Submitted Version","has_accepted_license":"1","publication":"Runtime Verification","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"date_updated":"2020-10-15T14:28:06Z","file_name":"monitorability.pdf","content_type":"application/pdf","date_created":"2020-10-15T14:28:06Z","checksum":"00661f9b7034f52e18bf24fa552b8194","file_size":478148,"file_id":"8665","creator":"esarac","relation":"main_file","success":1,"access_level":"open_access"}],"oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783030605070","9783030605087"]},"type":"conference","date_published":"2020-10-02T00:00:00Z","publisher":"Springer Nature","file_date_updated":"2020-10-15T14:28:06Z","quality_controlled":"1","page":"3-18","intvolume":"     12399","alternative_title":["LNCS"],"title":"Monitorability under assumptions","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2020-10-07T15:05:37Z","publication_status":"published","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Sarac","first_name":"Naci E","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"scopus_import":"1","_id":"8623","ddc":["000"],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","volume":12399,"abstract":[{"text":"We introduce the monitoring of trace properties under assumptions. An assumption limits the space of possible traces that the monitor may encounter. An assumption may result from knowledge about the system that is being monitored, about the environment, or about another, connected monitor. We define monitorability under assumptions and study its theoretical properties. In particular, we show that for every assumption A, the boolean combinations of properties that are safe or co-safe relative to A are monitorable under A. We give several examples and constructions on how an assumption can make a non-monitorable property monitorable, and how an assumption can make a monitorable property monitorable with fewer resources, such as integer registers.","lang":"eng"}],"day":"02","doi":"10.1007/978-3-030-60508-7_1","external_id":{"isi":["000728160600001"]},"isi":1,"year":"2020","citation":{"ista":"Henzinger TA, Sarac NE. 2020. Monitorability under assumptions. Runtime Verification. RV: Runtime Verification, LNCS, vol. 12399, 3–18.","mla":"Henzinger, Thomas A., and Naci E. Sarac. “Monitorability under Assumptions.” <i>Runtime Verification</i>, vol. 12399, Springer Nature, 2020, pp. 3–18, doi:<a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">10.1007/978-3-030-60508-7_1</a>.","short":"T.A. Henzinger, N.E. Sarac, in:, Runtime Verification, Springer Nature, 2020, pp. 3–18.","ieee":"T. A. Henzinger and N. E. Sarac, “Monitorability under assumptions,” in <i>Runtime Verification</i>, Los Angeles, CA, United States, 2020, vol. 12399, pp. 3–18.","chicago":"Henzinger, Thomas A, and Naci E Sarac. “Monitorability under Assumptions.” In <i>Runtime Verification</i>, 12399:3–18. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">https://doi.org/10.1007/978-3-030-60508-7_1</a>.","apa":"Henzinger, T. A., &#38; Sarac, N. E. (2020). Monitorability under assumptions. In <i>Runtime Verification</i> (Vol. 12399, pp. 3–18). Los Angeles, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">https://doi.org/10.1007/978-3-030-60508-7_1</a>","ama":"Henzinger TA, Sarac NE. Monitorability under assumptions. In: <i>Runtime Verification</i>. Vol 12399. Springer Nature; 2020:3-18. doi:<a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">10.1007/978-3-030-60508-7_1</a>"},"date_updated":"2023-09-05T15:08:26Z"},{"publication":"Automated Technology for Verification and Analysis","has_accepted_license":"1","oa_version":"Submitted Version","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"month":"10","language":[{"iso":"eng"}],"conference":{"end_date":"2020-10-23","location":"Hanoi, Vietnam","start_date":"2020-10-19","name":"ATVA: Automated Technology for Verification and Analysis"},"date_published":"2020-10-12T00:00:00Z","type":"conference","publication_identifier":{"eisbn":["9783030591526"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783030591519"]},"oa":1,"file":[{"file_id":"8729","creator":"dernst","success":1,"access_level":"open_access","relation":"main_file","date_updated":"2020-11-06T07:41:03Z","content_type":"application/pdf","file_name":"2020_LNCS_ATVA_Asadi_accepted.pdf","date_created":"2020-11-06T07:41:03Z","file_size":726648,"checksum":"ae83f27e5b189d5abc2e7514f1b7e1b5"}],"status":"public","related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"8728","scopus_import":"1","author":[{"last_name":"Asadi","first_name":"Ali","full_name":"Asadi, Ali"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mohammadi, Kiarash","last_name":"Mohammadi","first_name":"Kiarash"},{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","date_created":"2020-11-06T07:30:05Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","title":"Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth","alternative_title":["LNCS"],"intvolume":"     12302","page":"253-270","quality_controlled":"1","file_date_updated":"2020-11-06T07:41:03Z","publisher":"Springer Nature","date_updated":"2025-06-02T08:53:43Z","year":"2020","citation":{"apa":"Asadi, A., Chatterjee, K., Goharshady, A. K., Mohammadi, K., &#38; Pavlogiannis, A. (2020). Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In <i>Automated Technology for Verification and Analysis</i> (Vol. 12302, pp. 253–270). Hanoi, Vietnam: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">https://doi.org/10.1007/978-3-030-59152-6_14</a>","ama":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In: <i>Automated Technology for Verification and Analysis</i>. Vol 12302. Springer Nature; 2020:253-270. doi:<a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">10.1007/978-3-030-59152-6_14</a>","chicago":"Asadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” In <i>Automated Technology for Verification and Analysis</i>, 12302:253–70. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">https://doi.org/10.1007/978-3-030-59152-6_14</a>.","ieee":"A. Asadi, K. Chatterjee, A. K. Goharshady, K. Mohammadi, and A. Pavlogiannis, “Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth,” in <i>Automated Technology for Verification and Analysis</i>, Hanoi, Vietnam, 2020, vol. 12302, pp. 253–270.","short":"A. Asadi, K. Chatterjee, A.K. Goharshady, K. Mohammadi, A. Pavlogiannis, in:, Automated Technology for Verification and Analysis, Springer Nature, 2020, pp. 253–270.","mla":"Asadi, Ali, et al. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” <i>Automated Technology for Verification and Analysis</i>, vol. 12302, Springer Nature, 2020, pp. 253–70, doi:<a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">10.1007/978-3-030-59152-6_14</a>.","ista":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. 2020. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 12302, 253–270."},"isi":1,"external_id":{"isi":["000723555700014"]},"doi":"10.1007/978-3-030-59152-6_14","day":"12","abstract":[{"lang":"eng","text":"Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in   O((n+m)⋅t2)  time, given a tree decomposition of the MC with width t. Our results also imply a bound of   O(κ⋅(n+m)⋅t2)  for each objective on MDPs, where   κ  is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude."}],"volume":12302,"ddc":["000"]},{"volume":12301,"day":"09","doi":"10.1007/978-3-030-60440-0_26","abstract":[{"text":"A simple drawing D(G) of a graph G is one where each pair of edges share at most one point: either a common endpoint or a proper crossing. An edge e in the complement of G can be inserted into D(G) if there exists a simple drawing of   G+e  extending D(G). As a result of Levi’s Enlargement Lemma, if a drawing is rectilinear (pseudolinear), that is, the edges can be extended into an arrangement of lines (pseudolines), then any edge in the complement of G can be inserted. In contrast, we show that it is   NP -complete to decide whether one edge can be inserted into a simple drawing. This remains true even if we assume that the drawing is pseudocircular, that is, the edges can be extended to an arrangement of pseudocircles. On the positive side, we show that, given an arrangement of pseudocircles   A  and a pseudosegment   σ , it can be decided in polynomial time whether there exists a pseudocircle   Φσ  extending   σ  for which   A∪{Φσ}  is again an arrangement of pseudocircles.","lang":"eng"}],"citation":{"ista":"Arroyo Guevara AM, Klute F, Parada I, Seidel R, Vogtenhuber B, Wiedera T. 2020. Inserting one edge into a simple drawing is hard. Graph-Theoretic Concepts in Computer Science. WG: Workshop on Graph-Theoretic Concepts in Computer Science, LNCS, vol. 12301, 325–338.","mla":"Arroyo Guevara, Alan M., et al. “Inserting One Edge into a Simple Drawing Is Hard.” <i>Graph-Theoretic Concepts in Computer Science</i>, vol. 12301, Springer Nature, 2020, pp. 325–38, doi:<a href=\"https://doi.org/10.1007/978-3-030-60440-0_26\">10.1007/978-3-030-60440-0_26</a>.","short":"A.M. Arroyo Guevara, F. Klute, I. Parada, R. Seidel, B. Vogtenhuber, T. Wiedera, in:, Graph-Theoretic Concepts in Computer Science, Springer Nature, 2020, pp. 325–338.","ieee":"A. M. Arroyo Guevara, F. Klute, I. Parada, R. Seidel, B. Vogtenhuber, and T. Wiedera, “Inserting one edge into a simple drawing is hard,” in <i>Graph-Theoretic Concepts in Computer Science</i>, Leeds, United Kingdom, 2020, vol. 12301, pp. 325–338.","chicago":"Arroyo Guevara, Alan M, Fabian Klute, Irene Parada, Raimund Seidel, Birgit Vogtenhuber, and Tilo Wiedera. “Inserting One Edge into a Simple Drawing Is Hard.” In <i>Graph-Theoretic Concepts in Computer Science</i>, 12301:325–38. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-60440-0_26\">https://doi.org/10.1007/978-3-030-60440-0_26</a>.","ama":"Arroyo Guevara AM, Klute F, Parada I, Seidel R, Vogtenhuber B, Wiedera T. Inserting one edge into a simple drawing is hard. In: <i>Graph-Theoretic Concepts in Computer Science</i>. Vol 12301. Springer Nature; 2020:325-338. doi:<a href=\"https://doi.org/10.1007/978-3-030-60440-0_26\">10.1007/978-3-030-60440-0_26</a>","apa":"Arroyo Guevara, A. M., Klute, F., Parada, I., Seidel, R., Vogtenhuber, B., &#38; Wiedera, T. (2020). Inserting one edge into a simple drawing is hard. In <i>Graph-Theoretic Concepts in Computer Science</i> (Vol. 12301, pp. 325–338). Leeds, United Kingdom: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-60440-0_26\">https://doi.org/10.1007/978-3-030-60440-0_26</a>"},"year":"2020","date_updated":"2023-09-05T15:09:16Z","publisher":"Springer Nature","ec_funded":1,"quality_controlled":"1","page":"325-338","department":[{"_id":"UlWa"}],"date_created":"2020-11-06T08:45:03Z","article_processing_charge":"No","publication_status":"published","intvolume":"     12301","title":"Inserting one edge into a simple drawing is hard","alternative_title":["LNCS"],"scopus_import":"1","_id":"8732","author":[{"id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","full_name":"Arroyo Guevara, Alan M","orcid":"0000-0003-2401-8670","last_name":"Arroyo Guevara","first_name":"Alan M"},{"first_name":"Fabian","last_name":"Klute","full_name":"Klute, Fabian"},{"last_name":"Parada","first_name":"Irene","full_name":"Parada, Irene"},{"full_name":"Seidel, Raimund","last_name":"Seidel","first_name":"Raimund"},{"last_name":"Vogtenhuber","first_name":"Birgit","full_name":"Vogtenhuber, Birgit"},{"full_name":"Wiedera, Tilo","first_name":"Tilo","last_name":"Wiedera"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_identifier":{"isbn":["9783030604394","9783030604400"],"eissn":["1611-3349"],"issn":["0302-9743"]},"type":"conference","date_published":"2020-10-09T00:00:00Z","conference":{"start_date":"2020-06-24","name":"WG: Workshop on Graph-Theoretic Concepts in Computer Science","end_date":"2020-06-26","location":"Leeds, United Kingdom"},"language":[{"iso":"eng"}],"project":[{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"oa_version":"None","month":"10","publication":"Graph-Theoretic Concepts in Computer Science"},{"volume":12590,"acknowledgement":"Supported by the National Research, Development and Innovation Office, NKFIH, KKP-133864, K-131529, K-116769, K-132696, by the Higher Educational Institutional Excellence Program 2019 NKFIH-1158-6/2019, the Austrian Science Fund (FWF), grant Z 342-N31, by the Ministry of Education and Science of the Russian Federation MegaGrant No. 075-15-2019-1926, and by the ERC Synergy Grant “Dynasnet” No. 810115. A full version can be found at https://arxiv.org/abs/2006.14908.","year":"2020","citation":{"ista":"Pach J, Tardos G, Tóth G. 2020. Crossings between non-homotopic edges. 28th International Symposium on Graph Drawing and Network Visualization. GD: Graph Drawing and Network VisualizationLNCS vol. 12590, 359–371.","mla":"Pach, János, et al. “Crossings between Non-Homotopic Edges.” <i>28th International Symposium on Graph Drawing and Network Visualization</i>, vol. 12590, Springer Nature, 2020, pp. 359–71, doi:<a href=\"https://doi.org/10.1007/978-3-030-68766-3_28\">10.1007/978-3-030-68766-3_28</a>.","short":"J. Pach, G. Tardos, G. Tóth, in:, 28th International Symposium on Graph Drawing and Network Visualization, Springer Nature, 2020, pp. 359–371.","chicago":"Pach, János, Gábor Tardos, and Géza Tóth. “Crossings between Non-Homotopic Edges.” In <i>28th International Symposium on Graph Drawing and Network Visualization</i>, 12590:359–71. LNCS. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-68766-3_28\">https://doi.org/10.1007/978-3-030-68766-3_28</a>.","ieee":"J. Pach, G. Tardos, and G. Tóth, “Crossings between non-homotopic edges,” in <i>28th International Symposium on Graph Drawing and Network Visualization</i>, Virtual, Online, 2020, vol. 12590, pp. 359–371.","apa":"Pach, J., Tardos, G., &#38; Tóth, G. (2020). Crossings between non-homotopic edges. In <i>28th International Symposium on Graph Drawing and Network Visualization</i> (Vol. 12590, pp. 359–371). Virtual, Online: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-68766-3_28\">https://doi.org/10.1007/978-3-030-68766-3_28</a>","ama":"Pach J, Tardos G, Tóth G. Crossings between non-homotopic edges. In: <i>28th International Symposium on Graph Drawing and Network Visualization</i>. Vol 12590. LNCS. Springer Nature; 2020:359-371. doi:<a href=\"https://doi.org/10.1007/978-3-030-68766-3_28\">10.1007/978-3-030-68766-3_28</a>"},"date_updated":"2021-04-06T11:32:32Z","external_id":{"arxiv":["2006.14908"]},"day":"20","arxiv":1,"doi":"10.1007/978-3-030-68766-3_28","abstract":[{"lang":"eng","text":"We call a multigraph non-homotopic if it can be drawn in the plane in such a way that no two edges connecting the same pair of vertices can be continuously transformed into each other without passing through a vertex, and no loop can be shrunk to its end-vertex in the same way. It is easy to see that a non-homotopic multigraph on   n>1  vertices can have arbitrarily many edges. We prove that the number of crossings between the edges of a non-homotopic multigraph with n vertices and   m>4n  edges is larger than   cm2n  for some constant   c>0 , and that this bound is tight up to a polylogarithmic factor. We also show that the lower bound is not asymptotically sharp as n is fixed and   m⟶∞ ."}],"quality_controlled":"1","series_title":"LNCS","page":"359-371","publisher":"Springer Nature","scopus_import":"1","_id":"9299","author":[{"id":"E62E3130-B088-11EA-B919-BF823C25FEA4","full_name":"Pach, János","last_name":"Pach","first_name":"János"},{"first_name":"Gábor","last_name":"Tardos","full_name":"Tardos, Gábor"},{"last_name":"Tóth","first_name":"Géza","full_name":"Tóth, Géza"}],"department":[{"_id":"HeEd"}],"date_created":"2021-03-28T22:01:44Z","article_processing_charge":"No","publication_status":"published","intvolume":"     12590","title":"Crossings between non-homotopic edges","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2006.14908"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","type":"conference","date_published":"2020-09-20T00:00:00Z","publication_identifier":{"isbn":["9783030687656"],"eissn":["1611-3349"],"issn":["0302-9743"]},"oa":1,"language":[{"iso":"eng"}],"conference":{"name":"GD: Graph Drawing and Network Visualization","start_date":"2020-09-16","end_date":"2020-09-18","location":"Virtual, Online"},"publication":"28th International Symposium on Graph Drawing and Network Visualization","project":[{"grant_number":"Z00342","name":"The Wittgenstein Prize","_id":"268116B8-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa_version":"Preprint","month":"09"},{"publisher":"Springer Nature","editor":[{"first_name":"J","last_name":"Buchmann","full_name":"Buchmann, J"},{"first_name":"A","last_name":"Nitaj","full_name":"Nitaj, A"},{"full_name":"Rachidi, T","last_name":"Rachidi","first_name":"T"}],"page":"157-180","quality_controlled":"1","series_title":"LNCS","ec_funded":1,"publication_status":"published","department":[{"_id":"KrPi"}],"date_created":"2019-07-29T12:25:31Z","article_processing_charge":"No","title":"Sampling the integers with low relative error","intvolume":"     11627","_id":"6726","scopus_import":"1","author":[{"id":"488F98B0-F248-11E8-B48F-1D18A9856A87","last_name":"Walter","first_name":"Michael","full_name":"Walter, Michael","orcid":"0000-0003-3186-2482"}],"volume":11627,"doi":"10.1007/978-3-030-23696-0_9","day":"29","abstract":[{"text":"Randomness is an essential part of any secure cryptosystem, but many constructions rely on distributions that are not uniform. This is particularly true for lattice based cryptosystems, which more often than not make use of discrete Gaussian distributions over the integers. For practical purposes it is crucial to evaluate the impact that approximation errors have on the security of a scheme to provide the best possible trade-off between security and performance. Recent years have seen surprising results allowing to use relatively low precision while maintaining high levels of security. A key insight in these results is that sampling a distribution with low relative error can provide very strong security guarantees. Since floating point numbers provide guarantees on the relative approximation error, they seem a suitable tool in this setting, but it is not obvious which sampling algorithms can actually profit from them. While previous works have shown that inversion sampling can be adapted to provide a low relative error (Pöppelmann et al., CHES 2014; Prest, ASIACRYPT 2017), other works have called into question if this is possible for other sampling techniques (Zheng et al., Eprint report 2018/309). In this work, we consider all sampling algorithms that are popular in the cryptographic setting and analyze the relationship of floating point precision and the resulting relative error. We show that all of the algorithms either natively achieve a low relative error or can be adapted to do so.","lang":"eng"}],"date_updated":"2023-02-23T12:50:15Z","citation":{"ieee":"M. Walter, “Sampling the integers with low relative error,” in <i>Progress in Cryptology – AFRICACRYPT 2019</i>, vol. 11627, J. Buchmann, A. Nitaj, and T. Rachidi, Eds. Cham: Springer Nature, 2019, pp. 157–180.","chicago":"Walter, Michael. “Sampling the Integers with Low Relative Error.” In <i>Progress in Cryptology – AFRICACRYPT 2019</i>, edited by J Buchmann, A Nitaj, and T Rachidi, 11627:157–80. LNCS. Cham: Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-23696-0_9\">https://doi.org/10.1007/978-3-030-23696-0_9</a>.","ama":"Walter M. Sampling the integers with low relative error. In: Buchmann J, Nitaj A, Rachidi T, eds. <i>Progress in Cryptology – AFRICACRYPT 2019</i>. Vol 11627. LNCS. Cham: Springer Nature; 2019:157-180. doi:<a href=\"https://doi.org/10.1007/978-3-030-23696-0_9\">10.1007/978-3-030-23696-0_9</a>","apa":"Walter, M. (2019). Sampling the integers with low relative error. In J. Buchmann, A. Nitaj, &#38; T. Rachidi (Eds.), <i>Progress in Cryptology – AFRICACRYPT 2019</i> (Vol. 11627, pp. 157–180). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-23696-0_9\">https://doi.org/10.1007/978-3-030-23696-0_9</a>","ista":"Walter M. 2019.Sampling the integers with low relative error. In: Progress in Cryptology – AFRICACRYPT 2019. vol. 11627, 157–180.","short":"M. Walter, in:, J. Buchmann, A. Nitaj, T. Rachidi (Eds.), Progress in Cryptology – AFRICACRYPT 2019, Springer Nature, Cham, 2019, pp. 157–180.","mla":"Walter, Michael. “Sampling the Integers with Low Relative Error.” <i>Progress in Cryptology – AFRICACRYPT 2019</i>, edited by J Buchmann et al., vol. 11627, Springer Nature, 2019, pp. 157–80, doi:<a href=\"https://doi.org/10.1007/978-3-030-23696-0_9\">10.1007/978-3-030-23696-0_9</a>."},"year":"2019","conference":{"end_date":"2019-07-11","location":"Rabat, Morocco","name":"AFRICACRYPT: International Conference on Cryptology in Africa","start_date":"2019-07-09"},"language":[{"iso":"eng"}],"oa_version":"Preprint","project":[{"call_identifier":"H2020","_id":"258AA5B2-B435-11E9-9278-68D0E5697425","name":"Teaching Old Crypto New Tricks","grant_number":"682815"}],"month":"06","publication":"Progress in Cryptology – AFRICACRYPT 2019","main_file_link":[{"url":"https://eprint.iacr.org/2019/068","open_access":"1"}],"place":"Cham","status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication_identifier":{"isbn":["978-3-0302-3695-3"],"eisbn":["978-3-0302-3696-0"],"issn":["0302-9743","1611-3349"]},"oa":1,"date_published":"2019-06-29T00:00:00Z","type":"book_chapter"},{"file":[{"content_type":"application/pdf","file_name":"prob.pdf","date_updated":"2020-07-14T12:47:41Z","checksum":"45ebbc709af2b247d28c7c293c01504b","file_size":436635,"date_created":"2019-08-19T07:56:40Z","creator":"gavni","file_id":"6823","relation":"main_file","access_level":"open_access"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2019-09-06T00:00:00Z","type":"conference","publication_identifier":{"issn":["0302-9743"],"isbn":["978-303030805-6"]},"oa":1,"language":[{"iso":"eng"}],"conference":{"start_date":"2019-09-11","name":"RP: Reachability Problems","end_date":"2019-09-13","location":"Brussels, Belgium"},"publication":" Proceedings of the 13th International Conference of Reachability Problems","has_accepted_license":"1","oa_version":"Submitted Version","project":[{"grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"month":"09","volume":11674,"ddc":["000"],"date_updated":"2021-01-12T08:09:12Z","citation":{"ista":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov decision processes.  Proceedings of the 13th International Conference of Reachability Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.","mla":"Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” <i> Proceedings of the 13th International Conference of Reachability Problems</i>, vol. 11674, Springer, 2019, pp. 1–12, doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>.","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:,  Proceedings of the 13th International Conference of Reachability Problems, Springer, 2019, pp. 1–12.","ieee":"G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games on Markov decision processes,” in <i> Proceedings of the 13th International Conference of Reachability Problems</i>, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.","chicago":"Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding Games on Markov Decision Processes.” In <i> Proceedings of the 13th International Conference of Reachability Problems</i>, 11674:1–12. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision processes. In: <i> Proceedings of the 13th International Conference of Reachability Problems</i>. Vol 11674. Springer; 2019:1-12. doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>","apa":"Avni, G., Henzinger, T. A., Ibsen-Jensen, R., &#38; Novotny, P. (2019). Bidding games on Markov decision processes. In <i> Proceedings of the 13th International Conference of Reachability Problems</i> (Vol. 11674, pp. 1–12). Brussels, Belgium: Springer. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>"},"year":"2019","doi":"10.1007/978-3-030-30806-3_1","day":"06","abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the qualitative winner or quantitative payoff of the game. In bidding games, in each turn, we hold an auction between the two players to determine which player moves the token. Bidding games have largely been studied with concrete bidding mechanisms that are variants of a first-price auction: in each turn both players simultaneously submit bids, the higher\r\nbidder moves the token, and pays his bid to the lower bidder in Richman bidding, to the bank in poorman bidding, and in taxman bidding, the bid is split between the other player and the bank according to a predefined constant factor. Bidding games are deterministic games. They have an intriguing connection with a fragment of stochastic games called \r\n randomturn games. We study, for the first time, a combination of bidding games with probabilistic behavior; namely, we study bidding games that are played on Markov decision processes, where the players bid for the right to choose the next action, which determines the probability distribution according to which the next vertex is chosen. We study parity and meanpayoff bidding games on MDPs and extend results from the deterministic bidding setting to the probabilistic one."}],"page":"1-12","quality_controlled":"1","file_date_updated":"2020-07-14T12:47:41Z","publisher":"Springer","_id":"6822","scopus_import":1,"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Petr","last_name":"Novotny","full_name":"Novotny, Petr"}],"publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2019-08-19T07:58:10Z","alternative_title":["LNCS"],"title":"Bidding games on Markov decision processes","intvolume":"     11674"},{"publication_identifier":{"eisbn":["9783030302818"],"issn":["0302-9743"],"isbn":["9783030302801"]},"oa":1,"date_published":"2019-09-04T00:00:00Z","type":"conference","main_file_link":[{"url":"https://arxiv.org/abs/1906.08178","open_access":"1"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa_version":"Preprint","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"month":"09","publication":"16th International Conference on Quantitative Evaluation of Systems","conference":{"start_date":"2019-09-10","name":"QEST: Quantitative Evaluation of Systems","end_date":"2019-09-12","location":"Glasgow, United Kingdom"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-030-30281-8_7","arxiv":1,"day":"04","abstract":[{"text":"Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of   𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.","lang":"eng"}],"date_updated":"2025-06-02T08:53:47Z","citation":{"mla":"Ashok, Pranav, et al. “Strategy Representation by Decision Trees with Linear Classifiers.” <i>16th International Conference on Quantitative Evaluation of Systems</i>, vol. 11785, Springer Nature, 2019, pp. 109–28, doi:<a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">10.1007/978-3-030-30281-8_7</a>.","short":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, V. Toman, in:, 16th International Conference on Quantitative Evaluation of Systems, Springer Nature, 2019, pp. 109–128.","ista":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. 2019. Strategy representation by decision trees with linear classifiers. 16th International Conference on Quantitative Evaluation of Systems. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11785, 109–128.","ama":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. Strategy representation by decision trees with linear classifiers. In: <i>16th International Conference on Quantitative Evaluation of Systems</i>. Vol 11785. Springer Nature; 2019:109-128. doi:<a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">10.1007/978-3-030-30281-8_7</a>","apa":"Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C., &#38; Toman, V. (2019). Strategy representation by decision trees with linear classifiers. In <i>16th International Conference on Quantitative Evaluation of Systems</i> (Vol. 11785, pp. 109–128). Glasgow, United Kingdom: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">https://doi.org/10.1007/978-3-030-30281-8_7</a>","ieee":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, and V. Toman, “Strategy representation by decision trees with linear classifiers,” in <i>16th International Conference on Quantitative Evaluation of Systems</i>, Glasgow, United Kingdom, 2019, vol. 11785, pp. 109–128.","chicago":"Ashok, Pranav, Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Christoph Lampert, and Viktor Toman. “Strategy Representation by Decision Trees with Linear Classifiers.” In <i>16th International Conference on Quantitative Evaluation of Systems</i>, 11785:109–28. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">https://doi.org/10.1007/978-3-030-30281-8_7</a>."},"year":"2019","isi":1,"external_id":{"arxiv":["1906.08178"],"isi":["000679281300007"]},"volume":11785,"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ChLa"}],"date_created":"2019-10-14T06:57:49Z","article_processing_charge":"No","title":"Strategy representation by decision trees with linear classifiers","alternative_title":["LNCS"],"intvolume":"     11785","_id":"6942","scopus_import":"1","author":[{"first_name":"Pranav","last_name":"Ashok","full_name":"Ashok, Pranav"},{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Jan","last_name":"Křetínský","full_name":"Křetínský, Jan"},{"orcid":"0000-0001-8622-7887","full_name":"Lampert, Christoph","first_name":"Christoph","last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Toman","first_name":"Viktor","full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer Nature","page":"109-128","quality_controlled":"1"},{"conference":{"start_date":"2019-09-18","name":"CMSB: Computational Methods in Systems Biology","end_date":"2019-09-20","location":"Trieste, Italy"},"language":[{"iso":"eng"}],"month":"09","oa_version":"None","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"24573","name":"Design principles underlying genetic switch architecture","_id":"251EE76E-B435-11E9-9278-68D0E5697425"}],"publication":"17th International Conference on Computational Methods in Systems Biology","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_identifier":{"isbn":["9783030313036","9783030313043"],"issn":["0302-9743"],"eissn":["1611-3349"]},"date_published":"2019-09-17T00:00:00Z","type":"conference","publisher":"Springer Nature","page":"155-187","quality_controlled":"1","alternative_title":["LNCS"],"title":"Transient memory in gene regulation","intvolume":"     11773","publication_status":"published","date_created":"2019-12-04T16:07:50Z","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"article_processing_charge":"No","author":[{"full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","last_name":"Guet","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Igler, Claudia","last_name":"Igler","first_name":"Claudia","id":"46613666-F248-11E8-B48F-1D18A9856A87"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","last_name":"Petrov","first_name":"Tatjana"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali","first_name":"Ali","last_name":"Sezgin"}],"_id":"7147","scopus_import":"1","volume":11773,"abstract":[{"lang":"eng","text":"The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets.\r\n\r\nIn this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest.\r\n\r\nThe behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions."}],"doi":"10.1007/978-3-030-31304-3_9","day":"17","isi":1,"external_id":{"isi":["000557875100009"]},"date_updated":"2023-09-06T11:18:08Z","year":"2019","citation":{"ista":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. 2019. Transient memory in gene regulation. 17th International Conference on Computational Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNCS, vol. 11773, 155–187.","mla":"Guet, Calin C., et al. “Transient Memory in Gene Regulation.” <i>17th International Conference on Computational Methods in Systems Biology</i>, vol. 11773, Springer Nature, 2019, pp. 155–87, doi:<a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">10.1007/978-3-030-31304-3_9</a>.","short":"C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International Conference on Computational Methods in Systems Biology, Springer Nature, 2019, pp. 155–187.","ieee":"C. C. Guet, T. A. Henzinger, C. Igler, T. Petrov, and A. Sezgin, “Transient memory in gene regulation,” in <i>17th International Conference on Computational Methods in Systems Biology</i>, Trieste, Italy, 2019, vol. 11773, pp. 155–187.","chicago":"Guet, Calin C, Thomas A Henzinger, Claudia Igler, Tatjana Petrov, and Ali Sezgin. “Transient Memory in Gene Regulation.” In <i>17th International Conference on Computational Methods in Systems Biology</i>, 11773:155–87. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">https://doi.org/10.1007/978-3-030-31304-3_9</a>.","apa":"Guet, C. C., Henzinger, T. A., Igler, C., Petrov, T., &#38; Sezgin, A. (2019). Transient memory in gene regulation. In <i>17th International Conference on Computational Methods in Systems Biology</i> (Vol. 11773, pp. 155–187). Trieste, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">https://doi.org/10.1007/978-3-030-31304-3_9</a>","ama":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. Transient memory in gene regulation. In: <i>17th International Conference on Computational Methods in Systems Biology</i>. Vol 11773. Springer Nature; 2019:155-187. doi:<a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">10.1007/978-3-030-31304-3_9</a>"}},{"volume":11757,"isi":1,"external_id":{"isi":["000570006300017"]},"date_updated":"2023-09-06T11:24:10Z","year":"2019","citation":{"apa":"Ničković, D., Qin, X., Ferrere, T., Mateis, C., &#38; Deshmukh, J. (2019). Shape expressions for specifying and extracting signal features. In <i>19th International Conference on Runtime Verification</i> (Vol. 11757, pp. 292–309). Porto, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>","ama":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for specifying and extracting signal features. In: <i>19th International Conference on Runtime Verification</i>. Vol 11757. Springer Nature; 2019:292-309. doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>","chicago":"Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In <i>19th International Conference on Runtime Verification</i>, 11757:292–309. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>.","ieee":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions for specifying and extracting signal features,” in <i>19th International Conference on Runtime Verification</i>, Porto, Portugal, 2019, vol. 11757, pp. 292–309.","mla":"Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal Features.” <i>19th International Conference on Runtime Verification</i>, vol. 11757, Springer Nature, 2019, pp. 292–309, doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>.","short":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309.","ista":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. 2019. Shape expressions for specifying and extracting signal features. 19th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 11757, 292–309."},"abstract":[{"lang":"eng","text":"Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. "}],"doi":"10.1007/978-3-030-32079-9_17","day":"01","page":"292-309","quality_controlled":"1","publisher":"Springer Nature","author":[{"last_name":"Ničković","first_name":"Dejan","full_name":"Ničković, Dejan"},{"last_name":"Qin","first_name":"Xin","full_name":"Qin, Xin"},{"last_name":"Ferrere","first_name":"Thomas","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Mateis","first_name":"Cristinel","full_name":"Mateis, Cristinel"},{"last_name":"Deshmukh","first_name":"Jyotirmoy","full_name":"Deshmukh, Jyotirmoy"}],"_id":"7159","scopus_import":"1","alternative_title":["LNCS"],"title":"Shape expressions for specifying and extracting signal features","intvolume":"     11757","publication_status":"published","date_created":"2019-12-09T08:47:55Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_published":"2019-10-01T00:00:00Z","type":"conference","publication_identifier":{"isbn":["9783030320782","9783030320799"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"conference":{"start_date":"2019-10-08","name":"RV: Runtime Verification","location":"Porto, Portugal","end_date":"2019-10-11"},"publication":"19th International Conference on Runtime Verification","month":"10","oa_version":"None","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"}]},{"publication":"25th Anniversary of Euro-Par","oa_version":"None","month":"08","language":[{"iso":"eng"}],"conference":{"end_date":"2019-08-30","location":"Göttingen, Germany","name":"Euro-Par: European Conference on Parallel Processing","start_date":"2019-08-26"},"type":"conference","date_published":"2019-08-13T00:00:00Z","publication_identifier":{"isbn":["978-3-0302-9399-4"],"eissn":["1611-3349"],"issn":["0302-9743"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","scopus_import":"1","_id":"7228","author":[{"full_name":"Koval, Nikita","last_name":"Koval","first_name":"Nikita","id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Alistarh, Dan-Adrian","orcid":"0000-0003-3650-940X","last_name":"Alistarh","first_name":"Dan-Adrian","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Elizarov, Roman","first_name":"Roman","last_name":"Elizarov"}],"date_created":"2020-01-05T23:00:46Z","article_processing_charge":"No","department":[{"_id":"DaAl"}],"publication_status":"published","intvolume":"     11725","alternative_title":["LNCS"],"title":"Scalable FIFO channels for programming via communicating sequential processes","quality_controlled":"1","page":"317-333","publisher":"Springer Nature","year":"2019","citation":{"ista":"Koval N, Alistarh D-A, Elizarov R. 2019. Scalable FIFO channels for programming via communicating sequential processes. 25th Anniversary of Euro-Par. Euro-Par: European Conference on Parallel Processing, LNCS, vol. 11725, 317–333.","mla":"Koval, Nikita, et al. “Scalable FIFO Channels for Programming via Communicating Sequential Processes.” <i>25th Anniversary of Euro-Par</i>, vol. 11725, Springer Nature, 2019, pp. 317–33, doi:<a href=\"https://doi.org/10.1007/978-3-030-29400-7_23\">10.1007/978-3-030-29400-7_23</a>.","short":"N. Koval, D.-A. Alistarh, R. Elizarov, in:, 25th Anniversary of Euro-Par, Springer Nature, 2019, pp. 317–333.","ieee":"N. Koval, D.-A. Alistarh, and R. Elizarov, “Scalable FIFO channels for programming via communicating sequential processes,” in <i>25th Anniversary of Euro-Par</i>, Göttingen, Germany, 2019, vol. 11725, pp. 317–333.","chicago":"Koval, Nikita, Dan-Adrian Alistarh, and Roman Elizarov. “Scalable FIFO Channels for Programming via Communicating Sequential Processes.” In <i>25th Anniversary of Euro-Par</i>, 11725:317–33. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29400-7_23\">https://doi.org/10.1007/978-3-030-29400-7_23</a>.","apa":"Koval, N., Alistarh, D.-A., &#38; Elizarov, R. (2019). Scalable FIFO channels for programming via communicating sequential processes. In <i>25th Anniversary of Euro-Par</i> (Vol. 11725, pp. 317–333). Göttingen, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29400-7_23\">https://doi.org/10.1007/978-3-030-29400-7_23</a>","ama":"Koval N, Alistarh D-A, Elizarov R. Scalable FIFO channels for programming via communicating sequential processes. In: <i>25th Anniversary of Euro-Par</i>. Vol 11725. Springer Nature; 2019:317-333. doi:<a href=\"https://doi.org/10.1007/978-3-030-29400-7_23\">10.1007/978-3-030-29400-7_23</a>"},"date_updated":"2023-09-06T14:53:59Z","external_id":{"isi":["000851061400023"]},"isi":1,"day":"13","doi":"10.1007/978-3-030-29400-7_23","abstract":[{"lang":"eng","text":"Traditional concurrent programming involves manipulating shared mutable state. Alternatives to this programming style are communicating sequential processes (CSP) and actor models, which share data via explicit communication. These models have been known for almost half a century, and have recently had started to gain significant traction among modern programming languages. The common abstraction for communication between several processes is the channel. Although channels are similar to producer-consumer data structures, they have different semantics and support additional operations, such as the select expression. Despite their growing popularity, most known implementations of channels use lock-based data structures and can be rather inefficient.\r\n\r\nIn this paper, we present the first efficient lock-free algorithm for implementing a communication channel for CSP programming. We provide implementations and experimental results in the Kotlin and Go programming languages. Our new algorithm outperforms existing implementations on many workloads, while providing non-blocking progress guarantee. Our design can serve as an example of how to construct general communication data structures for CSP and actor models. "}],"volume":11725},{"language":[{"iso":"eng"}],"conference":{"end_date":"2019-09-20","location":"Prague, Czech Republic","name":"GD: Graph Drawing and Network Visualization","start_date":"2019-09-17"},"publication":"27th International Symposium on Graph Drawing and Network Visualization","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"}],"oa_version":"Preprint","month":"11","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1908.08129"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","type":"conference","date_published":"2019-11-28T00:00:00Z","publication_identifier":{"isbn":["978-3-0303-5801-3"],"issn":["0302-9743"],"eissn":["1611-3349"]},"oa":1,"ec_funded":1,"quality_controlled":"1","page":"230-243","publisher":"Springer Nature","scopus_import":"1","_id":"7230","author":[{"id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2401-8670","full_name":"Arroyo Guevara, Alan M","first_name":"Alan M","last_name":"Arroyo Guevara"},{"full_name":"Derka, Martin","last_name":"Derka","first_name":"Martin"},{"full_name":"Parada, Irene","first_name":"Irene","last_name":"Parada"}],"department":[{"_id":"UlWa"}],"date_created":"2020-01-05T23:00:47Z","article_processing_charge":"No","publication_status":"published","intvolume":"     11904","alternative_title":["LNCS"],"title":"Extending simple drawings","volume":11904,"citation":{"apa":"Arroyo Guevara, A. M., Derka, M., &#38; Parada, I. (2019). Extending simple drawings. In <i>27th International Symposium on Graph Drawing and Network Visualization</i> (Vol. 11904, pp. 230–243). Prague, Czech Republic: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-35802-0_18\">https://doi.org/10.1007/978-3-030-35802-0_18</a>","ama":"Arroyo Guevara AM, Derka M, Parada I. Extending simple drawings. In: <i>27th International Symposium on Graph Drawing and Network Visualization</i>. Vol 11904. Springer Nature; 2019:230-243. doi:<a href=\"https://doi.org/10.1007/978-3-030-35802-0_18\">10.1007/978-3-030-35802-0_18</a>","ieee":"A. M. Arroyo Guevara, M. Derka, and I. Parada, “Extending simple drawings,” in <i>27th International Symposium on Graph Drawing and Network Visualization</i>, Prague, Czech Republic, 2019, vol. 11904, pp. 230–243.","chicago":"Arroyo Guevara, Alan M, Martin Derka, and Irene Parada. “Extending Simple Drawings.” In <i>27th International Symposium on Graph Drawing and Network Visualization</i>, 11904:230–43. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-35802-0_18\">https://doi.org/10.1007/978-3-030-35802-0_18</a>.","mla":"Arroyo Guevara, Alan M., et al. “Extending Simple Drawings.” <i>27th International Symposium on Graph Drawing and Network Visualization</i>, vol. 11904, Springer Nature, 2019, pp. 230–43, doi:<a href=\"https://doi.org/10.1007/978-3-030-35802-0_18\">10.1007/978-3-030-35802-0_18</a>.","short":"A.M. Arroyo Guevara, M. Derka, I. Parada, in:, 27th International Symposium on Graph Drawing and Network Visualization, Springer Nature, 2019, pp. 230–243.","ista":"Arroyo Guevara AM, Derka M, Parada I. 2019. Extending simple drawings. 27th International Symposium on Graph Drawing and Network Visualization. GD: Graph Drawing and Network Visualization, LNCS, vol. 11904, 230–243."},"year":"2019","date_updated":"2023-09-06T14:56:00Z","external_id":{"arxiv":["1908.08129"],"isi":["000612918800018"]},"isi":1,"day":"28","arxiv":1,"doi":"10.1007/978-3-030-35802-0_18","abstract":[{"text":"Simple drawings of graphs are those in which each pair of edges share at most one point, either a common endpoint or a proper crossing. In this paper we study the problem of extending a simple drawing D(G) of a graph G by inserting a set of edges from the complement of G into D(G) such that the result is a simple drawing. In the context of rectilinear drawings, the problem is trivial. For pseudolinear drawings, the existence of such an extension follows from Levi’s enlargement lemma. In contrast, we prove that deciding if a given set of edges can be inserted into a simple drawing is NP-complete. Moreover, we show that the maximization version of the problem is APX-hard. We also present a polynomial-time algorithm for deciding whether one edge uv can be inserted into D(G) when {u,v} is a dominating set for the graph G.","lang":"eng"}]},{"conference":{"start_date":"2019-08-27","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","location":"Amsterdam, The Netherlands","end_date":"2019-08-29"},"language":[{"iso":"eng"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"oa_version":"Preprint","month":"08","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1907.11514"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_identifier":{"isbn":["978-3-0302-9661-2"],"eissn":["1611-3349"],"issn":["0302-9743"]},"oa":1,"type":"conference","date_published":"2019-08-13T00:00:00Z","publisher":"Springer Nature","quality_controlled":"1","page":"123-141","date_created":"2020-01-05T23:00:47Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","intvolume":"     11750","title":"Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty","alternative_title":["LNCS"],"scopus_import":"1","_id":"7231","author":[{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","full_name":"Kong, Hui","orcid":"0000-0002-3066-6941","last_name":"Kong","first_name":"Hui"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"full_name":"Jiang, Yu","last_name":"Jiang","first_name":"Yu"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"volume":11750,"day":"13","arxiv":1,"doi":"10.1007/978-3-030-29662-9_8","abstract":[{"lang":"eng","text":"Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature."}],"year":"2019","citation":{"ieee":"H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 123–141.","chicago":"Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:123–41. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>.","apa":"Kong, H., Bartocci, E., Jiang, Y., &#38; Henzinger, T. A. (2019). Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>","ama":"Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:123-141. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>","ista":"Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11750, 123–141.","short":"H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.","mla":"Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>."},"date_updated":"2023-09-06T14:55:15Z","external_id":{"isi":["000611677700008"],"arxiv":["1907.11514"]},"isi":1},{"doi":"10.1007/978-3-030-29662-9_4","day":"13","abstract":[{"lang":"eng","text":"We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. "}],"date_updated":"2023-09-06T14:57:17Z","citation":{"chicago":"Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal Logic.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:59–75. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>.","ieee":"T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.","apa":"Ferrere, T., Maler, O., &#38; Nickovic, D. (2019). Mixed-time signal temporal logic. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>","ama":"Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:59-75. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>","ista":"Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.","short":"T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.","mla":"Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 59–75, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>."},"year":"2019","isi":1,"external_id":{"isi":["000611677700004"]},"volume":11750,"publication_status":"published","date_created":"2020-01-05T23:00:48Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"title":"Mixed-time signal temporal logic","alternative_title":["LNCS"],"intvolume":"     11750","_id":"7232","scopus_import":"1","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","first_name":"Thomas","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143"},{"full_name":"Maler, Oded","first_name":"Oded","last_name":"Maler"},{"last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer Nature","page":"59-75","quality_controlled":"1","publication_identifier":{"isbn":["978-3-0302-9661-2"],"issn":["0302-9743"],"eissn":["1611-3349"]},"date_published":"2019-08-13T00:00:00Z","type":"conference","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","oa_version":"None","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"month":"08","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","conference":{"start_date":"2019-08-27","name":"FORMATS: Formal Modeling and Anaysis of Timed Systems","location":"Amsterdam, The Netherlands","end_date":"2019-08-29"},"language":[{"iso":"eng"}]}]