Title
Formalization of fractional order PD control systems in HOL4.
Abstract
Higher-order logic theorem proving method is applied to analyze fractional order PD control systems in this paper. Theorem proving is based on rigorous logic and correct mathematics theory. Firstly, existent conditions and formal model of fractional calculus Caputo definition is established in higher order logic theorem prover. Then some properties are verified, including homogeneity, linearity property, fractional differential of constant and relationship between integer order differential and fractional differential. And formalization of Laplace transform based on fractional calculus Caputo definition is given and we apply it to illustrate advantages of fractional calculus Caputo definition. Initial values based on fractional calculus Caputo definition have exact physical meanings. And then formal modeling of fractional order PD controller is verified based on the above properties. We also verify the stability and other properties of fractional order PD controller by theorem proving method. Lastly, steady-state error is analyzed based on formalization of fractional calculus Caputo definition. It shows that fractional order PD controller can achieve a better control performance than integer order PD controller.
Year
DOI
Venue
2018
10.1016/j.tcs.2017.08.011
Theoretical Computer Science
Keywords
Field
DocType
Fractional calculus,Caputo definition,Higher order logic,Theorem proving,Fractional order PD controller
Integer,Applied mathematics,Discrete mathematics,Laplace transform,PID controller,Automated theorem proving,Linearity,Fractional calculus,Control system,Mathematics,Higher-order logic,Calculus
Journal
Volume
Issue
ISSN
706
C
0304-3975
Citations 
PageRank 
References 
1
0.36
3
Authors
2
Name
Order
Citations
PageRank
Chunna Zhao1315.53
Shanshan Li229553.11