[{"publisher":"Springer","article_type":"original","page":"401-428","ec_funded":1,"quality_controlled":"1","publication_status":"published","date_created":"2021-05-16T22:01:47Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","title":"Faster algorithms for quantitative verification in bounded treewidth graphs","intvolume":"        57","_id":"9393","scopus_import":"1","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"volume":57,"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.","arxiv":1,"doi":"10.1007/s10703-021-00373-5","day":"01","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"}],"date_updated":"2023-10-10T11:13:20Z","year":"2021","citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System Design</i>, vol. 57. Springer, pp. 401–428, 2021.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>. Springer, 2021. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. 2021;57:401-428. doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>","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.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57, Springer, 2021, pp. 401–28, doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428."},"isi":1,"external_id":{"isi":["000645490300001"],"arxiv":["1504.07384"]},"language":[{"iso":"eng"}],"oa_version":"Preprint","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"month":"09","publication":"Formal Methods in System Design","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.07384"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"oa":1,"date_published":"2021-09-01T00:00:00Z","type":"journal_article"},{"date_updated":"2024-01-10T11:50:31Z","citation":{"ista":"Henzinger TA, Kupferman O, Qadeer S. 2003. From pre-historic to post-modern symbolic model checking. Formal Methods in System Design. 23(3), 303–327.","mla":"Henzinger, Thomas A., et al. “From Pre-Historic to Post-Modern Symbolic Model Checking.” <i>Formal Methods in System Design</i>, vol. 23, no. 3, Springer, 2003, pp. 303–27, doi:<a href=\"https://doi.org/10.1023/A:1026228213080\">10.1023/A:1026228213080</a>.","short":"T.A. Henzinger, O. Kupferman, S. Qadeer, Formal Methods in System Design 23 (2003) 303–327.","ieee":"T. A. Henzinger, O. Kupferman, and S. Qadeer, “From pre-historic to post-modern symbolic model checking,” <i>Formal Methods in System Design</i>, vol. 23, no. 3. Springer, pp. 303–327, 2003.","chicago":"Henzinger, Thomas A, Orna Kupferman, and Shaz Qadeer. “From Pre-Historic to Post-Modern Symbolic Model Checking.” <i>Formal Methods in System Design</i>. Springer, 2003. <a href=\"https://doi.org/10.1023/A:1026228213080\">https://doi.org/10.1023/A:1026228213080</a>.","apa":"Henzinger, T. A., Kupferman, O., &#38; Qadeer, S. (2003). From pre-historic to post-modern symbolic model checking. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1023/A:1026228213080\">https://doi.org/10.1023/A:1026228213080</a>","ama":"Henzinger TA, Kupferman O, Qadeer S. From pre-historic to post-modern symbolic model checking. <i>Formal Methods in System Design</i>. 2003;23(3):303-327. doi:<a href=\"https://doi.org/10.1023/A:1026228213080\">10.1023/A:1026228213080</a>"},"year":"2003","abstract":[{"text":"Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating expressions that represent state sets. Traditionally, symbolic model-checking tools are based on back- ward state traversal; their basic operation is the function pre, which, given a set of states, returns the set of all predecessor states. This is because specifiers usually employ formalisms with future-time modalities, which are naturally evaluated by iterating applications of pre. It has been shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which, given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only parts of the state space that are reachable from an initial state and relevant for the satisfaction or violation of the specification are explored; that is, errors can be detected as soon as possible.\r\nIn this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two μ-calculi. The pre-μ calculus is based on the pre operation, and the post-μ calculus is based on the post operation. These two μ-calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all ω-regular (linear-time) specifications can be expressed as post-μ queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.","lang":"eng"}],"doi":"10.1023/A:1026228213080","day":"20","extern":"1","acknowledgement":"This research was supported in part by the SRC contract 99-TJ-683.003 and the NSF grant CCR-9988172.","volume":23,"author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"}],"issue":"3","_id":"4460","scopus_import":"1","title":"From pre-historic to post-modern symbolic model checking","intvolume":"        23","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:08:58Z","page":"303 - 327","quality_controlled":"1","article_type":"original","publisher":"Springer","date_published":"2003-06-20T00:00:00Z","type":"journal_article","publist_id":"268","publication_identifier":{"issn":["0925-9856"]},"status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication":"Formal Methods in System Design","month":"06","oa_version":"None","language":[{"iso":"eng"}]},{"date_updated":"2023-05-08T12:22:38Z","citation":{"ista":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 2001. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design. 18(2), 97–116.","short":"R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, Formal Methods in System Design 18 (2001) 97–116.","mla":"Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.” <i>Formal Methods in System Design</i>, vol. 18, no. 2, Springer, 2001, pp. 97–116, doi:<a href=\"https://doi.org/10.1023/A:1008767206905\">10.1023/A:1008767206905</a>.","chicago":"Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” <i>Formal Methods in System Design</i>. Springer, 2001. <a href=\"https://doi.org/10.1023/A:1008767206905\">https://doi.org/10.1023/A:1008767206905</a>.","ieee":"R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order reduction in symbolic state-space exploration,” <i>Formal Methods in System Design</i>, vol. 18, no. 2. Springer, pp. 97–116, 2001.","ama":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction in symbolic state-space exploration. <i>Formal Methods in System Design</i>. 2001;18(2):97-116. doi:<a href=\"https://doi.org/10.1023/A:1008767206905\">10.1023/A:1008767206905</a>","apa":"Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (2001). Partial-order reduction in symbolic state-space exploration. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1023/A:1008767206905\">https://doi.org/10.1023/A:1008767206905</a>"},"year":"2001","doi":"10.1023/A:1008767206905","day":"01","abstract":[{"text":"State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.","lang":"eng"}],"acknowledgement":"Gerard Holzmann provided us with information on SPIN. Ken McMillan and Doron Peled contributed through discussions. The VIS group at UC Berkeley and Rajeev Ranjan in particular helped with the experiments.","volume":18,"extern":"1","_id":"4599","scopus_import":"1","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"last_name":"Brayton","first_name":"Robert","full_name":"Brayton, Robert"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"},{"full_name":"Rajamani, Sriram","last_name":"Rajamani","first_name":"Sriram"}],"issue":"2","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:41Z","title":"Partial-order reduction in symbolic state-space exploration","intvolume":"        18","page":"97 - 116","quality_controlled":"1","publisher":"Springer","article_type":"original","date_published":"2001-03-01T00:00:00Z","type":"journal_article","publication_identifier":{"issn":["0925-9856"]},"publist_id":"108","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication":"Formal Methods in System Design","oa_version":"None","month":"03","language":[{"iso":"eng"}]},{"doi":"10.1023/A:1008739929481","day":"01","abstract":[{"lang":"eng","text":"We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise-refinement) design and verification. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchronous message-passing protocols.\r\n"}],"date_updated":"2022-09-02T08:45:58Z","citation":{"mla":"Alur, Rajeev, and Thomas A. Henzinger. “Reactive Modules.” <i>Formal Methods in System Design</i>, vol. 15, no. 1, Springer, 1999, pp. 7–48, doi:<a href=\"https://doi.org/10.1023/A:1008739929481\">10.1023/A:1008739929481</a>.","short":"R. Alur, T.A. Henzinger, Formal Methods in System Design 15 (1999) 7–48.","ista":"Alur R, Henzinger TA. 1999. Reactive modules. Formal Methods in System Design. 15(1), 7–48.","ama":"Alur R, Henzinger TA. Reactive modules. <i>Formal Methods in System Design</i>. 1999;15(1):7-48. doi:<a href=\"https://doi.org/10.1023/A:1008739929481\">10.1023/A:1008739929481</a>","apa":"Alur, R., &#38; Henzinger, T. A. (1999). Reactive modules. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1023/A:1008739929481\">https://doi.org/10.1023/A:1008739929481</a>","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Reactive Modules.” <i>Formal Methods in System Design</i>. Springer, 1999. <a href=\"https://doi.org/10.1023/A:1008739929481\">https://doi.org/10.1023/A:1008739929481</a>.","ieee":"R. Alur and T. A. Henzinger, “Reactive modules,” <i>Formal Methods in System Design</i>, vol. 15, no. 1. Springer, pp. 7–48, 1999."},"year":"1999","acknowledgement":"We thank Albert Benveniste, Bob Kurshan, Ken McMillan, Amir Pnueli, and the VIS group at UC Berkeley for fruitful discussions. We also thank the anonymous referees for suggesting improvements. Alur was supported in part by the DARPA/NASA grant NAG2-1214 and Henzinger was supported in part by the ONR YIP award N00014-95-1-0520, the\r\nNSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the DARPA/NASA grant NAG2-1214, and by the SRC contract 97-DC-324.041.","volume":15,"extern":"1","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:35Z","title":"Reactive modules","intvolume":"        15","_id":"4582","scopus_import":"1","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"issue":"1","publisher":"Springer","article_type":"original","page":"7 - 48","quality_controlled":"1","publication_identifier":{"issn":["0925-9856"]},"publist_id":"125","date_published":"1999-01-01T00:00:00Z","type":"journal_article","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","month":"01","publication":"Formal Methods in System Design","language":[{"iso":"eng"}]},{"status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","type":"journal_article","date_published":"1997-01-01T00:00:00Z","publist_id":"98","publication_identifier":{"issn":["0925-9856"]},"language":[{"iso":"eng"}],"publication":"Formal Methods in System Design","month":"01","oa_version":"None","extern":"1","volume":11,"acknowledgement":"A preliminary version of this paper appeared in the Proceedings of the Fifth International Conference on Computer-Aided Verification (CAV 93), Springer-Verlag LNCS 818, pp. 181–193, 1993. We thank Sergio Yovine for a careful reading of the manuscript. This reaserch was partially supported by the BRA ESPRIT project REACT, by the ONR YIP\r\naward N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056, and by the ARPA grant NAG2-892.","year":"1997","citation":{"apa":"Alur, R., Courcoubetis, C., &#38; Henzinger, T. A. (1997). Computing accumulated delays in real-time systems. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1023/A:1008626013578\">https://doi.org/10.1023/A:1008626013578</a>","ama":"Alur R, Courcoubetis C, Henzinger TA. Computing accumulated delays in real-time systems. <i>Formal Methods in System Design</i>. 1997;11(2):137-156. doi:<a href=\"https://doi.org/10.1023/A:1008626013578\">10.1023/A:1008626013578</a>","ieee":"R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays in real-time systems,” <i>Formal Methods in System Design</i>, vol. 11, no. 2. Springer, pp. 137–156, 1997.","chicago":"Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated Delays in Real-Time Systems.” <i>Formal Methods in System Design</i>. Springer, 1997. <a href=\"https://doi.org/10.1023/A:1008626013578\">https://doi.org/10.1023/A:1008626013578</a>.","mla":"Alur, Rajeev, et al. “Computing Accumulated Delays in Real-Time Systems.” <i>Formal Methods in System Design</i>, vol. 11, no. 2, Springer, 1997, pp. 137–56, doi:<a href=\"https://doi.org/10.1023/A:1008626013578\">10.1023/A:1008626013578</a>.","short":"R. Alur, C. Courcoubetis, T.A. Henzinger, Formal Methods in System Design 11 (1997) 137–156.","ista":"Alur R, Courcoubetis C, Henzinger TA. 1997. Computing accumulated delays in real-time systems. Formal Methods in System Design. 11(2), 137–156."},"date_updated":"2022-08-16T13:43:41Z","abstract":[{"text":"We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.","lang":"eng"}],"day":"01","doi":"10.1023/A:1008626013578","quality_controlled":"1","page":"137 - 156","article_type":"original","publisher":"Springer","issue":"2","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"full_name":"Courcoubetis, Costas","last_name":"Courcoubetis","first_name":"Costas"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"}],"scopus_import":"1","_id":"4607","intvolume":"        11","title":"Computing accumulated delays in real-time systems","article_processing_charge":"No","date_created":"2018-12-11T12:09:43Z","publication_status":"published"}]