A combined feedback linearization (FBL) and sliding mode control (SMC) method is proposed for reusable launch vehicle (RLV) reentry flight control system designing. the feedback linearization is based on the full rota...
详细信息
ISBN:
(纸本)9781467318723;9781467318716
A combined feedback linearization (FBL) and sliding mode control (SMC) method is proposed for reusable launch vehicle (RLV) reentry flight control system designing. the feedback linearization is based on the full rotational equations of motion rather than on a conventional model derived from time-scale separation. the control system design is split into two separate tasks, control law and control allocation. First, the control law is designed by a sliding mode control method. the chattering brought by the SMC is eliminated efficiently by choosing a suitable reaching law and a continuous sign function. then, a bridging function based on dynamic pressure is used to blend continuous control effectors and pulsed thrusters to generate moments commanded by the sliding control law, that is the control allocation problem. An optimal control allocation method based on standard linear programming is used to distribute control command to each aerosurface accounting for position and rate constraints. And a 0-1 linear programming technique is used for reaction control thrusters control allocation. When coupled with fault detection and isolation logic, the control effectors can be reconfigured to minimize the impact of control effector failures or damage. Analysis and nonlinear simulation results show that the composite controller achieves the requirements of performance.
the proceedings contain 14 papers. the special focus in this conference is on Rewriting logic and its Applications. the topics include: Proving ground confluence of equational specifications modulo axioms;uniform stro...
ISBN:
(纸本)9783319998398
the proceedings contain 14 papers. the special focus in this conference is on Rewriting logic and its Applications. the topics include: Proving ground confluence of equational specifications modulo axioms;uniform strong normalization for multi-discipline calculi;real-time rewriting logic semantics for spatial concurrent constraint programming;Approximating any logic program by a CS-program;multi-paradigm programming in maude;MUnit: A unit framework for maude;parameterized programming for compositional system specification;Symbolic specification and verification of data-aware BPMN processes using rewriting modulo SMT;associative unification and symbolic reasoning modulo associativity in maude;proving structural properties of sequent systems in rewriting logic;formal modeling and analysis of the walter transactional data store;extending timbuk to verify functional programs.
We investigate a λ calculus with positive inductive and coinductive types, which we call λ μ,ν, using logical relations. We show that parametric theories have the strong categorical properties, that the representa...
详细信息
We present a pair of reasoning principles, definition and proof by rigid induction, which can be seen as proper generalizations of lazy-datatype induction to monadic effects other than partiality. We further show how ...
详细信息
ISBN:
(纸本)9781595938152
We present a pair of reasoning principles, definition and proof by rigid induction, which can be seen as proper generalizations of lazy-datatype induction to monadic effects other than partiality. We further show how these principles can be integrated into logical-relations arguments, and obtain as a particular instance a general and principled proof that the success-stream and failure-continuation models of backtracking are equivalent. As another application, we present a monadic model of general search trees, not necessarily traversed depth-first. the results are applicable to both lazy and eager languages, and we emphasize this by presenting most examples in both Haskell and SML.
In previous work we presented 1BC, a first-order Bayesian classifier. 1BC applies dynamic propositionalisation, in the sense that attributes representing first-order features are generated exhaustively within a given ...
详细信息
ISBN:
(纸本)9783540005674
In previous work we presented 1BC, a first-order Bayesian classifier. 1BC applies dynamic propositionalisation, in the sense that attributes representing first-order features are generated exhaustively within a given feature bias, but during learning rather than as a pre-processing step. In this paper we describe 1BC2, which learns from structured data by fitting various parametric distributions over sets and lists to the data. We evaluate the feasibility of the approach by various experiments.
the proceedings contain 12 papers. the special focus in this conference is Trends in Functional programming. the topics include: Constraint-free type error slicing;subtyping by folding an inductive relation into a coi...
ISBN:
(纸本)9783642320361
the proceedings contain 12 papers. the special focus in this conference is Trends in Functional programming. the topics include: Constraint-free type error slicing;subtyping by folding an inductive relation into a coinductive one;a library for generating compilers;towards modular compilers for effects;a distributed computing library for objective caml;forming parallel Haskell programs using novel refactoring techniques;functional high performance financial it;thread-safe priority queues in Haskell based on skiplists;correctness proof and efficient implementation;from structural recursion to generative and accumulative recursion;a graphical language and tool for defining itask workflows;applicative shortcut fusion.
We pinpoint the limitations of existing approaches to the treatment of strong and default negation in answer-set program updates and formulate the early recovery principle that plausibly constrains their interaction.
ISBN:
(纸本)9783642405648
We pinpoint the limitations of existing approaches to the treatment of strong and default negation in answer-set program updates and formulate the early recovery principle that plausibly constrains their interaction.
In this paper we introduce a logicprogramming based framework which allows the representation of conditional non-monotonic temporal beliefs and goals in a declarative way. We endow it with stable model like semantics...
详细信息
ISBN:
(纸本)9783642405648
In this paper we introduce a logicprogramming based framework which allows the representation of conditional non-monotonic temporal beliefs and goals in a declarative way. We endow it with stable model like semantics that allows us to deal with conflicting goals and generate possible alternatives. We show that our framework satisfies some usual properties on goals and that it allows imposing alternative constraints on the interaction between beliefs and goals. We prove the decidability of the usual reasoning tasks and show how they can be implemented using an ASP solver and an LTL reasoner in a modular way, thus taking advantage of existing LTL reasoners and ASP solvers.
the impossibility of semantically complete deductive calculi for logics for imperative programs has led to the study of two alternative approaches to completeness: "local" semantic completeness on the one ha...
详细信息
ISBN:
(数字)9783642005961
ISBN:
(纸本)9783642005954
the impossibility of semantically complete deductive calculi for logics for imperative programs has led to the study of two alternative approaches to completeness: "local" semantic completeness on the one hand (Cook's relative completeness, Harel's Arithmetical completeness), and completeness with respect to other forms of reasoning about programs. on the other. However, local semantic completeness is problematic on several counts, whereas proof theoretic completeness results often involve ad hoc ingredients. Such as formal theories for the natural numbers. the notion of inductive completeness, introduced in [18]. provides a generic proof theoretic framework which dispenses with extraneous ingredients. and yields local semantic completeness as a corollary. Here we prove that (first-order) Dynamic logic tor regular programs (DL) is inductively complete: a DL-formula phi is provable in (the first-order variant of) Pratt-Segerberg deductive calculus DL iff phi, is provable in first-order logic from the inductivetheory for program semantics. the method can be adapted to yield the schematic relative completeness of DL: if S is in expressive Structure, then every formula true in S is provable from the axiom-schemas that are valid in S. Harel's Completeness theorem falls out then as a special case.
暂无评论