[{"article_number":"23","file_date_updated":"2020-07-14T12:47:15Z","license":"https://creativecommons.org/licenses/by/4.0/","year":"2018","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published","related_material":{"record":[{"id":"963","relation":"earlier_version","status":"public"}]},"author":[{"full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Shibashis","last_name":"Guha","full_name":"Guha, Shibashis"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"volume":117,"date_created":"2019-02-14T14:12:09Z","date_updated":"2023-02-23T14:02:58Z","publication_identifier":{"issn":["1868-8969"]},"month":"08","oa":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","short":"CC BY (4.0)","image":"/images/cc_by.png"},"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.4230/LIPICS.MFCS.2018.23","conference":{"start_date":"2018-08-27","location":"Liverpool, United Kingdom","end_date":"2018-08-31","name":"MFCS: Mathematical Foundations of Computer Science"},"language":[{"iso":"eng"}],"type":"conference","alternative_title":["LIPIcs"],"abstract":[{"text":"Network games are widely used as a model for selfish resource-allocation problems. In the classicalmodel, each player selects a path connecting her source and target vertices. The cost of traversingan edge depends on theload; namely, number of players that traverse it. Thus, it abstracts the factthat different users may use a resource at different times and for different durations, which playsan important role in determining the costs of the users in reality. For example, when transmittingpackets in a communication network, routing traffic in a road network, or processing a task in aproduction system, actual sharing and congestion of resources crucially depends on time.In [13], we introducedtimed network games, which add a time component to network games.Each vertexvin the network is associated with a cost function, mapping the load onvto theprice that a player pays for staying invfor one time unit with this load. Each edge in thenetwork is guarded by the time intervals in which it can be traversed, which forces the players tospend time in the vertices. In this work we significantly extend the way time can be referred toin timed network games. In the model we study, the network is equipped withclocks, and, as intimed automata, edges are guarded by constraints on the values of the clocks, and their traversalmay involve a reset of some clocks. We argue that the stronger model captures many realisticnetworks. The addition of clocks breaks the techniques we developed in [13] and we developnew techniques in order to show that positive results on classic network games carry over to thestronger timed setting.","lang":"eng"}],"_id":"6005","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 117","title":"Timed network games with clocks","status":"public","ddc":["000"],"oa_version":"Published Version","file":[{"checksum":"41ab2ae9b63f5eb49fa995250c0ba128","date_updated":"2020-07-14T12:47:15Z","date_created":"2019-02-14T14:22:04Z","file_id":"6007","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":542889,"access_level":"open_access","file_name":"2018_LIPIcs_Avni.pdf"}],"scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","day":"01","citation":{"ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPICS.MFCS.2018.23","ista":"Avni G, Guha S, Kupferman O. 2018. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 117, 23.","apa":"Avni, G., Guha, S., & Kupferman, O. (2018). Timed network games with clocks (Vol. 117). Presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.MFCS.2018.23","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom, 2018, vol. 117.","mla":"Avni, Guy, et al. Timed Network Games with Clocks. Vol. 117, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPICS.MFCS.2018.23.","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPICS.MFCS.2018.23."},"date_published":"2018-08-01T00:00:00Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"133","intvolume":" 118","status":"public","title":"Synchronizing the asynchronous","ddc":["000"],"pubrep_id":"1039","oa_version":"Published Version","file":[{"file_name":"IST-2018-853-v2+2_concur2018.pdf","access_level":"open_access","file_size":745438,"content_type":"application/pdf","creator":"system","relation":"main_file","file_id":"5368","date_created":"2018-12-12T10:18:46Z","date_updated":"2020-07-14T12:44:44Z","checksum":"c90895f4c5fafc18ddc54d1c8848077e"}],"type":"conference","alternative_title":["LIPIcs"],"abstract":[{"lang":"eng","text":"Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs."}],"citation":{"chicago":"Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.21.","mla":"Kragl, Bernhard, et al. Synchronizing the Asynchronous. Vol. 118, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.21.","short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","ista":"Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 118, 21.","apa":"Kragl, B., Qadeer, S., & Henzinger, T. A. (2018). Synchronizing the asynchronous (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.21","ieee":"B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,” presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","ama":"Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.CONCUR.2018.21"},"date_published":"2018-08-13T00:00:00Z","scopus_import":1,"has_accepted_license":"1","day":"13","year":"2018","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"}],"publication_status":"published","related_material":{"record":[{"id":"6426","relation":"earlier_version","status":"public"},{"relation":"dissertation_contains","status":"public","id":"8332"}]},"author":[{"orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","first_name":"Bernhard","full_name":"Kragl, Bernhard"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"volume":118,"date_created":"2018-12-11T11:44:48Z","date_updated":"2023-09-07T13:18:00Z","article_number":"21","publist_id":"7790","file_date_updated":"2020-07-14T12:44:44Z","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","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"project":[{"grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"quality_controlled":"1","doi":"10.4230/LIPIcs.CONCUR.2018.21","conference":{"end_date":"2018-09-07","start_date":"2018-09-04","location":"Beijing, China","name":"CONCUR: International Conference on Concurrency Theory"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["18688969"]},"month":"08"},{"date_published":"2018-04-14T00:00:00Z","citation":{"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., & 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","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.","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","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.","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."},"page":"303 - 319","has_accepted_license":"1","article_processing_charge":"No","day":"14","scopus_import":"1","oa_version":"Published Version","file":[{"checksum":"e11db3b9c8e27a1c7d1c738cc5e4d25a","date_updated":"2020-07-14T12:45:58Z","date_created":"2019-02-06T07:33:05Z","file_id":"5928","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":3267209,"access_level":"open_access","file_name":"2018_LNCS_Nickovic.pdf"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"299","intvolume":" 10806","ddc":["000"],"title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","status":"public","abstract":[{"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.","lang":"eng"}],"type":"conference","alternative_title":["LNCS"],"doi":"10.1007/978-3-319-89963-3_18","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2018-04-14","location":"Thessaloniki, Greece","end_date":"2018-04-20"},"language":[{"iso":"eng"}],"oa":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","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["00445822600018"]},"isi":1,"quality_controlled":"1","month":"04","related_material":{"record":[{"relation":"later_version","status":"public","id":"10861"}]},"author":[{"full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","last_name":"Nickovic"},{"last_name":"Lebeltel","first_name":"Olivier","full_name":"Lebeltel, Olivier"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","first_name":"Thomas"},{"first_name":"Dogan","last_name":"Ulus","full_name":"Ulus, Dogan"}],"volume":10806,"date_created":"2018-12-11T11:45:41Z","date_updated":"2023-09-08T11:52:02Z","year":"2018","editor":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"full_name":"Huisman, Marieke","last_name":"Huisman","first_name":"Marieke"}],"department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","publist_id":"7582","file_date_updated":"2020-07-14T12:45:58Z"},{"abstract":[{"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.","lang":"eng"}],"publist_id":"7779","type":"conference","alternative_title":["ACM/IEEE Symposium on Logic in Computer Science"],"author":[{"last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Saraç, Ege","first_name":"Ege","last_name":"Saraç"}],"date_updated":"2023-09-08T11:49:13Z","date_created":"2018-12-11T11:44:52Z","oa_version":"None","volume":"Part F138033","_id":"144","year":"2018","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"A theory of register monitors","publication_status":"published","status":"public","department":[{"_id":"ToHe"}],"publisher":"IEEE","month":"07","day":"09","article_processing_charge":"No","scopus_import":"1","conference":{"end_date":"2018-07-12","location":"Oxford, UK","start_date":"2018-07-09","name":"LICS: Logic in Computer Science"},"doi":"10.1145/3209108.3209194","date_published":"2018-07-09T00:00:00Z","language":[{"iso":"eng"}],"citation":{"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.","short":"T. Ferrere, T.A. Henzinger, E. Saraç, in:, IEEE, 2018, pp. 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.","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.","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","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.","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"},"external_id":{"isi":["000545262800041"]},"quality_controlled":"1","isi":1,"page":"394 - 403"},{"date_published":"2018-04-11T00:00:00Z","publication":"Proceedings of the 21st International Conference on Hybrid Systems","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","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.","short":"A. Bakhirkin, T. Ferrere, O. Maler, in:, Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 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.","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."},"page":"177 - 186","day":"11","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1","oa_version":"Submitted Version","file":[{"checksum":"81eabc96430e84336ea88310ac0a1ad0","date_updated":"2020-07-14T12:45:17Z","date_created":"2020-05-14T12:18:29Z","file_id":"7833","relation":"main_file","creator":"dernst","file_size":5900421,"content_type":"application/pdf","access_level":"open_access","file_name":"2018_HSCC_Bakhirkin.pdf"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"182","status":"public","ddc":["000"],"title":"Efficient parametric identification for STL","abstract":[{"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.","lang":"eng"}],"type":"conference","alternative_title":["HSCC Proceedings"],"conference":{"end_date":"2018-04-13","start_date":"2018-04-11","location":"Porto, Portugal","name":"HSCC: Hybrid Systems: Computation and Control"},"doi":"10.1145/3178126.3178132","language":[{"iso":"eng"}],"external_id":{"isi":["000474781600020"]},"oa":1,"quality_controlled":"1","isi":1,"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"month":"04","publication_identifier":{"isbn":["978-1-4503-5642-8 "]},"author":[{"full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin","first_name":"Alexey"},{"last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas"},{"last_name":"Maler","first_name":"Oded","full_name":"Maler, Oded"}],"date_updated":"2023-09-11T13:30:51Z","date_created":"2018-12-11T11:45:04Z","year":"2018","publication_status":"published","publisher":"ACM","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:17Z","publist_id":"7739"},{"year":"2018","publisher":"Springer","department":[{"_id":"ToHe"}],"author":[{"last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"}],"volume":11316,"date_updated":"2023-09-12T07:44:01Z","date_created":"2018-12-30T22:59:14Z","publication_identifier":{"issn":["03029743"],"isbn":["9783030046118"]},"month":"11","external_id":{"arxiv":["1804.04372"],"isi":["000865933000002"]},"main_file_link":[{"url":"https://arxiv.org/abs/1804.04372","open_access":"1"}],"oa":1,"project":[{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF"}],"quality_controlled":"1","isi":1,"doi":"10.1007/978-3-030-04612-5_2","conference":{"location":"Oxford, UK","start_date":"2018-12-15","end_date":"2018-12-17","name":"14th International Conference on Web and Internet Economics, WINE"},"language":[{"iso":"eng"}],"type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner or payoff of the game. Such games are central in formal verification since they model the interaction between a non-terminating system and its environment. We study bidding games in which the players bid for the right to move the token. Two bidding rules have been defined. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the “bank” rather than the other player. While poorman reachability games have been studied before, we present, for the first time, results on infinite-duration poorman games. A central quantity in these games is the ratio between the two players’ initial budgets. The questions we study concern a necessary and sufficient ratio with which a player can achieve a goal. For reachability objectives, such threshold ratios are known to exist for both bidding rules. We show that the properties of poorman reachability games extend to complex qualitative objectives such as parity, similarly to the Richman case. Our most interesting results concern quantitative poorman games, namely poorman mean-payoff games, where we construct optimal strategies depending on the initial ratio, by showing a connection with random-turn based games. The connection in itself is interesting, because it does not hold for reachability poorman games. We also solve the complexity problems that arise in poorman bidding games."}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"5788","intvolume":" 11316","status":"public","title":"Infinite-duration poorman-bidding games","oa_version":"Preprint","scopus_import":"1","article_processing_charge":"No","day":"21","citation":{"ama":"Avni G, Henzinger TA, Ibsen-Jensen R. Infinite-duration poorman-bidding games. In: Vol 11316. Springer; 2018:21-36. doi:10.1007/978-3-030-04612-5_2","ieee":"G. Avni, T. A. Henzinger, and R. Ibsen-Jensen, “Infinite-duration poorman-bidding games,” presented at the 14th International Conference on Web and Internet Economics, WINE, Oxford, UK, 2018, vol. 11316, pp. 21–36.","apa":"Avni, G., Henzinger, T. A., & Ibsen-Jensen, R. (2018). Infinite-duration poorman-bidding games (Vol. 11316, pp. 21–36). Presented at the 14th International Conference on Web and Internet Economics, WINE, Oxford, UK: Springer. https://doi.org/10.1007/978-3-030-04612-5_2","ista":"Avni G, Henzinger TA, Ibsen-Jensen R. 2018. Infinite-duration poorman-bidding games. 14th International Conference on Web and Internet Economics, WINE, LNCS, vol. 11316, 21–36.","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, in:, Springer, 2018, pp. 21–36.","mla":"Avni, Guy, et al. Infinite-Duration Poorman-Bidding Games. Vol. 11316, Springer, 2018, pp. 21–36, doi:10.1007/978-3-030-04612-5_2.","chicago":"Avni, Guy, Thomas A Henzinger, and Rasmus Ibsen-Jensen. “Infinite-Duration Poorman-Bidding Games,” 11316:21–36. Springer, 2018. https://doi.org/10.1007/978-3-030-04612-5_2."},"page":"21-36","date_published":"2018-11-21T00:00:00Z"},{"has_accepted_license":"1","article_processing_charge":"No","day":"18","scopus_import":"1","date_published":"2018-07-18T00:00:00Z","citation":{"ista":"Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided Verification, LNCS, vol. 10981, 79–102.","ieee":"B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV: Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102.","apa":"Kragl, B., & Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981, pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer. https://doi.org/10.1007/978-3-319-96145-3_5","ama":"Kragl B, Qadeer S. Layered Concurrent Programs. In: Vol 10981. Springer; 2018:79-102. doi:10.1007/978-3-319-96145-3_5","chicago":"Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_5.","mla":"Kragl, Bernhard, and Shaz Qadeer. Layered Concurrent Programs. Vol. 10981, Springer, 2018, pp. 79–102, doi:10.1007/978-3-319-96145-3_5.","short":"B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102."},"page":"79 - 102","abstract":[{"lang":"eng","text":"We present layered concurrent programs, a compact and expressive notation for specifying refinement proofs of concurrent programs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. These programs are expressed in the ordinary syntax of imperative concurrent programs using gated atomic actions, sequencing, choice, and (recursive) procedure calls. Each concurrent program is automatically extracted from the layered program. We reduce refinement to the safety of a sequence of concurrent checker programs, one each to justify the connection between every two consecutive concurrent programs. These checker programs are also automatically extracted from the layered program. Layered concurrent programs have been implemented in the CIVL verifier which has been successfully used for the verification of several complex concurrent programs."}],"type":"conference","alternative_title":["LNCS"],"file":[{"date_created":"2018-12-17T12:52:12Z","date_updated":"2020-07-14T12:45:04Z","checksum":"c64fff560fe5a7532ec10626ad1c215e","relation":"main_file","file_id":"5705","file_size":1603844,"content_type":"application/pdf","creator":"dernst","file_name":"2018_LNCS_Kragl.pdf","access_level":"open_access"}],"oa_version":"Published Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"160","intvolume":" 10981","status":"public","title":"Layered Concurrent Programs","ddc":["000"],"month":"07","doi":"10.1007/978-3-319-96145-3_5","conference":{"name":"CAV: Computer Aided Verification","end_date":"2018-07-17","start_date":"2018-07-14","location":"Oxford, UK"},"language":[{"iso":"eng"}],"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","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"isi":["000491481600005"]},"project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"isi":1,"quality_controlled":"1","publist_id":"7761","file_date_updated":"2020-07-14T12:45:04Z","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8332"}]},"author":[{"full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"}],"volume":10981,"date_created":"2018-12-11T11:44:57Z","date_updated":"2023-09-13T08:45:09Z","year":"2018","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published"},{"publist_id":"7738","author":[{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Ferrere, Thomas","last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Niveditha","last_name":"Manjunath","full_name":"Manjunath, Niveditha"},{"full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"}],"date_created":"2018-12-11T11:45:04Z","date_updated":"2023-09-13T08:48:46Z","year":"2018","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.","publisher":"Association for Computing Machinery, Inc","department":[{"_id":"ToHe"}],"publication_status":"published","month":"04","doi":"10.1145/3178126.3178131","conference":{"location":"Porto, Portugal","start_date":"2018-04-11","end_date":"2018-04-13","name":"HSCC: Hybrid Systems: Computation and Control"},"language":[{"iso":"eng"}],"external_id":{"isi":["000474781600022"]},"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"isi":1,"quality_controlled":"1","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."}],"type":"conference","alternative_title":["HSCC Proceedings"],"oa_version":"None","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"183","title":"Localizing faults in simulink/stateflow models with STL","status":"public","article_processing_charge":"No","day":"11","scopus_import":"1","date_published":"2018-04-11T00:00:00Z","citation":{"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","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.","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","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.","short":"E. Bartocci, T. Ferrere, N. Manjunath, D. Nickovic, in:, Association for Computing Machinery, Inc, 2018, pp. 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."},"page":"197 - 206"},{"scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","day":"26","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","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.","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.","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","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.","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."},"page":"53 - 70","date_published":"2018-08-26T00:00:00Z","type":"conference","alternative_title":["LNCS"],"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,"}],"_id":"81","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","intvolume":" 11022","ddc":["000"],"title":"Monitoring temporal logic with clock variables","status":"public","oa_version":"Submitted Version","file":[{"checksum":"e5d81c9b50a6bd9d8a2c16953aad7e23","success":1,"date_updated":"2020-10-09T06:24:21Z","date_created":"2020-10-09T06:24:21Z","relation":"main_file","file_id":"8638","content_type":"application/pdf","file_size":537219,"creator":"dernst","access_level":"open_access","file_name":"2018_LNCS_Elgyuett.pdf"}],"month":"08","external_id":{"isi":["000884993200004"]},"oa":1,"project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","isi":1,"doi":"10.1007/978-3-030-00151-3_4","conference":{"end_date":"2018-09-06","location":"Beijing, China","start_date":"2018-09-04","name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"language":[{"iso":"eng"}],"publist_id":"7973","file_date_updated":"2020-10-09T06:24:21Z","year":"2018","publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"full_name":"Elgyütt, Adrian","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","last_name":"Elgyütt","first_name":"Adrian"},{"last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"volume":11022,"date_created":"2018-12-11T11:44:31Z","date_updated":"2023-09-13T08:58:34Z"},{"page":"215 - 232","citation":{"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.","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.","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.","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.","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","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"},"date_published":"2018-08-26T00:00:00Z","scopus_import":"1","day":"26","article_processing_charge":"No","has_accepted_license":"1","status":"public","title":"Online timed pattern matching using automata","ddc":["000"],"intvolume":" 11022","_id":"78","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Submitted Version","file":[{"checksum":"436b7574934324cfa7d1d3986fddc65b","date_created":"2020-05-14T11:34:34Z","date_updated":"2020-07-14T12:48:03Z","file_id":"7831","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":374851,"access_level":"open_access","file_name":"2018_LNCS_Bakhirkin.pdf"}],"alternative_title":["LNCS"],"type":"conference","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."}],"isi":1,"quality_controlled":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"oa":1,"external_id":{"isi":["000884993200013"]},"language":[{"iso":"eng"}],"conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems","location":"Bejing, China","start_date":"2018-09-04","end_date":"2018-09-06"},"doi":"10.1007/978-3-030-00151-3_13","month":"08","publication_identifier":{"isbn":["978-3-030-00150-6"]},"publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"year":"2018","date_updated":"2023-09-13T09:35:46Z","date_created":"2018-12-11T11:44:31Z","volume":11022,"author":[{"last_name":"Bakhirkin","first_name":"Alexey","full_name":"Bakhirkin, Alexey"},{"full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","first_name":"Thomas","last_name":"Ferrere"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"first_name":"Eugene","last_name":"Asarin","full_name":"Asarin, Eugene"}],"file_date_updated":"2020-07-14T12:48:03Z","publist_id":"7976"}]