Formalization of Asymptotic Notations

Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki

Research output: Chapter in Book/Report/Conference proceedingChapter


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.

Original languageEnglish
Title of host publicationSpringerBriefs in Applied Sciences and Technology
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages16
Publication statusPublished - 2022

Publication series

NameSpringerBriefs in Applied Sciences and Technology
ISSN (Print)2191-530X
ISSN (Electronic)2191-5318

ASJC Scopus subject areas

  • Biotechnology
  • General Chemical Engineering
  • General Mathematics
  • General Materials Science
  • Energy Engineering and Power Technology
  • General Engineering


Dive into the research topics of 'Formalization of Asymptotic Notations'. Together they form a unique fingerprint.

Cite this