[{"title":"Stateless model checking under a reads-value-from equivalence","author":[{"first_name":"Pratyush","last_name":"Agarwal","full_name":"Agarwal, Pratyush"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Shreya","full_name":"Pathak, Shreya","last_name":"Pathak"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"article_processing_charge":"Yes","external_id":{"arxiv":["2105.06424"],"isi":["000698732400016"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” 33rd International Conference on Computer-Aided Verification , vol. 12759, Springer Nature, 2021, pp. 341–66, doi:10.1007/978-3-030-81685-8_16.","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., & Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In 33rd International Conference on Computer-Aided Verification (Vol. 12759, pp. 341–366). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-81685-8_16","ama":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: 33rd International Conference on Computer-Aided Verification . Vol 12759. Springer Nature; 2021:341-366. doi:10.1007/978-3-030-81685-8_16","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in 33rd International Conference on Computer-Aided Verification , Virtual, 2021, vol. 12759, pp. 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.","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In 33rd International Conference on Computer-Aided Verification , 12759:341–66. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-81685-8_16.","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."},"project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"doi":"10.1007/978-3-030-81685-8_16","date_published":"2021-07-15T00:00:00Z","date_created":"2021-09-05T22:01:24Z","page":"341-366","day":"15","publication":"33rd International Conference on Computer-Aided Verification ","has_accepted_license":"1","isi":1,"year":"2021","publisher":"Springer Nature","quality_controlled":"1","oa":1,"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.","department":[{"_id":"KrCh"}],"file_date_updated":"2022-05-13T07:00:20Z","ddc":["000"],"date_updated":"2023-09-07T13:30:27Z","status":"public","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2021-07-20","end_date":"2021-07-23","location":"Virtual","name":"CAV: Computer Aided Verification "},"_id":"9987","related_material":{"record":[{"id":"10199","status":"public","relation":"dissertation_contains"}]},"volume":"12759 ","ec_funded":1,"file":[{"file_name":"2021_LNCS_Agarwal.pdf","date_created":"2022-05-13T07:00:20Z","file_size":1516756,"date_updated":"2022-05-13T07:00:20Z","creator":"dernst","success":1,"file_id":"11368","checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["978-3-030-81684-1"],"eisbn":["978-3-030-81685-8"]},"publication_status":"published","month":"07","scopus_import":"1","alternative_title":["LNCS"],"oa_version":"Published Version","abstract":[{"lang":"eng","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."}]},{"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"file_date_updated":"2021-11-04T07:24:48Z","ddc":["000"],"date_updated":"2023-09-07T13:30:27Z","keyword":["safety","risk","reliability and quality","software"],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","article_type":"original","_id":"10191","ec_funded":1,"issue":"OOPSLA","related_material":{"record":[{"relation":"dissertation_contains","id":"10199","status":"public"}]},"volume":5,"language":[{"iso":"eng"}],"file":[{"success":1,"file_id":"10215","checksum":"9d6dce7b611853c529bb7b1915ac579e","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2021_ProcACMPL_Bui.pdf","date_created":"2021-11-04T07:24:48Z","creator":"cchlebak","file_size":2903485,"date_updated":"2021-11-04T07:24:48Z"}],"publication_status":"published","publication_identifier":{"eissn":["2475-1421"]},"intvolume":" 5","month":"10","scopus_import":"1","oa_version":"Published Version","abstract":[{"text":"In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of n events over k threads and d variables, we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k· d) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when k is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.\r\n\r\n","lang":"eng"}],"title":"The reads-from equivalence for the TSO and PSO memory models","external_id":{"arxiv":["2011.11763"]},"article_processing_charge":"No","author":[{"last_name":"Bui","full_name":"Bui, Truc Lam","first_name":"Truc Lam"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Tushar","full_name":"Gautam, Tushar","last_name":"Gautam"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"ista":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 5(OOPSLA), 164.","chicago":"Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2021. https://doi.org/10.1145/3485541.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).","ieee":"T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from equivalence for the TSO and PSO memory models,” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.","apa":"Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., & Toman, V. (2021). The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3485541","ama":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 2021;5(OOPSLA). doi:10.1145/3485541","mla":"Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA, 164, Association for Computing Machinery, 2021, doi:10.1145/3485541."},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"article_number":"164","date_created":"2021-10-27T15:05:34Z","date_published":"2021-10-15T00:00:00Z","doi":"10.1145/3485541","publication":"Proceedings of the ACM on Programming Languages","day":"15","year":"2021","has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Association for Computing Machinery","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003."},{"degree_awarded":"PhD","publication_status":"published","publication_identifier":{"issn":["2663-337X"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2021-11-08T14:12:22Z","file_name":"toman_th_final.pdf","creator":"vtoman","date_updated":"2021-11-08T14:12:22Z","file_size":2915234,"file_id":"10225","checksum":"4f412a1ee60952221b499a4b1268df35","access_level":"open_access","relation":"main_file","content_type":"application/pdf"},{"date_created":"2021-11-08T14:12:46Z","file_name":"toman_thesis.zip","date_updated":"2021-11-09T09:00:50Z","file_size":8616056,"creator":"vtoman","file_id":"10226","checksum":"9584943f99127be2dd2963f6784c37d4","content_type":"application/zip","access_level":"closed","relation":"source_file"}],"ec_funded":1,"related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"10190"},{"relation":"part_of_dissertation","status":"public","id":"10191"},{"status":"public","id":"9987","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"141","status":"public"}]},"acknowledged_ssus":[{"_id":"SSU"}],"abstract":[{"text":"The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["ISTA Thesis"],"month":"10","date_updated":"2023-09-19T09:59:54Z","supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"ddc":["000"],"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"file_date_updated":"2021-11-09T09:00:50Z","_id":"10199","type":"dissertation","keyword":["concurrency","verification","model checking"],"status":"public","year":"2021","has_accepted_license":"1","day":"31","page":"166","date_created":"2021-10-29T20:09:01Z","date_published":"2021-10-31T00:00:00Z","doi":"10.15479/at:ista:10199","oa":1,"publisher":"Institute of Science and Technology Austria","citation":{"ista":"Toman V. 2021. Improved verification techniques for concurrent systems. Institute of Science and Technology Austria.","chicago":"Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/at:ista:10199.","ieee":"V. Toman, “Improved verification techniques for concurrent systems,” Institute of Science and Technology Austria, 2021.","short":"V. Toman, Improved Verification Techniques for Concurrent Systems, Institute of Science and Technology Austria, 2021.","ama":"Toman V. Improved verification techniques for concurrent systems. 2021. doi:10.15479/at:ista:10199","apa":"Toman, V. (2021). Improved verification techniques for concurrent systems. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:10199","mla":"Toman, Viktor. Improved Verification Techniques for Concurrent Systems. Institute of Science and Technology Austria, 2021, doi:10.15479/at:ista:10199."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","author":[{"last_name":"Toman","full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor"}],"title":"Improved verification techniques for concurrent systems","project":[{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Rigorous Systems Engineering"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}]},{"quality_controlled":"1","publisher":"Elsevier","oa":1,"doi":"10.1016/j.artint.2021.103499","date_published":"2021-03-16T00:00:00Z","date_created":"2021-03-28T22:01:40Z","isi":1,"year":"2021","day":"16","publication":"Artificial Intelligence","article_number":"103499","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Wolfgang","full_name":"Dvořák, Wolfgang","last_name":"Dvořák"},{"first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530"},{"last_name":"Svozil","full_name":"Svozil, Alexander","first_name":"Alexander"}],"external_id":{"isi":["000657537500003"],"arxiv":["1804.07031"]},"article_processing_charge":"No","title":"Algorithms and conditional lower bounds for planning problems","citation":{"mla":"Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for Planning Problems.” Artificial Intelligence, vol. 297, no. 8, 103499, Elsevier, 2021, doi:10.1016/j.artint.2021.103499.","ieee":"K. Chatterjee, W. Dvořák, M. H. Henzinger, and A. Svozil, “Algorithms and conditional lower bounds for planning problems,” Artificial Intelligence, vol. 297, no. 8. Elsevier, 2021.","short":"K. Chatterjee, W. Dvořák, M.H. Henzinger, A. Svozil, Artificial Intelligence 297 (2021).","apa":"Chatterjee, K., Dvořák, W., Henzinger, M. H., & Svozil, A. (2021). Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2021.103499","ama":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. 2021;297(8). doi:10.1016/j.artint.2021.103499","chicago":"Chatterjee, Krishnendu, Wolfgang Dvořák, Monika H Henzinger, and Alexander Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” Artificial Intelligence. Elsevier, 2021. https://doi.org/10.1016/j.artint.2021.103499.","ista":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. 2021. Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. 297(8), 103499."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.07031"}],"month":"03","intvolume":" 297","abstract":[{"text":"We consider planning problems for graphs, Markov Decision Processes (MDPs), and games on graphs in an explicit state space. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems with k different target sets: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in a given sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds, based on the boolean matrix multiplication (BMM) conjecture and strong exponential time hypothesis (SETH), establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs, and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) problem-separation results showing that for MDPs the coverage problem is harder than the sequential target problem.","lang":"eng"}],"oa_version":"Preprint","issue":"8","volume":297,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"35"}]},"publication_identifier":{"issn":["0004-3702"]},"publication_status":"published","language":[{"iso":"eng"}],"type":"journal_article","article_type":"original","status":"public","_id":"9293","department":[{"_id":"KrCh"}],"date_updated":"2023-09-26T10:41:42Z"},{"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 57, 401–428.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design. Springer, 2021. https://doi.org/10.1007/s10703-021-00373-5.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-021-00373-5","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 2021;57:401-428. doi:10.1007/s10703-021-00373-5","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” Formal Methods in System Design, vol. 57. Springer, pp. 401–428, 2021.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design, vol. 57, Springer, 2021, pp. 401–28, doi:10.1007/s10703-021-00373-5."},"title":"Faster algorithms for quantitative verification in bounded treewidth graphs","article_processing_charge":"No","external_id":{"arxiv":["1504.07384"],"isi":["000645490300001"]},"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","oa":1,"quality_controlled":"1","publisher":"Springer","publication":"Formal Methods in System Design","day":"01","year":"2021","isi":1,"date_created":"2021-05-16T22:01:47Z","doi":"10.1007/s10703-021-00373-5","date_published":"2021-09-01T00:00:00Z","page":"401-428","_id":"9393","status":"public","article_type":"original","type":"journal_article","date_updated":"2023-10-10T11:13:20Z","department":[{"_id":"KrCh"}],"oa_version":"Preprint","abstract":[{"text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.","lang":"eng"}],"intvolume":" 57","month":"09","main_file_link":[{"url":"https://arxiv.org/abs/1504.07384","open_access":"1"}],"scopus_import":"1","language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"ec_funded":1,"volume":57}]