A contribuição da Legimática para a qualidade formal do texto legislativo

O objetivo deste trabalho é identificar como as ferramentas propostas pela Legimática podem contribuir para diminuir as deficiências dos textos legislativos apontadas pela Legística. A preocupação com o processo de criação e com a qualidade do texto legislativo por ele produzido é o foco principal da Legística Formal. Esta atividade encontra amparo nas ferramentas propostas pela Legimática que auxiliam a elaboração de normas legais por meio de processadores eletrônicos de textos concebidos especificamente para este propósito, ou seja, redação de leis. Tais ferramentas garantem o emprego de regras formalmente estabelecidas para um texto legal, e de forma mais abrangente, facilitam a clareza, o rigor e a uniformidade da linguagem legislativa do documento produzido. A realização de pesquisas qualitativa e bibliográfica permitiu propor a criação de um software que auxilie no processo de elaboração normativa dos órgãos legislativos federais brasileiros baseando-se em considerações de especialistas, análise de ferramentas semelhantes e referências na literatura.

Las iglesias prefeudales en Alava: cronotipología y articulación espacial

[ES]El artículo constituye un avance de un proyecto de investigación en curso sobre las iglesias alavesas anteriores a los siglos XII-XIII,invisibles hasta la fecha a una metodología tradicionalmente de base analógica y formal. Se efectúa una nueva propuesta de análisis experimentada ya en la catedral de Santa María de Vitoria-Gasteiz y que se articula de la manera siguiente: 1. Lettura veloce de los principales momentos constructivos de los templos seleccionados con el objeto de individualizar estratigráficamente la fase o fases anteriores al periodo «románico». 2. Individualización y registro de las variables técnicas y formales más representativas de esta primera fase constructiva en cada una de las iglesias objeto de estudio. 3. Identificación numérica de las variables seleccionadas. 4. Creación de una tabla analítica que recoja la presencia o ausencia de estas variables en cada uno de los edificios a estudiar. 5. Agrupamiento de los edificios que comparten variables entre sí. 6. Transformación de las asociaciones tecnotipológicas en tablas cronotipológicas, es decir, en indicadores cronológicos. Resultado de todo ello ha sido la individualización de seis grupos de iglesias que se articulan diacrónicamente entre los siglos IX y XII. A modo de conclusión se avanzan, finalmente, algunas consideraciones interpretativas sobre la naturaleza de estos templos de época prefeudal.

The BACOMA cod-end. History and recent developments in BACOMA cod-end regulations and a proposal for abetter specification of the BACOMA cod-end for Baltic Sea cod fishery

To improve the cod stocks in the Baltic Sea, a number of regulations have recently been established by the International Baltic Sea Fisheries Commission (IBSFC) and the European Commission. According to these, fishermen are obliged to use nets with escape windows (BACOMA nets) with a mesh size of the escape window of 120 mm until end of September 2003. These nets however, retain only fish much larger than the legal minimum landing size would al-low. Due to the present stock structure only few of such large fish are however existent. As a consequence fishermen use a legal alternative net. This is a conventional trawl with a cod-end of 130 mm diamond-shaped meshes (IBSFC-rules of 1st April 2002), to be increased to 140 mm on 1st September 2003, according to the mentioned IBSFC-rule. Due legal alterations of the net by the fishermen (e.g. use of extra stiff net material) these nets have acquired extremely low selective properties, i. e. they catch very small fish and produce great amounts of discards. Due to the increase of the minimum landing size from 35 to 38 cm for cod in the Baltic, the amount of discards has even increased since the beginning of 2003. Experiments have now been carried out with the BACOMAnet on German and Swedish commercial and research vessels since arguments were brought forward that the BACOMA net was not yet sufficiently tested on commercial vessels. The results of all experiments conducted so far, are compiled and evaluated here. As a result of the Swedish, Danish and German initiative and research the European Commission reacted upon this in June 2003 and rejected the increase of the diamond-meshed non-BACOMA net from 130 mm to 140mm in September 2003. To protect the cod stocks in the Baltic Sea more effectively the use of traditional diamond meshed cod-ends with-out escape window are prohibited in community waters without derogation, becoming effective 1st of September 2003. To enable more effective and simplified control of the bottom trawl fishery in the Baltic Sea the principle of a ”One-Net-Rule“ is enforced. This is going to be the BACOMA net, with the meshes of the escape window being 110 mm for the time being. The description of the BACOMA net as given in the IBSFC-rules no.10 (revision of the 28th session, Berlin 2002) concentrates on the cod-end and the escape window but only to a less extent on the design and mesh-composition of the remaining parts of the net, such as belly and funnel and many details. Thus, the present description is not complete and leaves, according to fishermen, ample opportunity for manipulation. An initiative has been started in Germany with joint effort from scientists and the fishery to better describe the entire net and to produce a proposal for a more comprehensive description, leaving less space for manipulation. A proposal in this direction is given here and shall be seen as a starting point for a discussion and development towards an internationally uniform net, which is agreed amongst the fishery, scientists and politicians. The Baltic Sea fishery is invited to comment on this proposal, and recommendations for further improvement and specifications are welcomed. Once the design is agreed by the Baltic Fishermen Association, it shall be proposed to the IBSFC and European Commission via the Baltic Fishermen Association.

