[{"author":[{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","first_name":"Dejan"},{"last_name":"Da Costa","full_name":"Da Costa, Ana Oliveira","first_name":"Ana Oliveira"}],"scopus_import":"1","day":"14","oa_version":"Preprint","title":"Flavors of sequential information flow","volume":13182,"date_created":"2022-02-20T23:01:34Z","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."}],"intvolume":"     13182","publication_status":"published","publication_identifier":{"isbn":["9783030945824"],"issn":["03029743"],"eissn":["16113349"]},"arxiv":1,"month":"01","department":[{"_id":"ToHe"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"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.","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Flavors of sequential information flow,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Philadelphia, PA, United States, 2022, vol. 13182, pp. 1–19.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential information flow. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 13182. Springer Nature; 2022:1-19. doi:<a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">10.1007/978-3-030-94583-1_1</a>","mla":"Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 13182, Springer Nature, 2022, pp. 1–19, doi:<a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">10.1007/978-3-030-94583-1_1</a>.","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Flavors of sequential information flow. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 13182, pp. 1–19). Philadelphia, PA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">https://doi.org/10.1007/978-3-030-94583-1_1</a>","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.","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 13182:1–19. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-94583-1_1\">https://doi.org/10.1007/978-3-030-94583-1_1</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-030-94583-1_1","alternative_title":["LNCS"],"article_processing_charge":"No","publisher":"Springer Nature","date_updated":"2022-08-05T09:02:56Z","_id":"10774","type":"conference","page":"1-19","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2105.02013"}],"quality_controlled":"1","year":"2022","external_id":{"arxiv":["2105.02013"]},"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"status":"public","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","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.","conference":{"start_date":"2022-01-16","end_date":"2022-01-18","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","location":"Philadelphia, PA, United States"},"date_published":"2022-01-14T00:00:00Z"},{"month":"03","file":[{"relation":"main_file","checksum":"7f6f860b20b8de2a249e9c1b4eee15cf","file_name":"2022_LNCS_Bartocci.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","file_id":"11357","date_created":"2022-05-09T06:52:44Z","file_size":479146,"creator":"dernst","date_updated":"2022-05-09T06:52:44Z"}],"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"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.","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Information-Flow Interfaces.” In <i>Fundamental Approaches to Software Engineering</i>, 13241:3–22. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>.","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Information-flow interfaces. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>","mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow interfaces. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13241. Springer Nature; 2022:3-22. doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Information-flow interfaces,” in <i>Fundamental Approaches to Software Engineering</i>, Munich, Germany, 2022, vol. 13241, pp. 3–22.","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."},"title":"Information-flow interfaces","oa_version":"Published Version","day":"29","scopus_import":"1","author":[{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"first_name":"Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","first_name":"Dejan"},{"first_name":"Ana Oliveira","full_name":"Da Costa, Ana Oliveira","last_name":"Da Costa"}],"date_created":"2022-05-08T22:01:44Z","volume":13241,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"     13241","abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","file_date_updated":"2022-05-09T06:52:44Z","publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783030994280"],"issn":["0302-9743"]},"external_id":{"isi":["000782393600001"]},"year":"2022","isi":1,"status":"public","publication":"Fundamental Approaches to Software Engineering","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"conference":{"start_date":"2022-04-02","end_date":"2022-04-07","name":"FASE: Fundamental Approaches to Software Engineering","location":"Munich, Germany"},"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.","date_published":"2022-03-29T00:00:00Z","ec_funded":1,"publisher":"Springer Nature","article_processing_charge":"No","alternative_title":["LNCS"],"doi":"10.1007/978-3-030-99429-7_1","type":"conference","_id":"11355","date_updated":"2023-08-03T07:03:40Z","ddc":["000"],"page":"3-22","quality_controlled":"1"},{"publication":"International Journal on Software Tools for Technology Transfer","status":"public","date_published":"2020-08-03T00:00:00Z","related_material":{"record":[{"id":"299","relation":"earlier_version","status":"public"}]},"external_id":{"isi":["000555398600001"]},"isi":1,"year":"2020","keyword":["Information Systems","Software"],"page":"741-758","quality_controlled":"1","publisher":"Springer Nature","article_processing_charge":"No","doi":"10.1007/s10009-020-00582-z","type":"journal_article","_id":"10861","date_updated":"2023-09-08T11:52:02Z","language":[{"iso":"eng"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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.","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.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>.","mla":"Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. 2020;22(6):741-758. doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758.","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,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6. Springer Nature, pp. 741–758, 2020."},"issue":"6","month":"08","department":[{"_id":"ToHe"}],"intvolume":"        22","abstract":[{"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.","lang":"eng"}],"publication_status":"published","publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","oa_version":"None","scopus_import":"1","day":"03","author":[{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"},{"last_name":"Lebeltel","full_name":"Lebeltel, Olivier","first_name":"Olivier"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","orcid":"0000-0001-5199-3143","first_name":"Thomas"},{"first_name":"Dogan","last_name":"Ulus","full_name":"Ulus, Dogan"}],"date_created":"2022-03-18T10:10:53Z","article_type":"original","volume":22},{"publication":"28th EACSL Annual Conference on Computer Science Logic","status":"public","project":[{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"date_published":"2020-01-15T00:00:00Z","conference":{"end_date":"2020-01-16","start_date":"2020-01-13","name":"CSL: Computer Science Logic","location":"Barcelona, Spain"},"external_id":{"arxiv":["1910.06097"]},"year":"2020","ddc":["000"],"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LIPIcs"],"article_processing_charge":"No","doi":"10.4230/LIPIcs.CSL.2020.20","type":"conference","_id":"7348","date_updated":"2021-01-12T08:13:12Z","language":[{"iso":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Ferrere, T., Henzinger, T. A., &#38; Kragl, B. (2020). Monitoring event frequencies. In <i>28th EACSL Annual Conference on Computer Science Logic</i> (Vol. 152). Barcelona, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">https://doi.org/10.4230/LIPIcs.CSL.2020.20</a>","mla":"Ferrere, Thomas, et al. “Monitoring Event Frequencies.” <i>28th EACSL Annual Conference on Computer Science Logic</i>, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">10.4230/LIPIcs.CSL.2020.20</a>.","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.","chicago":"Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event Frequencies.” In <i>28th EACSL Annual Conference on Computer Science Logic</i>, Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">https://doi.org/10.4230/LIPIcs.CSL.2020.20</a>.","ieee":"T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,” in <i>28th EACSL Annual Conference on Computer Science Logic</i>, Barcelona, Spain, 2020, vol. 152.","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.","ama":"Ferrere T, Henzinger TA, Kragl B. Monitoring event frequencies. In: <i>28th EACSL Annual Conference on Computer Science Logic</i>. Vol 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">10.4230/LIPIcs.CSL.2020.20</a>"},"month":"01","arxiv":1,"file":[{"date_updated":"2020-07-14T12:47:56Z","creator":"bkragl","file_size":617206,"date_created":"2020-01-21T11:21:04Z","file_id":"7349","access_level":"open_access","content_type":"application/pdf","file_name":"main.pdf","checksum":"b9a691d658d075c6369d3304d17fb818","relation":"main_file"}],"article_number":"20","department":[{"_id":"ToHe"}],"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. "}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"       152","has_accepted_license":"1","file_date_updated":"2020-07-14T12:47:56Z","publication_status":"published","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959771320"]},"oa_version":"Published Version","title":"Monitoring event frequencies","day":"15","scopus_import":1,"author":[{"orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","full_name":"Kragl, Bernhard","orcid":"0000-0001-7745-9117","first_name":"Bernhard"}],"date_created":"2020-01-21T11:22:21Z","volume":152},{"date_published":"2019-05-01T00:00:00Z","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publication":"Journal of the ACM","status":"public","external_id":{"isi":["000495406300005"]},"year":"2019","isi":1,"quality_controlled":"1","type":"journal_article","date_updated":"2023-09-06T11:11:56Z","_id":"7109","publisher":"ACM","doi":"10.1145/3286976","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","issue":"3","citation":{"short":"T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019).","ieee":"T. Ferrere, O. Maler, D. Ničković, and A. Pnueli, “From real-time logic to timed automata,” <i>Journal of the ACM</i>, vol. 66, no. 3. ACM, 2019.","ama":"Ferrere T, Maler O, Ničković D, Pnueli A. From real-time logic to timed automata. <i>Journal of the ACM</i>. 2019;66(3). doi:<a href=\"https://doi.org/10.1145/3286976\">10.1145/3286976</a>","mla":"Ferrere, Thomas, et al. “From Real-Time Logic to Timed Automata.” <i>Journal of the ACM</i>, vol. 66, no. 3, 19, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3286976\">10.1145/3286976</a>.","apa":"Ferrere, T., Maler, O., Ničković, D., &#38; Pnueli, A. (2019). From real-time logic to timed automata. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3286976\">https://doi.org/10.1145/3286976</a>","chicago":"Ferrere, Thomas, Oded Maler, Dejan Ničković, and Amir Pnueli. “From Real-Time Logic to Timed Automata.” <i>Journal of the ACM</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3286976\">https://doi.org/10.1145/3286976</a>.","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."},"language":[{"iso":"eng"}],"article_number":"19","department":[{"_id":"ToHe"}],"month":"05","publication_identifier":{"issn":["0004-5411"]},"publication_status":"published","intvolume":"        66","abstract":[{"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.","lang":"eng"}],"article_type":"original","date_created":"2019-11-26T10:22:32Z","volume":66,"title":"From real-time logic to timed automata","oa_version":"None","author":[{"orcid":"0000-0001-5199-3143","first_name":"Thomas","last_name":"Ferrere","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"last_name":"Ničković","full_name":"Ničković, Dejan","first_name":"Dejan"},{"first_name":"Amir","last_name":"Pnueli","full_name":"Pnueli, Amir"}],"day":"01","scopus_import":"1"},{"abstract":[{"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. ","lang":"eng"}],"intvolume":"     11757","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030320782","9783030320799"]},"publication_status":"published","title":"Shape expressions for specifying and extracting signal features","oa_version":"None","author":[{"full_name":"Ničković, Dejan","last_name":"Ničković","first_name":"Dejan"},{"first_name":"Xin","last_name":"Qin","full_name":"Qin, Xin"},{"last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","first_name":"Thomas"},{"full_name":"Mateis, Cristinel","last_name":"Mateis","first_name":"Cristinel"},{"first_name":"Jyotirmoy","full_name":"Deshmukh, Jyotirmoy","last_name":"Deshmukh"}],"scopus_import":"1","day":"01","date_created":"2019-12-09T08:47:55Z","volume":11757,"language":[{"iso":"eng"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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.","chicago":"Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In <i>19th International Conference on Runtime Verification</i>, 11757:292–309. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>.","apa":"Ničković, D., Qin, X., Ferrere, T., Mateis, C., &#38; Deshmukh, J. (2019). Shape expressions for specifying and extracting signal features. In <i>19th International Conference on Runtime Verification</i> (Vol. 11757, pp. 292–309). Porto, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>","mla":"Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal Features.” <i>19th International Conference on Runtime Verification</i>, vol. 11757, Springer Nature, 2019, pp. 292–309, doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>.","ama":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for specifying and extracting signal features. In: <i>19th International Conference on Runtime Verification</i>. Vol 11757. Springer Nature; 2019:292-309. doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>","ieee":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions for specifying and extracting signal features,” in <i>19th International Conference on Runtime Verification</i>, Porto, Portugal, 2019, vol. 11757, pp. 292–309.","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."},"month":"10","department":[{"_id":"ToHe"}],"page":"292-309","quality_controlled":"1","publisher":"Springer Nature","doi":"10.1007/978-3-030-32079-9_17","article_processing_charge":"No","alternative_title":["LNCS"],"type":"conference","date_updated":"2023-09-06T11:24:10Z","_id":"7159","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"}],"publication":"19th International Conference on Runtime Verification","status":"public","date_published":"2019-10-01T00:00:00Z","conference":{"location":"Porto, Portugal","start_date":"2019-10-08","end_date":"2019-10-11","name":"RV: Runtime Verification"},"external_id":{"isi":["000570006300017"]},"year":"2019","isi":1},{"publisher":"Springer Nature","alternative_title":["LNCS"],"article_processing_charge":"No","doi":"10.1007/978-3-030-29662-9_4","type":"conference","_id":"7232","date_updated":"2023-09-06T14:57:17Z","page":"59-75","quality_controlled":"1","external_id":{"isi":["000611677700004"]},"isi":1,"year":"2019","status":"public","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"}],"date_published":"2019-08-13T00:00:00Z","conference":{"location":"Amsterdam, The Netherlands","end_date":"2019-08-29","start_date":"2019-08-27","name":"FORMATS: Formal Modeling and Anaysis of Timed Systems"},"oa_version":"None","title":"Mixed-time signal temporal logic","day":"13","scopus_import":"1","author":[{"orcid":"0000-0001-5199-3143","first_name":"Thomas","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"}],"date_created":"2020-01-05T23:00:48Z","volume":11750,"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. "}],"intvolume":"     11750","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-0302-9661-2"],"eissn":["1611-3349"]},"publication_status":"published","month":"08","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"apa":"Ferrere, T., Maler, O., &#38; Nickovic, D. (2019). Mixed-time signal temporal logic. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>","mla":"Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 59–75, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>.","chicago":"Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal Logic.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:59–75. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>.","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.","ieee":"T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.","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.","ama":"Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:59-75. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>"}},{"type":"conference","_id":"6428","date_updated":"2023-08-25T10:19:23Z","publisher":"ACM","article_processing_charge":"No","doi":"10.1145/3302504.3311800","quality_controlled":"1","ddc":["000"],"page":"57-66","external_id":{"isi":["000516713900007"]},"year":"2019","isi":1,"date_published":"2019-04-16T00:00:00Z","conference":{"location":"Montreal, Canada","name":"HSCC: Hybrid Systems Computation and Control","start_date":"2019-04-16","end_date":"2019-04-18"},"publication":"Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control","status":"public","project":[{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"date_created":"2019-05-13T08:13:46Z","title":"Interface-aware signal temporal logic","oa_version":"Submitted Version","scopus_import":"1","day":"16","author":[{"full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","first_name":"Thomas","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é"},{"last_name":"Ito","full_name":"Ito, Hisahiro","first_name":"Hisahiro"},{"first_name":"James","full_name":"Kapinski, James","last_name":"Kapinski"}],"file_date_updated":"2020-10-08T17:25:45Z","publication_identifier":{"isbn":["9781450362825"]},"publication_status":"published","abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","file":[{"file_name":"2019_ACM_Ferrere.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"b8e967081e051d1c55ca5d18fb187890","file_size":1055421,"date_created":"2020-10-08T17:25:45Z","date_updated":"2020-10-08T17:25:45Z","creator":"dernst","file_id":"8633"}],"department":[{"_id":"ToHe"}],"month":"04","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ama":"Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. Interface-aware signal temporal logic. In: <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2019:57-66. doi:<a href=\"https://doi.org/10.1145/3302504.3311800\">10.1145/3302504.3311800</a>","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.","ieee":"T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware signal temporal logic,” in <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, Montreal, Canada, 2019, pp. 57–66.","chicago":"Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James Kapinski. “Interface-Aware Signal Temporal Logic.” In <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, 57–66. ACM, 2019. <a href=\"https://doi.org/10.1145/3302504.3311800\">https://doi.org/10.1145/3302504.3311800</a>.","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.” <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2019, pp. 57–66, doi:<a href=\"https://doi.org/10.1145/3302504.3311800\">10.1145/3302504.3311800</a>.","apa":"Ferrere, T., Nickovic, D., Donzé, A., Ito, H., &#38; Kapinski, J. (2019). Interface-aware signal temporal logic. In <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i> (pp. 57–66). Montreal, Canada: ACM. <a href=\"https://doi.org/10.1145/3302504.3311800\">https://doi.org/10.1145/3302504.3311800</a>"},"language":[{"iso":"eng"}],"oa":1},{"year":"2018","isi":1,"related_material":{"record":[{"id":"10861","relation":"later_version","status":"public"}]},"external_id":{"isi":["00445822600018"]},"publist_id":"7582","status":"public","date_published":"2018-04-14T00:00:00Z","conference":{"start_date":"2018-04-14","end_date":"2018-04-20","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Thessaloniki, Greece"},"article_processing_charge":"No","alternative_title":["LNCS"],"doi":"10.1007/978-3-319-89963-3_18","publisher":"Springer","editor":[{"last_name":"Beyer","full_name":"Beyer, Dirk","first_name":"Dirk"},{"full_name":"Huisman, Marieke","last_name":"Huisman","first_name":"Marieke"}],"_id":"299","date_updated":"2023-09-08T11:52:02Z","type":"conference","page":"303 - 319","ddc":["000"],"quality_controlled":"1","month":"04","department":[{"_id":"ToHe"}],"file":[{"access_level":"open_access","content_type":"application/pdf","file_name":"2018_LNCS_Nickovic.pdf","checksum":"e11db3b9c8e27a1c7d1c738cc5e4d25a","relation":"main_file","date_updated":"2020-07-14T12:45:58Z","creator":"dernst","file_size":3267209,"date_created":"2019-02-06T07:33:05Z","file_id":"5928"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"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. <a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">https://doi.org/10.1007/978-3-319-89963-3_18</a>.","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.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2018). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In D. Beyer &#38; 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. <a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">https://doi.org/10.1007/978-3-319-89963-3_18</a>","mla":"Nickovic, Dejan, et al. <i>AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic</i>. Edited by Dirk Beyer and Marieke Huisman, vol. 10806, Springer, 2018, pp. 303–19, doi:<a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">10.1007/978-3-319-89963-3_18</a>.","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:<a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">10.1007/978-3-319-89963-3_18</a>","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.","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M. Huisman (Eds.), Springer, 2018, pp. 303–319."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"14","scopus_import":"1","author":[{"last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"last_name":"Lebeltel","full_name":"Lebeltel, Olivier","first_name":"Olivier"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere"},{"first_name":"Dogan","full_name":"Ulus, Dogan","last_name":"Ulus"}],"title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","oa_version":"Published Version","volume":10806,"date_created":"2018-12-11T11:45:41Z","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"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."}],"intvolume":"     10806","file_date_updated":"2020-07-14T12:45:58Z","publication_status":"published"},{"language":[{"iso":"eng"}],"oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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.","short":"A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, E. Asarin, in:, Springer, 2018, pp. 215–232.","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:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">10.1007/978-3-030-00151-3_13</a>","apa":"Bakhirkin, A., Ferrere, T., Nickovic, D., Maler, O., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">https://doi.org/10.1007/978-3-030-00151-3_13</a>","mla":"Bakhirkin, Alexey, et al. <i>Online Timed Pattern Matching Using Automata</i>. Vol. 11022, Springer, 2018, pp. 215–32, doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">10.1007/978-3-030-00151-3_13</a>.","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.","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Dejan Nickovic, Oded Maler, and Eugene Asarin. “Online Timed Pattern Matching Using Automata,” 11022:215–32. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">https://doi.org/10.1007/978-3-030-00151-3_13</a>."},"month":"08","file":[{"file_name":"2018_LNCS_Bakhirkin.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"436b7574934324cfa7d1d3986fddc65b","file_size":374851,"date_created":"2020-05-14T11:34:34Z","date_updated":"2020-07-14T12:48:03Z","creator":"dernst","file_id":"7831"}],"department":[{"_id":"ToHe"}],"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."}],"intvolume":"     11022","has_accepted_license":"1","publication_status":"published","publication_identifier":{"isbn":["978-3-030-00150-6"]},"file_date_updated":"2020-07-14T12:48:03Z","title":"Online timed pattern matching using automata","oa_version":"Submitted Version","author":[{"first_name":"Alexey","last_name":"Bakhirkin","full_name":"Bakhirkin, Alexey"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"last_name":"Asarin","full_name":"Asarin, Eugene","first_name":"Eugene"}],"day":"26","scopus_import":"1","date_created":"2018-12-11T11:44:31Z","volume":11022,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"status":"public","date_published":"2018-08-26T00:00:00Z","conference":{"location":"Bejing, China","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","end_date":"2018-09-06","start_date":"2018-09-04"},"external_id":{"isi":["000884993200013"]},"isi":1,"year":"2018","publist_id":"7976","ddc":["000"],"page":"215 - 232","quality_controlled":"1","publisher":"Springer","doi":"10.1007/978-3-030-00151-3_13","article_processing_charge":"No","alternative_title":["LNCS"],"type":"conference","date_updated":"2023-09-13T09:35:46Z","_id":"78"},{"file_date_updated":"2020-10-09T06:24:21Z","publication_status":"published","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,"}],"intvolume":"     11022","has_accepted_license":"1","date_created":"2018-12-11T11:44:31Z","volume":11022,"title":"Monitoring temporal logic with clock variables","oa_version":"Submitted Version","day":"26","scopus_import":"1","author":[{"first_name":"Adrian","last_name":"Elgyütt","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","full_name":"Elgyütt, Adrian"},{"first_name":"Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"chicago":"Elgyütt, Adrian, Thomas Ferrere, and Thomas A Henzinger. “Monitoring Temporal Logic with Clock Variables,” 11022:53–70. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">https://doi.org/10.1007/978-3-030-00151-3_4</a>.","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.","apa":"Elgyütt, A., Ferrere, T., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">https://doi.org/10.1007/978-3-030-00151-3_4</a>","mla":"Elgyütt, Adrian, et al. <i>Monitoring Temporal Logic with Clock Variables</i>. Vol. 11022, Springer, 2018, pp. 53–70, doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">10.1007/978-3-030-00151-3_4</a>.","ama":"Elgyütt A, Ferrere T, Henzinger TA. Monitoring temporal logic with clock variables. In: Vol 11022. Springer; 2018:53-70. doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">10.1007/978-3-030-00151-3_4</a>","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.","short":"A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70."},"language":[{"iso":"eng"}],"oa":1,"file":[{"file_name":"2018_LNCS_Elgyuett.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"e5d81c9b50a6bd9d8a2c16953aad7e23","file_size":537219,"date_created":"2020-10-09T06:24:21Z","creator":"dernst","date_updated":"2020-10-09T06:24:21Z","file_id":"8638"}],"department":[{"_id":"ToHe"}],"month":"08","quality_controlled":"1","ddc":["000"],"page":"53 - 70","type":"conference","_id":"81","date_updated":"2023-09-13T08:58:34Z","publisher":"Springer","alternative_title":["LNCS"],"article_processing_charge":"No","doi":"10.1007/978-3-030-00151-3_4","date_published":"2018-08-26T00:00:00Z","conference":{"location":"Beijing, China","end_date":"2018-09-06","start_date":"2018-09-04","name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"status":"public","project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"publist_id":"7973","external_id":{"isi":["000884993200004"]},"isi":1,"year":"2018"},{"type":"conference","_id":"182","date_updated":"2023-09-11T13:30:51Z","publisher":"ACM","article_processing_charge":"No","alternative_title":["HSCC Proceedings"],"doi":"10.1145/3178126.3178132","quality_controlled":"1","ddc":["000"],"page":"177 - 186","publist_id":"7739","external_id":{"isi":["000474781600020"]},"year":"2018","isi":1,"date_published":"2018-04-11T00:00:00Z","conference":{"location":"Porto, Portugal","name":"HSCC: Hybrid Systems: Computation and Control","start_date":"2018-04-11","end_date":"2018-04-13"},"status":"public","publication":"Proceedings of the 21st International Conference on Hybrid Systems","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:45:04Z","oa_version":"Submitted Version","title":"Efficient parametric identification for STL","scopus_import":"1","day":"11","author":[{"last_name":"Bakhirkin","full_name":"Bakhirkin, Alexey","first_name":"Alexey"},{"first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"}],"file_date_updated":"2020-07-14T12:45:17Z","publication_identifier":{"isbn":["978-1-4503-5642-8 "]},"publication_status":"published","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."}],"has_accepted_license":"1","file":[{"access_level":"open_access","content_type":"application/pdf","file_name":"2018_HSCC_Bakhirkin.pdf","checksum":"81eabc96430e84336ea88310ac0a1ad0","relation":"main_file","date_updated":"2020-07-14T12:45:17Z","creator":"dernst","date_created":"2020-05-14T12:18:29Z","file_size":5900421,"file_id":"7833"}],"department":[{"_id":"ToHe"}],"month":"04","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ama":"Bakhirkin A, Ferrere T, Maler O. Efficient parametric identification for STL. In: <i>Proceedings of the 21st International Conference on Hybrid Systems</i>. ACM; 2018:177-186. doi:<a href=\"https://doi.org/10.1145/3178126.3178132\">10.1145/3178126.3178132</a>","ieee":"A. Bakhirkin, T. Ferrere, and O. Maler, “Efficient parametric identification for STL,” in <i>Proceedings of the 21st International Conference on Hybrid Systems</i>, Porto, Portugal, 2018, pp. 177–186.","short":"A. Bakhirkin, T. Ferrere, O. Maler, in:, Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–186.","chicago":"Bakhirkin, Alexey, Thomas Ferrere, and Oded Maler. “Efficient Parametric Identification for STL.” In <i>Proceedings of the 21st International Conference on Hybrid Systems</i>, 177–86. ACM, 2018. <a href=\"https://doi.org/10.1145/3178126.3178132\">https://doi.org/10.1145/3178126.3178132</a>.","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.","apa":"Bakhirkin, A., Ferrere, T., &#38; Maler, O. (2018). Efficient parametric identification for STL. In <i>Proceedings of the 21st International Conference on Hybrid Systems</i> (pp. 177–186). Porto, Portugal: ACM. <a href=\"https://doi.org/10.1145/3178126.3178132\">https://doi.org/10.1145/3178126.3178132</a>","mla":"Bakhirkin, Alexey, et al. “Efficient Parametric Identification for STL.” <i>Proceedings of the 21st International Conference on Hybrid Systems</i>, ACM, 2018, pp. 177–86, doi:<a href=\"https://doi.org/10.1145/3178126.3178132\">10.1145/3178126.3178132</a>."},"language":[{"iso":"eng"}],"oa":1},{"language":[{"iso":"eng"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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.","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. <a href=\"https://doi.org/10.1145/3178126.3178131\">https://doi.org/10.1145/3178126.3178131</a>.","mla":"Bartocci, Ezio, et al. <i>Localizing Faults in Simulink/Stateflow Models with STL</i>. Association for Computing Machinery, Inc, 2018, pp. 197–206, doi:<a href=\"https://doi.org/10.1145/3178126.3178131\">10.1145/3178126.3178131</a>.","apa":"Bartocci, E., Ferrere, T., Manjunath, N., &#38; 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. <a href=\"https://doi.org/10.1145/3178126.3178131\">https://doi.org/10.1145/3178126.3178131</a>","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:<a href=\"https://doi.org/10.1145/3178126.3178131\">10.1145/3178126.3178131</a>","short":"E. Bartocci, T. Ferrere, N. Manjunath, D. Nickovic, in:, Association for Computing Machinery, Inc, 2018, pp. 197–206.","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."},"month":"04","department":[{"_id":"ToHe"}],"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."}],"publication_status":"published","oa_version":"None","title":"Localizing faults in simulink/stateflow models with STL","author":[{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","last_name":"Ferrere","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Niveditha","full_name":"Manjunath, Niveditha","last_name":"Manjunath"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic"}],"scopus_import":"1","day":"11","date_created":"2018-12-11T11:45:04Z","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"status":"public","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.","date_published":"2018-04-11T00:00:00Z","conference":{"location":"Porto, Portugal","end_date":"2018-04-13","start_date":"2018-04-11","name":"HSCC: Hybrid Systems: Computation and Control"},"external_id":{"isi":["000474781600022"]},"isi":1,"year":"2018","publist_id":"7738","page":"197 - 206","quality_controlled":"1","publisher":"Association for Computing Machinery, Inc","doi":"10.1145/3178126.3178131","alternative_title":["HSCC Proceedings"],"article_processing_charge":"No","type":"conference","date_updated":"2023-09-13T08:48:46Z","_id":"183"},{"date_created":"2019-02-13T09:19:28Z","oa_version":"Published Version","title":"Keynote: The first-order logic of signals","scopus_import":"1","day":"30","author":[{"last_name":"Bakhirkin","full_name":"Bakhirkin, Alexey","first_name":"Alexey"},{"last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","first_name":"Thomas","orcid":"0000-0001-5199-3143"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Nickovicl, Deian","last_name":"Nickovicl","first_name":"Deian"}],"file_date_updated":"2020-07-14T12:47:13Z","publication_status":"published","publication_identifier":{"isbn":["9781538655603"]},"abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","file":[{"date_created":"2020-05-14T16:01:29Z","file_size":338006,"creator":"dernst","date_updated":"2020-07-14T12:47:13Z","file_id":"7839","file_name":"2018_EMSOFT_Bakhirkin.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"234a33ad9055b3458fcdda6af251b33a"}],"department":[{"_id":"ToHe"}],"month":"09","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"short":"A. Bakhirkin, T. Ferrere, T.A. Henzinger, D. Nickovicl, in:, 2018 International Conference on Embedded Software, IEEE, 2018, pp. 1–10.","ieee":"A. Bakhirkin, T. Ferrere, T. A. Henzinger, and D. Nickovicl, “Keynote: The first-order logic of signals,” in <i>2018 International Conference on Embedded Software</i>, Turin, Italy, 2018, pp. 1–10.","ama":"Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. Keynote: The first-order logic of signals. In: <i>2018 International Conference on Embedded Software</i>. IEEE; 2018:1-10. doi:<a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">10.1109/emsoft.2018.8537203</a>","mla":"Bakhirkin, Alexey, et al. “Keynote: The First-Order Logic of Signals.” <i>2018 International Conference on Embedded Software</i>, IEEE, 2018, pp. 1–10, doi:<a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">10.1109/emsoft.2018.8537203</a>.","apa":"Bakhirkin, A., Ferrere, T., Henzinger, T. A., &#38; Nickovicl, D. (2018). Keynote: The first-order logic of signals. In <i>2018 International Conference on Embedded Software</i> (pp. 1–10). Turin, Italy: IEEE. <a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">https://doi.org/10.1109/emsoft.2018.8537203</a>","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Thomas A Henzinger, and Deian Nickovicl. “Keynote: The First-Order Logic of Signals.” In <i>2018 International Conference on Embedded Software</i>, 1–10. IEEE, 2018. <a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">https://doi.org/10.1109/emsoft.2018.8537203</a>.","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."},"language":[{"iso":"eng"}],"oa":1,"type":"conference","_id":"5959","date_updated":"2023-09-19T10:41:29Z","publisher":"IEEE","article_processing_charge":"No","doi":"10.1109/emsoft.2018.8537203","quality_controlled":"1","ddc":["000"],"page":"1-10","external_id":{"isi":["000492828500005"]},"isi":1,"year":"2018","conference":{"location":"Turin, Italy","name":"EMSOFT: International Conference on Embedded Software","start_date":"2018-09-30","end_date":"2018-10-05"},"date_published":"2018-09-30T00:00:00Z","publication":"2018 International Conference on Embedded Software","status":"public","project":[{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}]},{"title":"A theory of register monitors","oa_version":"None","publisher":"IEEE","doi":"10.1145/3209108.3209194","author":[{"last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","first_name":"Thomas"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Ege","full_name":"Saraç, Ege","last_name":"Saraç"}],"alternative_title":["ACM/IEEE Symposium on Logic in Computer Science"],"day":"09","scopus_import":"1","article_processing_charge":"No","type":"conference","date_created":"2018-12-11T11:44:52Z","date_updated":"2023-09-08T11:49:13Z","volume":"Part F138033","_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."}],"page":"394 - 403","publication_status":"published","quality_controlled":"1","external_id":{"isi":["000545262800041"]},"month":"07","isi":1,"year":"2018","publist_id":"7779","department":[{"_id":"ToHe"}],"status":"public","language":[{"iso":"eng"}],"date_published":"2018-07-09T00:00:00Z","conference":{"end_date":"2018-07-12","start_date":"2018-07-09","name":"LICS: Logic in Computer Science","location":"Oxford, UK"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"short":"T. Ferrere, T.A. Henzinger, E. Saraç, in:, IEEE, 2018, pp. 394–403.","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.","ama":"Ferrere T, Henzinger TA, Saraç E. A theory of register monitors. In: Vol Part F138033. IEEE; 2018:394-403. doi:<a href=\"https://doi.org/10.1145/3209108.3209194\">10.1145/3209108.3209194</a>","mla":"Ferrere, Thomas, et al. <i>A Theory of Register Monitors</i>. Vol. Part F138033, IEEE, 2018, pp. 394–403, doi:<a href=\"https://doi.org/10.1145/3209108.3209194\">10.1145/3209108.3209194</a>.","apa":"Ferrere, T., Henzinger, T. A., &#38; 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. <a href=\"https://doi.org/10.1145/3209108.3209194\">https://doi.org/10.1145/3209108.3209194</a>","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.","chicago":"Ferrere, Thomas, Thomas A Henzinger, and Ege Saraç. “A Theory of Register Monitors,” Part F138033:394–403. IEEE, 2018. <a href=\"https://doi.org/10.1145/3209108.3209194\">https://doi.org/10.1145/3209108.3209194</a>."}},{"month":"07","department":[{"_id":"ToHe"}],"file":[{"file_name":"2018_LNCS_Ferrere.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"a045c213c42c445f1889326f8db82a0a","file_size":485576,"date_created":"2020-10-09T06:22:41Z","creator":"dernst","date_updated":"2020-10-09T06:22:41Z","file_id":"8637"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"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. <a href=\"https://doi.org/10.1007/978-3-319-95582-7_9\">https://doi.org/10.1007/978-3-319-95582-7_9</a>","mla":"Ferrere, Thomas. <i>The Compound Interest in Relaxing Punctuality</i>. Vol. 10951, Springer, 2018, pp. 147–64, doi:<a href=\"https://doi.org/10.1007/978-3-319-95582-7_9\">10.1007/978-3-319-95582-7_9</a>.","chicago":"Ferrere, Thomas. “The Compound Interest in Relaxing Punctuality,” 10951:147–64. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-95582-7_9\">https://doi.org/10.1007/978-3-319-95582-7_9</a>.","ista":"Ferrere T. 2018. The compound interest in relaxing punctuality. FM: International Symposium on Formal Methods, LNCS, vol. 10951, 147–164.","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.","short":"T. Ferrere, in:, Springer, 2018, pp. 147–164.","ama":"Ferrere T. The compound interest in relaxing punctuality. In: Vol 10951. Springer; 2018:147-164. doi:<a href=\"https://doi.org/10.1007/978-3-319-95582-7_9\">10.1007/978-3-319-95582-7_9</a>"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"first_name":"Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas"}],"day":"12","scopus_import":"1","oa_version":"Submitted Version","title":"The compound interest in relaxing punctuality","volume":10951,"date_created":"2018-12-11T11:44:55Z","has_accepted_license":"1","intvolume":"     10951","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."}],"publication_status":"published","file_date_updated":"2020-10-09T06:22:41Z","isi":1,"year":"2018","external_id":{"isi":["000489765800009"]},"publist_id":"7765","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"status":"public","conference":{"location":"Oxford, UK","end_date":"2018-07-17","start_date":"2018-07-15","name":"FM: International Symposium on Formal Methods"},"date_published":"2018-07-12T00:00:00Z","doi":"10.1007/978-3-319-95582-7_9","article_processing_charge":"No","alternative_title":["LNCS"],"publisher":"Springer","date_updated":"2023-09-19T10:05:37Z","_id":"156","type":"conference","page":"147 - 164","ddc":["000"],"quality_controlled":"1"},{"intvolume":"     10419","abstract":[{"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.","lang":"eng"}],"publication_status":"published","publication_identifier":{"isbn":["978-331965764-6"]},"title":"On the quantitative semantics of regular expressions over real-valued signals","oa_version":"Submitted Version","scopus_import":1,"day":"03","author":[{"first_name":"Alexey","full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas"},{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"first_name":"Dogan","last_name":"Ulus","full_name":"Ulus, Dogan"}],"date_created":"2018-12-11T11:47:38Z","volume":10419,"language":[{"iso":"eng"}],"oa":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","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:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>","short":"A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206.","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.","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. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>.","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. <i>On the Quantitative Semantics of Regular Expressions over Real-Valued Signals</i>. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 189–206, doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>.","apa":"Bakhirkin, A., Ferrere, T., Maler, O., &#38; Ulus, D. (2017). On the quantitative semantics of regular expressions over real-valued signals. In A. Abate &#38; G. Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>"},"month":"08","department":[{"_id":"ToHe"}],"page":"189 - 206","quality_controlled":"1","main_file_link":[{"url":"https://hal.archives-ouvertes.fr/hal-01552132","open_access":"1"}],"publisher":"Springer","editor":[{"full_name":"Abate, Alessandro","last_name":"Abate","first_name":"Alessandro"},{"first_name":"Gilles","last_name":"Geeraerts","full_name":"Geeraerts, Gilles"}],"alternative_title":["LNCS"],"doi":"10.1007/978-3-319-65765-3_11","type":"conference","_id":"636","date_updated":"2021-01-12T08:07:14Z","status":"public","project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"conference":{"location":"Berlin, Germany","name":"FORMATS: Formal Modelling and Analysis of Timed Systems","end_date":"2017-09-07","start_date":"2017-09-05"},"date_published":"2017-08-03T00:00:00Z","year":"2017","publist_id":"7152"}]