arXiv subjects

Ufuk Topcu

Publications and source records attributed to Ufuk Topcu.

349 records · Page 20Linked to original sources

arXiv2014

Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems

We consider temporal logic verification of (possibly nonlinear) dynamical systems evolving over continuous state spaces. Our approach combines automata-based verification and the use of so-called barrier certificates. Automata-based verification allows the decomposition the verification task into a finite collection of simpler constraints over the continuous state space. The satisfaction of these constraints in turn can be (potentially conservatively) proved by appropriately constructed barrier certificates. As a result, our approach, together with optimization-based search for barrier certificates, allows computational verification of dynamical systems against temporal logic properties while avoiding explicit abstractions of the dynamics as commonly done in literature.

cs.FL↗

arXiv2013

Design and Stability of Load-Side Primary Frequency Control in Power Systems

We present a systematic method to design ubiquitous continuous fast-acting distributed load control for primary frequency regulation in power networks, by formulating an optimal load control (OLC) problem where the objective is to minimize the aggregate cost of tracking an operating point subject to power balance over the network. We prove that the swing dynamics and the branch power flows, coupled with frequency-based load control, serve as a distributed primal-dual algorithm to solve OLC. We establish the global asymptotic stability of a multimachine network under such type of load-side primary frequency control. These results imply that the local frequency deviations at each bus convey exactly the right information about the global power imbalance for the loads to make individual decisions that turn out to be globally optimal. Simulations confirm that the proposed algorithm can rebalance power and resynchronize bus frequencies after a disturbance with significantly improved transient performance.

eess.SY↗

arXiv2013

Exact Convex Relaxation of Optimal Power Flow in Radial Networks

The optimal power flow (OPF) problem determines power generation/demand that minimize a certain objective such as generation cost or power loss. It is nonconvex. We prove that, for radial networks, after shrinking its feasible set slightly, the global optimum of OPF can be recovered via a second-order cone programming (SOCP) relaxation under a condition that can be checked a priori. The condition holds for the IEEE 13-, 34-, 37-, 123-bus networks and two real-world networks, and has a physical interpretation.

math.OC↗

arXiv2013

Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications

The reactive synthesis problem is to find a finite-state controller that satisfies a given temporal-logic specification regardless of how its environment behaves. Developing a formal specification is a challenging and tedious task and initial specifications are often unrealizable. In many cases, the source of unrealizability is the lack of adequate assumptions on the environment of the system. In this paper, we consider the problem of automatically correcting an unrealizable specification given in the generalized reactivity (1) fragment of linear temporal logic by adding assumptions on the environment. When a temporal-logic specification is unrealizable, the synthesis algorithm computes a counter-strategy as a witness. Our algorithm then analyzes this counter-strategy and synthesizes a set of candidate environment assumptions that can be used to remove the counter-strategy from the environment's possible behaviors. We demonstrate the applicability of our approach with several case studies.

cs.LO↗

arXiv2013

Exact Convex Relaxation of Optimal Power Flow in Tree Networks

The optimal power flow (OPF) problem seeks to control power generation/demand to optimize certain objectives such as minimizing the generation cost or power loss in the network. It is becoming increasingly important for distribution networks, which are tree networks, due to the emergence of distributed generation and controllable loads. In this paper, we study the OPF problem in tree networks. The OPF problem is nonconvex. We prove that after a "small" modification to the OPF problem, its global optimum can be recovered via a second-order cone programming (SOCP) relaxation, under a "mild" condition that can be checked apriori. Empirical studies justify that the modification to OPF is "small" and that the "mild" condition holds for the IEEE 13-bus distribution network and two real-world networks with high penetration of distributed generation.

math.OC↗

arXiv2012

Synthesis of Reactive Protocols for Vehicle-to-Vehicle Communication

We present a synthesis method for communication protocols for active safety applications that satisfy certain formal specifications on quality of service requirements. The protocols are developed to provide reliable communication services for automobile active safety applications. The synthesis method transforms a specification into a distributed implementation of senders and receivers that together satisfy the quality of service requirements by transmitting messages over an unreliable medium. We develop a specification language and an execution model for the implementations, and demonstrate the viability of our method by developing a protocol for a traffic scenario in which a car runs a red light at a busy intersection.

eess.SY↗

arXiv2008

On base station localization for state estimation over lossy networks

We consider a state estimation problem where observations are made by multiple sensors. These observations are communicated over a lossy wireless network to a central base station that computes estimates via a Kalman filter. The goal is to determine the optimal location of the base station under a certain class of packet loss probability models. It is shown in the two sensor case that the base station is optimally located at one of the sensor locations. Empirical evidence suggests that the result holds in some generality.

math.OC↗