[{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_updated":"2023-02-23T11:04:00Z","status":"public","type":"journal_article","_id":"1733","ec_funded":1,"related_material":{"record":[{"status":"public","id":"2916","relation":"earlier_version"}]},"issue":"3","volume":560,"language":[{"iso":"eng"}],"publication_status":"published","intvolume":" 560","month":"12","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1210.2450"}],"scopus_import":1,"oa_version":"Submitted Version","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"}],"title":"Interface simulation distances","publist_id":"5392","author":[{"first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” Theoretical Computer Science, vol. 560, no. 3, Elsevier, 2014, pp. 348–63, doi:10.1016/j.tcs.2014.08.019.","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface simulation distances. Theoretical Computer Science. 2014;560(3):348-363. doi:10.1016/j.tcs.2014.08.019","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., & Radhakrishna, A. (2014). Interface simulation distances. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2014.08.019","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.","ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface simulation distances,” Theoretical Computer Science, vol. 560, no. 3. Elsevier, pp. 348–363, 2014.","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” Theoretical Computer Science. Elsevier, 2014. https://doi.org/10.1016/j.tcs.2014.08.019.","ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363."},"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_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"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_created":"2018-12-11T11:53:43Z","doi":"10.1016/j.tcs.2014.08.019","date_published":"2014-12-04T00:00:00Z","page":"348 - 363","publication":"Theoretical Computer Science","day":"04","year":"2014","oa":1,"quality_controlled":"1","publisher":"Elsevier"},{"ddc":["000","004"],"date_updated":"2023-02-23T12:23:54Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:26Z","_id":"2038","pubrep_id":"192","status":"public","article_type":"original","type":"journal_article","language":[{"iso":"eng"}],"file":[{"date_updated":"2020-07-14T12:45:26Z","file_size":346184,"creator":"system","date_created":"2018-12-12T10:10:59Z","file_name":"IST-2014-192-v1+1_AccumulativeValues.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"354c41d37500b56320afce94cf9a99c2","file_id":"4851"}],"publication_status":"published","ec_funded":1,"volume":15,"related_material":{"record":[{"status":"public","id":"3356","relation":"earlier_version"},{"relation":"earlier_version","status":"public","id":"5385"}]},"issue":"4","oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with "controlled accumulation," allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable."}],"intvolume":" 15","month":"09","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 4, 27, ACM, 2014, doi:10.1145/2629686.","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2014). Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2629686","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 2014;15(4). doi:10.1145/2629686","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 15 (2014).","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 4. ACM, 2014.","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic (TOCL). ACM, 2014. https://doi.org/10.1145/2629686.","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 15(4), 27."},"title":"Temporal specifications with accumulative values","article_processing_charge":"No","author":[{"full_name":"Boker, Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Orna","full_name":"Kupferman, Orna","last_name":"Kupferman"}],"publist_id":"5013","article_number":"27","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publication":"ACM Transactions on Computational Logic (TOCL)","day":"16","year":"2014","has_accepted_license":"1","date_created":"2018-12-11T11:55:21Z","doi":"10.1145/2629686","date_published":"2014-09-16T00:00:00Z","acknowledgement":"The research was supported in part by ERC Starting grant 278410 (QUALITY).","oa":1,"quality_controlled":"1","publisher":"ACM"},{"_id":"5411","status":"public","pubrep_id":"152","type":"technical_report","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"citation":{"apa":"Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional specifications for IOCO testing. IST Austria. https://doi.org/10.15479/AT:IST-2014-148-v2-1","ama":"Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional Specifications for IOCO Testing. IST Austria; 2014. doi:10.15479/AT:IST-2014-148-v2-1","ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications for IOCO testing. IST Austria, 2014.","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications for IOCO Testing, IST Austria, 2014.","mla":"Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing. IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1.","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing, IST Austria, 20p.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. Compositional Specifications for IOCO Testing. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-148-v2-1."},"date_updated":"2023-02-23T10:31:07Z","title":"Compositional specifications for IOCO testing","file_date_updated":"2020-07-14T12:46:46Z","department":[{"_id":"ToHe"}],"author":[{"full_name":"Daca, Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Krenn, Willibald","last_name":"Krenn","first_name":"Willibald"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing.\r\nIn this paper, we study compositional properties of the IOCO-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the IOCO conformance relation, the resulting methodology can be applied to a broader class of systems."}],"month":"01","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"day":"28","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"0e03aba625cc334141a3148432aa5760","file_id":"5543","date_updated":"2020-07-14T12:46:46Z","file_size":534732,"creator":"system","date_created":"2018-12-12T11:54:21Z","file_name":"IST-2014-148-v2+1_main_tr.pdf"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2014","date_published":"2014-01-28T00:00:00Z","doi":"10.15479/AT:IST-2014-148-v2-1","related_material":{"record":[{"relation":"later_version","status":"public","id":"2167"}]},"date_created":"2018-12-12T11:39:11Z","page":"20"},{"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"T. A. Henzinger and J. Otop, “Model measuring for hybrid systems,” in Proceedings of the 17th international conference on Hybrid systems: computation and control, Berlin, Germany, 2014, pp. 213–222.","short":"T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222.","ama":"Henzinger TA, Otop J. Model measuring for hybrid systems. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control. Springer; 2014:213-222. doi:10.1145/2562059.2562130","apa":"Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems. In Proceedings of the 17th international conference on Hybrid systems: computation and control (pp. 213–222). Berlin, Germany: Springer. https://doi.org/10.1145/2562059.2562130","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Hybrid Systems.” Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–22, doi:10.1145/2562059.2562130.","ista":"Henzinger TA, Otop J. 2014. Model measuring for hybrid systems. Proceedings of the 17th international conference on Hybrid systems: computation and control. HSCC: Hybrid Systems - Computation and Control, 213–222.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Hybrid Systems.” In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, 213–22. Springer, 2014. https://doi.org/10.1145/2562059.2562130."},"title":"Model measuring for hybrid systems","article_processing_charge":"No","author":[{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"4751","acknowledgement":"This work was supported in part by the Austrian Science Fund NFN RiSE (Rigorous Systems Engineering) and by the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).\r\nA Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/171","publisher":"Springer","quality_controlled":"1","publication":"Proceedings of the 17th international conference on Hybrid systems: computation and control","day":"01","year":"2014","date_created":"2018-12-11T11:56:23Z","date_published":"2014-04-01T00:00:00Z","doi":"10.1145/2562059.2562130","page":"213 - 222","_id":"2217","status":"public","conference":{"start_date":"2014-04-15","location":"Berlin, Germany","end_date":"2014-04-17","name":"HSCC: Hybrid Systems - Computation and Control"},"type":"conference","date_updated":"2023-02-23T12:25:23Z","department":[{"_id":"ToHe"}],"oa_version":"None","abstract":[{"text":"As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.\r\n\r\nThe contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem.","lang":"eng"}],"month":"04","scopus_import":1,"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"related_material":{"record":[{"status":"public","id":"5416","relation":"earlier_version"}]}},{"abstract":[{"lang":"eng","text":"We define the model-measuring problem: given a model M and specification φ, what is the maximal distance ρ such that all models M'within distance ρ from M satisfy (or violate)φ. The model measuring problem presupposes a distance function on models. We concentrate on automatic distance functions, which are defined by weighted automata.\r\nThe model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification, and robustness problems that measure how much a model can be perturbed without violating the specification.\r\nWe show that for automatic distance functions, and ω-regular linear-time and branching-time specifications, the model-measuring problem can be solved.\r\nWe use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for standard word and tree automata by the optimal-weight question for the weighted versions of these automata. We consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. \r\nWe give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications."}],"oa_version":"Published Version","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","month":"02","publication_status":"published","year":"2014","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"file":[{"checksum":"fcc3eab903cfcd3778b338d2d0d44d18","file_id":"5481","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2014-172-v1+1_report.pdf","date_created":"2018-12-12T11:53:20Z","creator":"system","file_size":383052,"date_updated":"2020-07-14T12:46:49Z"}],"day":"19","page":"14","date_created":"2018-12-12T11:39:13Z","date_published":"2014-02-19T00:00:00Z","doi":"10.15479/AT:IST-2014-172-v1-1","related_material":{"record":[{"id":"2327","status":"public","relation":"later_version"}]},"_id":"5417","type":"technical_report","pubrep_id":"175","status":"public","date_updated":"2023-02-23T10:38:10Z","citation":{"ista":"Henzinger TA, Otop J. 2014. From model checking to model measuring, IST Austria, 14p.","chicago":"Henzinger, Thomas A, and Jan Otop. From Model Checking to Model Measuring. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-172-v1-1.","apa":"Henzinger, T. A., & Otop, J. (2014). From model checking to model measuring. IST Austria. https://doi.org/10.15479/AT:IST-2014-172-v1-1","ama":"Henzinger TA, Otop J. From Model Checking to Model Measuring. IST Austria; 2014. doi:10.15479/AT:IST-2014-172-v1-1","short":"T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria, 2014.","ieee":"T. A. Henzinger and J. Otop, From model checking to model measuring. IST Austria, 2014.","mla":"Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring. IST Austria, 2014, doi:10.15479/AT:IST-2014-172-v1-1."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"file_date_updated":"2020-07-14T12:46:49Z","title":"From model checking to model measuring","department":[{"_id":"ToHe"}]},{"oa":1,"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"month":"02","abstract":[{"text":"As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.The contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem.","lang":"eng"}],"oa_version":"Published Version","page":"22","date_created":"2018-12-12T11:39:12Z","date_published":"2014-02-19T00:00:00Z","doi":"10.15479/AT:IST-2014-171-v1-1","related_material":{"record":[{"relation":"later_version","id":"2217","status":"public"}]},"year":"2014","publication_status":"published","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"day":"19","file":[{"checksum":"445456d22371e4e49aad2b9a0c13bf80","file_id":"5492","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2014-171-v1+1_report.pdf","date_created":"2018-12-12T11:53:32Z","creator":"system","file_size":712077,"date_updated":"2020-07-14T12:46:49Z"}],"type":"technical_report","pubrep_id":"171","status":"public","_id":"5416","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan"}],"title":"Model measuring for hybrid systems","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:46:49Z","citation":{"chicago":"Henzinger, Thomas A, and Jan Otop. Model Measuring for Hybrid Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-171-v1-1.","ista":"Henzinger TA, Otop J. 2014. Model measuring for hybrid systems, IST Austria, 22p.","mla":"Henzinger, Thomas A., and Jan Otop. Model Measuring for Hybrid Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-171-v1-1.","ieee":"T. A. Henzinger and J. Otop, Model measuring for hybrid systems. IST Austria, 2014.","short":"T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014.","apa":"Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-171-v1-1","ama":"Henzinger TA, Otop J. Model Measuring for Hybrid Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-171-v1-1"},"date_updated":"2023-02-23T10:33:21Z","ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"month":"02","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Recently there has been a significant effort to add 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, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains. "}],"date_published":"2014-02-19T00:00:00Z","doi":"10.15479/AT:IST-2014-170-v1-1","related_material":{"record":[{"relation":"later_version","id":"1656","status":"public"},{"relation":"later_version","id":"467","status":"public"},{"relation":"later_version","id":"5436","status":"public"}]},"date_created":"2018-12-12T11:39:12Z","page":"27","file":[{"file_name":"IST-2014-170-v1+1_main.pdf","date_created":"2018-12-12T11:53:36Z","file_size":573457,"date_updated":"2020-07-14T12:46:48Z","creator":"system","file_id":"5497","checksum":"31f90dcf2cf899c3f8c6427cfcc2b3c7","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"day":"19","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2014","status":"public","pubrep_id":"170","type":"technical_report","_id":"5415","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:46:48Z","title":"Nested weighted automata","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"ddc":["004"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:26:19Z","citation":{"ista":"Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted Automata. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-170-v1-1.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria; 2014. doi:10.15479/AT:IST-2014-170-v1-1","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2014). Nested weighted automata. IST Austria. https://doi.org/10.15479/AT:IST-2014-170-v1-1","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata. IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2014, doi:10.15479/AT:IST-2014-170-v1-1."}},{"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"title":"Regression-free synthesis for concurrency","author":[{"full_name":"Cerny, Pavol","last_name":"Cerny","first_name":"Pavol"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna"},{"last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid","first_name":"Leonid"},{"first_name":"Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach","full_name":"Tarrach, Thorsten","orcid":"0000-0003-4409-8487"}],"publist_id":"4749","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. “Regression-Free Synthesis for Concurrency,” 8559:568–84. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_38.","ista":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559, 568–584.","mla":"Cerny, Pavol, et al. Regression-Free Synthesis for Concurrency. Vol. 8559, Springer, 2014, pp. 568–84, doi:10.1007/978-3-319-08867-9_38.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2014, pp. 568–584.","ieee":"P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Regression-free synthesis for concurrency,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 568–584.","apa":"Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach, T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_38","ama":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Regression-free synthesis for concurrency. In: Vol 8559. Springer; 2014:568-584. doi:10.1007/978-3-319-08867-9_38"},"quality_controlled":"1","publisher":"Springer","oa":1,"doi":"10.1007/978-3-319-08867-9_38","date_published":"2014-07-22T00:00:00Z","date_created":"2018-12-11T11:56:23Z","page":"568 - 584","day":"22","has_accepted_license":"1","year":"2014","status":"public","pubrep_id":"297","type":"conference","conference":{"name":"CAV: Computer Aided Verification","location":"Vienna, Austria","end_date":"2014-07-22","start_date":"2014-07-18"},"_id":"2218","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:33Z","ddc":["000"],"date_updated":"2023-09-07T11:57:01Z","month":"07","intvolume":" 8559","alternative_title":["LNCS"],"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38","open_access":"1"}],"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in the repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs."}],"volume":8559,"related_material":{"record":[{"status":"public","id":"1130","relation":"dissertation_contains"}]},"ec_funded":1,"file":[{"file_name":"IST-2014-297-v1+1_cav14-final.pdf","date_created":"2018-12-12T10:13:14Z","file_size":416732,"date_updated":"2020-07-14T12:45:33Z","creator":"system","file_id":"4995","checksum":"a631d3105509f239724644e77a1212e2","content_type":"application/pdf","relation":"main_file","access_level":"open_access"},{"creator":"system","date_updated":"2020-07-14T12:45:33Z","file_size":616293,"date_created":"2018-12-12T10:13:15Z","file_name":"IST-2014-297-v2+1_cav14-final2.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"4996","checksum":"f8b0f748cc9fa697ca992cc56c87bc4e"}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-331908866-2"]},"publication_status":"published"},{"ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5411"},{"status":"public","id":"1155","relation":"dissertation_contains"}]},"publication_status":"published","publication_identifier":{"issn":["2159-4848"],"isbn":["978-1-4799-2255-0"]},"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1904.07083"}],"scopus_import":1,"month":"03","abstract":[{"text":"Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing. In this paper, we study compositional properties of the ioco-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the ioco conformance relation, the resulting methodology can be applied to a broader class of systems.","lang":"eng"}],"oa_version":"Preprint","department":[{"_id":"ToHe"}],"date_updated":"2023-09-07T11:58:33Z","conference":{"name":"ICST: International Conference on Software Testing, Verification and Validation","location":"Cleveland, USA","end_date":"2014-04-04","start_date":"2014-03-31"},"type":"conference","status":"public","_id":"2167","date_created":"2018-12-11T11:56:06Z","doi":"10.1109/ICST.2014.50","date_published":"2014-03-01T00:00:00Z","year":"2014","publication":"IEEE 7th International Conference on Software Testing, Verification and Validation","day":"01","oa":1,"publisher":"IEEE","quality_controlled":"1","article_processing_charge":"No","external_id":{"arxiv":["1904.07083"]},"publist_id":"4817","author":[{"full_name":"Daca, Przemyslaw","last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Krenn","full_name":"Krenn, Willibald","first_name":"Willibald"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan"}],"title":"Compositional specifications for IOCO testing","citation":{"mla":"Daca, Przemyslaw, et al. “Compositional Specifications for IOCO Testing.” IEEE 7th International Conference on Software Testing, Verification and Validation, 6823899, IEEE, 2014, doi:10.1109/ICST.2014.50.","apa":"Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional specifications for IOCO testing. In IEEE 7th International Conference on Software Testing, Verification and Validation. Cleveland, USA: IEEE. https://doi.org/10.1109/ICST.2014.50","ama":"Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional specifications for IOCO testing. In: IEEE 7th International Conference on Software Testing, Verification and Validation. IEEE; 2014. doi:10.1109/ICST.2014.50","ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, “Compositional specifications for IOCO testing,” in IEEE 7th International Conference on Software Testing, Verification and Validation, Cleveland, USA, 2014.","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, in:, IEEE 7th International Conference on Software Testing, Verification and Validation, IEEE, 2014.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. “Compositional Specifications for IOCO Testing.” In IEEE 7th International Conference on Software Testing, Verification and Validation. IEEE, 2014. https://doi.org/10.1109/ICST.2014.50.","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing. IEEE 7th International Conference on Software Testing, Verification and Validation. ICST: International Conference on Software Testing, Verification and Validation, 6823899."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"article_number":"6823899"},{"_id":"2063","conference":{"start_date":"2014-07-18","end_date":"2014-07-22","location":"Vienna, Austria","name":"CAV: Computer Aided Verification"},"type":"conference","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"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"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"status":"public","date_updated":"2023-09-07T11:58:33Z","citation":{"mla":"Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31.","apa":"Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 473–490.","short":"K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31.","ista":"Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca"}],"publist_id":"4978","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"CEGAR for qualitative analysis of probabilistic systems","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements."}],"oa_version":"None","quality_controlled":"1","publisher":"Springer","alternative_title":["LNCS"],"intvolume":" 8559","month":"07","publication_status":"published","year":"2014","language":[{"iso":"eng"}],"day":"01","page":"473 - 490","date_created":"2018-12-11T11:55:30Z","ec_funded":1,"doi":"10.1007/978-3-319-08867-9_31","date_published":"2014-07-01T00:00:00Z","related_material":{"record":[{"relation":"earlier_version","id":"5412","status":"public"},{"relation":"earlier_version","id":"5413","status":"public"},{"id":"5414","status":"public","relation":"earlier_version"},{"id":"1155","status":"public","relation":"dissertation_contains"}]},"volume":8559}]