Cell fate specification during Caenorhabditis elegans male tail development

The cells of the specialized mating structures of the nematode Caenorhabditis elegans adult male tail develop from sex-specific divisions of postembryonic blast cells. One male-specific blast cell, B, is the precursor to all the cells of the copulatory spicules. Both cell interactions and autonomous fate specification mechanisms are utilized in the B lineage to specify fate.

During development the anterior daughter of B, B.a, generates four distinct pairs of cells. Cell ablation experiments indicate that the cells of each pair respond to positional cues provided by other male-specific blast cells. F and U promote anterior fates, Y.p promotes some posterior fates, and the B.a progeny promote posterior fates. The cells within each pair may also interact.

The lin-3/let-23 signalling pathway, identified for its function in C. elegans hermaphrodite vulval induction, mediates the signal from F and U. Reduction-of-function mutations in lin-3 (EGF-like signal), let-23 (receptor), sem-5 (adaptor), let-60 (ras), or lin-45 (raf) disrupt the fates of the anterior cells, and mimic F and U ablation. In addition, ectopically expressed lin-3 disrupts the fates of the posterior cells, and can promote anterior fates even in the absence of F and U.

A genetic screen of over 9000 mutagenized gametes recovered 22 mutations in 20 loci that disrupt fate specification in male tail lineages. Seven of these mutations may represent new genes that play a role in male tail development.

The first division of the B cell is asymmetric. The gene vab-3 is required for specification of B.a fates, and it may represent a factor whose activity is localized to the B.a cell via the gene lin-17. lin-17 acts both at the first division of the B cell and at specific other cell divisions in the lineage.

Design, specification, and synthesis of aircraft electric power systems control logic

Cyber-physical systems integrate computation, networking, and physical processes. Substantial research challenges exist in the design and verification of such large-scale, distributed sensing, ac- tuation, and control systems. Rapidly improving technology and recent advances in control theory, networked systems, and computer science give us the opportunity to drastically improve our approach to integrated flow of information and cooperative behavior. Current systems rely on text-based spec- ifications and manual design. Using new technology advances, we can create easier, more efficient, and cheaper ways of developing these control systems. This thesis will focus on design considera- tions for system topologies, ways to formally and automatically specify requirements, and methods to synthesize reactive control protocols, all within the context of an aircraft electric power system as a representative application area.

This thesis consists of three complementary parts: synthesis, specification, and design. The first section focuses on the synthesis of central and distributed reactive controllers for an aircraft elec- tric power system. This approach incorporates methodologies from computer science and control. The resulting controllers are correct by construction with respect to system requirements, which are formulated using the specification language of linear temporal logic (LTL). The second section addresses how to formally specify requirements and introduces a domain-specific language for electric power systems. A software tool automatically converts high-level requirements into LTL and synthesizes a controller.

The final sections focus on design space exploration. A design methodology is proposed that uses mixed-integer linear programming to obtain candidate topologies, which are then used to synthesize controllers. The discrete-time control logic is then verified in real-time by two methods: hardware and simulation. Finally, the problem of partial observability and dynamic state estimation is ex- plored. Given a set placement of sensors on an electric power system, measurements from these sensors can be used in conjunction with control logic to infer the state of the system.

Formal languages, part theory, and change

A general definition of interpreted formal language is presented. The notion “is a part of" is formally developed and models of the resulting part theory are used as universes of discourse of the formal languages. It is shown that certain Boolean algebras are models of part theory.

With this development, the structure imposed upon the universe of discourse by a formal language is characterized by a group of automorphisms of the model of part theory. If the model of part theory is thought of as a static world, the automorphisms become the changes which take place in the world. Using this formalism, we discuss a notion of abstraction and the concept of definability. A Galois connection between the groups characterizing formal languages and a language-like closure over the groups is determined.

It is shown that a set theory can be developed within models of part theory such that certain strong formal languages can be said to determine their own set theory. This development is such that for a given formal language whose universe of discourse is a model of part theory, a set theory can be imbedded as a submodel of part theory so that the formal language has parts which are sets as its discursive entities.