[{"publist_id":"7973","oa":1,"date_published":"2018-08-26T00:00:00Z","type":"conference","file":[{"file_size":537219,"checksum":"e5d81c9b50a6bd9d8a2c16953aad7e23","date_created":"2020-10-09T06:24:21Z","content_type":"application/pdf","file_name":"2018_LNCS_Elgyuett.pdf","date_updated":"2020-10-09T06:24:21Z","relation":"main_file","access_level":"open_access","success":1,"creator":"dernst","file_id":"8638"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Submitted Version","project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"month":"08","has_accepted_license":"1","conference":{"start_date":"2018-09-04","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","location":"Beijing, China","end_date":"2018-09-06"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-030-00151-3_4","day":"26","abstract":[{"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,","lang":"eng"}],"date_updated":"2023-09-13T08:58:34Z","citation":{"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.","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>.","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>","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>","ista":"Elgyütt A, Ferrere T, Henzinger TA. 2018. Monitoring temporal logic with clock variables. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11022, 53–70.","mla":"Elgyütt, Adrian, et al. <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>.","short":"A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70."},"year":"2018","isi":1,"external_id":{"isi":["000884993200004"]},"volume":11022,"ddc":["000"],"publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:44:31Z","article_processing_charge":"No","title":"Monitoring temporal logic with clock variables","alternative_title":["LNCS"],"intvolume":"     11022","_id":"81","scopus_import":"1","author":[{"id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","full_name":"Elgyütt, Adrian","last_name":"Elgyütt","first_name":"Adrian"},{"orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","first_name":"Thomas","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer","page":"53 - 70","quality_controlled":"1","file_date_updated":"2020-10-09T06:24:21Z"},{"publisher":"IJCAI","ec_funded":1,"quality_controlled":"1","page":"4692 - 4699","article_processing_charge":"No","date_created":"2018-12-11T11:44:13Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","intvolume":"      2018","title":"Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives","scopus_import":"1","_id":"24","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Elgyütt, Adrian","first_name":"Adrian","last_name":"Elgyütt","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Rouillé, Owen","last_name":"Rouillé","first_name":"Owen"}],"volume":2018,"acknowledgement":"This research was supported by the Vienna Science and Technology Fund (WWTF) grant ICT15-003; Austrian Science Fund (FWF): S11407-N23(RiSE/SHiNE);and an ERC Start Grant (279307:Graph Games).\r\n","day":"01","arxiv":1,"doi":"10.24963/ijcai.2018/652","abstract":[{"text":"Partially-observable Markov decision processes (POMDPs) with discounted-sum payoff are a standard framework to model a wide range of problems related to decision making under uncertainty. Traditionally, the goal has been to obtain policies that optimize the expectation of the discounted-sum payoff. A key drawback of the expectation measure is that even low probability events with extreme payoff can significantly affect the expectation, and thus the obtained policies are not necessarily risk-averse. An alternate approach is to optimize the probability that the payoff is above a certain threshold, which allows obtaining risk-averse policies, but ignores optimization of the expectation. We consider the expectation optimization with probabilistic guarantee (EOPG) problem, where the goal is to optimize the expectation ensuring that the payoff is above a given threshold with at least a specified probability. We present several results on the EOPG problem, including the first algorithm to solve it.","lang":"eng"}],"citation":{"ieee":"K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé, “Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives,” presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018, pp. 4692–4699.","chicago":"Chatterjee, Krishnendu, Adrian Elgyütt, Petr Novotný, and Owen Rouillé. “Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives,” 2018:4692–99. IJCAI, 2018. <a href=\"https://doi.org/10.24963/ijcai.2018/652\">https://doi.org/10.24963/ijcai.2018/652</a>.","apa":"Chatterjee, K., Elgyütt, A., Novotný, P., &#38; Rouillé, O. (2018). Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives (Vol. 2018, pp. 4692–4699). Presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden: IJCAI. <a href=\"https://doi.org/10.24963/ijcai.2018/652\">https://doi.org/10.24963/ijcai.2018/652</a>","ama":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. In: Vol 2018. IJCAI; 2018:4692-4699. doi:<a href=\"https://doi.org/10.24963/ijcai.2018/652\">10.24963/ijcai.2018/652</a>","ista":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. 2018. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4692–4699.","mla":"Chatterjee, Krishnendu, et al. <i>Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives</i>. Vol. 2018, IJCAI, 2018, pp. 4692–99, doi:<a href=\"https://doi.org/10.24963/ijcai.2018/652\">10.24963/ijcai.2018/652</a>.","short":"K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp. 4692–4699."},"year":"2018","date_updated":"2025-06-02T08:53:48Z","external_id":{"isi":["000764175404117"],"arxiv":["1804.10601"]},"isi":1,"conference":{"start_date":"2018-07-13","name":"IJCAI: International Joint Conference on Artificial Intelligence","end_date":"2018-07-19","location":"Stockholm, Sweden"},"language":[{"iso":"eng"}],"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"oa_version":"Preprint","month":"07","main_file_link":[{"url":"https://arxiv.org/abs/1804.10601","open_access":"1"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"publist_id":"8031","type":"conference","date_published":"2018-07-01T00:00:00Z"}]