@inproceedings{4406,
abstract = {We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata.},
author = {De Wulf, Martin and Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François},
pages = {17 -- 30},
publisher = {Springer},
title = {{Antichains: A new algorithm for checking universality of finite automata}},
doi = {10.1007/11817963_5},
volume = {4144},
year = {2006},
}
@inproceedings{4431,
abstract = {We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science.},
author = {Thomas Henzinger and Sifakis, Joseph},
pages = {1 -- 15},
publisher = {Springer},
title = {{The embedded systems design challenge}},
doi = {10.1007/11813040_1},
volume = {4085},
year = {2006},
}
@inproceedings{4432,
abstract = {We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.},
author = {Thomas Henzinger and Prabhu, Vinayak S},
pages = {1 -- 17},
publisher = {Springer},
title = {{Timed alternating-time temporal logic}},
doi = {10.1007/11867340_1},
volume = {4202},
year = {2006},
}
@inproceedings{4436,
abstract = {We present an assume-guarantee interface algebra for real-time components. In our formalism a component implements a set of task sequences that share a resource. A component interface consists of an arrival rate function and a latency for each task sequence, and a capacity function for the shared resource. The interface specifies that the component guarantees certain task latencies depending on assumptions about task arrival rates and allocated resource capacities. Our algebra defines compatibility and refinement relations on interfaces. Interface compatibility can be checked on partial designs, even when some component interfaces are yet unknown. In this case interface composition computes as new assumptions the weakest constraints on the unknown components that are necessary to satisfy the specified guarantees. Interface refinement is defined in a way that ensures that compatible interfaces can be refined and implemented independently. Our algebra thus formalizes an interface-based design methodology that supports both the incremental addition of new components and the independent stepwise refinement of existing components. We demonstrate the flexibility and efficiency of the framework through simulation experiments.},
author = {Thomas Henzinger and Matic, Slobodan},
pages = {253 -- 266},
publisher = {IEEE},
title = {{An interface algebra for real-time components}},
doi = {10.1109/RTAS.2006.11},
year = {2006},
}
@inproceedings{4437,
abstract = {The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.},
author = {Thomas Henzinger and Piterman, Nir},
pages = {395 -- 410},
publisher = {Springer},
title = {{Solving games without determinization}},
doi = {10.1007/11874683_26},
volume = {4207},
year = {2006},
}
@article{4451,
abstract = {One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternation-free fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment.},
author = {Thomas Henzinger and Kupferman, Orna and Majumdar, Ritankar S},
journal = {Theoretical Computer Science},
number = {2},
pages = {173 -- 186},
publisher = {Elsevier},
title = {{On the universal and existential fragments of the mu-calculus}},
doi = {10.1016/j.tcs.2005.11.015},
volume = {354},
year = {2006},
}
@inproceedings{4523,
abstract = {We consider the problem if a given program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi.},
author = {Gulavani, Bhargav S and Thomas Henzinger and Kannan, Yamini and Nori, Aditya V and Rajamani, Sriram K},
pages = {117 -- 127},
publisher = {ACM},
title = {{Synergy: A new algorithm for property checking}},
doi = {10.1145/1181775.1181790},
year = {2006},
}
@inproceedings{4526,
abstract = {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.},
author = {Ghosal, Arkadeb and Thomas Henzinger and Iercan, Daniel and Kirsch, Christoph M and Sangiovanni-Vincentelli, Alberto},
pages = {132 -- 141},
publisher = {ACM},
title = {{A hierarchical coordination language for interacting real-time tasks}},
doi = {10.1145/1176887.1176907},
year = {2006},
}
@inproceedings{4528,
abstract = {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.},
author = {Fisher, Jasmin and Thomas Henzinger},
pages = {1675 -- 1682},
publisher = {IEEE},
title = {{Executable biology}},
doi = {10.1109/WSC.2006.322942},
year = {2006},
}
@inproceedings{4538,
abstract = {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.},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {512 -- 523},
publisher = {Springer},
title = {{Strategy improvement and randomized subexponential algorithms for stochastic parity games}},
doi = {10.1007/11672142_42},
volume = {3884},
year = {2006},
}
@inproceedings{4539,
abstract = {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.},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {257 -- 271},
publisher = {Springer},
title = {{Finitary winning in omega-regular games}},
doi = {10.1007/11691372_17},
volume = {3920},
year = {2006},
}
@inproceedings{4549,
abstract = {We present a compositional theory of system verification, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system properties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports the composition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbered distances between descriptions of a system at different levels of detail. We show that the classical Boolean rules for compositional reasoning have quantitative counterparts in our setting. While our general theory allows costs to be specified by arbitrary cost functions, we also consider a class of linear cost functions, which give rise to an instance of our framework where all operations are computable in polynomial time.},
author = {Krishnendu Chatterjee and de Alfaro, Luca and Faella, Marco and Thomas Henzinger and Majumdar, Ritankar S and Stoelinga, Mariëlle},
pages = {179 -- 188},
publisher = {IEEE},
title = {{Compositional quantitative reasoning}},
doi = {10.1109/QEST.2006.11},
year = {2006},
}
@article{4550,
abstract = {In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent's payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it sometimes suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of ω-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.},
author = {Krishnendu Chatterjee and Thomas Henzinger and Jurdziński, Marcin},
journal = {Theoretical Computer Science},
number = {1-2},
pages = {67 -- 82},
publisher = {Elsevier},
title = {{Games with secure equilibria}},
doi = {10.1016/j.tcs.2006.07.032},
volume = {365},
year = {2006},
}
@inproceedings{4551,
abstract = {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.
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. },
author = {Krishnendu Chatterjee and Majumdar, Ritankar S and Thomas Henzinger},
pages = {325 -- 336},
publisher = {Springer},
title = {{Markov decision processes with multiple objectives}},
doi = {10.1007/11672142_26},
volume = {3884},
year = {2006},
}
@inproceedings{4552,
abstract = {A concurrent reachability game is a two-player game played on a graph: at each state, the players simultaneously and independently select moves; the two moves determine jointly a probability distribution over the successor states. The objective for player 1 consists in reaching a set of target states; the objective for player 2 is to prevent this, so that the game is zero-sum. Our contributions are two-fold. First, we present a simple proof of the fact that in concurrent reachability games, for all epsilon > 0, memoryless epsilon-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an epsilon-optimal strategy achieves the objective with probability within epsilon of the value of the game. In contrast to previous proofs of this fact, which rely on the limit behavior of discounted games using advanced Puisieux series analysis, our proof is elementary and combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives.},
author = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger},
pages = {291 -- 300},
publisher = {IEEE},
title = {{Strategy improvement for concurrent reachability games}},
doi = {10.1109/QEST.2006.48},
year = {2006},
}
@inproceedings{4574,
abstract = {Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker Blast. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending Blast with calls to Tvla.},
author = {Beyer, Dirk and Thomas Henzinger and Théoduloz, Grégory},
pages = {532 -- 546},
publisher = {Springer},
title = {{Lazy shape analysis}},
doi = {10.1007/11817963_48},
volume = {4144},
year = {2006},
}
@inbook{3002,
abstract = {Arabidopsis thaliana is currently the most important model organism for basic molecular plant research. It is also a favourable model for developmental biology, as its embryogenesis follows a nearly invariant pattern of cell divisions and cell type specifications. Study of embryogenesis can involve genetic, physiological or biochemical approaches, but is always limited by the inaccessibility of the embryos which develop deep inside maternal tissue. Thus, for developmental studies, there is an increasing demand for methods which allow embryogenesis under artificial conditions, providing better accessibility to experimental manipulation. In this chapter, we address theoretical aspects of embryo culture, give some thoughts on which embryo culture system is suited best for which application and finally discuss three current methods which have been successfully used in Arabidopsis embryo culture. © 2006 Springer-Verlag Berlin Heidelberg.},
author = {Sauer, Michael and Jirí Friml},
booktitle = {Somatic Embryogenesis},
editor = {Mujib, Abdul and Šamaj, Jozef},
pages = {343 -- 354},
publisher = {Springer},
title = {{In vitro culture of Arabidopsis embryos}},
doi = {10.1007/7089_020},
volume = {2},
year = {2006},
}
@article{3005,
author = {Friml, Jirí and Benfey, Philip and Benková, Eva and Bennett, Malcolm and Berleth, Thomas and Geldner, Niko and Grebe, Markus and Heisler, Marcus and Hejátko, Jan and Jürgens, Gerd and Laux, Thomas and Lindsey, Keith and Lukowitz, Wolfgang and Luschnig, Christian and Offringa, Remko and Scheres, Ben and Swarup, Ranjan and Torres Ruiz, Ramón and Weijers, Dolf and Zažímalová, Eva},
journal = {Trends in Plant Science},
number = {1},
pages = {12 -- 14},
publisher = {Cell Press},
title = {{Apical-basal polarity: Why plant cells don't stand on their heads}},
doi = {10.1016/j.tplants.2005.11.010},
volume = {11},
year = {2006},
}
@article{3006,
abstract = {Dividing plant cells perform a remarkable task of building a new cell wall within the cytoplasm in a few minutes. A long-standing paradigm claims that this primordial cell wall, known as the cell plate, is generated by delivery of newly synthesized material from Golgi apparatus-originated secretory vesicles. Here, we show that, in diverse plant species, cell surface material, including plasma membrane proteins, cell wall components, and exogenously applied endocytic tracers, is rapidly delivered to the forming cell plate. Importantly, this occurs even when de novo protein synthesis is blocked. In addition, cytokinesis-specific syntaxin KNOLLE as well as plasma membrane (PM) resident proteins localize to endosomes that fuse to initiate the cell plate. The rate of endocytosis is strongly enhanced during cell plate formation, and its genetic or pharmacological inhibition leads to cytokinesis defects. Our results reveal that endocytic delivery of cell surface material significantly contributes to cell plate formation during plant cytokinesis. },
author = {Dhonukshe, Pankaj and Baluška, František and Schlicht, Markus and Hlavacka, Andrej and Šamaj, Jozef and Jirí Friml and Gadella, Theodorus W},
journal = {Developmental Cell},
number = {1},
pages = {137 -- 150},
publisher = {Cell Press},
title = {{Endocytosis of cell surface material mediates cell plate formation during plant cytokinesis}},
doi = {10.1016/j.devcel.2005.11.015},
volume = {10},
year = {2006},
}
@article{3007,
abstract = {Root gravitropism describes the orientation of root growth along the gravity vector and is mediated by differential cell elongation in the root meristem. This response requires the coordinated, asymmetric distribution of the phytohormone auxin within the root meristem, and depends on the concerted activities of PIN proteins and AUX1 - members of the auxin transport pathway. Here, we show that intracellular trafficking and proteasome activity combine to control PIN2 degradation during root gravitropism. Following gravi-stimulation, proteasome-dependent variations in PIN2 localization and degradation at the upper and lower sides of the root result in asymmetric distribution of PIN2. Ubiquitination of PIN2 occurs in a proteasome-dependent manner, indicating that the proteasome is involved in the control of PIN2 turnover. Stabilization of PIN2 affects its abundance and distribution, and leads to defects in auxin distribution and gravitropic responses. We describe the effects of auxin on PIN2 localization and protein levels, indicating that redistribution of auxin during the gravitropic response may be involved in the regulation of PIN2 protein.},
author = {Abas, Lindy and Benjamins, René and Malenica, Nenad and Paciorek, Tomasz and Wiśniewska, Justyna and Moulinier-Anzola, Jeanette C and Sieberer, Tobias and Jirí Friml and Luschnig, Christian},
journal = {Nature Cell Biology},
number = {3},
pages = {249 -- 256},
publisher = {Nature Publishing Group},
title = {{Intracellular trafficking and proteolysis of the Arabidopsis auxin-efflux facilitator PIN2 are involved in root gravitropism}},
doi = {10.1038/ncb1369},
volume = {8},
year = {2006},
}