Title :
Formal analysis of fractional order systems in HOL
Author :
Siddique, Umair ; Hasan, Osman
Author_Institution :
Res. Center for Modeling & Simulation, Nat. Univ. of Sci. & Technol., Islamabad, Pakistan
fDate :
Oct. 30 2011-Nov. 2 2011
Abstract :
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. This paper provides a 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.
Keywords :
process algebra; theorem proving; HOL theorem prover; Riemann-Liouville approach; circuit theory; control system; formal analysis; fractional calculus; fractional differentiator circuit; fractional electrical component; fractional integrator; higher-order-logic formalization; noninteger order; resistoductance; robotics; safety-critical fractional order system; signal processing; Analytical models; Calculus; Cognition; Equations; Fractional calculus; Linearity;
Conference_Titel :
Formal Methods in Computer-Aided Design (FMCAD), 2011
Conference_Location :
Austin, TX
Print_ISBN :
978-1-4673-0896-0