| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 5004022 | ISA Transactions | 2016 | 7 Pages |
Abstract
This paper presents a formalization of a fractional order linear system in a higher-order logic (HOL) theorem proving system. Based on the formalization of the Grünwald-Letnikov (GL) definition, we formally specify and verify the linear and superposition properties of fractional order systems. The proof provides a rigor and solid underpinnings for verifying concrete fractional order linear control systems. Our implementation in HOL demonstrates the effectiveness of our approach in practical applications.
Keywords
Related Topics
Physical Sciences and Engineering
Engineering
Control and Systems Engineering
Authors
Chunna Zhao, Likun Shi, Yong Guan, Xiaojuan Li, Zhiping Shi,