[{"publisher":"ACM","title":"A hierarchical coordination language for interacting real-time tasks","status":"public","publication_status":"published","_id":"4526","year":"2006","date_created":"2018-12-11T12:09:18Z","date_updated":"2021-01-12T07:59:27Z","author":[{"full_name":"Ghosal, Arkadeb","last_name":"Ghosal","first_name":"Arkadeb"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger"},{"last_name":"Iercan","first_name":"Daniel","full_name":"Iercan, Daniel"},{"full_name":"Kirsch, Christoph M","last_name":"Kirsch","first_name":"Christoph"},{"full_name":"Sangiovanni-Vincentelli, Alberto","last_name":"Sangiovanni Vincentelli","first_name":"Alberto"}],"type":"conference","extern":1,"publist_id":"201","abstract":[{"text":"We designed and implemented a new programming language called Hierarchical Timing Language (HTL) for hard realtime systems. Critical timing constraints are specified within the language,and ensured by the compiler. Programs in HTL are extensible in two dimensions without changing their timing behavior: new program modules can be added, and individual program tasks can be refined. The mechanism supporting time invariance under parallel composition is that different program modules communicate at specified instances of time. Time invariance under refinement is achieved by conservative scheduling of the top level. HTL is a coordination language, in that individual tasks can be implemented in "foreign" languages. As a case study, we present a distributed HTL implementation of an automotive steer-by-wire controller.","lang":"eng"}],"page":"132 - 141","quality_controlled":0,"citation":{"ista":"Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. 2006. A hierarchical coordination language for interacting real-time tasks. EMSOFT: Embedded Software , 132–141.","apa":"Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., & Sangiovanni Vincentelli, A. (2006). A hierarchical coordination language for interacting real-time tasks (pp. 132–141). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1176887.1176907","ieee":"A. Ghosal, T. A. Henzinger, D. Iercan, C. Kirsch, and A. Sangiovanni Vincentelli, “A hierarchical coordination language for interacting real-time tasks,” presented at the EMSOFT: Embedded Software , 2006, pp. 132–141.","ama":"Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. A hierarchical coordination language for interacting real-time tasks. In: ACM; 2006:132-141. doi:10.1145/1176887.1176907","chicago":"Ghosal, Arkadeb, Thomas A Henzinger, Daniel Iercan, Christoph Kirsch, and Alberto Sangiovanni Vincentelli. “A Hierarchical Coordination Language for Interacting Real-Time Tasks,” 132–41. ACM, 2006. https://doi.org/10.1145/1176887.1176907.","mla":"Ghosal, Arkadeb, et al. A Hierarchical Coordination Language for Interacting Real-Time Tasks. ACM, 2006, pp. 132–41, doi:10.1145/1176887.1176907.","short":"A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, A. Sangiovanni Vincentelli, in:, ACM, 2006, pp. 132–141."},"doi":"10.1145/1176887.1176907","date_published":"2006-01-01T00:00:00Z","conference":{"name":"EMSOFT: Embedded Software "},"month":"01","day":"01"},{"conference":{"name":"WSC: Winter Simulation Conference"},"doi":"10.1109/WSC.2006.322942","date_published":"2006-12-03T00:00:00Z","citation":{"ista":"Fisher J, Henzinger TA. 2006. Executable biology. WSC: Winter Simulation Conference, 1675–1682.","ieee":"J. Fisher and T. A. Henzinger, “Executable biology,” presented at the WSC: Winter Simulation Conference, 2006, pp. 1675–1682.","apa":"Fisher, J., & Henzinger, T. A. (2006). Executable biology (pp. 1675–1682). Presented at the WSC: Winter Simulation Conference, IEEE. https://doi.org/10.1109/WSC.2006.322942","ama":"Fisher J, Henzinger TA. Executable biology. In: IEEE; 2006:1675-1682. doi:10.1109/WSC.2006.322942","chicago":"Fisher, Jasmin, and Thomas A Henzinger. “Executable Biology,” 1675–82. IEEE, 2006. https://doi.org/10.1109/WSC.2006.322942.","mla":"Fisher, Jasmin, and Thomas A. Henzinger. Executable Biology. IEEE, 2006, pp. 1675–82, doi:10.1109/WSC.2006.322942.","short":"J. Fisher, T.A. Henzinger, in:, IEEE, 2006, pp. 1675–1682."},"quality_controlled":0,"page":"1675 - 1682","day":"03","month":"12","author":[{"last_name":"Fisher","first_name":"Jasmin","full_name":"Fisher, Jasmin"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"}],"date_created":"2018-12-11T12:09:19Z","date_updated":"2021-01-12T07:59:28Z","_id":"4528","year":"2006","title":"Executable biology","publication_status":"published","status":"public","publisher":"IEEE","abstract":[{"lang":"eng","text":"Computational modeling of biological systems is becoming increasingly common as scientists attempt to understand biological phenomena in their full complexity. Here we distinguish between two types of biological models mathematical and computational - according to their different representations of biological phenomena and their diverse potential. We call the approach of constructing computational models of biological systems executable biology, as it focuses on the design of executable computer algorithms that mimic biological phenomena. We give an overview of the main modeling efforts in this direction, and discuss some of the new challenges that executable biology poses for computer science and biology. We argue that for executable biology to reach its full potential as a mainstream biological technique, formal and algorithmic approaches must be integrated into biological research, driving biology towards a more precise engineering discipline."}],"publist_id":"197","extern":1,"type":"conference"},{"extern":1,"abstract":[{"text":"Games on graphs with ω-regular objectives provide a model for the control and synthesis of reactive systems. Every ω-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. While for one-shot liveness (reachability) objectives, classical and finitary liveness coincide, for repeated liveness (Büchi) objectives, the finitary formulation is strictly stronger. In this work we study games with finitary parity and Streett (fairness) objectives. We prove the determinacy of these games, present algorithms for solving these games, and characterize the memory requirements of winning strategies. Our algorithms can be used, for example, for synthesizing controllers that do not let the response time of a system increase without bound.","lang":"eng"}],"publist_id":"183","alternative_title":["LNCS"],"type":"conference","date_created":"2018-12-11T12:09:22Z","date_updated":"2021-01-12T07:59:32Z","volume":3920,"author":[{"full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger"}],"publication_status":"published","title":"Finitary winning in omega-regular games","status":"public","publisher":"Springer","intvolume":" 3920","year":"2006","_id":"4539","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327 and the NSF ITR grant CCR-0225610.","day":"15","month":"03","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_published":"2006-03-15T00:00:00Z","doi":"10.1007/11691372_17","quality_controlled":0,"page":"257 - 271","citation":{"ieee":"K. Chatterjee and T. A. Henzinger, “Finitary winning in omega-regular games,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2006, vol. 3920, pp. 257–271.","apa":"Chatterjee, K., & Henzinger, T. A. (2006). Finitary winning in omega-regular games (Vol. 3920, pp. 257–271). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. https://doi.org/10.1007/11691372_17","ista":"Chatterjee K, Henzinger TA. 2006. Finitary winning in omega-regular games. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 3920, 257–271.","ama":"Chatterjee K, Henzinger TA. Finitary winning in omega-regular games. In: Vol 3920. Springer; 2006:257-271. doi:10.1007/11691372_17","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Finitary Winning in Omega-Regular Games,” 3920:257–71. Springer, 2006. https://doi.org/10.1007/11691372_17.","short":"K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 257–271.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. Finitary Winning in Omega-Regular Games. Vol. 3920, Springer, 2006, pp. 257–71, doi:10.1007/11691372_17."}},{"doi":"10.1007/11672142_42","date_published":"2006-02-14T00:00:00Z","conference":{"name":"STACS: Theoretical Aspects of Computer Science"},"citation":{"apa":"Chatterjee, K., & Henzinger, T. A. (2006). Strategy improvement and randomized subexponential algorithms for stochastic parity games (Vol. 3884, pp. 512–523). Presented at the STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_42","ieee":"K. Chatterjee and T. A. Henzinger, “Strategy improvement and randomized subexponential algorithms for stochastic parity games,” presented at the STACS: Theoretical Aspects of Computer Science, 2006, vol. 3884, pp. 512–523.","ista":"Chatterjee K, Henzinger TA. 2006. Strategy improvement and randomized subexponential algorithms for stochastic parity games. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 3884, 512–523.","ama":"Chatterjee K, Henzinger TA. Strategy improvement and randomized subexponential algorithms for stochastic parity games. In: Vol 3884. Springer; 2006:512-523. doi:10.1007/11672142_42","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games,” 3884:512–23. Springer, 2006. https://doi.org/10.1007/11672142_42.","short":"K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 512–523.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games. Vol. 3884, Springer, 2006, pp. 512–23, doi:10.1007/11672142_42."},"page":"512 - 523","quality_controlled":0,"month":"02","day":"14","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger"}],"volume":3884,"date_created":"2018-12-11T12:09:22Z","date_updated":"2021-01-12T07:59:32Z","year":"2006","_id":"4538","intvolume":" 3884","publisher":"Springer","publication_status":"published","title":"Strategy improvement and randomized subexponential algorithms for stochastic parity games","status":"public","publist_id":"184","abstract":[{"text":"A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy improvement algorithm for stochastic parity games; this is the first non-brute-force algorithm for solving these games. From the strategy improvement algorithm we obtain a randomized subexponential-time algorithm to solve such games.","lang":"eng"}],"extern":1,"type":"conference","alternative_title":["LNCS"]},{"month":"02","day":"14","citation":{"short":"K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.","mla":"Chatterjee, Krishnendu, et al. Markov Decision Processes with Multiple Objectives. Vol. 3884, Springer, 2006, pp. 325–36, doi:10.1007/11672142_26.","chicago":"Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. https://doi.org/10.1007/11672142_26.","ama":"Chatterjee K, Majumdar R, Henzinger TA. Markov decision processes with multiple objectives. In: Vol 3884. Springer; 2006:325-336. doi:10.1007/11672142_26","apa":"Chatterjee, K., Majumdar, R., & Henzinger, T. A. (2006). Markov decision processes with multiple objectives (Vol. 3884, pp. 325–336). Presented at the STACS: Theoretical Aspects of Computer Science, Springer. https://doi.org/10.1007/11672142_26","ieee":"K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Markov decision processes with multiple objectives,” presented at the STACS: Theoretical Aspects of Computer Science, 2006, vol. 3884, pp. 325–336.","ista":"Chatterjee K, Majumdar R, Henzinger TA. 2006. Markov decision processes with multiple objectives. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 3884, 325–336."},"quality_controlled":0,"page":"325 - 336","conference":{"name":"STACS: Theoretical Aspects of Computer Science"},"doi":"10.1007/11672142_26","date_published":"2006-02-14T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple discounted reward objectives. Such MDPs occur in design problems where one wishes to simultaneously optimize several criteria, for example, latency and power. The possible trade-offs between the different objectives are characterized by the Pareto curve. We show that every Pareto-optimal point can be achieved by a memoryless strategy; however, unlike in the single-objective case, the memoryless strategy may require randomization. Moreover, we show that the Pareto curve can be approximated in polynomial time in the size of the MDP. Additionally, we study the problem if a given value vector is realizable by any strategy, and show that it can be decided in polynomial time; but the question whether it is realizable by a deterministic memoryless strategy is NP-complete. These results provide efficient algorithms for design exploration in MDP models with multiple objectives.\nThis research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202. "}],"publist_id":"161","extern":1,"year":"2006","_id":"4551","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202.","publication_status":"published","status":"public","title":"Markov decision processes with multiple objectives","publisher":"Springer","intvolume":" 3884","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Krishnendu Chatterjee"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger"}],"date_created":"2018-12-11T12:09:26Z","date_updated":"2021-01-12T07:59:38Z","volume":3884}]