Formalization of Asymptotic Notations

Many of the smart grids objectives, such as cost reduction and power mitigation, depend upon the integration of plug-in electric vehicles upon the successful implementations of DR programs. These smart grid operations depend upon the computational complexity of algorithms due to online settings. Algorithm design analysis, especially asymptotic notations are used to analyze and design low-computational algorithms. Traditionally, the analysis is conducted using the paper-and-pencil proof methods using notions of limits to model the asymptotic behaviors. However, paper-and-pencil methods are error prone due to human involvement. Whereas, low-computational complexity of online algorithms, in smart grids, is crucial for the reliable, cost-effective and efficient grid operations. Considering the mission-critical application of smart grids, in this chapter, we develop a theorem proving based formalization to conduct formal asymptotic analysis of online algorithms. We use the proposed formalization to formally verify Online cooRdinated CHARging Decision (ORCHARD) and online Expected Load Flattening (ELF) algorithm for plug-in electric vehicles.