title: Formal modeling and verification of fractional order linear systems.
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.
authors.affiliation: School of Information Science and Engineering, Yunnan University, Kunming 650091, China. Electronic address: chunnazhao@163.com.
authors.forename: Chunna
authors.initials: C
authors.lastname: Zhao
authors.affiliation: Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China.
authors.forename: Likun
authors.initials: L
authors.lastname: Shi
authors.affiliation: Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China.
authors.forename: Yong
authors.initials: Y
authors.lastname: Guan
authors.affiliation: Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China.
authors.forename: Xiaojuan
authors.initials: X
authors.lastname: Li
authors.affiliation: Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China.
authors.forename: Zhiping
authors.initials: Z
authors.lastname: Shi
keywords: Formal verification; Fractional order linear systems; High-order logic; Theorem proving