[{"type":"journal_article","isi":1,"intvolume":"       301","publisher":"Elsevier","author":[{"full_name":"Baier, Christel","first_name":"Christel","last_name":"Baier"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"first_name":"Jakob","last_name":"Piribauer","full_name":"Piribauer, Jakob"}],"file_date_updated":"2025-01-09T13:49:03Z","_id":"17474","has_accepted_license":"1","scopus_import":"1","article_number":"105214","quality_controlled":"1","citation":{"ama":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Entropic risk for turn-based stochastic games. <i>Information and Computation</i>. 2024;301. doi:<a href=\"https://doi.org/10.1016/j.ic.2024.105214\">10.1016/j.ic.2024.105214</a>","ieee":"C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Entropic risk for turn-based stochastic games,” <i>Information and Computation</i>, vol. 301. Elsevier, 2024.","mla":"Baier, Christel, et al. “Entropic Risk for Turn-Based Stochastic Games.” <i>Information and Computation</i>, vol. 301, 105214, Elsevier, 2024, doi:<a href=\"https://doi.org/10.1016/j.ic.2024.105214\">10.1016/j.ic.2024.105214</a>.","ista":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2024. Entropic risk for turn-based stochastic games. Information and Computation. 301, 105214.","chicago":"Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. “Entropic Risk for Turn-Based Stochastic Games.” <i>Information and Computation</i>. Elsevier, 2024. <a href=\"https://doi.org/10.1016/j.ic.2024.105214\">https://doi.org/10.1016/j.ic.2024.105214</a>.","apa":"Baier, C., Chatterjee, K., Meggendorfer, T., &#38; Piribauer, J. (2024). Entropic risk for turn-based stochastic games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2024.105214\">https://doi.org/10.1016/j.ic.2024.105214</a>","short":"C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, Information and Computation 301 (2024)."},"department":[{"_id":"KrCh"}],"date_created":"2024-09-01T22:01:07Z","acknowledgement":"Krishnendu Chatterjee reports financial support was provided by European Research Council.","article_processing_charge":"Yes (in subscription journal)","publication_identifier":{"eissn":["1090-2651"],"issn":["0890-5401"]},"external_id":{"isi":["001301143400001"],"arxiv":["2307.06611"]},"title":"Entropic risk for turn-based stochastic games","article_type":"original","volume":301,"year":"2024","publication":"Information and Computation","OA_place":"publisher","related_material":{"record":[{"status":"public","id":"14417","relation":"earlier_version"}]},"license":"https://creativecommons.org/licenses/by/4.0/","corr_author":"1","file":[{"content_type":"application/pdf","relation":"main_file","creator":"dernst","access_level":"open_access","date_updated":"2025-01-09T13:49:03Z","success":1,"file_size":724703,"file_name":"2024_InformationComputation_Baier.pdf","checksum":"f68e0c2f46f9b9c86815406bcf2ee2d4","date_created":"2025-01-09T13:49:03Z","file_id":"18817"}],"day":"01","oa":1,"language":[{"iso":"eng"}],"oa_version":"Published Version","date_updated":"2025-09-08T09:10:06Z","arxiv":1,"doi":"10.1016/j.ic.2024.105214","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"month":"12","OA_type":"hybrid","date_published":"2024-12-01T00:00:00Z","status":"public","publication_status":"published","abstract":[{"lang":"eng","text":"Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of turn-based stochastic games with the total reward objective. This gives rise to an objective function that demands the control of systems in a risk-averse manner. We show that the resulting games are determined and, in particular, admit optimal memoryless deterministic strategies. This contrasts risk measures that previously have been considered in the special case of Markov decision processes and that require randomization and/or memory. We provide several results on the decidability and the computational complexity of the threshold problem, i.e. whether the optimal value of ERisk exceeds a given threshold. Furthermore, an approximation algorithm for the optimal value of ERisk is provided."}],"ddc":["000"]},{"arxiv":1,"oa_version":"Preprint","date_updated":"2024-11-06T12:09:22Z","issue":"12","oa":1,"language":[{"iso":"eng"}],"day":"01","extern":"1","abstract":[{"lang":"eng","text":"We give two fully dynamic algorithms that maintain a (1 + ε)-approximation of the weight M of a minimum spanning forest (MSF) of an n-node graph G with edges weights in [1, W ], for any ε > 0. (1) Our deterministic algorithm takes O (W 2 log W /ε3) worst-case update time, which is O (1) if both W and ε are constants. (2) Our randomized (Monte-Carlo style) algorithm works with high probability and runs in worst-case O (log W /ε4) update time if W = O ((m∗)1/6/log2/3 n), where m∗ is the minimum number of edges in the graph throughout all the updates. It works even against an adaptive adversary. We complement our algorithmic results with two cell-probe lower bounds for dynamically maintaining an approximation of the weight of an MSF of a graph."}],"publication_status":"published","status":"public","date_published":"2021-12-01T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/2011.00977","open_access":"1"}],"month":"12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1016/j.ic.2021.104805","citation":{"ama":"Henzinger M, Peng P. Constant-time dynamic weight approximation for minimum spanning forest. <i>Information and Computation</i>. 2021;281(12). doi:<a href=\"https://doi.org/10.1016/j.ic.2021.104805\">10.1016/j.ic.2021.104805</a>","mla":"Henzinger, Monika, and Pan Peng. “Constant-Time Dynamic Weight Approximation for Minimum Spanning Forest.” <i>Information and Computation</i>, vol. 281, no. 12, 104805, Elsevier, 2021, doi:<a href=\"https://doi.org/10.1016/j.ic.2021.104805\">10.1016/j.ic.2021.104805</a>.","ieee":"M. Henzinger and P. Peng, “Constant-time dynamic weight approximation for minimum spanning forest,” <i>Information and Computation</i>, vol. 281, no. 12. Elsevier, 2021.","ista":"Henzinger M, Peng P. 2021. Constant-time dynamic weight approximation for minimum spanning forest. Information and Computation. 281(12), 104805.","chicago":"Henzinger, Monika, and Pan Peng. “Constant-Time Dynamic Weight Approximation for Minimum Spanning Forest.” <i>Information and Computation</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.ic.2021.104805\">https://doi.org/10.1016/j.ic.2021.104805</a>.","apa":"Henzinger, M., &#38; Peng, P. (2021). Constant-time dynamic weight approximation for minimum spanning forest. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2021.104805\">https://doi.org/10.1016/j.ic.2021.104805</a>","short":"M. Henzinger, P. Peng, Information and Computation 281 (2021)."},"article_number":"104805","quality_controlled":"1","scopus_import":"1","_id":"11756","author":[{"first_name":"Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","full_name":"Henzinger, Monika H"},{"first_name":"Pan","last_name":"Peng","full_name":"Peng, Pan"}],"publisher":"Elsevier","intvolume":"       281","type":"journal_article","publication":"Information and Computation","year":"2021","volume":281,"external_id":{"arxiv":["2011.00977"]},"title":"Constant-time dynamic weight approximation for minimum spanning forest","article_type":"original","publication_identifier":{"issn":["0890-5401"]},"article_processing_charge":"No","date_created":"2022-08-08T10:58:29Z"},{"publication_identifier":{"issn":["0890-5401"]},"date_created":"2022-08-08T11:20:03Z","article_processing_charge":"No","page":"219-239","year":"2018","publication":"Information and Computation","title":"Dynamic algorithms via the primal-dual method","article_type":"original","volume":261,"publisher":"Elsevier","intvolume":"       261","type":"journal_article","citation":{"short":"S. Bhattacharya, M. Henzinger, G. Italiano, Information and Computation 261 (2018) 219–239.","apa":"Bhattacharya, S., Henzinger, M., &#38; Italiano, G. (2018). Dynamic algorithms via the primal-dual method. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2018.02.005\">https://doi.org/10.1016/j.ic.2018.02.005</a>","chicago":"Bhattacharya, Sayan, Monika Henzinger, and Giuseppe Italiano. “Dynamic Algorithms via the Primal-Dual Method.” <i>Information and Computation</i>. Elsevier, 2018. <a href=\"https://doi.org/10.1016/j.ic.2018.02.005\">https://doi.org/10.1016/j.ic.2018.02.005</a>.","ista":"Bhattacharya S, Henzinger M, Italiano G. 2018. Dynamic algorithms via the primal-dual method. Information and Computation. 261(08), 219–239.","ieee":"S. Bhattacharya, M. Henzinger, and G. Italiano, “Dynamic algorithms via the primal-dual method,” <i>Information and Computation</i>, vol. 261, no. 08. Elsevier, pp. 219–239, 2018.","mla":"Bhattacharya, Sayan, et al. “Dynamic Algorithms via the Primal-Dual Method.” <i>Information and Computation</i>, vol. 261, no. 08, Elsevier, 2018, pp. 219–39, doi:<a href=\"https://doi.org/10.1016/j.ic.2018.02.005\">10.1016/j.ic.2018.02.005</a>.","ama":"Bhattacharya S, Henzinger M, Italiano G. Dynamic algorithms via the primal-dual method. <i>Information and Computation</i>. 2018;261(08):219-239. doi:<a href=\"https://doi.org/10.1016/j.ic.2018.02.005\">10.1016/j.ic.2018.02.005</a>"},"scopus_import":"1","quality_controlled":"1","author":[{"full_name":"Bhattacharya, Sayan","last_name":"Bhattacharya","first_name":"Sayan"},{"full_name":"Henzinger, Monika H","first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"first_name":"Giuseppe","last_name":"Italiano","full_name":"Italiano, Giuseppe"}],"_id":"11757","main_file_link":[{"url":"https://doi.org/10.1016/j.ic.2018.02.005","open_access":"1"}],"month":"08","doi":"10.1016/j.ic.2018.02.005","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We develop a dynamic version of the primal-dual method for optimization problems, and apply it to obtain the following results. (1) For the dynamic set-cover problem, we maintain an O ( f 2)-approximately optimal solution in O ( f · log(m + n)) amortized update time, where f is the maximum “frequency” of an element, n is the number of sets, and m is the maximum number of elements in the universe at any point in time. (2) For the dynamic b-matching problem, we maintain an O (1)-approximately optimal solution in O (log3 n) amortized update time, where n is the number of nodes in the graph."}],"publication_status":"published","extern":"1","status":"public","date_published":"2018-08-01T00:00:00Z","day":"01","issue":"08","oa_version":"Published Version","date_updated":"2024-11-06T08:13:33Z","oa":1,"language":[{"iso":"eng"}]},{"arxiv":1,"date_updated":"2026-04-16T10:00:03Z","oa_version":"Submitted Version","language":[{"iso":"eng"}],"ec_funded":1,"oa":1,"day":"01","corr_author":"1","publication_status":"published","abstract":[{"lang":"eng","text":"Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information. In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile where all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players' objective, then the objective of every player is violated. We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games."}],"status":"public","date_published":"2017-06-01T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1311.3238","open_access":"1"}],"month":"06","doi":"10.1016/j.ic.2016.10.012","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","citation":{"short":"K. Chatterjee, L. Doyen, E. Filiot, J. Raskin, Information and Computation 254 (2017) 296–315.","apa":"Chatterjee, K., Doyen, L., Filiot, E., &#38; Raskin, J. (2017). Doomsday equilibria for omega-regular games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">https://doi.org/10.1016/j.ic.2016.10.012</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean Raskin. “Doomsday Equilibria for Omega-Regular Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">https://doi.org/10.1016/j.ic.2016.10.012</a>.","ista":"Chatterjee K, Doyen L, Filiot E, Raskin J. 2017. Doomsday equilibria for omega-regular games. Information and Computation. 254, 296–315.","mla":"Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.” <i>Information and Computation</i>, vol. 254, Elsevier, 2017, pp. 296–315, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">10.1016/j.ic.2016.10.012</a>.","ieee":"K. Chatterjee, L. Doyen, E. Filiot, and J. Raskin, “Doomsday equilibria for omega-regular games,” <i>Information and Computation</i>, vol. 254. Elsevier, pp. 296–315, 2017.","ama":"Chatterjee K, Doyen L, Filiot E, Raskin J. Doomsday equilibria for omega-regular games. <i>Information and Computation</i>. 2017;254:296-315. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">10.1016/j.ic.2016.10.012</a>"},"quality_controlled":"1","scopus_import":"1","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"full_name":"Filiot, Emmanuel","last_name":"Filiot","first_name":"Emmanuel"},{"full_name":"Raskin, Jean","last_name":"Raskin","first_name":"Jean"}],"_id":"681","publisher":"Elsevier","intvolume":"       254","type":"journal_article","isi":1,"related_material":{"record":[{"relation":"earlier_version","id":"10885","status":"public"}]},"page":"296 - 315","publist_id":"7036","year":"2017","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"}],"publication":"Information and Computation","external_id":{"isi":["000402025600008"],"arxiv":["1311.3238"]},"title":"Doomsday equilibria for omega-regular games","article_type":"original","volume":254,"publication_identifier":{"issn":["0890-5401"]},"date_created":"2018-12-11T11:47:53Z","article_processing_charge":"No","department":[{"_id":"KrCh"}]},{"type":"journal_article","intvolume":"       222","day":"01","publisher":"Elsevier","language":[{"iso":"eng"}],"_id":"11758","author":[{"full_name":"Aceto, Luca","last_name":"Aceto","first_name":"Luca"},{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"full_name":"Sgall, Jiří","first_name":"Jiří","last_name":"Sgall"}],"quality_controlled":"1","date_updated":"2024-11-06T12:01:32Z","scopus_import":"1","oa_version":"None","issue":"1","citation":{"short":"L. Aceto, M. Henzinger, J. Sgall, Information and Computation 222 (2013) 1.","apa":"Aceto, L., Henzinger, M., &#38; Sgall, J. (2013). 38th International Colloquium on Automata, Languages and Programming. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2012.11.002\">https://doi.org/10.1016/j.ic.2012.11.002</a>","chicago":"Aceto, Luca, Monika Henzinger, and Jiří Sgall. “38th International Colloquium on Automata, Languages and Programming.” <i>Information and Computation</i>. Elsevier, 2013. <a href=\"https://doi.org/10.1016/j.ic.2012.11.002\">https://doi.org/10.1016/j.ic.2012.11.002</a>.","ieee":"L. Aceto, M. Henzinger, and J. Sgall, “38th International Colloquium on Automata, Languages and Programming,” <i>Information and Computation</i>, vol. 222, no. 1. Elsevier, p. 1, 2013.","mla":"Aceto, Luca, et al. “38th International Colloquium on Automata, Languages and Programming.” <i>Information and Computation</i>, vol. 222, no. 1, Elsevier, 2013, p. 1, doi:<a href=\"https://doi.org/10.1016/j.ic.2012.11.002\">10.1016/j.ic.2012.11.002</a>.","ista":"Aceto L, Henzinger M, Sgall J. 2013. 38th International Colloquium on Automata, Languages and Programming. Information and Computation. 222(1), 1.","ama":"Aceto L, Henzinger M, Sgall J. 38th International Colloquium on Automata, Languages and Programming. <i>Information and Computation</i>. 2013;222(1):1. doi:<a href=\"https://doi.org/10.1016/j.ic.2012.11.002\">10.1016/j.ic.2012.11.002</a>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1016/j.ic.2012.11.002","article_processing_charge":"No","month":"01","date_created":"2022-08-08T11:25:34Z","publication_identifier":{"issn":["0890-5401"]},"date_published":"2013-01-01T00:00:00Z","volume":222,"title":"38th International Colloquium on Automata, Languages and Programming","article_type":"letter_note","publication":"Information and Computation","status":"public","year":"2013","extern":"1","page":"1","publication_status":"published"},{"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","doi":"10.1006/inco.2001.3085","month":"02","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub","open_access":"1"}],"date_published":"2002-02-25T00:00:00Z","status":"public","extern":"1","abstract":[{"lang":"eng","text":"The simulation preorder for labeled transition systems is defined locally, and operationally, as a game that relates states with their immediate successor states. Simulation enjoys many appealing properties. First, simulation has a denotational characterization: system S simulates system I iff every computation tree embedded in the unrolling of I can be embedded also in the unrolling of S. Second, simulation has a logical characterization: S simulates I iff every universal branching-time formula satisfied by S is satisfied also by I. It follows that simulation is a suitable notion of implementation, and it is the coarsest abstraction of a system that preserves universal branching-time properties. Third, based on its local definition, simulation between finite-state systems can be checked in polynomial time. Finally, simulation implies trace containment, which cannot be defined locally and requires polynomial space for verification. Hence simulation is widely used both in manual and in automatic verification. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We propose a new view of fair simulation by extending the local definition of simulation to account for fairness: system View the MathML sourcefairly simulates system View the MathML source iff in the simulation game, there is a strategy that matches with each fair computation of View the MathML source a fair computation of View the MathML source. Our definition enjoys a denotational characterization and has a logical characterization: View the MathML source fairly simulates View the MathML source iff every fair computation tree (whose infinite paths are fair) embedded in the unrolling of View the MathML source can be embedded also in the unrolling of View the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by View the MathML source is satisfied also by View the MathML source (∀AFMC is the universal fragment of the alternation-free μ-calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace containment and is therefore useful as an efficiently computable local criterion for proving linear-time abstraction hierarchies of fair systems."}],"publication_status":"published","day":"25","oa":1,"language":[{"iso":"eng"}],"oa_version":"Published Version","date_updated":"2023-06-05T07:53:27Z","issue":"1","article_processing_charge":"No","date_created":"2018-12-11T12:09:02Z","acknowledgement":"We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers for their comments on this paper.","publication_identifier":{"issn":["0890-5401"]},"volume":173,"title":"Fair simulation","article_type":"original","publication":"Information and Computation","year":"2002","publist_id":"255","page":"64 - 81","type":"journal_article","intvolume":"       173","publisher":"Elsevier","_id":"4474","author":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"},{"full_name":"Rajamani, Sriram","last_name":"Rajamani","first_name":"Sriram"}],"scopus_import":"1","quality_controlled":"1","citation":{"chicago":"Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.” <i>Information and Computation</i>. Elsevier, 2002. <a href=\"https://doi.org/10.1006/inco.2001.3085\">https://doi.org/10.1006/inco.2001.3085</a>.","short":"T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173 (2002) 64–81.","apa":"Henzinger, T. A., Kupferman, O., &#38; Rajamani, S. (2002). Fair simulation. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.2001.3085\">https://doi.org/10.1006/inco.2001.3085</a>","ama":"Henzinger TA, Kupferman O, Rajamani S. Fair simulation. <i>Information and Computation</i>. 2002;173(1):64-81. doi:<a href=\"https://doi.org/10.1006/inco.2001.3085\">10.1006/inco.2001.3085</a>","ieee":"T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” <i>Information and Computation</i>, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.","mla":"Henzinger, Thomas A., et al. “Fair Simulation.” <i>Information and Computation</i>, vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:<a href=\"https://doi.org/10.1006/inco.2001.3085\">10.1006/inco.2001.3085</a>.","ista":"Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information and Computation. 173(1), 64–81."}},{"day":"01","oa_version":"None","date_updated":"2022-06-02T09:24:58Z","issue":"2","language":[{"iso":"eng"}],"oa":1,"main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/S0890540184710601?via%3Dihub"}],"month":"08","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","doi":"10.1006/inco.1994.1060","extern":"1","publication_status":"published","abstract":[{"lang":"eng","text":"We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-;time properties of reactive systems. The abstract notion of timed transition systems generalizes traditional transition systems conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. This framework can model real-time systems that communicate either through shared variables or by message passing and real-time issues such as timeouts, process priorities (interrupts), and process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit references to time through a special clock variable. Corresponding to the two styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules for establishing bounded-invariance and bounded-responce properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and response properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties."}],"status":"public","date_published":"1994-08-01T00:00:00Z","publisher":"Elsevier","intvolume":"       112","type":"journal_article","citation":{"ieee":"T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for timed transition systems,” <i>Information and Computation</i>, vol. 112, no. 2. Elsevier, pp. 273–337, 1994.","ista":"Henzinger TA, Manna Z, Pnueli A. 1994. Temporal proof methodologies for timed transition systems. Information and Computation. 112(2), 273–337.","mla":"Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Timed Transition Systems.” <i>Information and Computation</i>, vol. 112, no. 2, Elsevier, 1994, pp. 273–337, doi:<a href=\"https://doi.org/10.1006/inco.1994.1060\">10.1006/inco.1994.1060</a>.","ama":"Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for timed transition systems. <i>Information and Computation</i>. 1994;112(2):273-337. doi:<a href=\"https://doi.org/10.1006/inco.1994.1060\">10.1006/inco.1994.1060</a>","apa":"Henzinger, T. A., Manna, Z., &#38; Pnueli, A. (1994). Temporal proof methodologies for timed transition systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.1994.1060\">https://doi.org/10.1006/inco.1994.1060</a>","short":"T.A. Henzinger, Z. Manna, A. Pnueli, Information and Computation 112 (1994) 273–337.","chicago":"Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies for Timed Transition Systems.” <i>Information and Computation</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1006/inco.1994.1060\">https://doi.org/10.1006/inco.1994.1060</a>."},"scopus_import":"1","quality_controlled":"1","_id":"4501","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Zohar","last_name":"Manna","full_name":"Manna, Zohar"},{"last_name":"Pnueli","first_name":"Amir","full_name":"Pnueli, Amir"}],"publication_identifier":{"issn":["0890-5401"]},"article_processing_charge":"No","acknowledgement":"This research was supported in part by an IBM graduate fellowship, by the National Science Foundation under Grants CCR-9223226 and CCR-9200794. by the Defense Advanced Research Projects Agency under Contract N00039-84-C-0211. by the United States Air Force OMee of Scientific Research under Contracts F49620-93-141139 and F4962043-1-0056. and by the European Community ESPRIT Basic Research Action Project 6021 (REACT). A preliminary version of Part 1 of this paper appeared in the proceedings of the 1991 REX Workshop on Real Time Theory In Prate [HMP92a I a preliminary version of Part II appeared in the proceedings of the 1991 ACM Symposium on Principles of Programming Languages RIMP911. ","date_created":"2018-12-11T12:09:10Z","publist_id":"227","page":"273 - 337","publication":"Information and Computation","year":"1994","volume":112,"article_type":"original","title":"Temporal proof methodologies for timed transition systems"},{"issue":"2","oa_version":"None","date_updated":"2022-06-02T09:02:02Z","language":[{"iso":"eng"}],"day":"01","publication_status":"published","abstract":[{"lang":"eng","text":"We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of &quot;implementable&quot; real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory."}],"extern":"1","status":"public","date_published":"1994-06-01T00:00:00Z","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0890540184710455?via%3Dihub"}],"month":"06","doi":"10.1006/inco.1994.1045","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"ieee":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking for real-time systems,” <i>Information and Computation</i>, vol. 111, no. 2. Elsevier, pp. 193–244, 1994.","ista":"Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1994. Symbolic model checking for real-time systems. Information and Computation. 111(2), 193–244.","mla":"Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.” <i>Information and Computation</i>, vol. 111, no. 2, Elsevier, 1994, pp. 193–244, doi:<a href=\"https://doi.org/10.1006/inco.1994.1045\">10.1006/inco.1994.1045</a>.","ama":"Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for real-time systems. <i>Information and Computation</i>. 1994;111(2):193-244. doi:<a href=\"https://doi.org/10.1006/inco.1994.1045\">10.1006/inco.1994.1045</a>","apa":"Henzinger, T. A., Nicollin, X., Sifakis, J., &#38; Yovine, S. (1994). Symbolic model checking for real-time systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.1994.1045\">https://doi.org/10.1006/inco.1994.1045</a>","short":"T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Information and Computation 111 (1994) 193–244.","chicago":"Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. “Symbolic Model Checking for Real-Time Systems.” <i>Information and Computation</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1006/inco.1994.1045\">https://doi.org/10.1006/inco.1994.1045</a>."},"scopus_import":"1","quality_controlled":"1","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"full_name":"Nicollin, Xavier","first_name":"Xavier","last_name":"Nicollin"},{"full_name":"Sifakis, Joseph","last_name":"Sifakis","first_name":"Joseph"},{"last_name":"Yovine","first_name":"Sergio","full_name":"Yovine, Sergio"}],"_id":"4503","publisher":"Elsevier","intvolume":"       111","type":"journal_article","page":"193 - 244","publist_id":"226","year":"1994","publication":"Information and Computation","article_type":"original","title":"Symbolic model checking for real-time systems","volume":111,"publication_identifier":{"issn":["0890-5401"]},"date_created":"2018-12-11T12:09:11Z","acknowledgement":"We thank Peter Kopke for a careful reading.","article_processing_charge":"No"}]