[{"type":"journal_article","language":[{"iso":"eng"}],"publication_status":"published","title":"Guest editors' introduction to special issue on computational methods in systems biology","publisher":"ACM","month":"05","_id":"1808","doi":"10.1145/2745799","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","last_name":"Gupta"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"publication":"ACM Transactions on Modeling and Computer Simulation","publist_id":"5302","issue":"2","department":[{"_id":"ToHe"}],"date_published":"2015-05-01T00:00:00Z","oa_version":"None","volume":25,"status":"public","article_number":"7","date_updated":"2021-01-12T06:53:20Z","year":"2015","date_created":"2018-12-11T11:54:07Z","quality_controlled":"1","citation":{"mla":"Gupta, Ashutosh, and Thomas A. Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 7, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>.","ieee":"A. Gupta and T. A. Henzinger, “Guest editors’ introduction to special issue on computational methods in systems biology,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","apa":"Gupta, A., &#38; Henzinger, T. A. (2015). Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>","ista":"Gupta A, Henzinger TA. 2015. Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. 25(2), 7.","chicago":"Gupta, Ashutosh, and Thomas A Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>.","ama":"Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>","short":"A. Gupta, T.A. Henzinger, ACM Transactions on Modeling and Computer Simulation 25 (2015)."},"intvolume":"        25","day":"01"},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"article_processing_charge":"No","scopus_import":1,"quality_controlled":"1","year":"2015","date_created":"2018-12-11T11:54:15Z","date_updated":"2023-02-23T10:38:13Z","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"volume":11,"file":[{"content_type":"application/pdf","file_id":"4881","date_created":"2018-12-12T10:11:27Z","access_level":"open_access","date_updated":"2020-07-14T12:45:17Z","file_name":"IST-2015-390-v1+1_1502.07639.pdf","file_size":380203,"creator":"system","relation":"main_file","checksum":"7370e164d0a731f442424a92669efc34"}],"license":"https://creativecommons.org/licenses/by-nd/4.0/","oa_version":"Published Version","date_published":"2015-04-01T00:00:00Z","issue":"1","publication":"Logical Methods in Computer Science","publist_id":"5271","ddc":["000"],"author":[{"last_name":"Chakraborty","full_name":"Chakraborty, Soham","first_name":"Soham"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Ali","full_name":"Sezgin, Ali","last_name":"Sezgin"},{"last_name":"Vafeiadis","first_name":"Viktor","full_name":"Vafeiadis, Viktor"}],"doi":"10.2168/LMCS-11(1:20)2015","publisher":"International Federation of Computational Logic","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:45:17Z","type":"journal_article","day":"01","has_accepted_license":"1","intvolume":"        11","citation":{"mla":"Chakraborty, Soham, et al. “Aspect-Oriented Linearizability Proofs.” <i>Logical Methods in Computer Science</i>, vol. 11, no. 1, 20, International Federation of Computational Logic, 2015, doi:<a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">10.2168/LMCS-11(1:20)2015</a>.","ieee":"S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” <i>Logical Methods in Computer Science</i>, vol. 11, no. 1. International Federation of Computational Logic, 2015.","chicago":"Chakraborty, Soham, Thomas A Henzinger, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2015. <a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">https://doi.org/10.2168/LMCS-11(1:20)2015</a>.","ista":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 11(1), 20.","apa":"Chakraborty, S., Henzinger, T. A., Sezgin, A., &#38; Vafeiadis, V. (2015). Aspect-oriented linearizability proofs. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">https://doi.org/10.2168/LMCS-11(1:20)2015</a>","ama":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. <i>Logical Methods in Computer Science</i>. 2015;11(1). doi:<a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">10.2168/LMCS-11(1:20)2015</a>","short":"S. Chakraborty, T.A. Henzinger, A. Sezgin, V. Vafeiadis, Logical Methods in Computer Science 11 (2015)."},"ec_funded":1,"article_number":"20","status":"public","abstract":[{"lang":"eng","text":"Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. "}],"department":[{"_id":"ToHe"}],"pubrep_id":"390","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1832","month":"04","title":"Aspect-oriented linearizability proofs","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"2328"}]},"oa":1,"publication_status":"published","article_type":"original"},{"scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.7704"}],"volume":9035,"date_updated":"2025-05-28T11:57:04Z","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"grant_number":"618091","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Limits to selection in biology and in evolutionary computation","grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","page":"469 - 483","date_created":"2018-12-11T11:54:16Z","year":"2015","series_title":"Lecture Notes in Computer Science","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","first_name":"Mirco","last_name":"Giacobbe"},{"last_name":"Guet","first_name":"Calin C","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Paixao, Tiago","first_name":"Tiago","last_name":"Paixao","orcid":"0000-0003-2361-3953","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5267","date_published":"2015-04-01T00:00:00Z","oa_version":"Preprint","conference":{"location":"London, United Kingdom","end_date":"2015-04-18","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2015-04-11"},"type":"conference","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-662-46681-0_47","intvolume":"      9035","citation":{"short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483.","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking gene regulatory networks. 2015;9035:469-483. doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model checking gene regulatory networks. 9035, 469–483.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2015). Model checking gene regulatory networks. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking Gene Regulatory Networks.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>.","mla":"Giacobbe, Mirco, et al. <i>Model Checking Gene Regulatory Networks</i>. Vol. 9035, Springer, 2015, pp. 469–83, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>.","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking gene regulatory networks,” vol. 9035. Springer, pp. 469–483, 2015."},"day":"01","abstract":[{"lang":"eng","text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs –an important problem of interest in evolutionary biology– more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights."}],"status":"public","ec_funded":1,"alternative_title":["LNCS"],"department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"acknowledgement":"SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2 148797.\r\n","title":"Model checking gene regulatory networks","oa":1,"related_material":{"record":[{"id":"1351","status":"public","relation":"later_version"}]},"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"04","_id":"1835"},{"scopus_import":1,"quality_controlled":"1","page":"105 - 131","year":"2015","series_title":"Lecture Notes in Computer Science","date_created":"2018-12-11T11:54:16Z","date_updated":"2020-08-11T10:09:32Z","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"volume":9032,"oa_version":"None","conference":{"start_date":"2015-04-11","name":"ESOP: European Symposium on Programming","end_date":"2015-04-18","location":"London, United Kingdom"},"date_published":"2015-04-01T00:00:00Z","publist_id":"5266","author":[{"last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Kovács, Laura","first_name":"Laura","last_name":"Kovács"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun"},{"last_name":"Zwirchmayr","full_name":"Zwirchmayr, Jakob","first_name":"Jakob"}],"doi":"10.1007/978-3-662-46669-8_5","publisher":"Springer","language":[{"iso":"eng"}],"type":"conference","day":"01","citation":{"short":"P. Cerny, T.A. Henzinger, L. Kovács, A. Radhakrishna, J. Zwirchmayr, 9032 (2015) 105–131.","ama":"Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. Segment abstraction for worst-case execution time analysis. 2015;9032:105-131. doi:<a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">10.1007/978-3-662-46669-8_5</a>","chicago":"Cerny, Pavol, Thomas A Henzinger, Laura Kovács, Arjun Radhakrishna, and Jakob Zwirchmayr. “Segment Abstraction for Worst-Case Execution Time Analysis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">https://doi.org/10.1007/978-3-662-46669-8_5</a>.","apa":"Cerny, P., Henzinger, T. A., Kovács, L., Radhakrishna, A., &#38; Zwirchmayr, J. (2015). Segment abstraction for worst-case execution time analysis. Presented at the ESOP: European Symposium on Programming, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">https://doi.org/10.1007/978-3-662-46669-8_5</a>","ista":"Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. 2015. Segment abstraction for worst-case execution time analysis. 9032, 105–131.","mla":"Cerny, Pavol, et al. <i>Segment Abstraction for Worst-Case Execution Time Analysis</i>. Vol. 9032, Springer, 2015, pp. 105–31, doi:<a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">10.1007/978-3-662-46669-8_5</a>.","ieee":"P. Cerny, T. A. Henzinger, L. Kovács, A. Radhakrishna, and J. Zwirchmayr, “Segment abstraction for worst-case execution time analysis,” vol. 9032. Springer, pp. 105–131, 2015."},"intvolume":"      9032","ec_funded":1,"status":"public","abstract":[{"text":"In the standard framework for worst-case execution time (WCET) analysis of programs, the main data structure is a single instance of integer linear programming (ILP) that represents the whole program. The instance of this NP-hard problem must be solved to find an estimate forWCET, and it must be refined if the estimate is not tight.We propose a new framework for WCET analysis, based on abstract segment trees (ASTs) as the main data structure. The ASTs have two advantages. First, they allow computing WCET by solving a number of independent small ILP instances. Second, ASTs store more expressive constraints, thus enabling a more efficient and precise refinement procedure. In order to realize our framework algorithmically, we develop an algorithm for WCET estimation on ASTs, and we develop an interpolation-based counterexample-guided refinement scheme for ASTs. Furthermore, we extend our framework to obtain parametric estimates of WCET. We experimentally evaluate our approach on a set of examples from WCET benchmark suites and linear-algebra packages. We show that our analysis, with comparable effort, provides WCET estimates that in many cases significantly improve those computed by existing tools.","lang":"eng"}],"department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"04","_id":"1836","title":"Segment abstraction for worst-case execution time analysis","publication_status":"published"},{"intvolume":"        60","citation":{"chicago":"Geiger, Bernhard, Tatjana Petrov, Gernot Kubin, and Heinz Koeppl. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 2015. <a href=\"https://doi.org/10.1109/TAC.2014.2364971\">https://doi.org/10.1109/TAC.2014.2364971</a>.","apa":"Geiger, B., Petrov, T., Kubin, G., &#38; Koeppl, H. (2015). Optimal Kullback-Leibler aggregation via information bottleneck. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/TAC.2014.2364971\">https://doi.org/10.1109/TAC.2014.2364971</a>","ista":"Geiger B, Petrov T, Kubin G, Koeppl H. 2015. Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. 60(4), 1010–1022.","mla":"Geiger, Bernhard, et al. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 4, IEEE, 2015, pp. 1010–22, doi:<a href=\"https://doi.org/10.1109/TAC.2014.2364971\">10.1109/TAC.2014.2364971</a>.","ieee":"B. Geiger, T. Petrov, G. Kubin, and H. Koeppl, “Optimal Kullback-Leibler aggregation via information bottleneck,” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 4. IEEE, pp. 1010–1022, 2015.","short":"B. Geiger, T. Petrov, G. Kubin, H. Koeppl, IEEE Transactions on Automatic Control 60 (2015) 1010–1022.","ama":"Geiger B, Petrov T, Kubin G, Koeppl H. Optimal Kullback-Leibler aggregation via information bottleneck. <i>IEEE Transactions on Automatic Control</i>. 2015;60(4):1010-1022. doi:<a href=\"https://doi.org/10.1109/TAC.2014.2364971\">10.1109/TAC.2014.2364971</a>"},"day":"01","status":"public","abstract":[{"lang":"eng","text":"In this paper, we present a method for reducing a regular, discrete-time Markov chain (DTMC) to another DTMC with a given, typically much smaller number of states. The cost of reduction is defined as the Kullback-Leibler divergence rate between a projection of the original process through a partition function and a DTMC on the correspondingly partitioned state space. Finding the reduced model with minimal cost is computationally expensive, as it requires an exhaustive search among all state space partitions, and an exact evaluation of the reduction cost for each candidate partition. Our approach deals with the latter problem by minimizing an upper bound on the reduction cost instead of minimizing the exact cost. The proposed upper bound is easy to compute and it is tight if the original chain is lumpable with respect to the partition. Then, we express the problem in the form of information bottleneck optimization, and propose using the agglomerative information bottleneck algorithm for searching a suboptimal partition greedily, rather than exhaustively. The theory is illustrated with examples and one application scenario in the context of modeling bio-molecular interactions."}],"department":[{"_id":"CaGu"},{"_id":"ToHe"}],"acknowledgement":"This work was supported by the Austrian Research Association under Project 06/12684, by the Swiss National Science Foundation (SNSF) under Grant PP00P2 128503/1, by the SystemsX.ch (the Swiss Inititative for Systems Biology), and by a SNSF Early Postdoc.Mobility Fellowship grant P2EZP2_148797.\r\n","oa":1,"title":"Optimal Kullback-Leibler aggregation via information bottleneck","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1840","month":"04","publication_identifier":{"issn":["0018-9286"]},"scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1304.6603"}],"volume":60,"page":"1010 - 1022","quality_controlled":"1","year":"2015","date_created":"2018-12-11T11:54:18Z","date_updated":"2021-01-12T06:53:33Z","publist_id":"5262","issue":"4","publication":"IEEE Transactions on Automatic Control","author":[{"full_name":"Geiger, Bernhard","first_name":"Bernhard","last_name":"Geiger"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","last_name":"Petrov","full_name":"Petrov, Tatjana","first_name":"Tatjana"},{"full_name":"Kubin, Gernot","first_name":"Gernot","last_name":"Kubin"},{"full_name":"Koeppl, Heinz","first_name":"Heinz","last_name":"Koeppl"}],"oa_version":"Preprint","date_published":"2015-04-01T00:00:00Z","language":[{"iso":"eng"}],"type":"journal_article","doi":"10.1109/TAC.2014.2364971","publisher":"IEEE"},{"abstract":[{"text":"Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.","lang":"eng"}],"status":"public","ec_funded":1,"intvolume":"        52","citation":{"apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., &#38; Srba, J. (2015). Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>","chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>.","ista":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.","ieee":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” <i>Acta Informatica</i>, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.","mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>.","short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. 2015;52(2-3):269-297. doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>"},"has_accepted_license":"1","day":"01","article_type":"original","title":"Refinement checking on parametric modal transition systems","oa":1,"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1846","month":"04","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"volume":52,"file":[{"date_created":"2020-05-15T08:57:44Z","content_type":"application/pdf","file_id":"7854","access_level":"open_access","date_updated":"2020-07-14T12:45:19Z","file_name":"2015_ActaInfo_Benes.pdf","file_size":488482,"creator":"dernst","relation":"main_file","checksum":"fb4037ddc4fc05f33080dd3547ede350"}],"date_updated":"2021-01-12T06:53:35Z","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"page":"269 - 297","quality_controlled":"1","date_created":"2018-12-11T11:54:20Z","year":"2015","scopus_import":1,"article_processing_charge":"No","file_date_updated":"2020-07-14T12:45:19Z","type":"journal_article","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/s00236-015-0215-4","ddc":["000"],"author":[{"last_name":"Beneš","first_name":"Nikola","full_name":"Beneš, Nikola"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Larsen","full_name":"Larsen, Kim","first_name":"Kim"},{"last_name":"Möller","first_name":"Mikael","full_name":"Möller, Mikael"},{"first_name":"Salomon","full_name":"Sickert, Salomon","last_name":"Sickert"},{"last_name":"Srba","full_name":"Srba, Jiří","first_name":"Jiří"}],"publication":"Acta Informatica","publist_id":"5255","issue":"2-3","date_published":"2015-04-01T00:00:00Z","oa_version":"Submitted Version"},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"related_material":{"record":[{"id":"3864","relation":"earlier_version","status":"public"}]},"title":"Measuring and synthesizing systems in probabilistic environments","oa":1,"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"02","_id":"1856","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and synthesizing systems in probabilistic environments,” <i>Journal of the ACM</i>, vol. 62, no. 1. ACM, 2015.","mla":"Chatterjee, Krishnendu, et al. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>, vol. 62, no. 1, 9, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2015). Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2015. Measuring and synthesizing systems in probabilistic environments. Journal of the ACM. 62(1), 9.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>.","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. 2015;62(1). doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM 62 (2015)."},"intvolume":"        62","day":"01","article_number":"9","status":"public","abstract":[{"lang":"eng","text":"The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε &gt; 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way."}],"ec_funded":1,"issue":"1","publication":"Journal of the ACM","publist_id":"5244","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Jobstmann","first_name":"Barbara","full_name":"Jobstmann, Barbara"},{"last_name":"Singh","first_name":"Rohit","full_name":"Singh, Rohit"}],"oa_version":"Preprint","date_published":"2015-02-01T00:00:00Z","language":[{"iso":"eng"}],"type":"journal_article","doi":"10.1145/2699430","publisher":"ACM","scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1004.0739","open_access":"1"}],"volume":62,"quality_controlled":"1","date_created":"2018-12-11T11:54:23Z","year":"2015","date_updated":"2023-02-23T11:46:04Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}]},{"quality_controlled":"1","year":"2015","date_created":"2018-12-11T11:54:25Z","date_updated":"2021-01-12T06:53:41Z","article_number":"8","status":"public","abstract":[{"text":"Continuous-time Markov chains are commonly used in practice for modeling biochemical reaction networks in which the inherent randomness of themolecular interactions cannot be ignored. This has motivated recent research effort into methods for parameter inference and experiment design for such models. The major difficulty is that such methods usually require one to iteratively solve the chemical master equation that governs the time evolution of the probability distribution of the system. This, however, is rarely possible, and even approximation techniques remain limited to relatively small and simple systems. An alternative explored in this article is to base methods on only some low-order moments of the entire probability distribution. We summarize the theory behind such moment-based methods for parameter inference and experiment design and provide new case studies where we investigate their performance.","lang":"eng"}],"volume":25,"day":"01","scopus_import":1,"intvolume":"        25","citation":{"chicago":"Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference and Experiment Design for Stochastic Biochemical Reaction Networks.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2688906\">https://doi.org/10.1145/2688906</a>.","ista":"Ruess J, Lygeros J. 2015. Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. ACM Transactions on Modeling and Computer Simulation. 25(2), 8.","apa":"Ruess, J., &#38; Lygeros, J. (2015). Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2688906\">https://doi.org/10.1145/2688906</a>","ieee":"J. Ruess and J. Lygeros, “Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","mla":"Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference and Experiment Design for Stochastic Biochemical Reaction Networks.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 8, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2688906\">10.1145/2688906</a>.","short":"J. Ruess, J. Lygeros, ACM Transactions on Modeling and Computer Simulation 25 (2015).","ama":"Ruess J, Lygeros J. Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2688906\">10.1145/2688906</a>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1145/2688906","_id":"1861","month":"02","publisher":"ACM","title":"Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks","publication_status":"published","language":[{"iso":"eng"}],"type":"journal_article","oa_version":"None","date_published":"2015-02-01T00:00:00Z","acknowledgement":"HYCON2; EC; European Commission\r\n","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"publication":"ACM Transactions on Modeling and Computer Simulation","issue":"2","publist_id":"5238","author":[{"full_name":"Ruess, Jakob","first_name":"Jakob","last_name":"Ruess","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282"},{"full_name":"Lygeros, John","first_name":"John","last_name":"Lygeros"}]},{"title":"The equivalence problem for finite automata: Technical perspective","language":[{"iso":"eng"}],"publication_status":"published","type":"journal_article","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","_id":"1866","doi":"10.1145/2701001","publisher":"ACM","publication":"Communications of the ACM","issue":"2","publist_id":"5232","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"oa_version":"None","date_published":"2015-01-28T00:00:00Z","department":[{"_id":"ToHe"}],"status":"public","volume":58,"page":"86-86","year":"2015","date_created":"2018-12-11T11:54:26Z","date_updated":"2021-01-12T06:53:43Z","scopus_import":1,"intvolume":"        58","citation":{"ama":"Henzinger TA, Raskin J. The equivalence problem for finite automata: Technical perspective. <i>Communications of the ACM</i>. 2015;58(2):86-86. doi:<a href=\"https://doi.org/10.1145/2701001\">10.1145/2701001</a>","short":"T.A. Henzinger, J. Raskin, Communications of the ACM 58 (2015) 86–86.","mla":"Henzinger, Thomas A., and Jean Raskin. “The Equivalence Problem for Finite Automata: Technical Perspective.” <i>Communications of the ACM</i>, vol. 58, no. 2, ACM, 2015, pp. 86–86, doi:<a href=\"https://doi.org/10.1145/2701001\">10.1145/2701001</a>.","ieee":"T. A. Henzinger and J. Raskin, “The equivalence problem for finite automata: Technical perspective,” <i>Communications of the ACM</i>, vol. 58, no. 2. ACM, pp. 86–86, 2015.","chicago":"Henzinger, Thomas A, and Jean Raskin. “The Equivalence Problem for Finite Automata: Technical Perspective.” <i>Communications of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2701001\">https://doi.org/10.1145/2701001</a>.","ista":"Henzinger TA, Raskin J. 2015. The equivalence problem for finite automata: Technical perspective. Communications of the ACM. 58(2), 86–86.","apa":"Henzinger, T. A., &#38; Raskin, J. (2015). The equivalence problem for finite automata: Technical perspective. <i>Communications of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2701001\">https://doi.org/10.1145/2701001</a>"},"day":"28"},{"type":"conference","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-319-15317-9_19","author":[{"last_name":"Fahrenberg","first_name":"Uli","full_name":"Fahrenberg, Uli"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"full_name":"Legay, Axel","first_name":"Axel","last_name":"Legay"},{"last_name":"Traonouez","full_name":"Traonouez, Louis","first_name":"Louis"}],"publist_id":"5216","date_published":"2015-01-30T00:00:00Z","conference":{"start_date":"2014-09-10","name":"FACS: Formal Aspects of Component Software","end_date":"2014-09-12","location":"Bertinoro, Italy"},"oa_version":"Preprint","volume":8997,"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2021-01-12T06:53:49Z","date_created":"2018-12-11T11:54:31Z","year":"2015","page":"306 - 324","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1408.1256"}],"scopus_import":1,"publication_status":"published","oa":1,"title":"Compositionality for quantitative specifications","month":"01","_id":"1882","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"abstract":[{"lang":"eng","text":"We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations."}],"status":"public","ec_funded":1,"citation":{"ista":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.","chicago":"Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality for Quantitative Specifications,” 8997:306–24. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>.","apa":"Fahrenberg, U., Kretinsky, J., Legay, A., &#38; Traonouez, L. (2015). Compositionality for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>","mla":"Fahrenberg, Uli, et al. <i>Compositionality for Quantitative Specifications</i>. Vol. 8997, Springer, 2015, pp. 306–24, doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>.","ieee":"U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.","short":"U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324.","ama":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative specifications. In: Vol 8997. Springer; 2015:306-324. doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>"},"intvolume":"      8997","day":"30"},{"citation":{"ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>","short":"A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM, 2015, pp. 433–444.","ieee":"A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct representation of concurrent trace sets,” presented at the POPL: Principles of Programming Languages, Mumbai, India, 2015, pp. 433–444.","mla":"Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>. ACM, 2015, pp. 433–44, doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>.","apa":"Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>","ista":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct representation of concurrent trace sets. POPL: Principles of Programming Languages, 433–444.","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>."},"has_accepted_license":"1","day":"15","abstract":[{"lang":"eng","text":"We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.\r\n\r\nWe claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula."}],"status":"public","pubrep_id":"317","department":[{"_id":"ToHe"}],"publication_status":"published","oa":1,"title":"Succinct representation of concurrent trace sets","month":"01","_id":"1992","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"publication_identifier":{"isbn":["978-1-4503-3300-9"]},"file":[{"access_level":"open_access","date_updated":"2020-07-14T12:45:22Z","date_created":"2018-12-12T10:17:56Z","file_id":"5314","content_type":"application/pdf","file_name":"IST-2015-317-v1+1_author_version.pdf","creator":"system","file_size":399462,"checksum":"f0d4395b600f410a191256ac0b73af32","relation":"main_file"}],"date_updated":"2021-01-12T06:54:33Z","date_created":"2018-12-11T11:55:05Z","year":"2015","quality_controlled":"1","page":"433 - 444","author":[{"last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","first_name":"Arjun","last_name":"Radhakrishna"},{"last_name":"Samanta","first_name":"Roopsha","full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87"},{"id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","last_name":"Tarrach","full_name":"Tarrach, Thorsten","first_name":"Thorsten"}],"ddc":["005"],"publist_id":"5091","date_published":"2015-01-15T00:00:00Z","oa_version":"Submitted Version","conference":{"location":"Mumbai, India","end_date":"2015-01-17","name":"POPL: Principles of Programming Languages","start_date":"2015-01-15"},"type":"conference","file_date_updated":"2020-07-14T12:45:22Z","language":[{"iso":"eng"}],"publisher":"ACM","doi":"10.1145/2676726.2677008"},{"oa_version":"Published Version","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2015-04-24T00:00:00Z","alternative_title":["IST Austria Technical Report"],"pubrep_id":"331","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"ddc":["000"],"month":"04","_id":"5436","doi":"10.15479/AT:IST-2015-170-v2-2","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","language":[{"iso":"eng"}],"publication_status":"published","related_material":{"record":[{"id":"1656","relation":"later_version","status":"public"},{"relation":"later_version","status":"public","id":"467"},{"id":"5415","relation":"earlier_version","status":"public"}]},"oa":1,"title":"Nested weighted automata","type":"technical_report","file_date_updated":"2020-07-14T12:46:54Z","day":"24","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2015.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria, 29p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2015."},"date_created":"2018-12-12T11:39:19Z","year":"2015","page":"29","date_updated":"2023-02-23T12:25:21Z","status":"public","file":[{"file_name":"IST-2015-170-v2+2_report.pdf","date_updated":"2020-07-14T12:46:54Z","access_level":"open_access","file_id":"5541","content_type":"application/pdf","date_created":"2018-12-12T11:54:19Z","checksum":"3c402f47d3669c28d04d1af405a08e3f","relation":"main_file","creator":"system","file_size":569991}],"abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time.\r\nIn nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}]},{"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","full_name":"Boker, Udi","last_name":"Boker"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"ddc":["004","512","513"],"pubrep_id":"335","alternative_title":["IST Austria Technical Report"],"department":[{"_id":"ToHe"}],"date_published":"2015-05-18T00:00:00Z","oa_version":"Published Version","type":"technical_report","file_date_updated":"2020-07-14T12:46:55Z","publication_status":"published","language":[{"iso":"eng"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"1659"}]},"oa":1,"title":"The target discounted-sum problem","publisher":"IST Austria","_id":"5439","doi":"10.15479/AT:IST-2015-335-v1-1","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Boker, Udi, Thomas A Henzinger, and Jan Otop. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>.","apa":"Boker, U., Henzinger, T. A., &#38; Otop, J. (2015). <i>The target discounted-sum problem</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST Austria, 20p.","ieee":"U. Boker, T. A. Henzinger, and J. Otop, <i>The target discounted-sum problem</i>. IST Austria, 2015.","mla":"Boker, Udi, et al. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>.","short":"U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST Austria, 2015.","ama":"Boker U, Henzinger TA, Otop J. <i>The Target Discounted-Sum Problem</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>"},"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","day":"18","file":[{"checksum":"40405907aa012acece1bc26cf0be554d","relation":"main_file","creator":"system","file_size":589619,"file_name":"IST-2015-335-v1+1_report.pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:55Z","content_type":"application/pdf","file_id":"5517","date_created":"2018-12-12T11:53:55Z"}],"abstract":[{"text":"The target discounted-sum problem is the following: Given a rational discount factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata. ","lang":"eng"}],"status":"public","date_updated":"2023-02-23T10:08:48Z","year":"2015","date_created":"2018-12-12T11:39:20Z","page":"20"},{"ec_funded":1,"abstract":[{"lang":"eng","text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication."}],"contributor":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"}],"status":"public","has_accepted_license":"1","day":"13","citation":{"ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015.","mla":"Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute of Science and Technology Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>","ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>.","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>","short":"A. Fellner, (2015)."},"keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5549","month":"08","title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","oa":1,"related_material":{"record":[{"id":"1603","status":"public","relation":"popular_science"}]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2024-02-21T13:52:07Z","project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"year":"2015","date_created":"2018-12-12T12:31:29Z","file":[{"relation":"main_file","checksum":"b8bcb43c0893023cda66c1b69c16ac62","file_size":49557109,"creator":"system","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","file_id":"5597","date_created":"2018-12-12T13:02:31Z","content_type":"application/zip","date_updated":"2020-07-14T12:47:00Z","access_level":"open_access"}],"tmp":{"short":"CC0 (1.0)","name":"Creative Commons Public Domain Dedication (CC0 1.0)","image":"/images/cc_0.png","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode"},"article_processing_charge":"No","publisher":"Institute of Science and Technology Austria","datarep_id":"28","doi":"10.15479/AT:ISTA:28","file_date_updated":"2020-07-14T12:47:00Z","type":"research_data","date_published":"2015-08-13T00:00:00Z","license":"https://creativecommons.org/publicdomain/zero/1.0/","oa_version":"Published Version","ddc":["004"],"author":[{"last_name":"Fellner","full_name":"Fellner, Andreas","first_name":"Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5564"},{"acknowledgement":"The authors would like to acknowledge contributions from Baptiste Mottet who performed preliminary analysis regarding parameter inference for the considered case study in a student project (Mottet, 2014/2015).\r\nThe research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement No. [291734] and from SystemsX under the project SignalX.","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"10794","month":"06","article_type":"original","title":"Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study","oa":1,"publication_status":"published","has_accepted_license":"1","day":"10","intvolume":"         3","citation":{"ista":"Parise F, Lygeros J, Ruess J. 2015. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. Frontiers in Environmental Science. 3, 42.","chicago":"Parise, Francesca, John Lygeros, and Jakob Ruess. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>. Frontiers, 2015. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>.","apa":"Parise, F., Lygeros, J., &#38; Ruess, J. (2015). Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. Frontiers. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>","mla":"Parise, Francesca, et al. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>, vol. 3, 42, Frontiers, 2015, doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>.","ieee":"F. Parise, J. Lygeros, and J. Ruess, “Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study,” <i>Frontiers in Environmental Science</i>, vol. 3. Frontiers, 2015.","short":"F. Parise, J. Lygeros, J. Ruess, Frontiers in Environmental Science 3 (2015).","ama":"Parise F, Lygeros J, Ruess J. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. 2015;3. doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>"},"keyword":["General Environmental Science"],"ec_funded":1,"abstract":[{"lang":"eng","text":"Mathematical models are of fundamental importance in the understanding of complex population dynamics. For instance, they can be used to predict the population evolution starting from different initial conditions or to test how a system responds to external perturbations. For this analysis to be meaningful in real applications, however, it is of paramount importance to choose an appropriate model structure and to infer the model parameters from measured data. While many parameter inference methods are available for models based on deterministic ordinary differential equations, the same does not hold for more detailed individual-based models. Here we consider, in particular, stochastic models in which the time evolution of the species abundances is described by a continuous-time Markov chain. These models are governed by a master equation that is typically difficult to solve. Consequently, traditional inference methods that rely on iterative evaluation of parameter likelihoods are computationally intractable. The aim of this paper is to present recent advances in parameter inference for continuous-time Markov chain models, based on a moment closure approximation of the parameter likelihood, and to investigate how these results can help in understanding, and ultimately controlling, complex systems in ecology. Specifically, we illustrate through an agricultural pest case study how parameters of a stochastic individual-based model can be identified from measured data and how the resulting model can be used to solve an optimal control problem in a stochastic setting. In particular, we show how the matter of determining the optimal combination of two different pest control methods can be formulated as a chance constrained optimization problem where the control action is modeled as a state reset, leading to a hybrid system formulation."}],"article_number":"42","status":"public","date_published":"2015-06-10T00:00:00Z","oa_version":"Published Version","license":"https://creativecommons.org/licenses/by/4.0/","ddc":["000","570"],"author":[{"last_name":"Parise","first_name":"Francesca","full_name":"Parise, Francesca"},{"first_name":"John","full_name":"Lygeros, John","last_name":"Lygeros"},{"orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","last_name":"Ruess","full_name":"Ruess, Jakob","first_name":"Jakob"}],"publication":"Frontiers in Environmental Science","publisher":"Frontiers","doi":"10.3389/fenvs.2015.00042","file_date_updated":"2022-02-25T11:55:26Z","type":"journal_article","language":[{"iso":"eng"}],"article_processing_charge":"No","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"scopus_import":"1","publication_identifier":{"issn":["2296-665X"]},"date_updated":"2022-02-25T11:59:23Z","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"quality_controlled":"1","year":"2015","date_created":"2022-02-25T11:42:25Z","volume":3,"file":[{"success":1,"date_updated":"2022-02-25T11:55:26Z","access_level":"open_access","date_created":"2022-02-25T11:55:26Z","file_id":"10795","content_type":"application/pdf","file_name":"2015_FrontiersEnvironmScience_Parise.pdf","creator":"dernst","file_size":1371201,"checksum":"26c222487564e1be02a11d688d6f769d","relation":"main_file"}]},{"oa_version":"Submitted Version","conference":{"location":"Vienna, Austria","end_date":"2014-07-17","name":"HCVS: Horn Clauses for Verification and Synthesis","start_date":"2014-07-17"},"date_published":"2014-12-02T00:00:00Z","department":[{"_id":"ToHe"}],"publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS","alternative_title":["EPTCS"],"publist_id":"5435","author":[{"last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Popeea","full_name":"Popeea, Corneliu","first_name":"Corneliu"},{"last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey","first_name":"Andrey"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"1702","doi":"10.4204/EPTCS.169.5","month":"12","publisher":"Open Publishing","oa":1,"title":"Generalised interpolation by solving recursion free-horn clauses","publication_status":"published","language":[{"iso":"eng"}],"type":"conference","day":"02","intvolume":"       169","citation":{"apa":"Gupta, A., Popeea, C., &#38; Rybalchenko, A. (2014). Generalised interpolation by solving recursion free-horn clauses. In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i> (Vol. 169, pp. 31–38). Vienna, Austria: Open Publishing. <a href=\"https://doi.org/10.4204/EPTCS.169.5\">https://doi.org/10.4204/EPTCS.169.5</a>","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, 169:31–38. Open Publishing, 2014. <a href=\"https://doi.org/10.4204/EPTCS.169.5\">https://doi.org/10.4204/EPTCS.169.5</a>.","ista":"Gupta A, Popeea C, Rybalchenko A. 2014. Generalised interpolation by solving recursion free-horn clauses. Electronic Proceedings in Theoretical Computer Science, EPTCS. HCVS: Horn Clauses for Verification and Synthesis, EPTCS, vol. 169, 31–38.","mla":"Gupta, Ashutosh, et al. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, vol. 169, Open Publishing, 2014, pp. 31–38, doi:<a href=\"https://doi.org/10.4204/EPTCS.169.5\">10.4204/EPTCS.169.5</a>.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Generalised interpolation by solving recursion free-horn clauses,” in <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, Vienna, Austria, 2014, vol. 169, pp. 31–38.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing, 2014, pp. 31–38.","ama":"Gupta A, Popeea C, Rybalchenko A. Generalised interpolation by solving recursion free-horn clauses. In: <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>. Vol 169. Open Publishing; 2014:31-38. doi:<a href=\"https://doi.org/10.4204/EPTCS.169.5\">10.4204/EPTCS.169.5</a>"},"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1303.7378v2"}],"quality_controlled":"1","page":"31 - 38","date_created":"2018-12-11T11:53:33Z","year":"2014","date_updated":"2021-01-12T06:52:38Z","status":"public","abstract":[{"text":"In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools.","lang":"eng"}],"volume":169},{"main_file_link":[{"url":"http://arxiv.org/abs/1210.2450","open_access":"1"}],"scopus_import":1,"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_updated":"2023-02-23T11:04:00Z","date_created":"2018-12-11T11:53:43Z","year":"2014","page":"348 - 363","quality_controlled":"1","volume":560,"date_published":"2014-12-04T00:00:00Z","oa_version":"Submitted Version","author":[{"full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"issue":"3","publication":"Theoretical Computer Science","publist_id":"5392","publisher":"Elsevier","doi":"10.1016/j.tcs.2014.08.019","type":"journal_article","language":[{"iso":"eng"}],"day":"04","intvolume":"       560","citation":{"ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363.","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>. Elsevier, 2014. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>.","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., &#38; Radhakrishna, A. (2014). Interface simulation distances. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>, vol. 560, no. 3, Elsevier, 2014, pp. 348–63, doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>.","ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface simulation distances,” <i>Theoretical Computer Science</i>, vol. 560, no. 3. Elsevier, pp. 348–363, 2014.","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface simulation distances. <i>Theoretical Computer Science</i>. 2014;560(3):348-363. doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>"},"ec_funded":1,"abstract":[{"text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.","lang":"eng"}],"status":"public","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"_id":"1733","month":"12","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publication_status":"published","oa":1,"title":"Interface simulation distances","related_material":{"record":[{"id":"2916","status":"public","relation":"earlier_version"}]}},{"volume":8855,"page":"68 - 74","quality_controlled":"1","date_created":"2018-12-11T11:54:27Z","year":"2014","date_updated":"2021-01-12T06:53:44Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publication":"HVC 2014","publist_id":"5228","author":[{"full_name":"Hofferek, Georg","first_name":"Georg","last_name":"Hofferek"},{"last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"}],"conference":{"name":"HVC: Haifa Verification Conference","start_date":"2014-11-18","location":"Haifa, Israel","end_date":"2014-11-20"},"oa_version":"None","date_published":"2014-01-01T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","doi":"10.1007/978-3-319-13338-6_6","publisher":"Springer","intvolume":"      8855","citation":{"mla":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” <i>HVC 2014</i>, edited by Eran Yahav, vol. 8855, Springer, 2014, pp. 68–74, doi:<a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">10.1007/978-3-319-13338-6_6</a>.","ieee":"G. Hofferek and A. Gupta, “Suraq - a controller synthesis tool using uninterpreted functions,” in <i>HVC 2014</i>, Haifa, Israel, 2014, vol. 8855, pp. 68–74.","ista":"Hofferek G, Gupta A. 2014. Suraq - a controller synthesis tool using uninterpreted functions. HVC 2014. HVC: Haifa Verification Conference, LNCS, vol. 8855, 68–74.","chicago":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” In <i>HVC 2014</i>, edited by Eran Yahav, 8855:68–74. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">https://doi.org/10.1007/978-3-319-13338-6_6</a>.","apa":"Hofferek, G., &#38; Gupta, A. (2014). Suraq - a controller synthesis tool using uninterpreted functions. In E. Yahav (Ed.), <i>HVC 2014</i> (Vol. 8855, pp. 68–74). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">https://doi.org/10.1007/978-3-319-13338-6_6</a>","ama":"Hofferek G, Gupta A. Suraq - a controller synthesis tool using uninterpreted functions. In: Yahav E, ed. <i>HVC 2014</i>. Vol 8855. Springer; 2014:68-74. doi:<a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">10.1007/978-3-319-13338-6_6</a>","short":"G. Hofferek, A. Gupta, in:, E. Yahav (Ed.), HVC 2014, Springer, 2014, pp. 68–74."},"day":"01","status":"public","abstract":[{"lang":"eng","text":"Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified firstorder formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes."}],"ec_funded":1,"editor":[{"first_name":"Eran","full_name":"Yahav, Eran","last_name":"Yahav"}],"alternative_title":["LNCS"],"acknowledgement":"The work presented in this paper was supported in part by the European Research Council (ERC) under grant agreement QUAINT (I774-N23)","department":[{"_id":"ToHe"}],"title":"Suraq - a controller synthesis tool using uninterpreted functions","publication_status":"published","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"1869","month":"01"},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2021-01-12T06:53:45Z","year":"2014","date_created":"2018-12-11T11:54:27Z","quality_controlled":"1","page":"431 - 443","file":[{"checksum":"7b1aff1710a8bffb7080ec07f62d9a17","relation":"main_file","creator":"system","file_size":562151,"file_name":"IST-2017-804-v1+1_37.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:19Z","file_id":"4734","date_created":"2018-12-12T10:09:11Z","content_type":"application/pdf"}],"volume":29,"date_published":"2014-12-01T00:00:00Z","oa_version":"Published Version","conference":{"start_date":"2014-12-15","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","end_date":"2014-12-17","location":"Delhi, India"},"author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","full_name":"Samanta, Roopsha","last_name":"Samanta"}],"ddc":["004"],"publication":"Leibniz International Proceedings in Informatics, LIPIcs","publist_id":"5227","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPIcs.FSTTCS.2014.431","type":"conference","file_date_updated":"2020-07-14T12:45:19Z","language":[{"iso":"eng"}],"has_accepted_license":"1","day":"01","intvolume":"        29","citation":{"chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Finite-State Transducers.” In <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, 29:431–43. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>.","ista":"Henzinger TA, Otop J, Samanta R. 2014. Lipschitz robustness of finite-state transducers. Leibniz International Proceedings in Informatics, LIPIcs. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 29, 431–443.","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2014). Lipschitz robustness of finite-state transducers. In <i>Leibniz International Proceedings in Informatics, LIPIcs</i> (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>","ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of finite-state transducers,” in <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, Delhi, India, 2014, vol. 29, pp. 431–443.","mla":"Henzinger, Thomas A., et al. “Lipschitz Robustness of Finite-State Transducers.” <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, vol. 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–43, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>.","short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–443.","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers. In: <i>Leibniz International Proceedings in Informatics, LIPIcs</i>. Vol 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>"},"abstract":[{"lang":"eng","text":"We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using setsimilarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers."}],"status":"public","department":[{"_id":"ToHe"}],"pubrep_id":"804","alternative_title":["LIPIcs"],"_id":"1870","month":"12","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publication_status":"published","title":"Lipschitz robustness of finite-state transducers","oa":1},{"abstract":[{"text":"Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover.","lang":"eng"}],"status":"public","ec_funded":1,"editor":[{"first_name":"Franck","full_name":"Cassez, Franck","last_name":"Cassez"},{"last_name":"Raskin","first_name":"Jean-François","full_name":"Raskin, Jean-François"}],"citation":{"apa":"Gupta, A., Kovács, L., Kragl, B., &#38; Voronkov, A. (2014). Extensional crisis and proving identity. In F. Cassez &#38; J.-F. Raskin (Eds.), <i>ATVA 2014</i> (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>","ista":"Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving identity. ATVA 2014. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 185–200.","chicago":"Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional Crisis and Proving Identity.” In <i>ATVA 2014</i>, edited by Franck Cassez and Jean-François Raskin, 8837:185–200. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>.","ieee":"A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving identity,” in <i>ATVA 2014</i>, Sydney, Australia, 2014, vol. 8837, pp. 185–200.","mla":"Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” <i>ATVA 2014</i>, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 185–200, doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>.","short":"A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, F. Cassez, J.-F. Raskin (Eds.), ATVA 2014, Springer, 2014, pp. 185–200.","ama":"Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: Cassez F, Raskin J-F, eds. <i>ATVA 2014</i>. Vol 8837. Springer; 2014:185-200. doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>"},"intvolume":"      8837","has_accepted_license":"1","day":"01","oa":1,"title":"Extensional crisis and proving identity","publication_status":"published","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"1872","month":"01","alternative_title":["LNCS"],"pubrep_id":"641","acknowledgement":"This research was supported in part by the Austrian National Research Network RiSE (S11410-N23).","department":[{"_id":"ToHe"}],"volume":8837,"file":[{"checksum":"af4bd3fc1f4c93075e4dc5cbf625fe7b","relation":"main_file","creator":"system","file_size":244294,"file_name":"IST-2016-641-v1+1_atva2014.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:19Z","file_id":"4801","date_created":"2018-12-12T10:10:15Z","content_type":"application/pdf"}],"date_updated":"2021-01-12T06:53:45Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"}],"page":"185 - 200","quality_controlled":"1","year":"2014","date_created":"2018-12-11T11:54:28Z","scopus_import":1,"file_date_updated":"2020-07-14T12:45:19Z","type":"conference","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-319-11936-6_14","ddc":["000"],"author":[{"last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kovács, Laura","first_name":"Laura","last_name":"Kovács"},{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","last_name":"Kragl","full_name":"Kragl, Bernhard","first_name":"Bernhard"},{"full_name":"Voronkov, Andrei","first_name":"Andrei","last_name":"Voronkov"}],"publist_id":"5226","publication":"ATVA 2014","date_published":"2014-01-01T00:00:00Z","oa_version":"Submitted Version","conference":{"start_date":"2014-11-03","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2014-11-07","location":"Sydney, Australia"}}]