TY - CONF
AB - Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify the precise boundary between decidability and undecidability of the reachability problem for hybrid automata.
On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves the omega-languages of initialized rectangular automata with bounded nondeterminism.
On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch.
AU - Thomas Henzinger
AU - Kopke, Peter W
AU - Puri, Anuj
AU - Varaiya,P.
ID - 4502
TI - What's decidable about hybrid automata?
ER -
TY - CONF
AB - The analysis, verification, and control of hybrid automata with finite bisimulations can be reduced to finite-state problems. We advocate a time-abstract, phase-based methodology for checking if a given hybrid automaton has a finite bisimulation. First, we factor the automaton into two components, a boolean automaton with a discrete dynamics on the finite state space B m and a euclidean automaton with a continuous dynamics on the infinite state space n . Second, we investigate the phase portrait of the euclidean component. In this fashion, we obtain new decidability results for hybrid systems as well as new, uniform proofs of known decidability results.
AU - Thomas Henzinger
ID - 4518
TI - Hybrid automata with finite bisimulations
VL - 944
ER -
TY - CONF
AB - HyTech is a tool for the automated analysis of embedded systems. This document, designed for the first-time user of HyTech, guides the reader through the underlying system model, and through the input language for describing and analyzing systems. The guide gives several examples of usage, and some hints for gaining maximal computational efficiency from the tool.
The version of HyTech described in this guide was released in August 1995, and is available through anonymous ftp from ftp.cs.cornell.edu in the directory pub/tah/HyTech, and through the World-Wide Web via HyTech's home page http:/www.cs.cornell.edu/Info/People/tah/hytech.html.
AU - Thomas Henzinger
AU - Ho, Pei-Hsin
AU - Wong-Toi, Howard
ID - 4497
TI - A user guide to HyTech
VL - 1019
ER -
TY - CONF
AB - We present algorithms for computing similarity relations of labeled graphs. Similarity relations have applications for the refinement and verification of reactive systems. For finite graphs, we present an O(mn) algorithm for computing the similarity relation of a graph with n vertices and m edges (assuming m⩾n). For effectively presented infinite graphs, we present a symbolic similarity-checking procedure that terminates if a finite similarity relation exists. We show that 2D rectangular automata, which model discrete reactive systems with continuous environments, define effectively presented infinite graphs with finite similarity relations. It follows that the refinement problem and the ∀CTL* model-checking problem are decidable for 2D rectangular automata
AU - Henzinger, Monika
AU - Thomas Henzinger
AU - Kopke, Peter W
ID - 4498
TI - Computing simulations on finite and infinite graphs
ER -
TY - CONF
AB - We describe a new implementation of HYTECH, a symbolic model checker for hybrid systems. Given a parametric description of an embedded system as a collection of communicating automata, HYTECH automatically computes the conditions on the parameters under which the system satisfies its safety and timing requirements. While the original HYTECH prototype was based on the symbolic algebra tool Mathematica, the new implementation is written in C++ and builds on geometric algorithms instead of formula manipulation. The new HYTECH offers a cleaner and more expressive input language, greater portability, superior performance (typically two to three orders of magnitude), and new features such as diagnostic error-trace generation. We illustrate the effectiveness of the new implementation by applying HYTECH to the automatic parametric analysis of the generic railroad crossing benchmark problem and to an active structure control algorithm
AU - Thomas Henzinger
AU - Ho, Pei-Hsin
AU - Wong-Toi, Howard
ID - 4499
TI - HyTech: The next generation
ER -
TY - CONF
AB - We investigate the expressive power of timing restrictions on labeled transition systems. In particular, we show how constraints on clock variables together with a uniform liveness condition—the divergence of time—can express Büchi, Muller, Streett, Rabin, and weak and strong fairness conditions on a given labeled transition system. We then consider the effect, on both timed and time-abstract expressiveness, of varying the following parameters: time domain (discrete or dense), number of clocks, number of states, and size of constants used in timing restrictions.
AU - Thomas Henzinger
AU - Kopke, Peter W
AU - Wong-Toi, Howard
ID - 4500
TI - The expressive power of clocks
VL - 944
ER -
TY - JOUR
AB - The tra-1 gene is the terminal global selector of somatic sex in Caenorhabditis elegans: High tra-1 activity elicits female somatic development while low tra-1 activity elicits male development. Previous genetic studies defined a cascade of negatively interacting genes that regulates tra-1 activity in response to the primary sex-determining signal. Here, we investigate the last step in this regulatory cascade, by studying rare gain-of-function (gf) mutations of tra-1 that direct female somatic development irrespective of the upstream sex-determining signal. These mutations appear to abolish negative regulation of tra-1 in male tissues. We identify the lesions associated with 29 of these mutations and find that all affect a short stretch of amino acid residues present in both protein products of the tra-1 gene. Twenty-six alleles are associated with single nonconservative amino acid substitutions. Two alleles affect tra-1 RNA splicing and generate messages that omit part or all of the exon encoding this short stretch. These results suggest that sexual regulation of tra-1 is achieved post-translationally, by an inhibitory protein-protein interaction. The amino acid stretch altered by the tra-1(gf) mutations may define a site of interaction for negative regulators of tra-1. The stretch includes a potential phosphorylation site for glycogen synthase kinase 3 and may be conserved in the human gene GLI3, a homolog of tra-1 identified previously.
AU - de Bono, Mario
AU - Zarkower, D.
AU - Hodgkin, J.
ID - 6162
IS - 2
JF - Genes and Development
SN - 08909369
TI - Dominant feminizing mutations implicate protein-protein interactions as the main mode of regulation of the nematode sex-determining gene tra-1
VL - 9
ER -