Formal Analysis of Fractional Order Systems in Higher-order Logic


Fractional order systems, which involve integration and differentiation of non integer order, are increasingly being used in the fields of control systems, robotics, signal processing and circuit theory. Traditionally, the analysis of fractional order systems has been performed using paper-and-pencil based proofs or computer algebra systems. These analysis techniques compromise the accuracy of their results and thus are not recommended to be used for safety-critical fractional order systems. To overcome this limitation, we propose to leverage upon the high expressiveness of higher-order logic to formalize the theory of fractional calculus, which is the foremost mathematical concept in analyzing fractional order systems. In this research, we provide the higher-order-logic formalization of fractional calculus based on the Riemann-Liouville approach using the HOL theorem prover. To demonstrate the usefulness of the reported formalization, we utilize it to formally analyze some fractional order systems, namely, a fractional electrical component Resistoductance, a fractional integrator and a fractional differentiator circuit.



Proposed Framework


  • Umair Siddique, MS (2010–2011), SAVe Lab, SEECS, NUST, Pakistan



  1. U. Siddique and O. Hasan, “On the Formalization of Gamma Function in HOL”, Journal of Automated Reasoning (JAR), 53, pp. 407–429, doi:10.1007/s10817-014-9311-3, 2014.

  2. U. Siddique and O. Hasan, “Analysis Techniques for Fractional Order Systems: A Survey”, International Conference of Numerical Analysis and Applied Maths (ICNAAM-2012), American Institute of Physics, Vol. 1479, pp 2106–2109.

  3. U. Siddique and O. Hasan, “Formal Analysis of Fractional Order Systems in HOL”, Formal Methods in Computer Aided Design (FMCAD-2011), IEEE, pp. 163–170.

  4. U. Siddique, “Formal analysis of Fractional Order Systems in Higher-order Logic”, Masters Thesis, National University of Sciences and Technology (NUST), Islamabad, Pakistan. August, 2011.