[{"day":"04","scopus_import":1,"date_published":"2014-12-04T00:00:00Z","page":"348 - 363","citation":{"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.","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","ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363.","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","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.","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.","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."},"publication":"Theoretical Computer Science","issue":"3","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"}],"type":"journal_article","oa_version":"Submitted Version","intvolume":" 560","title":"Interface simulation distances","status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"1733","month":"12","language":[{"iso":"eng"}],"doi":"10.1016/j.tcs.2014.08.019","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","main_file_link":[{"url":"http://arxiv.org/abs/1210.2450","open_access":"1"}],"oa":1,"ec_funded":1,"publist_id":"5392","volume":560,"date_created":"2018-12-11T11:53:43Z","date_updated":"2023-02-23T11:04:00Z","related_material":{"record":[{"id":"2916","status":"public","relation":"earlier_version"}]},"author":[{"full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Elsevier","publication_status":"published","year":"2014"},{"language":[{"iso":"eng"}],"doi":"10.1145/2629686","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","oa":1,"month":"09","volume":15,"date_updated":"2023-02-23T12:23:54Z","date_created":"2018-12-11T11:55:21Z","related_material":{"record":[{"id":"3356","relation":"earlier_version","status":"public"},{"relation":"earlier_version","status":"public","id":"5385"}]},"author":[{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"ACM","publication_status":"published","acknowledgement":"The research was supported in part by ERC Starting grant 278410 (QUALITY).","year":"2014","publist_id":"5013","ec_funded":1,"file_date_updated":"2020-07-14T12:45:26Z","article_number":"27","date_published":"2014-09-16T00:00:00Z","article_type":"original","citation":{"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","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.","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 15(4), 27.","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","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.","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 15 (2014).","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."},"publication":"ACM Transactions on Computational Logic (TOCL)","has_accepted_license":"1","article_processing_charge":"No","day":"16","scopus_import":1,"file":[{"file_name":"IST-2014-192-v1+1_AccumulativeValues.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":346184,"file_id":"4851","relation":"main_file","date_updated":"2020-07-14T12:45:26Z","date_created":"2018-12-12T10:10:59Z","checksum":"354c41d37500b56320afce94cf9a99c2"}],"oa_version":"Submitted Version","pubrep_id":"192","intvolume":" 15","title":"Temporal specifications with accumulative values","status":"public","ddc":["000","004"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"2038","issue":"4","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."}],"type":"journal_article"},{"month":"01","day":"28","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"page":"20","oa":1,"citation":{"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.","mla":"Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing. IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1.","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications for IOCO Testing, IST Austria, 2014.","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing, IST Austria, 20p.","ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications for IOCO testing. IST Austria, 2014.","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"},"language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2014-148-v2-1","date_published":"2014-01-28T00:00:00Z","alternative_title":["IST Austria Technical Report"],"type":"technical_report","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.\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.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:46Z","status":"public","publication_status":"published","title":"Compositional specifications for IOCO testing","ddc":["000"],"department":[{"_id":"ToHe"}],"publisher":"IST Austria","_id":"5411","year":"2014","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-12T11:39:11Z","date_updated":"2023-02-23T10:31:07Z","file":[{"relation":"main_file","file_id":"5543","checksum":"0e03aba625cc334141a3148432aa5760","date_created":"2018-12-12T11:54:21Z","date_updated":"2020-07-14T12:46:46Z","access_level":"open_access","file_name":"IST-2014-148-v2+1_main_tr.pdf","content_type":"application/pdf","file_size":534732,"creator":"system"}],"oa_version":"Published Version","author":[{"full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","last_name":"Daca"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Krenn, Willibald","first_name":"Willibald","last_name":"Krenn"},{"full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","last_name":"Nickovic"}],"related_material":{"record":[{"id":"2167","relation":"later_version","status":"public"}]},"pubrep_id":"152"},{"title":"Model measuring for hybrid systems","status":"public","_id":"2217","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","type":"conference","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"}],"page":"213 - 222","publication":"Proceedings of the 17th international conference on Hybrid systems: computation and control","citation":{"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.","short":"T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222.","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.","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.","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","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.","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"},"date_published":"2014-04-01T00:00:00Z","scopus_import":1,"day":"01","article_processing_charge":"No","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"year":"2014","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","date_updated":"2023-02-23T12:25:23Z","date_created":"2018-12-11T11:56:23Z","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"related_material":{"record":[{"id":"5416","status":"public","relation":"earlier_version"}]},"publist_id":"4751","ec_funded":1,"quality_controlled":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"language":[{"iso":"eng"}],"conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2014-04-17","start_date":"2014-04-15","location":"Berlin, Germany"},"doi":"10.1145/2562059.2562130","month":"04"},{"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"day":"19","month":"02","citation":{"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","ieee":"T. A. Henzinger and J. Otop, From model checking to model measuring. IST Austria, 2014.","ista":"Henzinger TA, Otop J. 2014. From model checking to model measuring, IST Austria, 14p.","ama":"Henzinger TA, Otop J. From Model Checking to Model Measuring. IST Austria; 2014. doi:10.15479/AT:IST-2014-172-v1-1","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.","short":"T.A. Henzinger, 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."},"oa":1,"page":"14","date_published":"2014-02-19T00:00:00Z","doi":"10.15479/AT:IST-2014-172-v1-1","language":[{"iso":"eng"}],"type":"technical_report","alternative_title":["IST Austria Technical Report"],"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."}],"file_date_updated":"2020-07-14T12:46:49Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5417","year":"2014","department":[{"_id":"ToHe"}],"publisher":"IST Austria","publication_status":"published","title":"From model checking to model measuring","status":"public","ddc":["000"],"pubrep_id":"175","related_material":{"record":[{"id":"2327","status":"public","relation":"later_version"}]},"author":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"}],"oa_version":"Published Version","file":[{"access_level":"open_access","file_name":"IST-2014-172-v1+1_report.pdf","creator":"system","content_type":"application/pdf","file_size":383052,"file_id":"5481","relation":"main_file","checksum":"fcc3eab903cfcd3778b338d2d0d44d18","date_created":"2018-12-12T11:53:20Z","date_updated":"2020-07-14T12:46:49Z"}],"date_created":"2018-12-12T11:39:13Z","date_updated":"2023-02-23T10:38:10Z"}]