--- _id: '1733' abstract: - lang: eng 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. author: - first_name: Pavol full_name: Cerny, Pavol last_name: Cerny - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Arjun full_name: Radhakrishna, Arjun id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87 last_name: Radhakrishna citation: 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 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. 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. ista: Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 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. short: P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363. date_created: 2018-12-11T11:53:43Z date_published: 2014-12-04T00:00:00Z date_updated: 2023-02-23T11:04:00Z day: '04' department: - _id: ToHe - _id: KrCh doi: 10.1016/j.tcs.2014.08.019 ec_funded: 1 intvolume: ' 560' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1210.2450 month: '12' oa: 1 oa_version: Submitted Version page: 348 - 363 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Theoretical Computer Science publication_status: published publisher: Elsevier publist_id: '5392' quality_controlled: '1' related_material: record: - id: '2916' relation: earlier_version status: public scopus_import: 1 status: public title: Interface simulation distances type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 560 year: '2014' ... --- _id: '2038' 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. acknowledgement: The research was supported in part by ERC Starting grant 278410 (QUALITY). article_number: '27' article_processing_charge: No article_type: original author: - first_name: Udi full_name: Boker, Udi id: 31E297B6-F248-11E8-B48F-1D18A9856A87 last_name: Boker - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman citation: 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 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 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. 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. 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. short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 15 (2014). date_created: 2018-12-11T11:55:21Z date_published: 2014-09-16T00:00:00Z date_updated: 2023-02-23T12:23:54Z day: '16' ddc: - '000' - '004' department: - _id: ToHe - _id: KrCh doi: 10.1145/2629686 ec_funded: 1 file: - access_level: open_access checksum: 354c41d37500b56320afce94cf9a99c2 content_type: application/pdf creator: system date_created: 2018-12-12T10:10:59Z date_updated: 2020-07-14T12:45:26Z file_id: '4851' file_name: IST-2014-192-v1+1_AccumulativeValues.pdf file_size: 346184 relation: main_file file_date_updated: 2020-07-14T12:45:26Z has_accepted_license: '1' intvolume: ' 15' issue: '4' language: - iso: eng month: '09' oa: 1 oa_version: Submitted Version project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: ACM Transactions on Computational Logic (TOCL) publication_status: published publisher: ACM publist_id: '5013' pubrep_id: '192' quality_controlled: '1' related_material: record: - id: '3356' relation: earlier_version status: public - id: '5385' relation: earlier_version status: public scopus_import: 1 status: public title: Temporal specifications with accumulative values type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 15 year: '2014' ... --- _id: '5411' 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." alternative_title: - IST Austria Technical Report author: - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Willibald full_name: Krenn, Willibald last_name: Krenn - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic citation: 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 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 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. ieee: P. Daca, T. A. Henzinger, W. Krenn, and 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. 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. date_created: 2018-12-12T11:39:11Z date_published: 2014-01-28T00:00:00Z date_updated: 2023-02-23T10:31:07Z day: '28' ddc: - '000' department: - _id: ToHe doi: 10.15479/AT:IST-2014-148-v2-1 file: - access_level: open_access checksum: 0e03aba625cc334141a3148432aa5760 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:21Z date_updated: 2020-07-14T12:46:46Z file_id: '5543' file_name: IST-2014-148-v2+1_main_tr.pdf file_size: 534732 relation: main_file file_date_updated: 2020-07-14T12:46:46Z has_accepted_license: '1' language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: '20' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '152' related_material: record: - id: '2167' relation: later_version status: public status: public title: Compositional specifications for IOCO testing type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '2217' abstract: - lang: eng 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." 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" article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop citation: 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' 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.' 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.' 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.' 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.' short: 'T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222.' conference: end_date: 2014-04-17 location: Berlin, Germany name: 'HSCC: Hybrid Systems - Computation and Control' start_date: 2014-04-15 date_created: 2018-12-11T11:56:23Z date_published: 2014-04-01T00:00:00Z date_updated: 2023-02-23T12:25:23Z day: '01' department: - _id: ToHe doi: 10.1145/2562059.2562130 ec_funded: 1 language: - iso: eng month: '04' oa_version: None page: 213 - 222 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication: 'Proceedings of the 17th international conference on Hybrid systems: computation and control' publication_status: published publisher: Springer publist_id: '4751' quality_controlled: '1' related_material: record: - id: '5416' relation: earlier_version status: public scopus_import: 1 status: public title: Model measuring for hybrid systems type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5417' 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." alternative_title: - IST Austria Technical Report author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop citation: ama: Henzinger TA, Otop J. From Model Checking to Model Measuring. IST Austria; 2014. doi: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 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. 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. 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. short: T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria, 2014. date_created: 2018-12-12T11:39:13Z date_published: 2014-02-19T00:00:00Z date_updated: 2023-02-23T10:38:10Z day: '19' ddc: - '000' department: - _id: ToHe doi: 10.15479/AT:IST-2014-172-v1-1 file: - access_level: open_access checksum: fcc3eab903cfcd3778b338d2d0d44d18 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:20Z date_updated: 2020-07-14T12:46:49Z file_id: '5481' file_name: IST-2014-172-v1+1_report.pdf file_size: 383052 relation: main_file file_date_updated: 2020-07-14T12:46:49Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '14' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '175' related_material: record: - id: '2327' relation: later_version status: public status: public title: From model checking to model measuring type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5416' abstract: - lang: eng 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. alternative_title: - IST Austria Technical Report author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop citation: ama: Henzinger TA, Otop J. Model Measuring for Hybrid Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-171-v1-1 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 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. ieee: T. A. Henzinger and J. Otop, Model measuring for hybrid systems. IST Austria, 2014. 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. short: T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014. date_created: 2018-12-12T11:39:12Z date_published: 2014-02-19T00:00:00Z date_updated: 2023-02-23T10:33:21Z day: '19' ddc: - '005' department: - _id: ToHe doi: 10.15479/AT:IST-2014-171-v1-1 file: - access_level: open_access checksum: 445456d22371e4e49aad2b9a0c13bf80 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:32Z date_updated: 2020-07-14T12:46:49Z file_id: '5492' file_name: IST-2014-171-v1+1_report.pdf file_size: 712077 relation: main_file file_date_updated: 2020-07-14T12:46:49Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '22' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '171' related_material: record: - id: '2217' relation: later_version status: public status: public title: Model measuring for hybrid systems type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5415' 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. ' alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop citation: 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 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. ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata. IST Austria, 2014. ista: Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p. mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2014, doi:10.15479/AT:IST-2014-170-v1-1. short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014. date_created: 2018-12-12T11:39:12Z date_published: 2014-02-19T00:00:00Z date_updated: 2023-02-23T12:26:19Z day: '19' ddc: - '004' department: - _id: KrCh - _id: ToHe doi: 10.15479/AT:IST-2014-170-v1-1 file: - access_level: open_access checksum: 31f90dcf2cf899c3f8c6427cfcc2b3c7 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:36Z date_updated: 2020-07-14T12:46:48Z file_id: '5497' file_name: IST-2014-170-v1+1_main.pdf file_size: 573457 relation: main_file file_date_updated: 2020-07-14T12:46:48Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '27' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '170' related_material: record: - id: '1656' relation: later_version status: public - id: '467' relation: later_version status: public - id: '5436' relation: later_version status: public status: public title: Nested weighted automata type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '2218' 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. alternative_title: - LNCS author: - first_name: Pavol full_name: Cerny, Pavol last_name: Cerny - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Arjun full_name: Radhakrishna, Arjun id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87 last_name: Radhakrishna - first_name: Leonid full_name: Ryzhyk, Leonid last_name: Ryzhyk - first_name: Thorsten full_name: Tarrach, Thorsten id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87 last_name: Tarrach orcid: 0000-0003-4409-8487 citation: 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' 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' 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. 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.' 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. conference: end_date: 2014-07-22 location: Vienna, Austria name: 'CAV: Computer Aided Verification' start_date: 2014-07-18 date_created: 2018-12-11T11:56:23Z date_published: 2014-07-22T00:00:00Z date_updated: 2023-09-07T11:57:01Z day: '22' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-319-08867-9_38 ec_funded: 1 file: - access_level: open_access checksum: a631d3105509f239724644e77a1212e2 content_type: application/pdf creator: system date_created: 2018-12-12T10:13:14Z date_updated: 2020-07-14T12:45:33Z file_id: '4995' file_name: IST-2014-297-v1+1_cav14-final.pdf file_size: 416732 relation: main_file - access_level: open_access checksum: f8b0f748cc9fa697ca992cc56c87bc4e content_type: application/pdf creator: system date_created: 2018-12-12T10:13:15Z date_updated: 2020-07-14T12:45:33Z file_id: '4996' file_name: IST-2014-297-v2+1_cav14-final2.pdf file_size: 616293 relation: main_file file_date_updated: 2020-07-14T12:45:33Z has_accepted_license: '1' intvolume: ' 8559' language: - iso: eng main_file_link: - open_access: '1' url: https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38 month: '07' oa: 1 oa_version: Submitted Version page: 568 - 584 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication_identifier: isbn: - 978-331908866-2 publication_status: published publisher: Springer publist_id: '4749' pubrep_id: '297' quality_controlled: '1' related_material: record: - id: '1130' relation: dissertation_contains status: public status: public title: Regression-free synthesis for concurrency type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8559 year: '2014' ... --- _id: '2167' 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. 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. article_number: '6823899' article_processing_charge: No author: - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Willibald full_name: Krenn, Willibald last_name: Krenn - first_name: Dejan full_name: Nickovic, Dejan last_name: Nickovic citation: 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' 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' 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. 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. 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.' 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. short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, in:, IEEE 7th International Conference on Software Testing, Verification and Validation, IEEE, 2014. conference: end_date: 2014-04-04 location: Cleveland, USA name: 'ICST: International Conference on Software Testing, Verification and Validation' start_date: 2014-03-31 date_created: 2018-12-11T11:56:06Z date_published: 2014-03-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: ToHe doi: 10.1109/ICST.2014.50 ec_funded: 1 external_id: arxiv: - '1904.07083' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1904.07083 month: '03' oa: 1 oa_version: Preprint project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication: IEEE 7th International Conference on Software Testing, Verification and Validation publication_identifier: isbn: - 978-1-4799-2255-0 issn: - 2159-4848 publication_status: published publisher: IEEE publist_id: '4817' quality_controlled: '1' related_material: record: - id: '5411' relation: earlier_version status: public - id: '1155' relation: dissertation_contains status: public scopus_import: 1 status: public title: Compositional specifications for IOCO testing type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '2063' 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. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca citation: 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' 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' 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. 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.' ista: 'Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.' 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. short: K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490. conference: end_date: 2014-07-22 location: Vienna, Austria name: 'CAV: Computer Aided Verification' start_date: 2014-07-18 date_created: 2018-12-11T11:55:30Z date_published: 2014-07-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-08867-9_31 ec_funded: 1 intvolume: ' 8559' language: - iso: eng month: '07' oa_version: None page: 473 - 490 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF 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 - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication_status: published publisher: Springer publist_id: '4978' quality_controlled: '1' related_material: record: - id: '5412' relation: earlier_version status: public - id: '5413' relation: earlier_version status: public - id: '5414' relation: earlier_version status: public - id: '1155' relation: dissertation_contains status: public status: public title: CEGAR for qualitative analysis of probabilistic systems type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8559 year: '2014' ...