@article{3836, abstract = {Hierarchical Timing Language (HTL) is a coordination language for distributed, hard real-time applications. HTL is a hierarchical extension of Giotto and, like its predecessor, based on the logical execution time (LET) paradigm of real-time programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine (or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram structure needs to be flattened; the flattening makes separatecompilation difficult, and may result in E machinecode of exponential size. In this paper, we propose a generalization of the E machine, which supports a hierarchicalprogram structure at runtime through real-time trigger mechanisms that are arranged in a tree. We present the generalized E machine, and a modular compiler for HTL that generates code of linear size. The compiler may generate code for any part of a given HTL program separately in any order.}, author = {Ghosal, Arkadeb and Iercan, Daniel and Kirsch, Christoph and Henzinger, Thomas A and Sangiovanni Vincentelli, Alberto}, journal = {Science of Computer Programming}, number = {2}, pages = {96 -- 112}, publisher = {Elsevier}, title = {{Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code}}, doi = {10.1016/j.scico.2010.06.004}, volume = {77}, year = {2012}, } @article{3168, abstract = {The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a mathematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the combinatorial complexity by quotienting the reachable set of molecular species into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently, we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper, we prove that this quotienting yields a sufficient condition for weak lumpability (that is to say that the quotient system is still Markovian for a given set of initial distributions) and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system (which means that the conditional probability of being in a given state in the original system knowing that we are in its equivalence class is an invariant of the system). We illustrate the framework on a case study of the epidermal growth factor (EGF)/insulin receptor crosstalk.}, author = {Feret, Jérôme and Henzinger, Thomas A and Koeppl, Heinz and Petrov, Tatjana}, journal = {Theoretical Computer Science}, pages = {137 -- 164}, publisher = {Elsevier}, title = {{Lumpability abstractions of rule based systems}}, doi = {10.1016/j.tcs.2011.12.059}, volume = {431}, year = {2012}, } @article{3846, abstract = {We summarize classical and recent results about two-player games played on graphs with ω-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A}, journal = {Journal of Computer and System Sciences}, number = {2}, pages = {394 -- 413}, publisher = {Elsevier}, title = {{A survey of stochastic ω regular games}}, doi = {10.1016/j.jcss.2011.05.002}, volume = {78}, year = {2012}, } @article{2972, abstract = {Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (i.e., the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objectives. Our main results are as follows: (a) exponential memory is sufficient and may be necessary for winning strategies in energy parity games; (b) the problem of deciding the winner in energy parity games can be solved in NP ∩ coNP; and (c) we give an algorithm to solve energy parity by reduction to energy games. We also show that the problem of deciding the winner in energy parity games is logspace-equivalent to the problem of deciding the winner in mean-payoff parity games, which can thus be solved in NP ∩ coNP. As a consequence we also obtain a conceptually simple algorithm to solve mean-payoff parity games.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, journal = {Theoretical Computer Science}, pages = {49 -- 60}, publisher = {Elsevier}, title = {{Energy parity games}}, doi = {10.1016/j.tcs.2012.07.038}, volume = {458}, year = {2012}, } @article{3249, abstract = {Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of "fit" or "desirability". We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.}, author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun}, journal = {Theoretical Computer Science}, number = {1}, pages = {21 -- 35}, publisher = {Elsevier}, title = {{Simulation distances}}, doi = {10.1016/j.tcs.2011.08.002}, volume = {413}, year = {2012}, }