## Formal Analysis of Linear Control Systems using Theorem Proving
Adnan Rashid and Osman Hasan
School of Electrical Engineering and Computer Science (SEECS) National University of Sciences and Technology (NUST) Islamabad, Pakistan
{adnan.rashid,osman.hasan}@seecs.nust.edu.pk
Abstract. Control systems are an integral part of almost every engineering and physical system and thus their accurate analysis is of utmost importance. Traditionally, control systems are analyzed using paper-andpencil proof and computer simulation methods, however, both of these methods cannot provide accurate analysis due to their inherent limitations. Model checking has been widely used to analyze control systems but the continuous nature of their environment and physical components cannot be truly captured by a state-transition system in this technique. To overcome these limitations, we propose to use higher-order-logic theorem proving for analyzing linear control systems based on a formalized theory of the Laplace transform method. For this purpose, we have formalized the foundations of linear control system analysis in higherorder logic so that a linear control system can be readily modeled and analyzed. The paper presents a new formalization of the Laplace transform and the formal verification of its properties that are frequently used in the transfer function based analysis to judge the frequency response, gain margin and phase margin, and stability of a linear control system. We also formalize the active realizations of various controllers, like Proportional-Integral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), and various active and passive compensators, like lead, lag and lag-lead. For illustration, we present a formal analysis of an unmanned free-swimming submersible vehicle using the HOL Light theorem prover.
Keywords: Control Systems, Higher-order Logic, Theorem Proving
## 1 Introduction
Linear control systems are widely used to regulate the behavior of many safetycritical applications, such as process control, aerospace, robotics and transportation. The first step in the analysis of a linear control system is the construction of its equivalent mathematical model by using the physical and engineering laws. For example, in the case of electrical systems, we need to model the currents and voltages passing through the electrical components and their interactions in the
## 2 A. Rashid and O. Hasan
corresponding electrical circuit using the system governing laws, such as Kirchhoff's current law (KCL) and Kirchhoff's voltage law (KVL). The mathematical model is then used to derive differential equations describing the relationship between the inputs and outputs of the underlying system. The next step in the analysis of a linear control system is to solve these equations to obtain a transfer function, which is in turn used to assess many interesting control system characteristics, such as frequency response, phase margin and gain margin. However, solving these equations in the time domain is not so straightforward as they usually involve the integral and differential operators. The Laplace transform, which is an integral based transform method, is thus often used to convert these differential equations to their equivalent algebraic equations in s -domain by converting the differential and integral operations into multiplication and division operators, respectively. This algebraic equation can be quite easily solved to obtain the corresponding transfer function, frequency response, gain margin and the phase margin and perform the stability analysis of the given control system.
Traditionally, the linear control system analysis is performed using paperand-pencil proof methods. However, these methods are human-error prone and cannot be relied upon for the analysis of safety-critical applications. Moreover, there is always a risk of misusing an existing mathematical result as this manual analysis method does not provide the assurance that a mathematical law would be used only if all of its required assumptions are valid. Computer simulation and numerical methods are also frequently used to analyze linear control systems. However, they also compromise the accuracy of the results due to the involvement of computer arithmetic and the associated round-off errors. Computer algebra systems (CAS), such as Mathematica [14], are also used for the Laplace transform based analysis of linear control systems. However, CAS are primarily based on unverified symbolic algorithms and thus there is no formal proof to ascertain the accuracy of their analysis results. Given the inaccurate nature of all the abovementioned analysis techniques, they are not very suitable to analyze control systems used in safety-critical domains, where even a slight error in analysis may lead to disastrous consequences, including the loss of human lives.
To overcome the above-mentioned limitations, model checking [11] has been also used to analyze control systems [12,22] but the continuous nature of their environment and physical components cannot be truly captured by a statetransition system in this technique. Similarly, a Hoare logic based framework [6] and the KeYmaera tool [2] have been used for the formal frequency domain analysis and verification of the safety properties of control systems with sampled-time controllers, respectively. However, the former is limited to the analysis of systems that can be expressed using a block diagram with a tree structure, whereas in the later, the continuous nature of the models is abstracted in the formal modeling process and hence the completeness of the analysis is compromised in both cases.
Recently, the HOL Light theorem prover has been used for the formal analysis of control systems. Hasan et al. presented a formalization of the block diagrams in HOL Light and used it to reason about the transfer function and the steady-
state error analysis of a feedback control system [10]. Ahmed et al. used this formalization of block diagrams to verify the steady-state error of a unity feedback control system [1]. Similarly, Beillahi et al. formalized the signal flow graphs in HOL Light, which can be used to formally verify transfer functions of linear control systems [5]. However, all these existing works focus on the verification of the transfer functions for a control system and, to the best of our knowledge, no prior work dealing with the formal analysis of dynamics of a linear control system exists in the literature of higher-order-logic theorem proving.
In this paper, we present a framework to conduct the formal analysis of dynamical characteristics of a linear control system using higher-order-logic theorem proving. The main idea behind the proposed framework, depicted in Fig. 1, is to formalize all the foundational components of a linear control system to facilitate formal modeling and reasoning about linear control systems within the sound core of a theorem prover. For this purpose, we built upon the higherorder-logic formalizations of Multivariable calculus [9] and a library of analog components, like resistor, capacitor and inductor [21]. We present a new formalization of Laplace transform , which includes the formal verification of some of its frequently used properties in reasoning about the transfer function of an n -order system. We also formalized some widely used characteristics of linear control systems , such as frequency response, gain margin and phase margin, which can be used for the stability analysis of a linear control system. Moreover, we formalize the active realizations of various controllers , such as ProportionalIntegral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), Proportional (P), Integral (I) and Derivative (D) and various active and passive compensators , such as lag, lead and lag-lead.
The proposed framework, depicted in Fig. 1, allows us to build a formal model of the given linear control system, based on the active realizations of its
Fig. 1: Proposed Framework
<details>
<summary>Image 1 Details</summary>
### Visual Description
## Diagram: Control Systems Architecture with Higher-Order Logic Integration
### Overview
This diagram illustrates the hierarchical structure of a control systems framework, integrating mathematical foundations (Higher-Order Logic) with control theory components. It emphasizes the flow of information and dependencies between subsystems, formal models, and verification tools.
### Components/Axes
#### Top Section: Control Systems
- **Controllers**
- **Compensators**
- **Properties**
- **Differential Equation**
- **Transfer Function**
#### Left Section: Higher-Order Logic
- **Analog Library**
- **Multivariate Calculus**
- **Laplace Transform**
- **PID, PD, PI, P, I, D** (Proportional-Integral-Derivative controllers)
- **Lag, Lead, Lag-lead** (Compensation techniques)
#### Middle Section: Control Systems Subcomponents
- **Gain Margin**
- **Phase Margin**
- **Frequency Response**
#### Right Section: Formal Verification
- **Formal Model**
- **HOL Light Theorem Prover**
#### Arrows and Connections
- **Higher-Order Logic** β **Control Systems** (via arrows)
- **Control Systems** β **Differential Equation** and **Transfer Function**
- **Differential Equation** and **Transfer Function** β **Properties**
- **Properties** β **Formal Model**
- **Formal Model** β **HOL Light Theorem Prover**
### Detailed Analysis
- **Higher-Order Logic** (blue section): Contains foundational mathematical tools (e.g., Laplace Transform, Multivariate Calculus) and control strategies (PID, Lag-lead). These are prerequisites for designing control systems.
- **Control Systems** (green section): Includes core components like Controllers, Compensators, and properties (Gain Margin, Phase Margin). These are linked to mathematical models (Differential Equation, Transfer Function).
- **Properties** (lighter green): Represents system characteristics derived from differential equations and transfer functions.
- **Formal Model** (purple): Acts as an intermediate layer between control systems properties and the verification tool.
- **HOL Light Theorem Prover** (orange): A formal verification tool that validates the correctness of the formal model.
### Key Observations
1. **Hierarchical Flow**: The diagram shows a top-down flow from mathematical foundations (Higher-Order Logic) to control system design, then to formal verification.
2. **Interconnectedness**: Properties (e.g., Gain Margin) are central, linking differential equations, transfer functions, and formal models.
3. **Verification Focus**: The HOL Light Theorem Prover is positioned at the bottom, suggesting its role in ensuring the correctness of the entire system.
### Interpretation
This diagram highlights the integration of mathematical rigor (Higher-Order Logic) with practical control system design. The flow from foundational tools to formal verification underscores the importance of **formal methods** in ensuring system stability and correctness. The emphasis on properties like Gain Margin and Phase Margin indicates a focus on **robustness** and **stability analysis**. The use of the HOL Light Theorem Prover suggests a commitment to **mathematical proof-based validation**, which is critical in safety-critical systems.
**Note**: No numerical data or trends are present in the diagram; it is a conceptual representation of system architecture and dependencies.
</details>
controllers and compensators, the passive realizations of compensators and differential equations. Moreover, it also allows to formalize the behavior of the
given linear control system in terms of its differential equation, transfer function specification and its properties, such as phase margin, frequency response and gain margin. We can then use these formalized models and properties to verify an implication relationship between them, i.e., model implies its specification. In order to demonstrate the effectiveness of our proposed formalization, we formalize the control system of an unmanned free-swimming submersible vehicle [15]. We have used the HOL Light theorem prover [8] for the proposed formalization in order to build upon its multivariable calculus theories. We have also developed a tactic that can be used to automatically verify the transfer function of any control system up to 20 th order . This tactic was found to be very handy in the formal analysis of the unmanned submersible vehicle.
## 2 Multivariable Calculus Theories in HOL Light
An N-dimensional vector is formalized in the multivariable theory of HOL Light as a R N column matrix of real numbers [9]. All of the multivariable calculus theorems are verified for functions with an arbitrary data-type R N β R M .
A complex number is defined as a 2-dimensional vector, i.e., a R 2 matrix.
```
Definition 1. |- \a. Cx a = complex (a, &0)
|- ii = complex (&0, &1)
```
Cx : R β R 2 is a type casting function that accepts a real number and returns its corresponding complex number with the imaginary part equal to zero, where the & operator type casts a natural number to its corresponding real number. Similarly, ii (iota) represents a complex number having the real part equal to zero and the magnitude of the imaginary part equal to 1.
```
Definition 2. |- \z. Re z = z$1
```
The function Re accepts a complex number (2-dimensional vector) and returns its real part. Here, the notation z $ i represents the i th component of vector z . Similarly, Im takes a complex number and returns its imaginary part. The function lift accepts a variable of type R and maps it to a 1-dimensional vector with the input variable as its single component. Similarly, drop takes a 1-dimensional vector and returns its single element as a real number.
```
Definition 3. |- \x. exp x = Re (cexp (Cx x))
```
The complex exponential and real exponentials are represented as cexp : R 2 β R 2 and exp : R β R in HOL Light, respectively.
```
Definition 4. - \forall f i. integral i f = (@y. (f has integral y) i)
\verbatim
\f a f i. real integral i f = (@y. (f has real integral y) i)
```
The function integral represents the vector integral and is defined using the Hilbert choice operator @ in the functional form. It takes the integrand function f , having an arbitrary type R N β R M , and a vector-space i : R N β B , which defines the region of convergence as B represents the boolean data type, and returns a vector R M , which is the integral of f on i . The function has integral represents the same relationship in the relational form. Similarly, the function real integral accepts the integrand function f : R β R and a set of real numbers i : R β B and returns the real-valued integral of function f over i . The region of integration, for both of the above integrals can be defined to be bounded by a vector interval [ a, b ] or real interval [ a, b ] using the HOL Light functions interval [ a , b ] and real interval [ a , b ], respectively.
## Definition 5.
β f net. vector derivative f net = (@f'.(f has vector derivative f') net)
The function vector derivative takes a function f : R 1 β R M and a net : R 1 β B , which defines the point at which f has to be differentiated, and returns a vector of data-type R M , which represents the differential of f at net . The function has vector derivative defines this relationship in the relational form.
$$D e f n i t i o n 6 . \, \vdash \forall f \, n e t . \, l i m \, n e t \, f = ( \mathbb { O } _ { 1 } . \, ( f \to 1 ) \, n e t )$$
The function lim accepts a net with elements of arbitrary data-type A and a function f : A β R M and returns l of data-type R M , i.e., the value to which f converges at the given net .
## 3 Formalization of Laplace Transform
Mathematically, Laplace transform is defined for a function f : R 1 β C as [4]:
$$\mathcal { L } [ f ( t ) ] = F ( s ) = \int _ { 0 } ^ { \infty } f ( t ) e ^ { - s t } d t , \, s \epsilon \, \mathbb { C } & & ( 1 )$$
We formalize Equation 1 in HOL Light as follows:
$$\text {Definition 7.} \, \vdash \forall s f . l a p l a c e t r a n s t o r f i s = \\ \text {integral } \{ t | \& 0 \leq d r o p \} ( \lambda t . c x p \left ( - ( s * C x \, ( d r o p \, t ) ) \right ) * f \, t )$$
The function laplace transform accepts a complex-valued function f : R 1 β R 2 and a complex number s and returns the Laplace transform of f as represented by Equation 1. In the above definition, we used the complex exponential function cexp : R 2 β R 2 because the return data-type of the function f is R 2 . Here, the data-type of t is R 1 and to multiply it with the complex number s , it is first converted into a real number by using drop and then it is converted to data-type R 2 using Cx . Next, we use the vector function integral (Definition 4) to integrate the expression f ( t ) e -iΟt over the positive real line since the datatype of this expression is R 2 . The region of integration is { t | &0 <= drop t } , which represents the positive real line. Laplace transform was earlier formalized using a limiting process as [20]:
```
|- \s f. laplace f s = lim at posinfinity (\b. integral
(interval [lift (&0), lift b]) (\t. cexp (--(s * Cx (drop t))) * f t))
```
However, the HOL Light definition of the integral function implicitly encompasses infinite limits of integration. So, our definition covers the region of integration, i.e., [0 , β ), as { t | &0 <= drop t } and is equivalent to the definition given in [20]. However, our definition considerably simplifies the reasoning process in the verification of Laplace transform properties since it does not involve the notion of limit.
The Laplace transform of a function f exists, if f is piecewise smooth and is of exponential order on the positive real line [4,19]. A function is said to be piecewise smooth on an interval if it is piecewise differentiable on that interval.
```
Definition 8. + \s f. laplace exists f s <=>
( \b . f piecewise differentiable on interval [lift (&0),lift b] ) ^
( \m a. Re s > drop a \^ exp order cond f M a)
```
The function exp order cond in the above definition represents the exponential order condition necessary for the existence of the Laplace transform [20,4]:
```
Definition 9. |- \f M a. exp order f M a <=> &0 < M ^ { * } \\ ( \forall t . &0 <= t \Rightarrow n o r m ( f ( l i f t ) ) \leq M * \exp ( d r o p a * t ) )
```
We used Definitions 7, 8 and 9 to formally verify some of the classical properties of Laplace transform, given in Table 1. The properties namely linearity, frequency shifting, differentiation and integration were already verified using the formal definition of the Laplace transform [20]. We formally verified these using our new definition of the Laplace transform. Moreover, we formally verified some new properties, such as, time shifting, time scaling, cosine and sine-based modulations and the Laplace transform of a n -order differential equation. The assumptions of these theorems describe the existence of the corresponding Laplace transforms. For example, the predicate laplace exists higher deriv in the theorem corresponding to the n -order differential equation ensures that the La-
Table 1: Properties of Laplace Transform
| Property | Formalized Form |
|---------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Integrability e - st f ( t ) integrable on [0 , β ) | β f s. laplace exists f s β ( Ξ» t. cexp (--(s β Cx (drop t))) β f t) integrable on { t | &0 <= drop t } |
| Linearity L [ Ξ±f ( t )+ Ξ²g ( t )] = Ξ±F ( s )+ Ξ²G ( s ) | β f g s a b. laplace exists f s β§ laplace exists g s β laplace transform ( Ξ» t. a β f t + b β g t) s a β laplace transform f s + b β laplace transform g s |
| Frequency Shifting L [ e s 0 t f ( t )] = F ( s - s 0 ) | β f s s0. laplace exists f s β laplace transform ( Ξ» t. cexp (s0 β Cx (drop t)) β f t) s = laplace transform f (s - s0) |
<details>
<summary>Image 2 Details</summary>
### Visual Description
```markdown
## Table: Laplace Transform Rules for Time Domain Operations
### Overview
The table presents mathematical operations in the time domain (left column) and their corresponding Laplace transform rules (right column), including logical conditions and transform expressions.
### Components/Axes
- **Left Column**: Time domain operations (differentiation, integration, time shifting, scaling, modulation).
- **Right Column**: Logical conditions and Laplace transform rules using:
- `β` (for all)
- `β` (implies)
- `laplace_exists`, `laplace_transform`
- `lift`, `drop`, `Cx`, `s`, `t`, `Οβ`, `j`, `Re`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs`, `Vs
</details>
| First-order Differ- entiation in Time Domain L [ d dt f ( t ) ] = sF ( s ) - f (0) | β f s. laplace exists f s β§ ( β t. f differentiable at t) β§ laplace exists ( Ξ» t. vector derivative f (at t)) s β laplace transform ( Ξ» t. vector derivative f (at t)) s = |
|------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Higher-order Diffe- rentiation in Time Domain L [ d n n f ( t )] = s n F ( s ) | s β laplace transform f s - f (lift (&0)) β f s n. laplace exists higher deriv n f s β§ ( β t. differentiable higher derivative n f t) |
| dt - β n k =1 s k - 1 d n - k f (0) dx n - k | β laplace transform ( Ξ» t. higher vector derivative n f t) s = s pow n β laplace transform f s - vsum (1..n) ( Ξ» x. s pow (x - 1) β higher vector derivative (n - x) f (lift (&0))) |
| Integration in Time Domain L [ β« t 0 f ( Ο ) dΟ ] = 1 s F ( s ) | β f s. &0 < Re s β§ laplace exists f s β§ laplace exists ( Ξ» x. integral (interval [lift (&0),x]) f) s β§ ( β x. f continuous on interval [lift (&0),x]) β laplace transform ( Ξ» x. integral (interval [lift (&0),x]) f) s = Cx (& 1 ) β laplace transform f s |
| Time Shifting L [ f ( t - t 0 ) u ( t - t 0 )] = e - t 0 s F ( s ) | s β f s t0. &0 < drop t0 β§ laplace exists f s β laplace transform (shifted fun f t0) s = cexp (--(s β Cx (drop t0))) β laplace transform f s |
| Time Scaling L [ f ( ct )] = 1 c F ( s c ) , 0 < c | β f s c. &0 < c β§ laplace exists f s β§ laplace exists f ( s Cx c ) β laplace transform ( Ξ» t. f(c % t)) s = Cx (& 1 ) Cx c β laplace transform f ( s Cx c ) |
| Cosine Based Modulation L [ f ( t ) cos ( Ο 0 t )] = F ( s - jΟ 0 ) 2 + F ( s + jΟ 0 ) 2 | β f s w0. laplace exists f s β laplace transform ( Ξ» t. ccos (Cx w0 β Cx (drop t)) β f t) s = laplace transform f ( s - ii β Cx w0 ) Cx (& 2 ) + laplace transform f ( s + ii β Cx w0 ) Cx (& 2 ) |
| Sine Based Modulation L [ f ( t ) cos ( Ο 0 t )] = F ( s - jΟ 0 ) 2 j - F ( s + jΟ 0 ) | β f s w0. laplace exists f s β laplace transform ( Ξ» t. csin (Cx w0 β Cx (drop t)) β f t) s = laplace transform f ( s - ii β Cx w0 ) Cx (& 2 ) β ii - laplace transform f ( s + ii β Cx w0 ) |
| n -order Differ- ential Equation L ( β n k =0 Ξ± k d k y dt k ) = F ( s ) β n k =0 Ξ± k s k - β n k =0 β k i =1 s i - 1 d k - i f (0) dt k - i | β f lst s n. laplace exists higher deriv n f s β§ ( β t. differentiable higher derivative n f t) β laplace transform ( Ξ» t. diff eq n order n lst f t) s = laplace transform f s β vsum (0..n) ( Ξ» k. EL k lst β s pow k) - vsum (0..n) ( Ξ» k. EL k lst β vsum (1..k) ( Ξ» i. s pow (i - 1) β higher vector derivative (k - i) f (lift (&0)))) |
|------------------------------------------------------------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
place of all the derivatives up to the n th order of the function f exist. Similarly, the predicate differentiable higher derivative provides the differentiability of the function f and its higher derivatives up to the n th order. The verification of these properties not only ensures the correctness of our definitions but also plays a vital role in minimizing the user effort in reasoning about Laplace transform based analysis of systems, as will be depicted in Sections 4 and 5 of this paper.
The generalized linear differential equation describes the input-output relationship for a generic n -order linear control system [15]:
$$\sum _ { k = 0 } ^ { n } \alpha _ { k } \frac { d ^ { k } } { d t ^ { k } } y ( t ) = \sum _ { k = 0 } ^ { m } \beta _ { k } \frac { d ^ { k } } { d t ^ { k } } x ( t ) , \quad m \leq n \quad ( 2 )$$
where y ( t ) is the output and x ( t ) is the input to the system. The constants Ξ± k and Ξ² k are the coefficients of the output and input differentials with order k , respectively. The greatest index n of the non-zero coefficient Ξ± n determines the order of the underlying system. The corresponding transfer function is obtained by setting the initial conditions equal to zero [15]:
$$\frac { Y ( s ) } { X ( s ) } = \frac { \sum _ { k = 0 } ^ { m } \beta _ { k } s ^ { k } } { \sum _ { k = 0 } ^ { n } \alpha _ { k } s ^ { k } } \quad ( 3 )$$
We verified the transfer function, given in Equation 3, for the generic n-order linear control system as the following HOL Light theorem.
## Theorem 1. β y x m n inlst outlst s.
```
Theorem 1. + \y x m n inlst outlst s.
( \forall t. differentiable higher deriv m n x y t) ^
laplace exists of higher deriv m n x y s ^ zero init conditions m n x y ^
diff eq n order sys m n inlst outlst x y ^
~(laplace transform x s = Cx (&0)) ^
~(vsum (0..n) ( \lambda. t. EL t outlst * s pow t) = Cx (&0))
=> laplace transform y s = vsum (0..m) ( \lambda.t. EL t inlst * s pow t)
:= laplace transform x s = vsum (0..n) ( \lambda.t. EL t outlst * s pow t)
```
The first assumption ensures that the functions y and x are differentiable up to the n th and m th order, respectively. The next assumption represents the Laplace transform existence condition up to the n th order derivative of function y and m th order derivative of the function x . The next assumption models the zero initial conditions for both of the functions y and x , respectively. The next assumption represents the formalization of Equation 2 and the last two assumptions provide
the conditions for the design of a reliable linear control system. Finally, the conclusion of the above theorem represents the transfer function given by Equation 3. The verification of this theorem is very useful as it allows to automate the verification of the transfer function of any linear control system as described in Sections 4 and 5 of the paper. The formalization, described in this section, took around 2000 lines of HOL Light code [17] and around 130 man-hours.
## 4 Formalization of Linear Control Systems Foundations
A general closed-loop control system is depicted in Fig. 2a. Here, X ( s ) and Y ( s ) represent the Laplace transforms of the time domain input x ( t ) and the output y ( t ), respectively. G ( s ) and H ( s ) represent the forward path and the feedback path transfer functions, respectively. Similarly, G ( s ) H ( s ) is the open loop transfer function of the system and Y ( s ) /X ( s ) is the closed loop transfer function [7]. Table 2 presents the formalization of the frequency response, phase margin and gain margin of this control system. These properties are used to study the dynamics of a linear control system in the frequency domain and to perform its stability analysis.
The frequency response is used to analyze the dynamics of the system by studying the impact of different frequency components on the intended behaviour of the given linear control system. We also formally verified the frequency response of a generic n -order system based on assumptions that are very similar to the ones used for Theorem 1.
Table 2: Properties of Linear Control Systems
| Property | Formalized Form |
|------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Frequency Response M ( jΟ ) = M ( s ) | ( jΟ ) = Y ( s ) X ( s ) β£ β£ β£ β£ β£ ( jΟ ) = Y ( jΟ ) X ( jΟ ) | β y x w. frequency response x y w = laplace transform y ( ii β Cx w ) laplace transform x ( ii β Cx w ) |
| Frequency Response of an n -order System Y ( jΟ ) X ( jΟ ) = β m k =0 Ξ² k ( jΟ ) k β n k =0 Ξ± k ( jΟ ) k | β y x m n inlst outlst s. ( β t. differentiable higher deriv m n x y t) β§ laplace exists of higher deriv m n x y w β§ zero init conditions m n x y β§ diff eq n order sys m n inlst outlst y x β§ non zero denom cond n x w outlst β frequency response x y w = vsum ( 0 .. m ) ( Ξ» t . EL t inlst β ( ii β Cx w ) pow t ) vsum ( 0 .. n ) ( Ξ» t . EL t outlst β ( ii β Cx w ) pow t ) |
| Phase Margin [ β G ( jΟ ) H ( jΟ )] Ο = Ο gc + 180 o | β g h wgc. phase margin g h wgc = pi + Arg (g (ii β Cx wgc) β h (ii β Cx wgc)) |
| Gain Margin [ 20 log 10 β£ β£ β£ G ( jΟ ) H ( jΟ ) β£ β£ β£ Ο = Ο pc ] dB | β g h wpc. gain margin db g h wpc = &20 β log ( norm ( g ( ii β Cx wpc ) β h ( ii β Cx wpc ))) log (& 10 ) |
Phase margin and gain margin provide useful information about controlling the stability of the system [7]. Phase margin represents 180 o shifted phase angle of the open loop transfer function evaluated at the gain crossover frequency ( Ο gc ), which is the frequency at which the magnitude of the open loop transfer function is equal to 0 dB. The gain margin represents the magnitude of the open loop transfer function evaluated at the phase crossover frequency ( Ο pc ), which is the frequency at which the resultant phase curve of the open loop gain has a phase of 180 o . In our formal definitions of these notions, the function Arg(z) represents the argument of a complex number z .
Fig. 2: Control Systems Foundations (a) Closed Loop Control System (b) Generic Active Realization of Controller (c) PID Configuration (d) Lag/lead Compensator Configuration (e) Generic Passive Realization of Compensator (f) Lag-lead Compensator Configuration
<details>
<summary>Image 3 Details</summary>
### Visual Description
## Block Diagram and Circuit Analysis
### Overview
The image contains six technical diagrams (a-f) representing electronic systems and circuits. Diagrams (a) and (b) depict signal processing and operational amplifier configurations, while (c)-(f) illustrate impedance models and voltage divider circuits. All components are labeled with standard electrical symbols.
### Components/Axes
**Diagram (a): Block Diagram**
- Input: $ X(s) $ (positive and negative terminals)
- Transfer functions: $ G(s) $, $ H(s) $
- Output: $ Y(s) $
- Feedback loop: $ H(s) $ connects output to input via summing junction
**Diagram (b): Operational Amplifier Circuit**
- Components:
- $ C_A $, $ C_B $ (capacitors)
- $ i_{C_A}(t) $, $ i_{C_B}(t) $ (capacitor currents)
- $ v_i(t) $, $ v_a(t) $, $ v_o(t) $ (voltages)
- Configuration: Non-inverting amplifier with capacitive feedback
**Diagram (c): Impedance Models**
- Left: $ R_1 $ in parallel with $ C_1 $
- Right: $ R_2 $ in series with $ C_2 $
**Diagram (d): Parallel RC Circuits**
- Left: $ R_1 $ || $ C_1 $
- Right: $ R_2 $ || $ C_2 $
**Diagram (e): Capacitive Voltage Divider**
- Components: $ C_A $, $ C_B $ in series
- Voltages: $ v_i(t) $ (input), $ v_o(t) $ (output)
**Diagram (f): Combined Impedance Network**
- Left: $ R_1 $ || $ C_1 $
- Right: $ R_2 $ in series with $ C_2 $
### Detailed Analysis
**Diagram (a)** shows a feedback system with forward path $ G(s) $ and feedback path $ H(s) $. The summing junction combines $ X(s) $ and $ -H(s)Y(s) $.
**Diagram (b)** implements a non-inverting amplifier with capacitive feedback. The op-amp's negative input is connected to $ C_B $, while the positive input receives $ v_i(t) $ through $ C_A $.
**Diagrams (c)-(f)** represent different impedance configurations:
- (c): Series/parallel RC combinations
- (d): Pure parallel RC networks
- (e): Capacitive voltage divider
- (f): Mixed series-parallel RC network
### Key Observations
1. All diagrams use standard electrical symbols (resistors, capacitors, op-amps)
2. Time-domain signals ($ v(t) $) appear in (b) and (f), while (a) uses Laplace-domain transfer functions
3. Capacitors appear in all diagrams except (a)
4. Feedback appears in (a) and (b) but not in (c)-(f)
### Interpretation
These diagrams collectively demonstrate:
1. **Signal Processing**: Diagram (a) shows a basic feedback system with transfer functions
2. **Amplifier Design**: Diagram (b) implements a capacitive feedback amplifier
3. **Impedance Modeling**: Diagrams (c)-(f) show various RC network configurations for frequency response analysis
4. **Voltage Division**: Diagram (e) illustrates capacitive voltage division
The progression from block diagrams to physical circuits suggests a system design flow from mathematical modeling to implementation. The recurring use of capacitors indicates high-frequency applications or filtering requirements.
</details>
The controllers form the most vital part of any control system as they are mainly responsible for the correct operation of every component of the underlying system. Controllers are modeled using their active realizations based on an electrical circuit, which comprises of an inverting operational amplifier (op-amp) with unity gain, and two components, i.e., C A and C B , which are shown as rectangular boxes in Fig. 2b. The boxes C A and C B contain different configurations of the passive components, i.e., resistors and capacitors [16]. By making an appropriate choice of these passive components, we obtain various controllers, such as P, I, D, PI, PD, PID [15]. For the analysis of these controllers, we first need to formalize them in higher-order logic. This step requires a formal library of analog components [21,17], describing the voltage-current relationships of resistor, capacitors and inductors, and the KCL and KVL, which model the currents and voltages in an electrical circuit.
The PID controller, depicted in Fig. 2c, can be formalized as follows:
```
Definition 10. |- \C1 R1 Vi R2 C2 Vo Vb Va.
pid controller implem Vi Vo Va Vb C1 C2 R1 R2 <>
( \t. &0 < drop t => kcl [\t. capacitor current C1 (\t. Vi t - Va t) t;
\t. resistor current R1 (\t. Vi t - Va t) t;
\t. resistor current R2 (\t. Vb t - Va t) t] ^
( \t. &0 < drop t => kcl [\t. resistor current R2 (\t. Va t - Vb t) t;
\t. capacitor current C2 (\t. Vo t - Vb t) t] ^
( \t. &0 < drop t => Va t = Cx (&0))
```
where Vi and Vo are the input and the output voltages, respectively, having data type R 1 β C , and Va and Vb are the voltages at nodes a and b , respectively. The functions resistor current and capcitor current are the currents across the resistor and capacitor, respectively. The function kcl accepts a list of currents across the components of the circuit and a time variable t and returns the predicate that guarantees that the sum of all the currents leaving a particular node at time t is zero. The first conjunct of the above definition represents the application of KCL across node a . Similarly, the second conjunct models the KCL at node b , whereas the last conjunct provides the voltage across the non-inverting input of the op-amp using the virtual ground condition, as shown in Fig. 2b. We also develop a simplification tactic KCL SIMP TAC , which simplifies the implementations of the PID controller as well as other controllers and compensators. The details can be found in [17].
Next, we model the dynamical behaviour of the PID controller using the n -order differential equation:
```
Definition 11. ! R1 R2 C1 C2. inlst pid contr R1 R2 C1 C2 =
[--Cx (&1); --Cx (R2 * C2 + R1 * C1); --Cx (R1 * R2 * C1 * C2)]
! ! R1 C2. outlst pid contr R1 C2 = [Cx (&0); Cx (R1 * C2)]
! ! Vo R1 R2 C1 C2 Vi t. pid controller behav spec R1 R2 C1 C2 Vi Vo t <>
diff eq n order 1 (outlst pid contr R1 C2) Vo t =
diff eq n order 2 (inlst pid contr R1 R2 C1 C2) Vi t
```
We verified the behavioural specification based on the implementation of the PID controller as the following theorem:
```
Theorem 2. - β R1 R2 C1 C2 Vi Va Vb Vo t. &0 < R1 β§ &0 < R2 β§
&0 < C1 β§ &0 < C2 β§ (βt. differentiable higher derivative Vi Vo Vb t) β§
pid controller implem Vi Vo Va Vb C1 C2 R1 R2
β (&0 < drop t β pid controller behav spec R1 R2 C1 C2 Vi Vo t)
```
The first four assumptions model the design requirement for the underlying system. The next assumption provides the differentiability of the higher-order derivatives of Vi , Vo and Vb up to the order 1, 2 and 2, respectively. The last assumption presents the implementation for the PID controller. Finally, the conclusion presents its behavioral specification. We also develop a simplification tactic DIFF SIMP TAC , which simplifies the behavioural specifications of the PID controller as well as the other controllers and compensators [17].
Next, we verified the transfer function of the PID controller as follows:
```
Theorem 3. β’ \ R1 R2 C1 C2 Vi Vo s t. &0 < R1 ^ \& 0 < R2 ^ \& 0 < C1 ^
~(laplace transform Vi s = Cx (&0)) ^ \sim (Cx R1 * Cx C2 * s = Cx (&0)) ^
&0 < C2 ^ \wedge ( \forall t. differentiable higher derivative Vi Vo t) ^
laplace exists higher deriv Vi Vo s ^ zero initial conditions Vi Vo ^
( \forall t. pid controller behav spec R1 R2 C1 C2 Vi Vo t)
=> laplace transform Vo s =
laplace transform Vi s
--(Cx(R1 * C1 * R2 * C2) * s pow 2 + (Cx(R2 * C2) + Cx(C1 * R1)) * s + Cx(&1))
```
Cx ( R1 β C2 ) β s
The first six assumptions present the design requirements for the underlying system. The next two assumptions provide the differentiability and the Laplace existence condition for the higher-order derivatives of Vi and Vo up to the order 2 and 1, respectively. The next assumption models the zero initial conditions for the voltage functions Vi and Vo . The last assumption presents the behavioural specification of the PID controller. Finally, the conclusion of Theorem 3 presents its required transfer function. By judicious selection of the configuration of passive components, we obtain various controllers, such as P, I, D, PI, PD and perform the above-mentioned analysis for all of them.
Compensators are widely used in control systems, to improve their frequency response, steady-state error and the stability and hence, act as a fundamental block of a control system. Like controllers, the compensators are also modeled using their active realizations. A compensator uses the same analog circuit, which is used for the controllers, presented in Fig. 2b, by making an appropriate choice of the passive components C A and C B , as shown in Fig. 2d. It acts as a lag-compensator under the condition R 2 C 2 > R 1 C 1 , whereas for the case of R 1 C 1 > R 2 C 2 , it acts as a lead-compensator. The configurations of the passive components for the controllers and compensators, and their formalization is presented in [17].
Compensators are also modeled using their passive realizations based on an electrical circuit, which comprises of two components, i.e., C A and C B , which are shown as rectangular boxes in Fig. 2e. The boxes C A and C B contain different configurations of the passive components, i.e., resistors and capacitors. By making an appropriate choice of these passive components, we obtain various compensators, such as lag, lead and lag-lead [15]. The configuration of the lag-lead compensator is shown in Fig. 2f. Moreover, the configurations of the passive components for the compensators and their formalization in HOL Light is presented in [17].
The formalization of this section took around 300 lines of HOL Light code and around 14 man-hours. This clearly illustrates the effectiveness of our foundational formalization, presented in the previous section.
## 5 Unmanned Free-Swimming Submersible Vehicle
Unmanned Free-Swimming Submersible (UFSS) vehicles are a kind of autonomous underwater vehicles (AUVs) that are used to perform different tasks and operations in the submerged areas of the water. These vehicles have their own power
and control systems, which are autonomously operated and controlled by the onboard computer system without any involvement of human assistance as it is difficult for humans to work in an underwater environment. UFSS vehicles are used in many safety-critical domains to perform different tasks, such as underwater navigation and object detection [13], performing deep sea rescue and salvage operations [23], searching for sea mines [24] and securing sea harbour [24]. Due to their wider usage in the above-mentioned safety-critical applications, an accurate analysis of their control system is of utmost importance.
We present a formal analysis of the pitch control system of a UFSS vehicle. The pitch control system is responsible for the uninterrupted operation and functionality of the UFSS vehicle by manipulating different parameters, such as, elevator surface, pitch angle [15]. Fig. 3 depicts its block diagram.
Fig. 3: Pitch Control Model for Unmanned Free-swimming Submersible Vehicle
<details>
<summary>Image 4 Details</summary>
### Visual Description
## Block Diagram: Vehicle Pitch Control System
### Overview
The diagram illustrates a closed-loop control system for vehicle pitch dynamics. It includes feedback mechanisms, actuator dynamics, and vehicle response characteristics. The system uses proportional and derivative gains to stabilize pitch angle (ΞΈ(s)) based on commanded inputs and sensor feedback.
### Components/Axes
1. **Input/Output Signals**:
- **Pitch Command (ΞΈ_e(s))**: Reference signal for desired pitch angle.
- **Pitch (ΞΈ(s))**: Actual pitch angle of the vehicle.
2. **Control Elements**:
- **Pitch Gain (-Kβ)**: Proportional gain block amplifying the error between commanded and actual pitch.
- **Elevator Actuator**: Converts control signals into physical deflection (Ξ΄_e(s)).
- **Elevator Deflection (Ξ΄_e(s))**: Output of the actuator, modeled as a first-order lag: `2/(s + 2)`.
3. **Vehicle Dynamics**:
- Transfer function:
`[-0.125(s + 0.435)] / [(s + 1.23)(sΒ² + 0.226s + 0.0169)]`
Represents the vehicle's response to elevator deflection.
4. **Feedback Path**:
- **Pitch Rate Sensor**: Measures pitch rate (dΞΈ/dt), represented as `-Kβs` (derivative gain).
- Feedback loop closes around the pitch command to adjust control signals.
### Detailed Analysis
- **Signal Flow**:
1. The pitch command (ΞΈ_e(s)) is compared with the actual pitch (ΞΈ(s)) to generate an error signal.
2. The error is amplified by **-Kβ** and sent to the elevator actuator.
3. The actuator's output (Ξ΄_e(s)) is filtered by `2/(s + 2)` before affecting vehicle dynamics.
4. Vehicle dynamics propagate Ξ΄_e(s) through the transfer function to produce ΞΈ(s).
5. The pitch rate sensor (-Kβs) measures the derivative of ΞΈ(s) and feeds it back to adjust the control signal, forming a closed loop.
- **Transfer Function Details**:
- **Numerator**: `-0.125(s + 0.435)` introduces a zero at **s = -0.435**, affecting high-frequency response.
- **Denominator**: Poles at **s = -1.23** (real) and roots of **sΒ² + 0.226s + 0.0169** (complex conjugates with damping ratio β 0.64 and natural frequency β 0.13 rad/s). These poles dominate the system's transient response.
### Key Observations
1. **Feedback Stabilization**: The derivative feedback (-Kβs) adds damping to counteract oscillations in the vehicle dynamics.
2. **Actuator Lag**: The elevator actuator's first-order lag (`2/(s + 2)`) introduces a time delay, potentially limiting system bandwidth.
3. **Pole-Zero Interaction**: The zero at -0.435 partially cancels the slowest pole (-1.23), improving response speed but risking instability if gains are poorly tuned.
### Interpretation
This system is a **rate feedback control** design for aircraft or missile pitch stabilization. The proportional gain (-Kβ) ensures tracking of the pitch command, while the derivative feedback (-Kβs) suppresses oscillations. The vehicle dynamics' slow poles (β0.13 rad/s) suggest a sluggish open-loop response, necessitating aggressive feedback gains. However, the actuator lag and pole-zero proximity (-0.435 vs. -1.23) require careful tuning to avoid overshoot or instability. The diagram emphasizes the interplay between actuator dynamics, vehicle inertia, and feedback control in achieving stable flight attitudes.
</details>
The dynamics of the UFSS vehicle are represented by its corresponding differential equation, which presents the relationship between the pitch command angle ΞΈ e ( t ) and the pitch angle ΞΈ ( t ), and is given as follows:
$$\begin{array} { r l r } & { \frac { d ^ { 4 } \theta } { d t ^ { 4 } } + 3 . 4 5 6 \frac { d ^ { 3 } \theta } { d t ^ { 3 } } + ( 3 . 2 0 7 + 0 . 2 5 K _ { 2 } ) \frac { d ^ { 2 } \theta } { d t ^ { 2 } } + ( 0 . 6 1 6 + 0 . 1 0 8 8 K _ { 2 } + 0 . 2 5 K _ { 1 } ) \frac { d \theta } { d t } + } \\ & { ( 0 . 1 0 8 8 K _ { 1 } + 0 . 0 4 1 6 ) = 0 . 2 5 K _ { 1 } \frac { d \theta _ { e } } { d t } + 0 . 1 0 8 8 K _ { 1 } } \end{array} ( 4 )$$
We formalize the above differential equation as follows [18]:
```
Definition 12. 1+ \ K1. inlst ufsv K1 = [Cx(#0.1088) * Cx K1;Cx (#0.25) * Cx K1]
\[Cx(#0.1088) * Cx K1 + Cx(#0.0416);Cx(#0.25) * Cx K1 + Cx(#0.1088) * Cx K2
+ Cx(#0.6106);Cx(#0.25) * Cx K2 + Cx(#3.207);Cx(#3.456);Cx (&1)]
\[ diff eq ufsv inlst ufsv outlst ufsv theta thetae K1 K2 <=>
(\/t. diff eq n order 4 (outlst ufsv K1 K2) theta t =
diff eq n order 1 (inlst ufsv K1) thetae t)
```
where thetae and theta represent the input and the output of the pitch control system and K1 and K2 are the pitch gain and pitch rate sensor gain, respectively. The symbol # is used to represent a decimal number of data type R in HOL Light and is same as symbol & for the integer literal of data type R .
The transfer function of the pitch control of the UFSS vehicle is as follows:
$$\frac { \theta ( s ) } { \theta _ { e } ( s ) } = \frac { 0 . 2 5 K _ { 1 } s + 0 . 1 0 8 8 K _ { 1 } } { s ^ { 4 } + 3 . 4 5 6 s ^ { 3 } + ( 3 . 2 0 7 + 0 . 2 5 K _ { 2 } ) s ^ { 2 } + ( 0 . 6 1 0 6 + 0 . 1 0 8 8 K _ { 2 } + } \quad ( 5 )$$
We verified the above transfer function as the following HOL Light theorem:
```
We verified the above transfer function as the following HOL Light theorem:
Theorem 4. 1 9 thetae theta s K1 K2.
( \forall t . differentiable higher deriv thetae t) ^
laplace exists of higher deriv theta e theta s ^
zero init conditions thetae theta ^
diff eq ufsv inlst ufsv outlst ufsv thetae theta K1 K2 ^
non zero denominator condition theta s
\laplace transform theta s
= laplace transform theta e s
(Cx(#0.25) * Cx K1) * s + Cx(#0.1088) * Cx K1
```
The first two assumptions present the differentiability and the Laplace existence condition of the higher-order derivatives of thetae and theta up to order 1 and 4, respectively. The next assumption provides the zero initial conditions for thetae and theta . The next assumption presents the differential equation specification for the pitch control system of UFSS vehicle. The final assumption models the non-negativity of the denominator of the transfer function presented in the conclusion of the above theorem. We also verified the open loop transfer function ΞΈ ( s ) /Ξ΄ e ( s ), frequency response (open and closed loop) and gain margin, for the UFSS vehicle and the details can be found in [17].
The distinguishing feature of Theorem 4 and the other properties, compared to traditional analysis methods is their generic nature, i.e., all of the variables and functions are universally quantified and can thus be specialized in order to obtain the results for some given values. Moreover, all of the required assumptions are guaranteed to be explicitly mentioned along with the theorems due to the inherent soundness of the theorem proving approach. The high expressiveness of the higher-order logic enables us to model the differential equation and the corresponding transfer function in their true continuous form, whereas, in model checking they are mostly discretized and modeled using a state-transition system, which compromises the accuracy of the analysis.
To facilitate control engineers in using our formalization, we developed an automatic tactic TRANSFER FUN TAC , which automatically verifies the transfer function of the systems up to 20 th -order. This tactic was successfully used for the automatic verification of the transfer functions of the controllers, compensators and the pitch control system of the UFSS vehicle. This automatic verification tactic only requires the differential equation and the transfer function of the
underlying system and automatically verifies the transfer function. Thus, the formal analysis of the UFSS vehicle took only 25 lines of code and about half an hour, thanks to our automatic tactic and the foundational formalization of Section 3.
## 6 Conclusion
This paper presented a higher-order-logic theorem proving based approach for the formal analysis of the dynamical aspects of linear control systems using theorem proving. The main idea behind the proposed framework is to use a formalization of Laplace transform theory in higher-order logic to formally analyze the dynamic aspects of linear control systems. For this purpose, we develop a new formalization of Laplace transform theory, which includes its formal definition and verification of its properties, such as linearity, frequency shifting, differentiation and integration in time domain, time shifting, time scaling, cosine and sinebased modulation and the Laplace transform of an n -order differential equation, which are used for the verification of the transfer function of a generic n -order linear control system. Moreover, the paper also presents the formal verification of some widely used linear control system characteristics, such as frequency response, phase margin and the gain margin, using the verified transfer function, which can be used for the stability analysis of a linear control system. We also formalize the active realization of various controllers, such as PID, PD, PI, P, I, D, and various compensators, such as lag and lead. Finally, we formalize the passive realization of the various compensators, such as lag, lead and lag-lead and verified the corresponding behavioral (differential equation) and the transfer function specifications. To facilitate the usage of these formalizations in analyzing real-world linear control systems, we developed some simplification and automatic verification tactics, in particular the tactic TRANSFER FUN TAC , which automatically verifies the transfer function of any real-world linear control system based on its differential equation. These foundations can be used to analyze a wide range of linear control systems and for illustration purposes, the paper presents the formal analysis of an unmanned free-swimming submersible vehicle.
In future, we plan to link the proposed formalization with Simulink so that the users can provide the system model as a block diagram. This diagram can be used to extract the corresponding transfer function [3], which can in turn be formally verified, almost automatically, to be equivalent to the corresponding block diagram based on the reported formalization and reasoning support.
## Acknowledgements
This work was supported by the National Research Program for Universities grant (number 1543) of Higher Education Commission (HEC), Pakistan.
## References
1. Ahmad, M., Hasan, O.: Formal Verification of Steady-State Errors in UnityFeedback Control Systems. In: Formal Methods for Industrial Critical Systems. pp. 1-15. Springer (2014)
2. ArΒ΄ echiga, N., Loos, S.M., Platzer, A., Krogh, B.H.: Using Theorem Provers to Guarantee Closed-loop System Properties. In: American Control Conference (ACC), 2012. pp. 3573-3580. IEEE (2012)
3. Babuska, R., Stramigioli, S.: Matlab and Simulink for Modeling and Control. Delft University of Technology (1999)
4. Beerends, R.J., Morsche, H.G., Van den Berg, J.C., Van de Vrie, E.M.: Fourier and Laplace Transforms. Cambridge University Press, Cambridge (2003)
5. Beillahi, S.M., Siddique, U., Tahar, S.: Formal Analysis of Power Electronic Systems. In: Formal Engineering Methods. pp. 270-286. Springer (2015)
6. Boulton, R.J., Hardy, R., Martin, U.: A Hoare Logic for Single-input Single-output Continuous-time Control Systems. In: International Workshop on Hybrid Systems: Computation and Control. pp. 113-125. Springer (2003)
7. Ghosh, S.: Control Systems, vol. 1000. Pearson Education (2010)
8. Harrison, J.: HOL Light: A Tutorial Introduction. In: Formal Methods in Computer-Aided Design. LNCS, vol. 1166, pp. 265-269. Springer (1996)
9. Harrison, J.: The HOL Light Theory of Euclidean Space. Journal of Automated Reasoning 50(2), 173-190 (2013)
10. Hasan, O., Ahmad, M.: Formal Analysis of Steady State Errors in Feedback Control Systems using HOL-Light. In: Design, Automation and Test in Europe. pp. 14231426 (2013)
11. Hasan, O., Tahar, S.: Formal verification methods. Encyclopedia of Information Science and Technology, IGI Global Pub pp. 7162-7170 (2015)
12. Johnson, M.E.: Model Checking Safety Properties of Servo-loop Control Systems. In: Dependable Systems and Networks. pp. 45-50. IEEE (2002)
13. Kondo, H., Ura, T.: Navigation of an AUV for Investigation of Underwater Structures. Control Engineering Practice 12(12), 1551-1559 (2004)
14. Lutovac, M., ToΛ siΒ΄ c, D.: Symbolic Analysis and Design of Control Systems using Mathematica. International Journal of Control 79(11), 1368-1381 (2006)
15. Nise, N.S.: Control Systems Engineering. John Wiley & Sons (2007)
16. Ogata, K., Yang, Y.: Modern Control Engineering (1970)
17. Rashid, A.: Formal Analysis of Linear Control Systems using Theorem Proving. http://save.seecs.nust.edu.pk/projects/falcstp (2017)
18. Rashid, A., Hasan, O.: On the Formalization of Fourier Transform in Higher-order Logic. In: International Conference on Interactive Theorem Proving. LNCS, vol. 9807, pp. 483-490. Springer (2016)
19. Rashid, A., Hasan, O.: Formalization of Transform Methods using HOL Light. In: Conference on Intelligent Computer Mathematics. LNAI, vol. 10383, pp. 319-332. Springer (2017)
20. Taqdees, S.H., Hasan, O.: Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light. In: Logic for Programming, Artificial Intelligence, and Reasoning. pp. 744-758. Springer (2013)
21. Taqdees, S.H., Hasan, O.: Formally Verifying Transfer Functions of Linear Analog Circuits. IEEE Design & Test, http://save.seecs.nust.edu.pk/pubs/2017/ DTnA\_2017.pdf (2017)
22. Tiwari, A., Khanna, G.: Series of Abstractions for Hybrid Automata. In: Hybrid Systems: Computation and Control. pp. 465-478. Springer (2002)
23. Wernli, R.L.: Low Cost UUV's for Military Applications: Is the Technology Ready? In: Pacific Congress on Marine Science and Technology (2001)
24. Willcox, S., Vaganay, J., Grieve, R., Rish, J.: The Bluefin BPAUV: An Organic Widearea Bottom Mapping and Mine-hunting Vehicle. Unmanned Untethered Submersible Technology (2001)