TY - CONF
AB - We present a new software system architecture for the implementation of hard real-time applications. The core of the system is a microkernel whose reactivity (interrupt handling as in synchronous reactive programs) and proactivity (task scheduling as in traditional RTOSs) are fully programmable. The microkernel, which we implemented on a StrongARM processor, consists of two interacting domain-specific virtual machines, a reactive E (Embedded) machine and a proactive S (Scheduling) machine. The microkernel code (or microcode) that runs on the microkernel is partitioned into E and S code. E code manages the interaction of the system with the physical environment: the execution of E code is triggered by environment interrupts, which signal external events such as the arrival of a message or sensor value, and it releases application tasks to the S machine. S code manages the interaction of the system with the processor: the execution of S code is triggered by hardware interrupts, which signal internal events such as the completion of a task or time slice, and it dispatches application tasks to the CPU, possibly preempting a running task. This partition of the system orthogonalizes the two main concerns of real-time implementations: E code refers to environment time and thus defines the reactivity of the system in a hardware- and scheduler-independent fashion; S code refers to CPU time and defines a system scheduler. If both time lines can be reconciled, then the code is called time safe; violations of time safety are handled again in a programmable way, by run-time exceptions. The separation of E from S code permits the independent programming, verification, optimization, composition, dynamic adaptation, and reuse of both reaction and scheduling mechanisms. Our measurements show that the system overhead is very acceptable even for large sets of task, generally in the 0.2--0.3% range.
AU - Kirsch, Christoph M
AU - Sanvido, Marco A
AU - Thomas Henzinger
ID - 4418
TI - A programmable microkernel for real-time systems
ER -
TY - JOUR
AB - We define five increasingly comprehensive classes of infinite-state systems, called STS1--STS5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.STS1 These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by iteratively applying predecessor and Boolean operations on state sets, starting from a finite number of observable state sets. Any such iteration is guaranteed to terminate in that only a finite number of state sets can be generated. This enables model checking of the μ-calculus.STS2 These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive Boolean operations. This enables model checking of the existential and universal fragments of the μ-calculus.STS3 These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive Boolean operations (intersection is restricted to intersection with observables). This enables model checking of all ω-regular properties, including linear temporal logic.STS4 These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the μ-calculus.STS5 These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered (this is a weaker termination condition than above). This enables model checking of reachability properties.
AU - Thomas Henzinger
AU - Majumdar, Ritankar S
AU - Raskin, Jean-François
ID - 4454
IS - 1
JF - ACM Transactions on Computational Logic (TOCL)
TI - A classification of symbolic transition systems
VL - 6
ER -
TY - CONF
AB - We define quantitative similarity functions between timed transition systems that measure the degree of closeness of two systems as a real, in contrast to the traditional boolean yes/no approach to timed simulation and language inclusion. Two systems are close if for each timed trace of one system, there exists a corresponding timed trace in the other system with the same sequence of events and closely corresponding event timings. We show that timed CTL is robust with respect to our quantitative version of bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula. We also define a discounted version of CTL over timed systems, which assigns to every CTL formula a real value that is obtained by discounting real time. We prove the robustness of discounted CTL by establishing that close states in the bisimilarity metric have close values for all discounted CTL formulas.
AU - Thomas Henzinger
AU - Majumdar, Ritankar S
AU - Prabhu, Vinayak S
ID - 4455
TI - Quantifying similarities between timed systems
VL - 3829
ER -
TY - CONF
AB - A modular program analysis considers components independently and provides a succinct summary for each component, which is used when checking the rest of the system. Consider a system consisting of a library and a client. A temporal summary, or interface, of the library specifies legal sequences of library calls. The interface is safe if no call sequence violates the library's internal invariants; the interface is permissive if it contains every such sequence. Modular program analysis requires full interfaces, which are both safe and permissive: the client does not cause errors in the library if and only if it makes only sequences of library calls that are allowed by the full interface of the library.Previous interface-based methods have focused on safe interfaces, which may be too restrictive and thus reject good clients. We present an algorithm for automatically synthesizing software interfaces that are both safe and permissive. The algorithm generates interfaces as graphs whose vertices are labeled with predicates over the library's internal state, and whose edges are labeled with library calls. The interface state is refined incrementally until the full interface is constructed. In other words, the algorithm automatically synthesizes a typestate system for the library, against which any client can be checked for compatibility. We present an implementation of the algorithm which is based on the BLAST model checker, and we evaluate some case studies.
AU - Thomas Henzinger
AU - Jhala, Ranjit
AU - Majumdar, Ritankar S
ID - 4456
TI - Permissive interfaces
ER -
TY - CONF
AB - We present a compositional approach to the implementation of hard real-time software running on a distributed platform. We explain how several code suppliers, coordinated by a system integrator, can independently generate different parts of the distributed software. The task structure, interaction, and timing is specified as a Giotto program. Each supplier is given a part of the Giotto program and a timing interface, from which the supplier generates task and scheduling code. The integrator then checks, individually for each supplier, in pseudo-polynomial time, if the supplied code meets its timing specification. If all checks succeed, then the supplied software parts are guaranteed to work together and implement the original Giotto program. The feasibility of the approach is demonstrated by a prototype implementation.
AU - Thomas Henzinger
AU - Kirsch, Christoph M
AU - Matic, Slobodan
ID - 4457
TI - Composable code generation for distributed Giotto
ER -
TY - CONF
AB - We show how to automatically construct and refine rectangular abstractions of systems of linear differential equations. From a hybrid automaton whose dynamics are given by a system of linear differential equations, our method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton. We prove an optimality criterion for successive refinements. We also show that this method can take into account a safety property to be verified, refining only relevant parts of the state space. The practicability of the method is illustrated on a benchmark case study.
AU - Doyen, Laurent
AU - Thomas Henzinger
AU - Raskin, Jean-François
ID - 4536
TI - Automatic rectangular refinement of affine hybrid systems
VL - 3829
ER -
TY - CONF
AB - Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete.
We study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives.
AU - Krishnendu Chatterjee
AU - Thomas Henzinger
ID - 4541
TI - Semiperfect-information games
VL - 3821
ER -
TY - CONF
AB - The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We show that for Rabin winning conditions, both problems are in NP. As these problems were known to be NP-hard, it follows that they are NP-complete for Rabin conditions, and dually, coNP-complete for Streett conditions. The proof proceeds by showing that pure memoryless strategies suffice for qualitatively and quantitatively winning stochastic graph games with Rabin conditions. This insight is of interest in its own right, as it implies that controllers for Rabin objectives have simple implementations. We also prove that for every ω-regular condition, optimal winning strategies are no more complex than almost-sure winning strategies.
AU - Krishnendu Chatterjee
AU - de Alfaro, Luca
AU - Thomas Henzinger
ID - 4553
TI - The complexity of stochastic Rabin and Streett games
VL - 3580
ER -
TY - CONF
AB - Games played on graphs may have qualitative objectives, such as the satisfaction of an ω-regular property, or quantitative objectives, such as the optimization of a real-valued reward. When games are used to model reactive systems with both fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding objective combines both a qualitative and a quantitative component. In a general case of interest, the qualitative component is a parity condition and the quantitative component is a mean-payoff reward. We study and solve such mean-payoff parity games. We also prove some interesting facts about mean-payoff parity games which distinguish them both from mean-payoff and from parity games. In particular, we show that optimal strategies exist in mean-payoff parity games, but they may require infinite memory.
AU - Krishnendu Chatterjee
AU - Thomas Henzinger
AU - Jurdziński, Marcin
ID - 4554
TI - Mean-payoff parity games
ER -
TY - CONF
AB - Planning in adversarial and uncertain environments can be modeled as the problem of devising strategies in stochastic perfect information games. These games are generalizations of Markov decision processes (MDPs): there are two (adversarial) players, and a source of randomness. The main practical obstacle to computing winning strategies in such games is the size of the state space. In practice therefore, one typically works with abstractions of the model. The diffculty is to come up with an abstraction that is neither too coarse to remove all winning strategies (plans), nor too fine to be intractable. In verification, the paradigm of counterexample-guided abstraction refinement has been successful to construct useful but parsimonious abstractions automatically. We extend this paradigm to probabilistic models (namely, perfect information games and, as a special case, MDPs). This allows us to apply the counterexample-guided abstraction paradigm to the AI planning problem. As special cases, we get planning algorithms for MDPs and deterministic systems that automatically construct system abstractions.
AU - Krishnendu Chatterjee
AU - Thomas Henzinger
AU - Jhala, Ranjit
AU - Majumdar, Ritankar S
ID - 4557
TI - Counterexample-guided planning
ER -
TY - CONF
AB - We define and study a quantitative generalization of the traditional boolean framework of model-based specification and verification. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a system with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values.
Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quantitative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specified by quantitative-bound automata, which are finite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an integer f(K). Along with the linear-time, automaton-based view of quantitative verification, we present a corresponding branching-time view based on a quantitative-bound μ-calculus, and we study the relationship, expressive power, and complexity of both views.
AU - Chakrabarti, Arindam
AU - Krishnendu Chatterjee
AU - Thomas Henzinger
AU - Kupferman, Orna
AU - Majumdar, Ritankar S
ID - 4560
TI - Verifying quantitative properties using bound functions
VL - 3725
ER -
TY - CONF
AB - We present a language for specifying web service interfaces. A web service interface puts three kinds of constraints on the users of the service. First, the interface specifies the methods that can be called by a client, together with types of input and output parameters; these are called signature constraints. Second, the interface may specify propositional constraints on method calls and output values that may oc- cur in a web service conversation; these are called consis- tency constraints. Third, the interface may specify temporal constraints on the ordering of method calls; these are called protocol constraints. The interfaces can be used to check, first, if two or more web services are compatible, and second, if a web service A can be safely substituted for a web ser- vice B. The algorithm for compatibility checking verifies that two or more interfaces fulfill each others’ constraints. The algorithm for substitutivity checking verifies that service A demands fewer and fulfills more constraints than service B.
AU - Beyer, Dirk
AU - Chakrabarti, Arindam
AU - Thomas Henzinger
ID - 4576
TI - Web service interfaces
ER -
TY - CONF
AB - BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how BLAST can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use Ccured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that BLAST can remove many of the run-time checks added by Ccured and provide useful information to the programmer about many of the remaining checks.
AU - Beyer, Dirk
AU - Thomas Henzinger
AU - Jhala, Ranjit
AU - Majumdar, Ritankar S
ID - 4579
TI - Checking memory safety with BLAST
VL - 3442
ER -
TY - CONF
AB - Surveying results from [5] and [6], we motivate and introduce the theory behind formalizing rich interfaces for software and hardware components. Rich interfaces specify the protocol aspects of component interaction. Their formalization, called interface automata, permits a compiler to check the compatibility of component interaction protocols. Interface automata support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, while still maintaining compatibility.
AU - de Alfaro, Luca
AU - Thomas Henzinger
ID - 4624
TI - Interface-based design
VL - 195
ER -
TY - JOUR
AB - Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators ⋄ and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path.
We interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics.
AU - de Alfaro, Luca
AU - Faella, Marco
AU - Thomas Henzinger
AU - Majumdar, Ritankar S
AU - Stoelinga, Mariëlle
ID - 4625
IS - 1
JF - Theoretical Computer Science
TI - Model checking discounted temporal properties
VL - 345
ER -
TY - CONF
AB - We present the first demonstration of Jozsa's "counterfactual computation", using an optical Grover's search algorithm. We put the algorithm in a superposition of 'running' and 'not-running', obtaining information even though the algorithm does not run.
AU - Onur Hosten
AU - Rakher, Matthew T
AU - Barreiro, Julio T
AU - Peters, Nicholas A
AU - Kwiat, Paul G
ID - 575
TI - Counterfactual quantum computation
VL - 1
ER -
TY - JOUR
AB - A current challenge in neuroscience is to bridge the gaps between genes, proteins, neurons, neural circuits, and behavior in a single animal model. The nematode Caenorhabditis elegans has unique features that facilitate this synthesis. Its nervous system includes exactly 302 neurons, and their pattern of synaptic connectivity is known. With only five olfactory neurons, C. elegans can dynamically respond to dozens of attractive and repellant odors. Thermosensory neurons enable the nematode to remember its cultivation temperature and to track narrow isotherms. Polymodal sensory neurons detect a wide range of nociceptive cues and signal robust escape responses. Pairing of sensory stimuli leads to long-lived changes in behavior consistent with associative learning. Worms exhibit social behaviors and complex ultradian rhythms driven by Ca2+ oscillators with clock-like properties. Genetic analysis has identified gene products required for nervous system function and elucidated the molecular and neural bases of behaviors.
AU - de Bono, Mario
AU - Villu Maricq, Andres
ID - 6153
JF - Annual Review of Neuroscience
SN - 0147-006X
TI - Neuronal substrates of complex behaviors in C. elegans
VL - 28
ER -
TY - JOUR
AU - Cheung, Benny H.H.
AU - Cohen, Merav
AU - Rogers, Candida
AU - Albayram, Onder
AU - de Bono, Mario
ID - 6154
IS - 10
JF - Current Biology
SN - 0960-9822
TI - Experience-dependent modulation of C. elegans behavior by ambient oxygen
VL - 15
ER -
TY - GEN
AB - Our understanding of the role played by neurotransmitter receptors in the developing brain has advanced in recent years. The major excitatory and inhibitory neurotransmitters in the brain, glutamate and GABA, activate both ionotropic (ligand-gated ion channels) and metabotropic (G protein-coupled) receptors, and are generally associated with neuronal communication in the mature brain. However, before the emergence of their role in neurotransmission in adulthood, they also act to influence earlier developmental events, some of which occur prior to synapse formation: such as proliferation, migration, differentiation or survival processes during neural development. To fulfill these actions in the constructing of the nervous system, different types of glutamate and GABA receptors need to be expressed both at the right time and at the right place. The identification by molecular cloning of 16 ionotropic glutamate receptor subunits, eight metabotropic glutamate receptor subtypes, 21 ionotropic and two metabotropic GABA receptor subunits, some of which exist in alternatively splice variants, has enriched our appreciation of how molecular diversity leads to functional diversity in the brain. It now appears that many different types of glutamate and GABA receptor subunits have prominent expression in the embryonic and/or postnatal brain, whereas others are mainly present in the adult brain. Although the significance of this differential expression of subunits is not fully understood, it appears that the change in subunit composition is essential for normal development in particular brain regions. This review focuses on emerging information relating to the expression and role of glutamatergic and GABAergic neurotransmitter receptors during prenatal and postnatal development.
AU - Luján, Rafael
AU - Ryuichi Shigemoto
AU - López-Bendito, Guillermina
ID - 2647
IS - 3
T2 - Neuroscience
TI - Glutamate and GABA receptor signalling in the developing brain
VL - 130
ER -
TY - JOUR
AB - Hyperpolarization-activated and cyclic nucleotide-gated (HCN) channels are involved in the control of neuronal excitability and plasticity. In this study, we used immunoblotting and immunohistochemical techniques to reveal the developmental expression and subcellular distribution of the HCN1 subunit in the cerebellar cortex. During postnatal development, the spatio-temporal expression of HCN1 correlated well with the morphological events occurring during the ontogenesis of cerebellar interneurons. Using immunoblotting techniques, HCN1 was weakly detected during the first postnatal week and continued to increase throughout postnatal development, peaking at postnatal day (P)15. At the light-microscopic level, HCN1 immunoreactivity was very weak until P7 whereas from P10-12 to adulthood it was strongly detected in the lower third of the molecular layer and in the Purkinje cell layer. HCN1 was present in axons running through the molecular layer and in the pericellular basket around Purkinje cells at P12, but in the periaxonal plexus (the pinceau) surrounding their initial segment only after P15. Using immunofluorescence, HCN1 colocalized with GAD65 and synaptophysin, demonstrating that the subunit was present in inhibitory axons and axon terminals. At the electron-microscopic level, in adulthood, HCN1 immunoparticles were detected at postsynaptic sites in basket and Purkinje cells but most immunoparticles were found at presynaptic sites in basket cell axons and in terminals. In the axon terminals, the distribution of HCN1 was relatively uniform along the extrasynaptic plasma membrane; this was confirmed using quantitative techniques. The present findings suggest that HCN1 channels may provide a significant route for modulating co-ordinated cerebellar synaptic transmission through basket cells.
AU - Luján, Rafael
AU - Albasanz, José L
AU - Ryuichi Shigemoto
AU - Juíz, José M
ID - 2648
IS - 8
JF - European Journal of Neuroscience
TI - Preferential localization of the hyperpolarization-activated cyclic nucleotide-gated cation channel subunit HCN1 in basket cell terminals of the rat cerebellum
VL - 21
ER -