Existing linearized section location methods for distribution networks are only applicable to single faults. In response, this paper proposes a linear integer programming method for section location in distribution ne...
详细信息
ISBN:
(数字)9798331532765
ISBN:
(纸本)9798331532772
Existing linearized section location methods for distribution networks are only applicable to single faults. In response, this paper proposes a linear integer programming method for section location in distribution networks that is suitable for multiple faults. Firstly, based on fault-tolerant mechanism analysis, a switch function tailored for multiple faults is developed. Secondly, the method incorporates phasor measurement unit (PMU) information fault information into the section location process, constructing a logical model for section location in distribution networks. Finally, by applying three transformation principles between logical and algebraic relationships, the logical model is converted into a linear integer programming model, which is solved using MATLAB+CPLEX. Case studies demonstrate that the proposed linear integer programming method for section location in distribution networks achieves fast location speed and robust fault tolerance, making it suitable for both single and multiple faults.
Weighted Markov decision processes (MDPs) have long been used to model quantitative aspects of systems in the presence of uncertainty. However, much of the literature on such MDPs takes a monolithic approach, by model...
详细信息
Weighted Markov decision processes (MDPs) have long been used to model quantitative aspects of systems in the presence of uncertainty. However, much of the literature on such MDPs takes a monolithic approach, by modelling a system as a particular MDP;properties of the system are then inferred by analysis of that particular MDP. In contrast in this paper we develop compositional methods for reasoning about weighted MDPs, as a possible basis for compositional reasoning about their quantitative behaviour. In particular we approach these systems from a process algebraic point of view. For these we define a coinductive simulation-based behavioural preorder which is compositional in the sense that it is preserved by structural operators for constructing weighted MDPs from components. For finitary convergent processes, which are finite-state and finitely branching systems without divergence, we provide two characterisations of the behavioural preorder. the first uses a novel quantitative probabilistic logic, while the second is in terms of a novel form of testing, in which benefits are accrued during the execution of tests. (C) 2013 Elsevier B.V. All rights reserved.
Weighted Markov decision processes (MDPs) have long been used to model quantitative aspects of systems in the presence of uncertainty. However, much of the literature on such MDPs takes a monolithic approach, by model...
详细信息
Weighted Markov decision processes (MDPs) have long been used to model quantitative aspects of systems in the presence of uncertainty. However, much of the literature on such MDPs takes a monolithic approach, by modelling a system as a particular MDP;properties of the system are then inferred by analysis of that particular MDP. In contrast in this paper we develop compositional methods for reasoning about weighted MDPs, as a possible basis for compositional reasoning about their quantitative behaviour. In particular we approach these systems from a process algebraic point of view. For these we define a coinductive simulation-based behavioural preorder which is compositional in the sense that it is preserved by structural operators for constructing weighted MDPs from components. For finitary convergent processes, which are finite-state and finitely branching systems without divergence, we provide two characterisations of the behavioural preorder. the first uses a novel quantitative probabilistic logic, while the second is in terms of a novel form of testing, in which benefits are accrued during the execution of tests. (C) 2013 Elsevier B.V. All rights reserved.
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is only evaluated if the first argument does not suffice to determine the value of the expression. In programmin...
详细信息
this paper contributes to a line of research which aims to combine numerical information withlogical inference in order to find the most likely states of a biological system under various (actual or hypothetical) con...
详细信息
Finite maps or finite relations between infinite sets do not even form a category, since the necessary identities are not finite. We show relation-algebraic extensions of semigroupoids where the operations that would ...
详细信息
Finite maps or finite relations between infinite sets do not even form a category, since the necessary identities are not finite. We show relation-algebraic extensions of semigroupoids where the operations that would produce infinite results have been replaced with variants that preserve finiteness, but still satisfy useful algebraic laws. the resulting theories allow calculational reasoning in the relation-algebraic style with only minor sacrifices;our emphasis on generality even provides some concepts in theories where they had not been available before. the semigroupoid theories presented in this paper also can directly guide library interface design and thus be used for principled relation-algebraicprogramming;an example implementation in Haskell allows manipulating finite binary relations as data in a point-free relation-algebraicprogramming style that integrates naturally withthe current Haskell collection types. this approach enables seamless integration of relation-algebraic formulations to provide elegant solutions of problems that, with different data organisation, are awkward to tackle. (C) 2007 Elsevier Inc. All rights reserved.
We present an algebraic embedding of Neighbourhood logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our fra...
详细信息
We present an algebraic embedding of Neighbourhood logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our framework, and Galois connections produce properties for free. A further simplification is achieved, since the semiring methods used are easy and fairly standard. Moreover, this embedding allows us to reuse knowledge from Neighbourhood logic in other areas of Computer Science. Since in its original axiomatisation the logic cannot handle intervals of infinite length and therefore not fully model and specify reactive and hybrid systems, using lazy semirings we introduce an extension of NL to intervals of finite and infinite length. Furthermore, we discuss connections between the (extended) logic and other application areas, like Allen's thirteen relations between intervals, the branching time temporal logic CTL* and hybrid systems. (C) 2007 Elsevier Inc. All rights reserved.
We explore the power of relational semantics and equational reasoning in the style of Kleene algebra for analyzing programs with mutable, statically scoped local variables. We provide (i) a fully compositional relatio...
详细信息
We explore the power of relational semantics and equational reasoning in the style of Kleene algebra for analyzing programs with mutable, statically scoped local variables. We provide (i) a fully compositional relational semantics for a first-order programming language with constructs for local variable declaration and destructive update;and (ii) an equational proof system based on Kleene algebra with tests for proving the equivalence of programs in this language. We show that the proof system is sound and complete relative to the underlying equational theory without local variables. We illustrate the use of the system with several examples. (C) 2007 Elsevier Inc. All rights reserved.
the proceedings contain 14 papers. the topics discussed include: reflecting linear arithmetic: from dense linear orders to Presburger arithmetic;lightweight verification with dependent types;trends and challenges in s...
the proceedings contain 14 papers. the topics discussed include: reflecting linear arithmetic: from dense linear orders to Presburger arithmetic;lightweight verification with dependent types;trends and challenges in satisfiability modulo theories;formal device and programming model for a serial interface;combinations of theories and the Bernays-Schönfinkel-ramsey class;a history-based verification of distributed applications;symbolic fault injection;a termination checker for Isabelle Hoare logic;the heterogeneous tool set;fully verified JAVA CARD API reference implementation;automated formal verification of PLC programs written in IL;and combining deduction and algebraic constraints for hybrid system analysis.
We present a Haskell interface for manipulating finite binary relations as data in a point-free relation-algebraicprogramming style that integrates naturally withthe current Haskell collection types. this approach e...
详细信息
暂无评论