La gestión de las actividades musicales del G-9 en contextos de educación fornal y no formal

479 p.

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.

Control of dynamical systems with temporal logic specifications

This thesis is motivated by safety-critical applications involving autonomous air, ground, and space vehicles carrying out complex tasks in uncertain and adversarial environments. We use temporal logic as a language to formally specify complex tasks and system properties. Temporal logic specifications generalize the classical notions of stability and reachability that are studied in the control and hybrid systems communities. Given a system model and a formal task specification, the goal is to automatically synthesize a control policy for the system that ensures that the system satisfies the specification. This thesis presents novel control policy synthesis algorithms for optimal and robust control of dynamical systems with temporal logic specifications. Furthermore, it introduces algorithms that are efficient and extend to high-dimensional dynamical systems.

The first contribution of this thesis is the generalization of a classical linear temporal logic (LTL) control synthesis approach to optimal and robust control. We show how we can extend automata-based synthesis techniques for discrete abstractions of dynamical systems to create optimal and robust controllers that are guaranteed to satisfy an LTL specification. Such optimal and robust controllers can be computed at little extra computational cost compared to computing a feasible controller.

The second contribution of this thesis addresses the scalability of control synthesis with LTL specifications. A major limitation of the standard automaton-based approach for control with LTL specifications is that the automaton might be doubly-exponential in the size of the LTL specification. We introduce a fragment of LTL for which one can compute feasible control policies in time polynomial in the size of the system and specification. Additionally, we show how to compute optimal control policies for a variety of cost functions, and identify interesting cases when this can be done in polynomial time. These techniques are particularly relevant for online control, as one can guarantee that a feasible solution can be found quickly, and then iteratively improve on the quality as time permits.

The final contribution of this thesis is a set of algorithms for computing feasible trajectories for high-dimensional, nonlinear systems with LTL specifications. These algorithms avoid a potentially computationally-expensive process of computing a discrete abstraction, and instead compute directly on the system's continuous state space. The first method uses an automaton representing the specification to directly encode a series of constrained-reachability subproblems, which can be solved in a modular fashion by using standard techniques. The second method encodes an LTL formula as mixed-integer linear programming constraints on the dynamical system. We demonstrate these approaches with numerical experiments on temporal logic motion planning problems with high-dimensional (10+ states) continuous systems.

Formal methods for control synthesis in partially observed environments : application to autonomous robotic manipulation

Modern robots are increasingly expected to function in uncertain and dynamically challenging environments, often in proximity with humans. In addition, wide scale adoption of robots requires on-the-fly adaptability of software for diverse application. These requirements strongly suggest the need to adopt formal representations of high level goals and safety specifications, especially as temporal logic formulas. This approach allows for the use of formal verification techniques for controller synthesis that can give guarantees for safety and performance. Robots operating in unstructured environments also face limited sensing capability. Correctly inferring a robot's progress toward high level goal can be challenging.

This thesis develops new algorithms for synthesizing discrete controllers in partially known environments under specifications represented as linear temporal logic (LTL) formulas. It is inspired by recent developments in finite abstraction techniques for hybrid systems and motion planning problems. The robot and its environment is assumed to have a finite abstraction as a Partially Observable Markov Decision Process (POMDP), which is a powerful model class capable of representing a wide variety of problems. However, synthesizing controllers that satisfy LTL goals over POMDPs is a challenging problem which has received only limited attention.

This thesis proposes tractable, approximate algorithms for the control synthesis problem using Finite State Controllers (FSCs). The use of FSCs to control finite POMDPs allows for the closed system to be analyzed as finite global Markov chain. The thesis explicitly shows how transient and steady state behavior of the global Markov chains can be related to two different criteria with respect to satisfaction of LTL formulas. First, the maximization of the probability of LTL satisfaction is related to an optimization problem over a parametrization of the FSC. Analytic computation of gradients are derived which allows the use of first order optimization techniques.

The second criterion encourages rapid and frequent visits to a restricted set of states over infinite executions. It is formulated as a constrained optimization problem with a discounted long term reward objective by the novel utilization of a fundamental equation for Markov chains - the Poisson equation. A new constrained policy iteration technique is proposed to solve the resulting dynamic program, which also provides a way to escape local maxima.

The algorithms proposed in the thesis are applied to the task planning and execution challenges faced during the DARPA Autonomous Robotic Manipulation - Software challenge.