--- _id: '10774' abstract: - lang: eng text: We study the problem of specifying sequential information-flow properties of systems. Information-flow properties are hyperproperties, as they compare different traces of a system. Sequential information-flow properties can express changes, over time, in the information-flow constraints. For example, information-flow constraints during an initialization phase of a system may be different from information-flow constraints that are required during the operation phase. We formalize several variants of interpreting sequential information-flow constraints, which arise from different assumptions about what can be observed of the system. For this purpose, we introduce a first-order logic, called Hypertrace Logic, with both trace and time quantifiers for specifying linear-time hyperproperties. We prove that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted quantifier prefixes, cannot specify the majority of the studied variants of sequential information flow, including all variants in which the transition between sequential phases (such as initialization and operation) happens asynchronously. Our results rely on new equivalences between sets of traces that cannot be distinguished by certain classes of formulas from Hypertrace Logic. This presents a new approach to proving inexpressiveness results for HyperLTL. acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of the Austrian Science Fund (FWF) and by the FWF project W1255-N23. alternative_title: - LNCS article_processing_charge: No author: - first_name: Ezio full_name: Bartocci, Ezio last_name: Bartocci - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - 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: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Ana Oliveira full_name: Da Costa, Ana Oliveira last_name: Da Costa citation: ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential information flow. In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 13182. Springer Nature; 2022:1-19. doi:10.1007/978-3-030-94583-1_1' apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa, A. O. (2022). Flavors of sequential information flow. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13182, pp. 1–19). Philadelphia, PA, United States: Springer Nature. https://doi.org/10.1007/978-3-030-94583-1_1' chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 13182:1–19. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-94583-1_1. ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Flavors of sequential information flow,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Philadelphia, PA, United States, 2022, vol. 13182, pp. 1–19. ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors of sequential information flow. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182, 1–19.' mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13182, Springer Nature, 2022, pp. 1–19, doi:10.1007/978-3-030-94583-1_1. short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp. 1–19. conference: end_date: 2022-01-18 location: Philadelphia, PA, United States name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation' start_date: 2022-01-16 date_created: 2022-02-20T23:01:34Z date_published: 2022-01-14T00:00:00Z date_updated: 2022-08-05T09:02:56Z day: '14' department: - _id: ToHe doi: 10.1007/978-3-030-94583-1_1 external_id: arxiv: - '2105.02013' intvolume: ' 13182' language: - iso: eng main_file_link: - open_access: '1' url: ' https://doi.org/10.48550/arXiv.2105.02013' month: '01' oa: 1 oa_version: Preprint page: 1-19 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_identifier: eissn: - '16113349' isbn: - '9783030945824' issn: - '03029743' publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Flavors of sequential information flow type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13182 year: '2022' ... --- _id: '11355' abstract: - lang: eng text: "Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees.\r\nAlthough there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain." acknowledgement: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 956123 and was funded in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093. alternative_title: - LNCS article_processing_charge: No author: - first_name: Ezio full_name: Bartocci, Ezio last_name: Bartocci - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - 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: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Ana Oliveira full_name: Da Costa, Ana Oliveira last_name: Da Costa citation: ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow interfaces. In: Fundamental Approaches to Software Engineering. Vol 13241. Springer Nature; 2022:3-22. doi:10.1007/978-3-030-99429-7_1' apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa, A. O. (2022). Information-flow interfaces. In Fundamental Approaches to Software Engineering (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. https://doi.org/10.1007/978-3-030-99429-7_1' chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Information-Flow Interfaces.” In Fundamental Approaches to Software Engineering, 13241:3–22. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-99429-7_1. ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Information-flow interfaces,” in Fundamental Approaches to Software Engineering, Munich, Germany, 2022, vol. 13241, pp. 3–22. ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13241, 3–22.' mla: Bartocci, Ezio, et al. “Information-Flow Interfaces.” Fundamental Approaches to Software Engineering, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:10.1007/978-3-030-99429-7_1. short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22. conference: end_date: 2022-04-07 location: Munich, Germany name: 'FASE: Fundamental Approaches to Software Engineering' start_date: 2022-04-02 date_created: 2022-05-08T22:01:44Z date_published: 2022-03-29T00:00:00Z date_updated: 2023-08-03T07:03:40Z day: '29' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-030-99429-7_1 ec_funded: 1 external_id: isi: - '000782393600001' file: - access_level: open_access checksum: 7f6f860b20b8de2a249e9c1b4eee15cf content_type: application/pdf creator: dernst date_created: 2022-05-09T06:52:44Z date_updated: 2022-05-09T06:52:44Z file_id: '11357' file_name: 2022_LNCS_Bartocci.pdf file_size: 479146 relation: main_file success: 1 file_date_updated: 2022-05-09T06:52:44Z has_accepted_license: '1' intvolume: ' 13241' isi: 1 language: - iso: eng license: https://creativecommons.org/licenses/by/4.0/ month: '03' oa: 1 oa_version: Published Version page: 3-22 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: Fundamental Approaches to Software Engineering publication_identifier: eissn: - 1611-3349 isbn: - '9783030994280' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Information-flow interfaces tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 13241 year: '2022' ... --- _id: '7348' abstract: - lang: eng text: 'The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence. ' alternative_title: - LIPIcs article_number: '20' article_processing_charge: No author: - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - 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: Bernhard full_name: Kragl, Bernhard id: 320FC952-F248-11E8-B48F-1D18A9856A87 last_name: Kragl orcid: 0000-0001-7745-9117 citation: ama: 'Ferrere T, Henzinger TA, Kragl B. Monitoring event frequencies. In: 28th EACSL Annual Conference on Computer Science Logic. Vol 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CSL.2020.20' apa: 'Ferrere, T., Henzinger, T. A., & Kragl, B. (2020). Monitoring event frequencies. In 28th EACSL Annual Conference on Computer Science Logic (Vol. 152). Barcelona, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2020.20' chicago: Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event Frequencies.” In 28th EACSL Annual Conference on Computer Science Logic, Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CSL.2020.20. ieee: T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,” in 28th EACSL Annual Conference on Computer Science Logic, Barcelona, Spain, 2020, vol. 152. ista: 'Ferrere T, Henzinger TA, Kragl B. 2020. Monitoring event frequencies. 28th EACSL Annual Conference on Computer Science Logic. CSL: Computer Science Logic, LIPIcs, vol. 152, 20.' mla: Ferrere, Thomas, et al. “Monitoring Event Frequencies.” 28th EACSL Annual Conference on Computer Science Logic, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.CSL.2020.20. short: T. Ferrere, T.A. Henzinger, B. Kragl, in:, 28th EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. conference: end_date: 2020-01-16 location: Barcelona, Spain name: 'CSL: Computer Science Logic' start_date: 2020-01-13 date_created: 2020-01-21T11:22:21Z date_published: 2020-01-15T00:00:00Z date_updated: 2021-01-12T08:13:12Z day: '15' ddc: - '000' department: - _id: ToHe doi: 10.4230/LIPIcs.CSL.2020.20 external_id: arxiv: - '1910.06097' file: - access_level: open_access checksum: b9a691d658d075c6369d3304d17fb818 content_type: application/pdf creator: bkragl date_created: 2020-01-21T11:21:04Z date_updated: 2020-07-14T12:47:56Z file_id: '7349' file_name: main.pdf file_size: 617206 relation: main_file file_date_updated: 2020-07-14T12:47:56Z has_accepted_license: '1' intvolume: ' 152' language: - iso: eng month: '01' oa: 1 oa_version: Published Version project: - _id: 25F2ACDE-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: 28th EACSL Annual Conference on Computer Science Logic publication_identifier: isbn: - '9783959771320' issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: 1 status: public title: Monitoring event frequencies tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 152 year: '2020' ... --- _id: '10861' abstract: - lang: eng text: We introduce in this paper AMT2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance. article_processing_charge: No article_type: original author: - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Olivier full_name: Lebeltel, Olivier last_name: Lebeltel - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Dogan full_name: Ulus, Dogan last_name: Ulus citation: ama: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 2020;22(6):741-758. doi:10.1007/s10009-020-00582-z' apa: 'Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. Springer Nature. https://doi.org/10.1007/s10009-020-00582-z' chicago: 'Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” International Journal on Software Tools for Technology Transfer. Springer Nature, 2020. https://doi.org/10.1007/s10009-020-00582-z.' ieee: 'D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” International Journal on Software Tools for Technology Transfer, vol. 22, no. 6. Springer Nature, pp. 741–758, 2020.' ista: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 22(6), 741–758.' mla: 'Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” International Journal on Software Tools for Technology Transfer, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:10.1007/s10009-020-00582-z.' short: D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758. date_created: 2022-03-18T10:10:53Z date_published: 2020-08-03T00:00:00Z date_updated: 2023-09-08T11:52:02Z day: '03' department: - _id: ToHe doi: 10.1007/s10009-020-00582-z external_id: isi: - '000555398600001' intvolume: ' 22' isi: 1 issue: '6' keyword: - Information Systems - Software language: - iso: eng month: '08' oa_version: None page: 741-758 publication: International Journal on Software Tools for Technology Transfer publication_identifier: eissn: - 1433-2787 issn: - 1433-2779 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '299' relation: earlier_version status: public scopus_import: '1' status: public title: 'AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic' type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 22 year: '2020' ... --- _id: '6428' abstract: - lang: eng text: 'Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system.' article_processing_charge: No author: - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Alexandre full_name: Donzé, Alexandre last_name: Donzé - first_name: Hisahiro full_name: Ito, Hisahiro last_name: Ito - first_name: James full_name: Kapinski, James last_name: Kapinski citation: ama: 'Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. Interface-aware signal temporal logic. In: Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM; 2019:57-66. doi:10.1145/3302504.3311800' apa: 'Ferrere, T., Nickovic, D., Donzé, A., Ito, H., & Kapinski, J. (2019). Interface-aware signal temporal logic. In Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control (pp. 57–66). Montreal, Canada: ACM. https://doi.org/10.1145/3302504.3311800' chicago: 'Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James Kapinski. “Interface-Aware Signal Temporal Logic.” In Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, 57–66. ACM, 2019. https://doi.org/10.1145/3302504.3311800.' ieee: 'T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware signal temporal logic,” in Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, Montreal, Canada, 2019, pp. 57–66.' ista: 'Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. 2019. Interface-aware signal temporal logic. Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and Control, 57–66.' mla: 'Ferrere, Thomas, et al. “Interface-Aware Signal Temporal Logic.” Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 57–66, doi:10.1145/3302504.3311800.' short: 'T. Ferrere, D. Nickovic, A. Donzé, H. Ito, J. Kapinski, in:, Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 57–66.' conference: end_date: 2019-04-18 location: Montreal, Canada name: 'HSCC: Hybrid Systems Computation and Control' start_date: 2019-04-16 date_created: 2019-05-13T08:13:46Z date_published: 2019-04-16T00:00:00Z date_updated: 2023-08-25T10:19:23Z day: '16' ddc: - '000' department: - _id: ToHe doi: 10.1145/3302504.3311800 external_id: isi: - '000516713900007' file: - access_level: open_access checksum: b8e967081e051d1c55ca5d18fb187890 content_type: application/pdf creator: dernst date_created: 2020-10-08T17:25:45Z date_updated: 2020-10-08T17:25:45Z file_id: '8633' file_name: 2019_ACM_Ferrere.pdf file_size: 1055421 relation: main_file success: 1 file_date_updated: 2020-10-08T17:25:45Z has_accepted_license: '1' isi: 1 language: - iso: eng month: '04' oa: 1 oa_version: Submitted Version page: 57-66 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: 'Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control' publication_identifier: isbn: - '9781450362825' publication_status: published publisher: ACM quality_controlled: '1' scopus_import: '1' status: public title: Interface-aware signal temporal logic type: conference user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 year: '2019' ... --- _id: '7109' abstract: - lang: eng text: We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended. article_number: '19' article_processing_charge: No article_type: original author: - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Dejan full_name: Ničković, Dejan last_name: Ničković - first_name: Amir full_name: Pnueli, Amir last_name: Pnueli citation: ama: Ferrere T, Maler O, Ničković D, Pnueli A. From real-time logic to timed automata. Journal of the ACM. 2019;66(3). doi:10.1145/3286976 apa: Ferrere, T., Maler, O., Ničković, D., & Pnueli, A. (2019). From real-time logic to timed automata. Journal of the ACM. ACM. https://doi.org/10.1145/3286976 chicago: Ferrere, Thomas, Oded Maler, Dejan Ničković, and Amir Pnueli. “From Real-Time Logic to Timed Automata.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3286976. ieee: T. Ferrere, O. Maler, D. Ničković, and A. Pnueli, “From real-time logic to timed automata,” Journal of the ACM, vol. 66, no. 3. ACM, 2019. ista: Ferrere T, Maler O, Ničković D, Pnueli A. 2019. From real-time logic to timed automata. Journal of the ACM. 66(3), 19. mla: Ferrere, Thomas, et al. “From Real-Time Logic to Timed Automata.” Journal of the ACM, vol. 66, no. 3, 19, ACM, 2019, doi:10.1145/3286976. short: T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019). date_created: 2019-11-26T10:22:32Z date_published: 2019-05-01T00:00:00Z date_updated: 2023-09-06T11:11:56Z day: '01' department: - _id: ToHe doi: 10.1145/3286976 external_id: isi: - '000495406300005' intvolume: ' 66' isi: 1 issue: '3' language: - iso: eng month: '05' oa_version: None project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: Journal of the ACM publication_identifier: issn: - 0004-5411 publication_status: published publisher: ACM quality_controlled: '1' scopus_import: '1' status: public title: From real-time logic to timed automata type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 66 year: '2019' ... --- _id: '7159' abstract: - lang: eng text: 'Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. ' alternative_title: - LNCS article_processing_charge: No author: - first_name: Dejan full_name: Ničković, Dejan last_name: Ničković - first_name: Xin full_name: Qin, Xin last_name: Qin - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Cristinel full_name: Mateis, Cristinel last_name: Mateis - first_name: Jyotirmoy full_name: Deshmukh, Jyotirmoy last_name: Deshmukh citation: ama: 'Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for specifying and extracting signal features. In: 19th International Conference on Runtime Verification. Vol 11757. Springer Nature; 2019:292-309. doi:10.1007/978-3-030-32079-9_17' apa: 'Ničković, D., Qin, X., Ferrere, T., Mateis, C., & Deshmukh, J. (2019). Shape expressions for specifying and extracting signal features. In 19th International Conference on Runtime Verification (Vol. 11757, pp. 292–309). Porto, Portugal: Springer Nature. https://doi.org/10.1007/978-3-030-32079-9_17' chicago: Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In 19th International Conference on Runtime Verification, 11757:292–309. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-32079-9_17. ieee: D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions for specifying and extracting signal features,” in 19th International Conference on Runtime Verification, Porto, Portugal, 2019, vol. 11757, pp. 292–309. ista: 'Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. 2019. Shape expressions for specifying and extracting signal features. 19th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 11757, 292–309.' mla: Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal Features.” 19th International Conference on Runtime Verification, vol. 11757, Springer Nature, 2019, pp. 292–309, doi:10.1007/978-3-030-32079-9_17. short: D. Ničković, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309. conference: end_date: 2019-10-11 location: Porto, Portugal name: 'RV: Runtime Verification' start_date: 2019-10-08 date_created: 2019-12-09T08:47:55Z date_published: 2019-10-01T00:00:00Z date_updated: 2023-09-06T11:24:10Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-030-32079-9_17 external_id: isi: - '000570006300017' intvolume: ' 11757' isi: 1 language: - iso: eng month: '10' oa_version: None page: 292-309 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25F2ACDE-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Rigorous Systems Engineering publication: 19th International Conference on Runtime Verification publication_identifier: isbn: - '9783030320782' - '9783030320799' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Shape expressions for specifying and extracting signal features type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 11757 year: '2019' ... --- _id: '7232' abstract: - lang: eng text: 'We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. ' alternative_title: - LNCS article_processing_charge: No author: - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic citation: ama: 'Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: 17th International Conference on Formal Modeling and Analysis of Timed Systems. Vol 11750. Springer Nature; 2019:59-75. doi:10.1007/978-3-030-29662-9_4' apa: 'Ferrere, T., Maler, O., & Nickovic, D. (2019). Mixed-time signal temporal logic. In 17th International Conference on Formal Modeling and Analysis of Timed Systems (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-030-29662-9_4' chicago: Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal Logic.” In 17th International Conference on Formal Modeling and Analysis of Timed Systems, 11750:59–75. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_4. ieee: T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,” in 17th International Conference on Formal Modeling and Analysis of Timed Systems, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75. ista: 'Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.' mla: Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” 17th International Conference on Formal Modeling and Analysis of Timed Systems, vol. 11750, Springer Nature, 2019, pp. 59–75, doi:10.1007/978-3-030-29662-9_4. short: T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75. conference: end_date: 2019-08-29 location: Amsterdam, The Netherlands name: 'FORMATS: Formal Modeling and Anaysis of Timed Systems' start_date: 2019-08-27 date_created: 2020-01-05T23:00:48Z date_published: 2019-08-13T00:00:00Z date_updated: 2023-09-06T14:57:17Z day: '13' department: - _id: ToHe doi: 10.1007/978-3-030-29662-9_4 external_id: isi: - '000611677700004' intvolume: ' 11750' isi: 1 language: - iso: eng month: '08' oa_version: None page: 59-75 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: 17th International Conference on Formal Modeling and Analysis of Timed Systems publication_identifier: eissn: - 1611-3349 isbn: - 978-3-0302-9661-2 issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Mixed-time signal temporal logic type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 11750 year: '2019' ... --- _id: '299' abstract: - lang: eng text: We introduce in this paper AMT 2.0 , a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. alternative_title: - LNCS article_processing_charge: No author: - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Olivier full_name: Lebeltel, Olivier last_name: Lebeltel - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Dogan full_name: Ulus, Dogan last_name: Ulus citation: ama: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In: Beyer D, Huisman M, eds. Vol 10806. Springer; 2018:303-319. doi:10.1007/978-3-319-89963-3_18' apa: 'Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2018). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In D. Beyer & M. Huisman (Eds.) (Vol. 10806, pp. 303–319). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89963-3_18' chicago: 'Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” edited by Dirk Beyer and Marieke Huisman, 10806:303–19. Springer, 2018. https://doi.org/10.1007/978-3-319-89963-3_18.' ieee: 'D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10806, pp. 303–319.' ista: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2018. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10806, 303–319.' mla: 'Nickovic, Dejan, et al. AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic. Edited by Dirk Beyer and Marieke Huisman, vol. 10806, Springer, 2018, pp. 303–19, doi:10.1007/978-3-319-89963-3_18.' short: D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M. Huisman (Eds.), Springer, 2018, pp. 303–319. conference: end_date: 2018-04-20 location: Thessaloniki, Greece name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2018-04-14 date_created: 2018-12-11T11:45:41Z date_published: 2018-04-14T00:00:00Z date_updated: 2023-09-08T11:52:02Z day: '14' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-319-89963-3_18 editor: - first_name: Dirk full_name: Beyer, Dirk last_name: Beyer - first_name: Marieke full_name: Huisman, Marieke last_name: Huisman external_id: isi: - '00445822600018' file: - access_level: open_access checksum: e11db3b9c8e27a1c7d1c738cc5e4d25a content_type: application/pdf creator: dernst date_created: 2019-02-06T07:33:05Z date_updated: 2020-07-14T12:45:58Z file_id: '5928' file_name: 2018_LNCS_Nickovic.pdf file_size: 3267209 relation: main_file file_date_updated: 2020-07-14T12:45:58Z has_accepted_license: '1' intvolume: ' 10806' isi: 1 language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: 303 - 319 publication_status: published publisher: Springer publist_id: '7582' quality_controlled: '1' related_material: record: - id: '10861' relation: later_version status: public scopus_import: '1' status: public title: 'AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 10806 year: '2018' ... --- _id: '144' abstract: - lang: eng text: The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these register monitors according to the number k of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every k 1, monitors with k + 1 counters (with instruction set 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety -languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are as expressive as real-time Turing machines. alternative_title: - ACM/IEEE Symposium on Logic in Computer Science article_processing_charge: No author: - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - 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: Ege full_name: Saraç, Ege last_name: Saraç citation: ama: 'Ferrere T, Henzinger TA, Saraç E. A theory of register monitors. In: Vol Part F138033. IEEE; 2018:394-403. doi:10.1145/3209108.3209194' apa: 'Ferrere, T., Henzinger, T. A., & Saraç, E. (2018). A theory of register monitors (Vol. Part F138033, pp. 394–403). Presented at the LICS: Logic in Computer Science, Oxford, UK: IEEE. https://doi.org/10.1145/3209108.3209194' chicago: Ferrere, Thomas, Thomas A Henzinger, and Ege Saraç. “A Theory of Register Monitors,” Part F138033:394–403. IEEE, 2018. https://doi.org/10.1145/3209108.3209194. ieee: 'T. Ferrere, T. A. Henzinger, and E. Saraç, “A theory of register monitors,” presented at the LICS: Logic in Computer Science, Oxford, UK, 2018, vol. Part F138033, pp. 394–403.' ista: 'Ferrere T, Henzinger TA, Saraç E. 2018. A theory of register monitors. LICS: Logic in Computer Science, ACM/IEEE Symposium on Logic in Computer Science, vol. Part F138033, 394–403.' mla: Ferrere, Thomas, et al. A Theory of Register Monitors. Vol. Part F138033, IEEE, 2018, pp. 394–403, doi:10.1145/3209108.3209194. short: T. Ferrere, T.A. Henzinger, E. Saraç, in:, IEEE, 2018, pp. 394–403. conference: end_date: 2018-07-12 location: Oxford, UK name: 'LICS: Logic in Computer Science' start_date: 2018-07-09 date_created: 2018-12-11T11:44:52Z date_published: 2018-07-09T00:00:00Z date_updated: 2023-09-08T11:49:13Z day: '09' department: - _id: ToHe doi: 10.1145/3209108.3209194 external_id: isi: - '000545262800041' isi: 1 language: - iso: eng month: '07' oa_version: None page: 394 - 403 publication_status: published publisher: IEEE publist_id: '7779' quality_controlled: '1' scopus_import: '1' status: public title: A theory of register monitors type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: Part F138033 year: '2018' ... --- _id: '182' abstract: - lang: eng text: We describe a new algorithm for the parametric identification problem for signal temporal logic (STL), stated as follows. Given a densetime real-valued signal w and a parameterized temporal logic formula φ, compute the subset of the parameter space that renders the formula satisfied by the signal. Unlike previous solutions, which were based on search in the parameter space or quantifier elimination, our procedure works recursively on φ and computes the evolution over time of the set of valid parameter assignments. This procedure is similar to that of monitoring or computing the robustness of φ relative to w. Our implementation and experiments demonstrate that this approach can work well in practice. alternative_title: - HSCC Proceedings article_processing_charge: No author: - first_name: Alexey full_name: Bakhirkin, Alexey last_name: Bakhirkin - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Oded full_name: Maler, Oded last_name: Maler citation: ama: 'Bakhirkin A, Ferrere T, Maler O. Efficient parametric identification for STL. In: Proceedings of the 21st International Conference on Hybrid Systems. ACM; 2018:177-186. doi:10.1145/3178126.3178132' apa: 'Bakhirkin, A., Ferrere, T., & Maler, O. (2018). Efficient parametric identification for STL. In Proceedings of the 21st International Conference on Hybrid Systems (pp. 177–186). Porto, Portugal: ACM. https://doi.org/10.1145/3178126.3178132' chicago: Bakhirkin, Alexey, Thomas Ferrere, and Oded Maler. “Efficient Parametric Identification for STL.” In Proceedings of the 21st International Conference on Hybrid Systems, 177–86. ACM, 2018. https://doi.org/10.1145/3178126.3178132. ieee: A. Bakhirkin, T. Ferrere, and O. Maler, “Efficient parametric identification for STL,” in Proceedings of the 21st International Conference on Hybrid Systems, Porto, Portugal, 2018, pp. 177–186. ista: 'Bakhirkin A, Ferrere T, Maler O. 2018. Efficient parametric identification for STL. Proceedings of the 21st International Conference on Hybrid Systems. HSCC: Hybrid Systems: Computation and Control, HSCC Proceedings, , 177–186.' mla: Bakhirkin, Alexey, et al. “Efficient Parametric Identification for STL.” Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–86, doi:10.1145/3178126.3178132. short: A. Bakhirkin, T. Ferrere, O. Maler, in:, Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–186. conference: end_date: 2018-04-13 location: Porto, Portugal name: 'HSCC: Hybrid Systems: Computation and Control' start_date: 2018-04-11 date_created: 2018-12-11T11:45:04Z date_published: 2018-04-11T00:00:00Z date_updated: 2023-09-11T13:30:51Z day: '11' ddc: - '000' department: - _id: ToHe doi: 10.1145/3178126.3178132 external_id: isi: - '000474781600020' file: - access_level: open_access checksum: 81eabc96430e84336ea88310ac0a1ad0 content_type: application/pdf creator: dernst date_created: 2020-05-14T12:18:29Z date_updated: 2020-07-14T12:45:17Z file_id: '7833' file_name: 2018_HSCC_Bakhirkin.pdf file_size: 5900421 relation: main_file file_date_updated: 2020-07-14T12:45:17Z has_accepted_license: '1' isi: 1 language: - iso: eng month: '04' oa: 1 oa_version: Submitted Version page: 177 - 186 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication: Proceedings of the 21st International Conference on Hybrid Systems publication_identifier: isbn: - '978-1-4503-5642-8 ' publication_status: published publisher: ACM publist_id: '7739' quality_controlled: '1' scopus_import: '1' status: public title: Efficient parametric identification for STL type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2018' ... --- _id: '183' abstract: - lang: eng text: 'Fault-localization is considered to be a very tedious and time-consuming activity in the design of complex Cyber-Physical Systems (CPS). This laborious task essentially requires expert knowledge of the system in order to discover the cause of the fault. In this context, we propose a new procedure that AIDS designers in debugging Simulink/Stateflow hybrid system models, guided by Signal Temporal Logic (STL) specifications. The proposed method relies on three main ingredients: (1) a monitoring and a trace diagnostics procedure that checks whether a tested behavior satisfies or violates an STL specification, localizes time segments and interfaces variables contributing to the property violations; (2) a slicing procedure that maps these observable behavior segments to the internal states and transitions of the Simulink model; and (3) a spectrum-based fault-localization method that combines the previous analysis from multiple tests to identify the internal states and/or transitions that are the most likely to explain the fault. We demonstrate the applicability of our approach on two Simulink models from the automotive and the avionics domain.' acknowledgement: This work was partially supported by the Austrian Science Fund (FWF) under grants S11402-N23 and S11405-N23 (RiSE/SHiNE), the CPS/IoT project (HRSM), the EU ICT COST Action IC1402 on Run-time Verification beyond Monitoring (ARVI), the AMASS project (ECSEL 692474), and the ENABLE-S3 project (ECSEL 692455). The CPS/IoT project receives support from the Austrian government through the Federal Ministry of Science, Research and Economy (BMWFW) in the funding program Hochschulraum-Strukturmittel (HRSM) 2016. The ECSEL Joint Undertaking receives support from the European Union’s Horizon 2020 research and innovation programme and Austria, Denmark, Germany, Finland, Czech Republic, Italy, Spain, Portugal, Poland, Ireland, Belgium, France, Netherlands, United Kingdom, Slovakia, Norway. alternative_title: - HSCC Proceedings article_processing_charge: No author: - first_name: Ezio full_name: Bartocci, Ezio last_name: Bartocci - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Niveditha full_name: Manjunath, Niveditha last_name: Manjunath - first_name: Dejan full_name: Nickovic, Dejan last_name: Nickovic citation: ama: 'Bartocci E, Ferrere T, Manjunath N, Nickovic D. Localizing faults in simulink/stateflow models with STL. In: Association for Computing Machinery, Inc; 2018:197-206. doi:10.1145/3178126.3178131' apa: 'Bartocci, E., Ferrere, T., Manjunath, N., & Nickovic, D. (2018). Localizing faults in simulink/stateflow models with STL (pp. 197–206). Presented at the HSCC: Hybrid Systems: Computation and Control, Porto, Portugal: Association for Computing Machinery, Inc. https://doi.org/10.1145/3178126.3178131' chicago: Bartocci, Ezio, Thomas Ferrere, Niveditha Manjunath, and Dejan Nickovic. “Localizing Faults in Simulink/Stateflow Models with STL,” 197–206. Association for Computing Machinery, Inc, 2018. https://doi.org/10.1145/3178126.3178131. ieee: 'E. Bartocci, T. Ferrere, N. Manjunath, and D. Nickovic, “Localizing faults in simulink/stateflow models with STL,” presented at the HSCC: Hybrid Systems: Computation and Control, Porto, Portugal, 2018, pp. 197–206.' ista: 'Bartocci E, Ferrere T, Manjunath N, Nickovic D. 2018. Localizing faults in simulink/stateflow models with STL. HSCC: Hybrid Systems: Computation and Control, HSCC Proceedings, , 197–206.' mla: Bartocci, Ezio, et al. Localizing Faults in Simulink/Stateflow Models with STL. Association for Computing Machinery, Inc, 2018, pp. 197–206, doi:10.1145/3178126.3178131. short: E. Bartocci, T. Ferrere, N. Manjunath, D. Nickovic, in:, Association for Computing Machinery, Inc, 2018, pp. 197–206. conference: end_date: 2018-04-13 location: Porto, Portugal name: 'HSCC: Hybrid Systems: Computation and Control' start_date: 2018-04-11 date_created: 2018-12-11T11:45:04Z date_published: 2018-04-11T00:00:00Z date_updated: 2023-09-13T08:48:46Z day: '11' department: - _id: ToHe doi: 10.1145/3178126.3178131 external_id: isi: - '000474781600022' isi: 1 language: - iso: eng month: '04' oa_version: None page: 197 - 206 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Association for Computing Machinery, Inc publist_id: '7738' quality_controlled: '1' scopus_import: '1' status: public title: Localizing faults in simulink/stateflow models with STL type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2018' ... --- _id: '81' abstract: - lang: eng text: We solve the offline monitoring problem for timed propositional temporal logic (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider extends linear temporal logic (LTL) with clock variables and reset quantifiers, providing a mechanism to specify real-time constraints. We first describe a general monitoring algorithm based on an exhaustive computation of the set of satisfying clock assignments as a finite union of zones. We then propose a specialized monitoring algorithm for the one-variable case using a partition of the time domain based on the notion of region equivalence, whose complexity is linear in the length of the signal, thereby generalizing a known result regarding the monitoring of metric temporal logic (MTL). The region and zone representations of time constraints are known from timed automata verification and can also be used in the discrete-time case. Our prototype implementation appears to outperform previous discrete-time implementations of TPTL monitoring, alternative_title: - LNCS article_processing_charge: No author: - first_name: Adrian full_name: Elgyütt, Adrian id: 4A2E9DBA-F248-11E8-B48F-1D18A9856A87 last_name: Elgyütt - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Elgyütt A, Ferrere T, Henzinger TA. Monitoring temporal logic with clock variables. In: Vol 11022. Springer; 2018:53-70. doi:10.1007/978-3-030-00151-3_4' apa: 'Elgyütt, A., Ferrere, T., & Henzinger, T. A. (2018). Monitoring temporal logic with clock variables (Vol. 11022, pp. 53–70). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Beijing, China: Springer. https://doi.org/10.1007/978-3-030-00151-3_4' chicago: Elgyütt, Adrian, Thomas Ferrere, and Thomas A Henzinger. “Monitoring Temporal Logic with Clock Variables,” 11022:53–70. Springer, 2018. https://doi.org/10.1007/978-3-030-00151-3_4. ieee: 'A. Elgyütt, T. Ferrere, and T. A. Henzinger, “Monitoring temporal logic with clock variables,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Beijing, China, 2018, vol. 11022, pp. 53–70.' ista: 'Elgyütt A, Ferrere T, Henzinger TA. 2018. Monitoring temporal logic with clock variables. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11022, 53–70.' mla: Elgyütt, Adrian, et al. Monitoring Temporal Logic with Clock Variables. Vol. 11022, Springer, 2018, pp. 53–70, doi:10.1007/978-3-030-00151-3_4. short: A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70. conference: end_date: 2018-09-06 location: Beijing, China name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' start_date: 2018-09-04 date_created: 2018-12-11T11:44:31Z date_published: 2018-08-26T00:00:00Z date_updated: 2023-09-13T08:58:34Z day: '26' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-030-00151-3_4 external_id: isi: - '000884993200004' file: - access_level: open_access checksum: e5d81c9b50a6bd9d8a2c16953aad7e23 content_type: application/pdf creator: dernst date_created: 2020-10-09T06:24:21Z date_updated: 2020-10-09T06:24:21Z file_id: '8638' file_name: 2018_LNCS_Elgyuett.pdf file_size: 537219 relation: main_file success: 1 file_date_updated: 2020-10-09T06:24:21Z has_accepted_license: '1' intvolume: ' 11022' isi: 1 language: - iso: eng month: '08' oa: 1 oa_version: Submitted Version page: 53 - 70 project: - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication_status: published publisher: Springer publist_id: '7973' quality_controlled: '1' scopus_import: '1' status: public title: Monitoring temporal logic with clock variables type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 11022 year: '2018' ... --- _id: '78' abstract: - lang: eng text: We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal ω that match a given temporal pattern ϕ. As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by ϕ and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads ω, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated. alternative_title: - LNCS article_processing_charge: No author: - first_name: Alexey full_name: Bakhirkin, Alexey last_name: Bakhirkin - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Dejan full_name: Nickovic, Dejan last_name: Nickovic - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Eugene full_name: Asarin, Eugene last_name: Asarin citation: ama: 'Bakhirkin A, Ferrere T, Nickovic D, Maler O, Asarin E. Online timed pattern matching using automata. In: Vol 11022. Springer; 2018:215-232. doi:10.1007/978-3-030-00151-3_13' apa: 'Bakhirkin, A., Ferrere, T., Nickovic, D., Maler, O., & Asarin, E. (2018). Online timed pattern matching using automata (Vol. 11022, pp. 215–232). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Bejing, China: Springer. https://doi.org/10.1007/978-3-030-00151-3_13' chicago: Bakhirkin, Alexey, Thomas Ferrere, Dejan Nickovic, Oded Maler, and Eugene Asarin. “Online Timed Pattern Matching Using Automata,” 11022:215–32. Springer, 2018. https://doi.org/10.1007/978-3-030-00151-3_13. ieee: 'A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, and E. Asarin, “Online timed pattern matching using automata,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Bejing, China, 2018, vol. 11022, pp. 215–232.' ista: 'Bakhirkin A, Ferrere T, Nickovic D, Maler O, Asarin E. 2018. Online timed pattern matching using automata. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11022, 215–232.' mla: Bakhirkin, Alexey, et al. Online Timed Pattern Matching Using Automata. Vol. 11022, Springer, 2018, pp. 215–32, doi:10.1007/978-3-030-00151-3_13. short: A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, E. Asarin, in:, Springer, 2018, pp. 215–232. conference: end_date: 2018-09-06 location: Bejing, China name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' start_date: 2018-09-04 date_created: 2018-12-11T11:44:31Z date_published: 2018-08-26T00:00:00Z date_updated: 2023-09-13T09:35:46Z day: '26' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-030-00151-3_13 external_id: isi: - '000884993200013' file: - access_level: open_access checksum: 436b7574934324cfa7d1d3986fddc65b content_type: application/pdf creator: dernst date_created: 2020-05-14T11:34:34Z date_updated: 2020-07-14T12:48:03Z file_id: '7831' file_name: 2018_LNCS_Bakhirkin.pdf file_size: 374851 relation: main_file file_date_updated: 2020-07-14T12:48:03Z has_accepted_license: '1' intvolume: ' 11022' isi: 1 language: - iso: eng month: '08' oa: 1 oa_version: Submitted Version page: 215 - 232 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication_identifier: isbn: - 978-3-030-00150-6 publication_status: published publisher: Springer publist_id: '7976' quality_controlled: '1' scopus_import: '1' status: public title: Online timed pattern matching using automata type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 11022 year: '2018' ... --- _id: '156' abstract: - lang: eng text: 'Imprecision in timing can sometimes be beneficial: Metric interval temporal logic (MITL), disabling the expression of punctuality constraints, was shown to translate to timed automata, yielding an elementary decision procedure. We show how this principle extends to other forms of dense-time specification using regular expressions. By providing a clean, automaton-based formal framework for non-punctual languages, we are able to recover and extend several results in timed systems. Metric interval regular expressions (MIRE) are introduced, providing regular expressions with non-singular duration constraints. We obtain that MIRE are expressively complete relative to a class of one-clock timed automata, which can be determinized using additional clocks. Metric interval dynamic logic (MIDL) is then defined using MIRE as temporal modalities. We show that MIDL generalizes known extensions of MITL, while translating to timed automata at comparable cost.' alternative_title: - LNCS article_processing_charge: No author: - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 citation: ama: 'Ferrere T. The compound interest in relaxing punctuality. In: Vol 10951. Springer; 2018:147-164. doi:10.1007/978-3-319-95582-7_9' apa: 'Ferrere, T. (2018). The compound interest in relaxing punctuality (Vol. 10951, pp. 147–164). Presented at the FM: International Symposium on Formal Methods, Oxford, UK: Springer. https://doi.org/10.1007/978-3-319-95582-7_9' chicago: Ferrere, Thomas. “The Compound Interest in Relaxing Punctuality,” 10951:147–64. Springer, 2018. https://doi.org/10.1007/978-3-319-95582-7_9. ieee: 'T. Ferrere, “The compound interest in relaxing punctuality,” presented at the FM: International Symposium on Formal Methods, Oxford, UK, 2018, vol. 10951, pp. 147–164.' ista: 'Ferrere T. 2018. The compound interest in relaxing punctuality. FM: International Symposium on Formal Methods, LNCS, vol. 10951, 147–164.' mla: Ferrere, Thomas. The Compound Interest in Relaxing Punctuality. Vol. 10951, Springer, 2018, pp. 147–64, doi:10.1007/978-3-319-95582-7_9. short: T. Ferrere, in:, Springer, 2018, pp. 147–164. conference: end_date: 2018-07-17 location: Oxford, UK name: 'FM: International Symposium on Formal Methods' start_date: 2018-07-15 date_created: 2018-12-11T11:44:55Z date_published: 2018-07-12T00:00:00Z date_updated: 2023-09-19T10:05:37Z day: '12' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-319-95582-7_9 external_id: isi: - '000489765800009' file: - access_level: open_access checksum: a045c213c42c445f1889326f8db82a0a content_type: application/pdf creator: dernst date_created: 2020-10-09T06:22:41Z date_updated: 2020-10-09T06:22:41Z file_id: '8637' file_name: 2018_LNCS_Ferrere.pdf file_size: 485576 relation: main_file success: 1 file_date_updated: 2020-10-09T06:22:41Z has_accepted_license: '1' intvolume: ' 10951' isi: 1 language: - iso: eng month: '07' oa: 1 oa_version: Submitted Version page: 147 - 164 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '7765' quality_controlled: '1' scopus_import: '1' status: public title: The compound interest in relaxing punctuality type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 10951 year: '2018' ... --- _id: '5959' abstract: - lang: eng text: Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain. article_processing_charge: No author: - first_name: Alexey full_name: Bakhirkin, Alexey last_name: Bakhirkin - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - 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: Deian full_name: Nickovicl, Deian last_name: Nickovicl citation: ama: 'Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. Keynote: The first-order logic of signals. In: 2018 International Conference on Embedded Software. IEEE; 2018:1-10. doi:10.1109/emsoft.2018.8537203' apa: 'Bakhirkin, A., Ferrere, T., Henzinger, T. A., & Nickovicl, D. (2018). Keynote: The first-order logic of signals. In 2018 International Conference on Embedded Software (pp. 1–10). Turin, Italy: IEEE. https://doi.org/10.1109/emsoft.2018.8537203' chicago: 'Bakhirkin, Alexey, Thomas Ferrere, Thomas A Henzinger, and Deian Nickovicl. “Keynote: The First-Order Logic of Signals.” In 2018 International Conference on Embedded Software, 1–10. IEEE, 2018. https://doi.org/10.1109/emsoft.2018.8537203.' ieee: 'A. Bakhirkin, T. Ferrere, T. A. Henzinger, and D. Nickovicl, “Keynote: The first-order logic of signals,” in 2018 International Conference on Embedded Software, Turin, Italy, 2018, pp. 1–10.' ista: 'Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. 2018. Keynote: The first-order logic of signals. 2018 International Conference on Embedded Software. EMSOFT: International Conference on Embedded Software, 1–10.' mla: 'Bakhirkin, Alexey, et al. “Keynote: The First-Order Logic of Signals.” 2018 International Conference on Embedded Software, IEEE, 2018, pp. 1–10, doi:10.1109/emsoft.2018.8537203.' short: A. Bakhirkin, T. Ferrere, T.A. Henzinger, D. Nickovicl, in:, 2018 International Conference on Embedded Software, IEEE, 2018, pp. 1–10. conference: end_date: 2018-10-05 location: Turin, Italy name: 'EMSOFT: International Conference on Embedded Software' start_date: 2018-09-30 date_created: 2019-02-13T09:19:28Z date_published: 2018-09-30T00:00:00Z date_updated: 2023-09-19T10:41:29Z day: '30' ddc: - '000' department: - _id: ToHe doi: 10.1109/emsoft.2018.8537203 external_id: isi: - '000492828500005' file: - access_level: open_access checksum: 234a33ad9055b3458fcdda6af251b33a content_type: application/pdf creator: dernst date_created: 2020-05-14T16:01:29Z date_updated: 2020-07-14T12:47:13Z file_id: '7839' file_name: 2018_EMSOFT_Bakhirkin.pdf file_size: 338006 relation: main_file file_date_updated: 2020-07-14T12:47:13Z has_accepted_license: '1' isi: 1 language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 1-10 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: 2018 International Conference on Embedded Software publication_identifier: isbn: - '9781538655603' publication_status: published publisher: IEEE quality_controlled: '1' scopus_import: '1' status: public title: 'Keynote: The first-order logic of signals' type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2018' ... --- _id: '636' abstract: - lang: eng text: Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems. alternative_title: - LNCS author: - first_name: Alexey full_name: Bakhirkin, Alexey last_name: Bakhirkin - first_name: Thomas full_name: Ferrere, Thomas id: 40960E6E-F248-11E8-B48F-1D18A9856A87 last_name: Ferrere orcid: 0000-0001-5199-3143 - first_name: Oded full_name: Maler, Oded last_name: Maler - first_name: Dogan full_name: Ulus, Dogan last_name: Ulus citation: ama: 'Bakhirkin A, Ferrere T, Maler O, Ulus D. On the quantitative semantics of regular expressions over real-valued signals. In: Abate A, Geeraerts G, eds. Vol 10419. Springer; 2017:189-206. doi:10.1007/978-3-319-65765-3_11' apa: 'Bakhirkin, A., Ferrere, T., Maler, O., & Ulus, D. (2017). On the quantitative semantics of regular expressions over real-valued signals. In A. Abate & G. Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_11' chicago: Bakhirkin, Alexey, Thomas Ferrere, Oded Maler, and Dogan Ulus. “On the Quantitative Semantics of Regular Expressions over Real-Valued Signals.” edited by Alessandro Abate and Gilles Geeraerts, 10419:189–206. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_11. ieee: 'A. Bakhirkin, T. Ferrere, O. Maler, and D. Ulus, “On the quantitative semantics of regular expressions over real-valued signals,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 189–206.' ista: 'Bakhirkin A, Ferrere T, Maler O, Ulus D. 2017. On the quantitative semantics of regular expressions over real-valued signals. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 189–206.' mla: Bakhirkin, Alexey, et al. On the Quantitative Semantics of Regular Expressions over Real-Valued Signals. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 189–206, doi:10.1007/978-3-319-65765-3_11. short: A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206. conference: end_date: 2017-09-07 location: Berlin, Germany name: 'FORMATS: Formal Modelling and Analysis of Timed Systems' start_date: 2017-09-05 date_created: 2018-12-11T11:47:38Z date_published: 2017-08-03T00:00:00Z date_updated: 2021-01-12T08:07:14Z day: '03' department: - _id: ToHe doi: 10.1007/978-3-319-65765-3_11 editor: - first_name: Alessandro full_name: Abate, Alessandro last_name: Abate - first_name: Gilles full_name: Geeraerts, Gilles last_name: Geeraerts intvolume: ' 10419' language: - iso: eng main_file_link: - open_access: '1' url: https://hal.archives-ouvertes.fr/hal-01552132 month: '08' oa: 1 oa_version: Submitted Version page: 189 - 206 project: - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication_identifier: isbn: - 978-331965764-6 publication_status: published publisher: Springer publist_id: '7152' quality_controlled: '1' scopus_import: 1 status: public title: On the quantitative semantics of regular expressions over real-valued signals type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 10419 year: '2017' ...