A hoare logic for single-input single-output continuous-time control systems

被引：0

作者：

Boulton, RJ ^{[1
]}

Hardy, R ^{[1
]}

Martin, U ^{[1
]}

机构：

[1] Univ St Andrews, Sch Comp Sci, St Andrews, Fife, Scotland

来源：

HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS | 2003年 / 2623卷

关键词：

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper presents a Hoare-style logic for reasoning about the frequency response of control systems in the continuous-time domain. Two properties, the gain (amplitude) and phase shift, of a control system are considered. These properties are for a sinusoidal input of variable frequency. The logic operates over a simplified form of block diagram, including arbitrary transfer functions, feedback loops, and summation of signals. Reasoning is compositional, i.e. properties of a system can be deduced from properties of its subsystems. A prototype tool has been implemented in a mechanised theorem prover.

引用

页码：113 / 125

页数：13

共 50 条

[31] Optimal control and sub-optimal control for single-input single-output deadbeat repetitive systems
Kondo, E
Kiyota, T
Matsuda, J
PROCEEDINGS OF THE 36TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-5, 1997, : 3755 - 3756
[32] Absolute stability of single-input single-output systems with constant internal point time delays
de la Sen, M
INFORMATICA, 2003, 14 (03) : 357 - 374
[33] GLOBAL OUTPUT TRACKING FOR A CLASS OF SINGLE-INPUT SINGLE-OUTPUT NONLINEAR-SYSTEMS
TORNAMBE, A
INTERNATIONAL JOURNAL OF SYSTEMS SCIENCE, 1994, 25 (07) : 1145 - 1155
[34] Aliasing error modelling in single-input single-output linear estimation systems
Kotsakis, C
Sideris, MG
GRAVITY GEOID AND GEODYNAMICS 2000, 2002, 123 : 43 - 48
[35] Zero-based equalizers for single-input single-output and single-input multiple-output channels
Abeysekera, Saman S.
Ye, Yun
SIGNAL PROCESSING, 2008, 88 (07) : 1868 - 1880
[36] STABILIZATION THEORY FOR SINGLE-INPUT SINGLE-OUTPUT TWO-DIMENSIONAL SYSTEMS
BISIACCO, M
CIRCUITS SYSTEMS AND SIGNAL PROCESSING, 1987, 6 (01) : 77 - 93
[37] PREDICTIVE CONTROLLER DESIGN FOR SINGLE-INPUT/SINGLE-OUTPUT (SISO) SYSTEMS.
Maurath, Paul R.
Mellichamp, Duncan A.
Seborg, Dale E.
Industrial and Engineering Chemistry Research, 1988, 27 (06): : 956 - 963
[38] Structural decomposition of linear singular systems: the single-input and single-output case
He, MG
Chen, BM
SYSTEMS & CONTROL LETTERS, 2002, 47 (04) : 327 - 334
[39] U-PARAMETER DESIGN OF ROBUST SINGLE-INPUT SINGLE-OUTPUT SYSTEMS
DORATO, P
LI, YZ
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 1991, 36 (08) : 971 - 975
[40] On maximum sector bounds for absolute stability of single-input single-output systems
Wulff, K.
Shorten, R.
INTERNATIONAL JOURNAL OF CONTROL, 2007, 80 (06) : 832 - 842

← 1 2 3 4 5 →