@inproceedings{4525,
abstract = {We present a new high-level programming language, called xGiotto, for programming applications with hard real-time constraints. Like its predecessor, xGiotto is based on the LET (logical execution time) assumption: the programmer specifies when the outputs of a task become available, and the compiler checks if the specification can be implemented on a given platform. However, while the predecessor language xGiotto was purely time-triggered, xGiotto accommodates also asynchronous events. Indeed, through a mechanism called event scoping, events are the main structuring principle of the new language. The xGiotto compiler and run-time system implement event scoping through a tree-based event filter. The compiler also checks programs for determinism (absence of race conditions).},
author = {Ghosal, Arkadeb and Thomas Henzinger and Kirsch, Christoph M and Sanvido, Marco A},
pages = {167 -- 170},
publisher = {Springer},
title = {{Event-driven programming with logical execution times}},
doi = {10.1007/978-3-540-24743-2_24},
volume = {2993},
year = {2004},
}
@inproceedings{4555,
abstract = {Strategies in repeated games can be classified as to whether or not they use memory and/or randomization. We consider Markov decision processes and 2-player graph games, both of the deterministic and probabilistic varieties. We characterize when memory and/or randomization are required for winning with respect to various classes of w-regular objectives, noting particularly when the use of memory can be traded for the use of randomization. In particular, we show that Markov decision processes allow randomized memoryless optimal strategies for all M?ller objectives. Furthermore, we show that 2-player probabilistic graph games allow randomized memoryless strategies for winning with probability 1 those M?ller objectives which are upward-closed. Upward-closure means that if a set α of infinitely repeating vertices is winning, then all supersets of α are also winning.},
author = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger},
pages = {206 -- 217},
publisher = {IEEE},
title = {{Trading memory for randomness}},
doi = {10.1109/QEST.2004.10051},
year = {2004},
}
@article{4556,
abstract = {We study the problem of determining stack boundedness and the exact maximum stack size for three classes of interrupt-driven programs. Interrupt-driven programs are used in many real-time applications that require responsive interrupt handling. In order to ensure responsiveness, programmers often enable interrupt processing in the body of lower-priority interrupt handlers. In such programs a programming error can allow interrupt handlers to be interrupted in a cyclic fashion to lead to an unbounded stack, causing the system to crash. For a restricted class of interrupt-driven programs, we show that there is a polynomial-time procedure to check stack boundedness, while determining the exact maximum stack size is PSPACE-complete. For a larger class of programs, the two problems are both PSPACE-complete, and for the largest class of programs we consider, the two problems are PSPACE-hard and can be solved in exponential time. While the complexities are high, our algorithms are exponential only in the number of handlers, and polynomial in the size of the program.},
author = {Krishnendu Chatterjee and Ma, Di and Majumdar, Ritankar S and Zhao, Tian and Thomas Henzinger and Palsberg, Jens},
journal = {Information and Computation},
number = {2},
pages = {144 -- 174},
publisher = {Elsevier},
title = {{Stack size analysis for interrupt-driven programs}},
doi = {10.1016/j.ic.2004.06.001},
volume = {194},
year = {2004},
}
@inproceedings{4558,
abstract = {We study perfect-information stochastic parity games. These are two-player nonterminating games which are played on a graph with turn-based probabilistic transitions. A play results in an infinite path and the conflicting goals of the two players are ω-regular path properties, formalized as parity winning conditions. The qualitative solution of such a game amounts to computing the set of vertices from which a player has a strategy to win with probability 1 (or with positive probability). The quantitative solution amounts to computing the value of the game in every vertex, i.e., the highest probability with which a player can guarantee satisfaction of his own objective in a play that starts from the vertex.For the important special case of one-player stochastic parity games (parity Markov decision processes) we give polynomial-time algorithms both for the qualitative and the quantitative solution. The running time of the qualitative solution is O(d · m3/2) for graphs with m edges and d priorities. The quantitative solution is based on a linear-programming formulation.For the two-player case, we establish the existence of optimal pure memoryless strategies. This has several important ramifications. First, it implies that the values of the games are rational. This is in contrast to the concurrent stochastic parity games of de Alfaro et al.; there, values are in general algebraic numbers, optimal strategies do not exist, and ε-optimal strategies have to be mixed and with infinite memory. Second, the existence of optimal pure memoryless strategies together with the polynomial-time solution forone-player case implies that the quantitative two-player stochastic parity game problem is in NP ∩ co-NP. This generalizes a result of Condon for stochastic games with reachability objectives. It also constitutes an exponential improvement over the best previous algorithm, which is based on a doubly exponential procedure of de Alfaro and Majumdar for concurrent stochastic parity games and provides only ε-approximations of the values.},
author = {Krishnendu Chatterjee and Jurdziński, Marcin and Thomas Henzinger},
pages = {121 -- 130},
publisher = {SIAM},
title = {{Quantitative stochastic parity games}},
year = {2004},
}
@inproceedings{4577,
abstract = {While model checking has been successful in uncovering subtle bugs in code, its adoption in software engineering practice has been hampered by the absence of a simple interface to the programmer in an integrated development environment. We describe an integration of the software model checker BLAST into the Eclipse development environment. We provide a verification interface for practical solutions for some typical program analysis problems - assertion checking, reachability analysis, dead code analysis, and test generation - directly on the source code. The analysis is completely automatic, and assumes no knowledge of model checking or formal notation. Moreover, the interface supports incremental program verification to support incremental design and evolution of code.},
author = {Beyer, Dirk and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {251 -- 255},
publisher = {IEEE},
title = {{An eclipse plug-in for model checking}},
doi = {10.1109/WPC.2004.1311069 },
year = {2004},
}
@inproceedings{4578,
abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. Blast is based on lazy predicate abstraction driven by interpolation-based predicate discovery. In this paper, we present the Blast specification language. The language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications. },
author = {Beyer, Dirk and Chlipala, Adam J and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {2 -- 18},
publisher = {Springer},
title = {{The BLAST query language for software verification}},
doi = {10.1007/978-3-540-27864-1_2},
volume = {3148},
year = {2004},
}
@inproceedings{4581,
abstract = {We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test vector generation is fully automatic (no user intervention) and exact (no false positives).},
author = {Beyer, Dirk and Chlipala, Adam J and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {326 -- 335},
publisher = {IEEE},
title = {{Generating tests from counterexamples}},
doi = {10.1109/ICSE.2004.1317455},
year = {2004},
}
@inproceedings{4629,
abstract = {Temporal logic is two-valued: a property is 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.},
author = {de Alfaro, Luca and Faella, Marco and Thomas Henzinger and Majumdar, Ritankar S and Stoelinga, Mariëlle},
pages = {77 -- 92},
publisher = {Springer},
title = {{Model checking discounted temporal properties}},
doi = {10.1007/978-3-540-24730-2_6},
volume = {2988},
year = {2004},
}
@article{6155,
abstract = {The genome of the nematode Caenorhabditis elegans encodes seven soluble guanylate cyclases (sGCs) [1]. In mammals, sGCs function as α/β heterodimers activated by gaseous ligands binding to a haem prosthetic group 2, 3. The principal activator is nitric oxide, which acts through sGCs to regulate diverse cellular events. In C. elegans the function of sGCs is mysterious: the worm genome does not appear to encode nitric oxide synthase, and all C. elegans sGC subunits are more closely related to mammalian β than α subunits [1]. Here, we show that two of the seven C. elegans sGCs, GCY-35 and GCY-36, promote aggregation behavior. gcy-35 and gcy-36 are expressed in a small number of neurons. These include the body cavity neurons AQR, PQR, and URX, which are directly exposed to the blood equivalent of C. elegans and regulate aggregation behavior [4]. We show that GCY-35 and GCY-36 act as α-like and β-like sGC subunits and that their function in the URX sensory neurons is sufficient for strong nematode aggregation. Neither GCY-35 nor GCY-36 is absolutely required for C. elegans to aggregate. Instead, these molecules may transduce one of several pathways that induce C. elegans to aggregate or may modulate aggregation by responding to cues in C. elegans body fluid.},
author = {Cheung, Benny H.H and Arellano-Carbajal, Fausto and Rybicki, Irene and de Bono, Mario},
issn = {0960-9822},
journal = {Current Biology},
number = {12},
pages = {1105--1111},
publisher = {Elsevier},
title = {{Soluble guanylate cyclases act in neurons exposed to the body fluid to promote C. elegans aggregation behavior}},
doi = {10.1016/j.cub.2004.06.027},
volume = {14},
year = {2004},
}
@misc{2636,
author = {Momiyama, Akiko and Ryuichi Shigemoto},
booktitle = {Tanpakushitsu kakusan koso Protein nucleic acid enzyme},
number = {3 Suppl},
pages = {287 -- 294},
publisher = {Kyoritsu Shuppan},
title = {{Function and distribution of glutamate receptors in the central synapses}},
volume = {49},
year = {2004},
}