Formal asymptotic analysis of online scheduling algorithms for plug-in electric vehicles' charging

Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki, Syed Rafay Hasan

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


A large-scale integration of plug-in electric vehicles (PEVs) into the power grid system has necessitated the design of online scheduling algorithms to accommodate the after-effects of this new type of load, i.e., PEVs, on the overall efficiency of the power system. In online settings, the low computational complexity of the corresponding scheduling algorithms is of paramount importance for the reliable, secure, and efficient operation of the grid system.Generally, the computational complexity of an algorithm is computed using asymptotic analysis. Traditionally, the analysis is performed using the paper-pencil proof method, which is error-prone and thus not suitable for analyzing the mission-critical online scheduling algorithms for PEVcharging. To overcome these issues, this paper presents a formal asymptotic analysis approach for online scheduling algorithms for PEV charging using higher-order-logic theorem proving, which is a sound computer-based verification approach. For illustration purposes, we present the complexity analysis of two state-of-the-art online algorithms: the Online cooRdinated CHARging Decision (ORCHARD) algorithm and online Expected Load Flattening (ELF) algorithm. C 2018 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (

Original languageEnglish
Article number19
Issue number1
Publication statusPublished - Jan 2019


  • Asymptotic analysis
  • Computational complexity
  • HOL-Light

ASJC Scopus subject areas

  • Control and Optimization
  • Energy (miscellaneous)
  • Engineering (miscellaneous)
  • Energy Engineering and Power Technology
  • Electrical and Electronic Engineering
  • Fuel Technology
  • Renewable Energy, Sustainability and the Environment


Dive into the research topics of 'Formal asymptotic analysis of online scheduling algorithms for plug-in electric vehicles' charging'. Together they form a unique fingerprint.

Cite this