# A Deductive Approach towards Reasoning about Algebraic Transition Systems

Authors: Jun Fu; Jinzhao Wu; Hongyan Tan
Journal: Mathematical Problems in Engineering
 (2015)

---

## Abstract

Algebraic transition systems are extended from labeled transition systems by allowing transitions labeled by algebraic equations for modeling more complex systems in detail. We present a deductive approach for specifying and verifying algebraic transition systems. We modify the standard dynamic logic by introducing algebraic equations into modalities. Algebraic transition systems are embedded in modalities of logic formulas which specify properties of algebraic transition systems. The semantics of modalities and formulas is defined with solutions of algebraic equations. A proof system for this logic is constructed to verify properties of algebraic transition systems. The proof system combines with inference rules decision procedures on the theory of polynomial ideals to reduce a proof-search problem to an algebraic computation problem. The proof system proves to be sound but inherently incomplete. Finally, a typical example illustrates that reasoning about algebraic transition systems with our approach is feasible.


---

## Body

## 1. Introduction

System verification requires a mathematical structure on which the system in question is described precisely.Labeled transition systems [1] are such structures proposed for this purpose, which are widely used to specify hardware and software systems [2], for example, integrated circuit system, communication protocols, and concurrent algorithms. A labeled transition system is a specified transition system (first presented by Keller [3]) whose transitions are labeled by abstract labels. Abstract labels are sufficient for modelling atomic actions which trigger transitions of systems, but they are insufficient to describe enough details on transitions of complex systems. For instance, we concern much with the details on how a train reduces its speed in the brake mode, which is usually specified by mathematical equations.Algebraic transition systems [4] are extended from labeled transition systems by labeling transitions with algebraic assertions, which are conjunctions of polynomial equations. Transitions labeled with algebraic assertions are able to describe how states change according to those polynomial equations. That is very necessary for modelling complex systems. What is more significant is that many mathematical techniques on polynomials are available to the analysis of complex systems, such as the theory of polynomial ideals [5]. On the other hand, conventional methods are not competent for the verification for algebraic transition systems due to the complexity of algebraic assertions. To the best of our knowledge, there is no approach for reasoning about algebraic transition systems. Our study is motivated mainly by this.Our approach is related totheorem proving which is a well-established verification method of labeled transition systems. The theorem proving method [6, 7] tries to find a proof of the desired property, which is written as a theorem in logic languages. Another verification method, calledmodel checking, uses a finite-state traversal technique algorithm [8, 9]. Hence model checking method automatically checks whether a given system satisfies the desired properties by traversing the state space of the system. However, model checking requires systems to be finite-state systems or those systems whose state space can be divided into finite quotient subspaces [10, 11]. While theorem proving method is not restricted by finite-state systems and hence applies to complex systems, most of which have infinite state spaces. Since the state spaces of algebraic transition systems are defined on R
n which is infinite, we choose theorem proving method to verify of algebraic transition systems.Inspired by [4, 12–14], we present a deductive approach for specifying and verifying algebraic transition systems. Our approach includes a modification of dynamic logic (A
D
L) and a proof system for A
D
L. The A
D
L is extended from dynamic logic [15] by allowing algebraic equations in modalities. There are two standard modalities [
α
] and α where α is defined with algebraic equations. The [
α
] refers to the states reachable by all runs of α, while α indicates the states reachable by some runs of α. The formal semantics of modalities is defined with zero sets of polynomials. These modalities embedded in logical formulas are used to model behaviors of algebraic transition systems. The properties of algebraic transition systems are specified with A
D
L formulas. The satisfaction of formulas is defined with zero sets of polynomials and the semantics of modalities. For deciding whether the desired properties are satisfied, a proof system of the sequent-calculus style, called A
D
L calculus, is constructed. This proof system aims to find a proof of the desired properties with inference rules. Several special rules are customized to handle modalities with algebraic equations by reducing the proof-search problem to an algebraic computation problem. The algebraic computation procedures enhance the reasoning power of our proof systems. The proof system is proved to be sound but inherently incomplete as many other proof systems. Reasoning about algebraic transition systems with our approach is demonstrated with a typical example.In recent decades, the deductive approach for specifying and verifying transition systems has received fruitful results [16]. T
L
A
+ [17] is a specification language designed by Lamport for formally describing and reasoning about distributed systems. Systems are specified in T
L
A
+ as formulas of the Temporal Logic of Actions (TLA) [6], which is a variant of temporal logic. The T
L
A
+ proof system (TLAPS) [18, 19] is a general platform for development of T
L
A
+ proofs. A whole proof in TLAPS is decomposed into a collection of subproofs which are sent to backend verifiers including SMT solvers, theorem provers, and proof assistants. Compared with T
L
A
+ and TLAPS, our approach is designed for the direct proof of properties on algebraic transitions. With our approach the proof problem is reduced to an algebraic computation problem such as the ideal membership problem on ideal theory. Our proof system can be considered as a backend verifier of TLAPS for algebraic transition systems.Combined with mathematical procedures, the deductive approach can be used for the verification of more complex systems, for example, real-time systems and reactive systems [20–22]. Platzer [12, 23] developed a deductive framework for the verification of hybrid systems, which are dynamic systems containing continuous evolutions and discrete transitions. A discrete transition in [12] is specified as an explicit assignment of a variable. For instance, the primed variable x
′ in the discrete transition x
′
=
f
(
x
1
,
…
,
x
n
), which assigns the value of f
(
x
1
,
…
,
x
n
) to x
′, can be immediately eliminated by a replacement with f
(
x
1
,
…
,
x
n
). In contrast, a transition in algebraic transition system is modelled as an algebraic equation. Consider the transition f
(
x
′
,
x
1
,
…
,
x
n
)
=
0 as an example. The primed variable x
′ in this transition will be directly eliminated only if x
′ can be equivalently written as a polynomial on x
1
,
…
,
x
n, such as x
′
=
f
′
(
x
1
,
…
,
x
n
). In most cases, the transitions in algebraic transition systems generalise the discrete parts of hybrid systems. Algebraic transition systems cannot simply be seen as subsets of hybrid systems and therefore are not covered by usual methods. Somehow our approach can be considered as a complement to usual methods for verifying complex systems.The rest of this paper is organized as follows. Section2 presents some preliminary concepts and some theorems which lie in the core of our approach. We introduce our understanding of algebraic transition systems in Section 3. The algebraic modification of dynamic logic is described in Section 4. In Section 5 we construct a proof system for this logic and prove the soundness and inherent incompleteness of the proof system in Section 7. Our approach is illustrated by reasoning about a train control system in Section 6. Section 8 concludes with some ideas for future work.


## 2. Preliminary

In this section, we introduce several important conclusions on polynomial ideal theory, which lie in the core of our approach.We begin with the concepts of polynomials and ideals. LetN be the set of natural numbers including 0, R the set of reals, and C the set of complex numbers obtained as thealgebraic closure of the reals. Let V
=
{
x
1
,
…
,
x
n
} be a set of variables. The set of polynomials on the variables, whose coefficients are drawn from the reals, is denoted by R
[
x
1
,
…
,
x
n
].Definition 1 (zero set).
Letf
(
x
1
,
…
,
x
n
)
∈
R
[
x
1
,
…
,
x
n
] be a polynomial on V; the zero set of f
(
x
1
,
…
,
x
n
), denoted by Z
e
r
o
(
f
), is the set of points in the complex plane such that(1)
Z
e
r
o
f
=
z
→
∈
C
n
∣
f
z
→
=
0
,where f
(
z
→
) is obtained from f
(
x
1
,
…
,
x
n
) by replacing all variables with the elements of the point z
→.We writef instead of f
(
x
1
,
…
,
x
n
) when the variables are understood in the context. Let F
=
{
f
1
,
…
,
f
s
} be a finite set of polynomials over R
[
x
1
,
…
,
x
n
]; its corresponding zero set is defined as(2)
Z
e
r
o
F
=
z
→
∈
C
n
∣
f
i
z
→
=
0
,
∀
1
≤
i
≤
s
.We say the polynomial f
vanishes at the set Z
e
r
o
(
F
) if f
(
z
→
)
=
0 for all z
→
∈
Z
e
r
o
(
F
).Definition 2 (ideals).
A subsetI
⊆
R
[
x
1
,
…
,
x
n
] is an ideal, if and only if(1)
0
∈
I;
(2)
for allf
1, f
2
∈
I, (
f
1
+
f
2
)
∈
I;
(3)
iff
∈
I and g
∈
R
[
x
1
,
…
,
x
n
], then f
g
∈
I, where f
g indicates the product of polynomials f, g.An ideal generated by a set of polynomialsF
=
{
f
1
,
…
,
f
s
}, denoted by F, is the smallest ideal containing F and equivalently(3)
F
=
∑
i
=
1
s
g
i
f
i
∣
g
i
∈
R
x
1
,
…
,
x
n
,
∀
1
≤
i
≤
s
.The ideal F is said to be finitely generated if the set F is finite. Hilbert’s basis theorem says that every ideal in C
[
x
1
,
…
,
x
n
] is finitely generated.The basic relation of an ideal and its generators is that they have the same zero set according to the following theorem.Theorem 3.
Given an idealI
=
F generated by F
=
{
f
1
,
…
,
f
s
}, then the zero set of I and the zero set of F are the same:(4)
Z
e
r
o
I
=
Z
e
r
o
F
.Proof.
(1) SinceF
⊂
I, we immediately conclude that Z
e
r
o
(
F
)
⊃
Z
e
r
o
(
I
). That is, (5)
z
→
∈
Z
e
r
o
I
⟹
∀
f
∈
I
f
z
→
=
0
⟹
∀
f
∈
F
f
z
→
=
0
⟹
z
→
∈
Z
e
r
o
F
.(2) Conversely, (6)
z
→
∈
Z
e
r
o
F
⟹
f
1
z
→
=
⋯
=
f
s
z
→
=
0
⟹
∀
h
=
g
1
f
1
+
⋯
+
g
s
f
s
h
z
→
=
0
⟹
∀
h
∈
I
h
z
→
=
0
⟹
z
→
∈
Z
e
r
o
I
.Definition 4 (radical ideal).
LetI
⊂
R
[
x
1
,
…
,
x
n
] be an ideal. Theradical of I, denoted by I, is the set(7)
I
=
f
∣
∃
n
∈
N
f
n
∈
I
.The following theorem asserts a significant relation between zero sets and ideal membership, which is the underlying algebraic principle of axiom rules in Section5.Theorem 5.
Givenf
,
f
1
,
…
,
f
s
∈
R
[
x
1
,
…
,
x
n
] and F
=
{
f
1
,
…
,
f
s
}, if there is an integer q
∈
N such that f
q
∈
F, that is, f
∈
F, then f vanishes at the zero set of F; that is, Z
e
r
o
(
F
)
⊂
Z
e
r
o
(
f
). Equivalently,(8)
f
∈
F
⟹
Z
e
r
o
F
⊂
Z
e
r
o
f
.Proof.
This theorem immediately corresponds to one direction of the famous theorem calledHilbert’s Nullstellensatz. The proof of Hilbert’s Nullstellensatz can be found in [5].A fundamental question in ideal theory is checking whether a given polynomial belongs to the radical of an ideal, which is known asradical membership problem. This problem involves the following theorem.Theorem 6.
Letf
∈
R
[
x
1
,
…
,
x
n
] be a polynomial and let I
=
f
1
,
…
,
f
s
⊆
R
[
x
1
,
…
,
x
n
] be an ideal. Then f belongs to the radical of the ideal I if and only if the constant 1 belongs to the ideal I
~
=
f
1
,
…
,
f
s
,
1
-
y
f
⊂
R
[
x
1
,
…
,
x
n
,
y
]; that is,(9)
f
∈
I
⟺
1
∈
f
1
,
…
,
f
s
,
1
-
y
f
,where y is a new variable different from x
1
,
…
,
x
n.Proof.
A proof of this theorem can be found in any standard text on ideal theory (see Proposition  8 in  [5]).The core of solving radical membership problem requires a special kind of generators, calledreduced Gröbner basis. Every ideal of R
[
x
1
,
…
,
x
n
] has a unique finite reduced Gröbner basis [24]. To determine if f
∈
f
1
,
…
,
f
s
⊂
R
[
x
1
,
…
,
x
n
], we compute the reduced Gröbner basis of the ideal f
1
,
…
,
f
s
,
1
-
y
f
⊂
R
[
x
1
,
…
,
x
n
,
y
]. If the result is {
1
}, then f
∈
I. Otherwise, f
∉
I.Another application of reduced Gröbner basis, shown by the following theorem, is deciding whether there exists a zero set for a finite set of polynomials.Theorem 7.
LetF
⊂
R
[
x
1
,
…
,
x
n
] be a finite set of polynomials and G the reduced Gröbner basis for F. Then F has an empty zero set if and only if 1
∈
G; that is, Z
e
r
o
(
F
)
=
∅
⇔
1
∈
G.Proof.
A proof of this theorem can be found in Corollary  4.3.7 in text [24].


## 3. Algebraic Transition Systems

In this section, we demonstrate how algebraic assertions enrich the abstract labels of labeled transition systems.Definition 8 (algebraic assertions).
Analgebraic assertion
ψ over the set of variables V is defined as a finite union of polynomial equations of the form(10)
ψ
≝
f
1
=
0
∧
f
2
=
0
∧
⋯
∧
f
s
=
0
,where, for each 1
≤
i
≤
s, f
i
∈
R
[
x
1
,
…
,
x
n
].For an algebraic assertionψ, its zero set is defined as(11)
Z
e
r
o
ψ
=
v
→
∈
C
n
∣
f
i
v
→
=
0
,
∀
1
≤
i
≤
s
.We say that a point v
→
∈
C
n satisfies ψ, denoted by v
→
⊨
ψ, if v
→ belongs to the zero set of ψ; that is, v
→
∈
Z
e
r
o
(
ψ
).An algebraic transition system is specialized from a labeled transition system. Each transition of an algebraic transition system is labeled with an algebraic assertion instead of an abstract label.Definition 9 (algebraic transition system).
An algebraic transition systemA is a tuple A
=
S
,
T
,
Ψ
,
λ, where (i)
S is the set of states;
(ii)
T
⊂
S
×
S is the set of transitions;
(iii)
Ψ is a set of algebraic assertions on V
∪
V
′ including the null label τ;
(iv)
λ
:
T
→
Ψ is a label function assigning each transition to an algebraic assertion.For an algebraic transition systemA, a state s
∈
S is a function which maps each variable in V to a real. According to the label function λ, each transition t
∈
T is labeled with an algebraic assertion denoted by λ
(
t
)
∈
Ψ. The algebraic assertion λ
(
t
) is defined on V
∪
V
′, where V denotes the current-state variables and V
′ denotes the next-state variables.The transition relation ofA, which describes how states change, is defined by algebraic assertions on V
∪
V
′. For each t
∈
T, the transition relation ρ
t is determined by the label λ
(
t
) as follows:(12)
ρ
t
=
s
,
s
′
∣
s
,
s
′
∈
S
∧
λ
t
s
,
s
′
=
0
,where s, s
′ indicate the current state and the next state, respectively, and λ
(
t
)
(
s
,
s
′
) is evaluated by substituting each variable v
∈
V of λ
(
t
) with the corresponding value in s and each variable v
′
∈
V
′ with the corresponding value in s
′, respectively. In particular, the null label τ specifies an identical relation on S; that is, ρ
τ
=
s
,
s
∣
s
∈
S. The transition labeled by ψ from s to s
′ is denoted by s
→
ψ
s
′.An algebraic transition system isdeterministic if there is at most one transition and one label for any state; otherwise it isnondeterministic. As for a deterministic algebraic transition system, the next state is determined uniquely by the current state. For instance, given an algebraic assertion ψ
≝
x
′
-
x
-
1
=
0, the next state is obtained by adding 1 to the variable x in the current state. We say the transition labeled by ψ is deterministic and nondeterministic if ψ
≝
(
x
′
)
2
-
x
2
-
3
x
-
2
=
0 (because the next state can take x
′
=
x
+
1 or x
′
=
x
+
2). Obviously, an algebraic transition must be deterministic if for all ψ
∈
Ψ each variable x
′
∈
V
′ in ψ can be written as a unique polynomial over V. In this case, each algebraic assertion can be written as ψ
≝
⋀
i
x
i
′
=
f
i
(
x
1
,
…
,
x
n
) with each x
i
′
∈
V
′ and x
1
,
…
,
x
n
∈
V. Hence the value of each variable x
i
′ in the next state is uniquely determined by x
1
,
…
,
x
n in the current state according to f
i
(
x
1
,
…
,
x
n
).Definition 10 (run).
Given an algebraic transition systemA
=
S
,
T
,
Ψ
,
λ, a run σ of A is defined by a sequence of transitions as follows:(13)
σ
:
s
0
⟶
ψ
0
s
1
⟶
ψ
1
s
2
⋯
,where the ith element of σ is denoted by σ
i and for each i
≥
0 there exists a transition σ
i
=
s
i
,
s
i
+
1
∈
T from state s
i
∈
S to state s
i
+
1
∈
S such that(14)
λ
σ
i
=
ψ
i
,
ψ
i
s
i
,
s
i
+
1
=
0
.Example 11.
In order to illustrate algebraic transition systems, we present a simplified train control system shown in Figure1. Assume that a train has two modes: the acceleration mode (A
c
c) and the deceleration mode (D
e
c). The train keeps checking the current mode and velocity. If it is in mode A
c
c and its velocity reaches 10, it will invert the acceleration power (a
=
-
a) and change its mode to mode D
e
c. Then the position s of the train evolves with velocity v along s
=
s
+
v
Δ
t and v
=
v
+
a
Δ
t. If the velocity of the train slows down to 5 in mode D
e
c, it will invert its deceleration power (a
=
-
a) and switch to mode A
c
c. Compared with real-time systems and hybrid system, the behavior of algebraic transition systems is discrete, such as the discrete behavior of the train with time period Δ
t. Note that we use the relaxed version of algebraic assertions. For instance, we write a
′
=
-
a as the relaxed version of a
′
+
a
=
0. The D
e
c and A
c
c can be any certain constants.Figure 1
A simple train control system.In contrast with classical labeled transition systems with abstract labels [3], algebraic transitions systems are widely useful for modeling data flows, due to algebraic assertions describing how data changes between states in detail. What is more significant is that the introduction of concepts on ideal theory leads to the presence of more powerful and efficient algebraic methods for reasoning about complex systems.


## 4. Algebraic Dynamic Logic

In this section, we present algebraic dynamic logic (A
D
L), in which algebraic transition systems are modeled as modalities by modifying first-order dynamic logic. Properties about the behavior of algebraic transition systems can be expressed as A
D
L formulas. After introducing the syntax of algebraic programs and formulas, we define an algebraic semantics of A
D
L, according to algebraic transition systems as mentioned in Section 3.


### 4.1. Syntax

The formulas ofA
D
L are strings built over a finite set V
=
{
x
1
,
…
,
x
n
} of real-valued variables and a signature S
i
g consisting of function symbols, predicate symbols, and constant symbols. In algebraic dynamic logic, modalities are extended toalgebraic programs which are the combination of algebraic assertions and operational connectives.Definition 12 (algebraic programs).
The set ofalgebraic programs
P
r
m
(
V
,
S
i
g
) is defined inductively as follows. (i)
Ifψ is an algebraic assertion on V
∪
V
′ defined in Definition 8, then theassignment
ψ
∈
P
r
m
(
V
,
S
i
g
) is an algebraic program.
(ii)
Ifψ is an algebraic assertion on V, then theguard
ψ
?
∈
P
r
m
(
V
,
S
i
g
) is an algebraic program.
(iii)
Ifα and β are algebraic programs, then thesequential composition
α
;
β
∈
P
r
m
(
V
,
S
i
g
).
(iv)
Ifα and β are algebraic programs, then thenondeterministic choice
α
∪
β
∈
P
r
m
(
V
,
S
i
g
).
(v)
Ifα is an algebraic program, then theiteration
α
∗
∈
P
r
m
(
V
,
S
i
g
).As previously mentioned, the effect of an assignmentψ
≝
⋀
i
f
i
x
1
,
…
,
x
n
,
x
1
′
,
…
,
x
n
′
=
0 is specified as a transition relation of algebraic transition systems. Furthermore, each f
i of ψ simultaneously takes place to change the current state. Assignments in computer programming languages are special cases of algebraic assertions since each next-state variable can easily be written as a unique polynomial in current-state variables according to assignment statements. The guard ψ
? is used to check whether the subsequent transition is possible. For the guard of (
ψ
?
;
α
), the program α is allowed to happen, only when ψ is satisfied in the current state. Not all programs need a guard. Any program without a guard always takes place. The program α
;
β says that β is executed after doing α. The program α
∪
β means that one of α and β is nondeterministically chosen and executed, and the program α
∗ says that α is executed some finite number of times.Due to the operational structure of programs in standard dynamic logic [15], an algebraic transition system can be translated into an algebraic program without effort. Algebraic programs encode algebraic transition systems into modalities of A
D
L formulas, which specify properties of algebraic transition systems according to the following definition.Definition 13 (formulas).
The set ofA
D
L formulas F
r
m
(
V
,
S
i
g
) is obtained inductively as follows. (i)
Iff
(
x
1
,
…
,
x
n
)
∈
R
[
x
1
,
…
,
x
n
] is a polynomial defined over V, then f
(
x
1
,
…
,
x
n
)
=
0
∈
F
r
m
(
V
,
S
i
g
) is anatomic formula.
(ii)
Ifϕ
,
φ
∈
F
r
m
(
V
,
S
i
g
), then ¬
ϕ
,
(
ϕ
∧
φ
)
,
(
ϕ
∨
φ
)
,
(
ϕ
→
φ
)
∈
F
r
m
(
V
,
S
i
g
).
(iii)
Ifϕ
∈
F
r
m
(
V
,
S
i
g
) and x
∈
V, then ∀
x
ϕ, ∃
x
ϕ
∈
F
r
m
(
V
,
S
i
g
).
(iv)
Ifϕ
∈
F
r
m
(
V
,
S
i
g
) and α
∈
P
r
m
(
V
,
S
i
g
), then [
α
]
ϕ
,
α
ϕ
∈
F
r
m
(
V
,
S
i
g
).The existential quantification can be defined with universal quantification and∃
x
ϕ is abbreviated to ¬
∀
x
¬
ϕ. The relation between [
α
]
ϕ and α
ϕ is α
ϕ
≝
¬
α
¬
ϕ. The formula [
α
]
φ expresses that all runs of program α lead to the states on which the formula φ holds. Likewise, α
ϕ means that there exists at least a run of program α after which the formula φ holds. As for [
α
]
ϕ and α
ϕ, the algebraic program α plays the role of encoding an algebraic transition system, while ϕ claims that behavior of the algebraic transition system satisfies the property specified by ϕ. For example, the formula x
′
=
0
;
(
x
′
=
x
+
1
)
∗  (
x
-
3
=
0
) asserts that there exists a run during the loop of x
′
=
x
+
1 such that x reaches 3 eventually.Variables occurring in the scope of the quantifiers∀ and ∃ arebound to quantifiers, and variables of V
′ occurring in modalities arebound to modalities. Variables arefree if they are not in the scope of quantifiers and modalities. We assume that all variables are not bound to both of quantifiers and modalities at the same time. The interaction of quantifiers ∀, ∃ and modalities ·, · makes the formulas subtle. Particularly, the order of quantifiers occurring before and after modalities makes the understanding of formulas slightly different. For instance, ∀
x
x
′
=
x
ϕ means that all the choices of the parameter x valued to x
′ keep ϕ true. However, for x
′
=
x
∀
x
ϕ, the variable x in x
′
=
x is free and different from x in ∀
x
ϕ which is a parameter and can be substituted with another variable symbol not occurring in ϕ. The way of unifying quantification and modalities in [15] is using a specialwildcard assignment to redefine quantification such that ∀
x
ϕ
↔
x
′
=
?
ϕ and ∃
x
ϕ
↔
x
′
=
?
ϕ, where the wildcard assignment x
′
=
? indicates an arbitrary assignment to x.Example 14.
We formalize the train control system shown in Figure1 into the following algebraic program:(15)
t
r
a
i
n
≝
A
c
∪
D
c
;
d
r
i
v
e
∗
,where(16)
A
c
≝
m
o
d
e
-
A
c
c
=
0
?
;
v
-
10
=
0
?
;
a
′
+
a
=
0
∧
m
o
d
e
′
-
D
e
c
=
0
D
c
≝
m
o
d
e
-
D
e
c
=
0
?
;
v
-
5
=
0
?
;
a
′
+
a
=
0
∧
m
o
d
e
′
-
A
c
c
=
0
d
r
i
v
e
≝
v
′
-
v
-
a
Δ
t
=
0
∧
s
′
-
s
-
v
Δ
t
=
0
.
We use nondeterministic choice∪ to join A
c and D
c together. In the phase of A
c, it tests whether the current mode is A
c
c and then checks whether the current velocity reaches 10. If so, the mode switches to D
e
c and the acceleration power a is inverted. The subsequent action is executing d
r
i
v
e in which the velocity v and the position z evolve along v
′
-
v
-
a
Δ
t
=
0 and s
′
-
s
-
v
Δ
t
=
0, respectively. The phase of D
c is similar to A
c. The control system repeats (
A
c
∪
D
c
;
d
r
i
v
e
) for indefinitely many times (or forever).
Furthermore, we express properties of the train control system asA
D
L formulas. For instance, the following statement about the train control system “the velocity of the train never reaches 11” is equivalently expressed as the formula(17)
t
r
a
i
n
¬
v
-
11
=
0
.


### 4.2. Semantics

The semantics ofA
D
L is defined in the fashion of Kripke [25], where possible worlds represent states of algebraic transition systems and transition relations along the runs of algebraic transition systems are represented as the accessibility relation.For the setV and signature S
i
g, aninterpretation
I is a map, which maps each function symbol in S
i
g to an algebraic assertion on V
∪
V
′ and each predicate symbol in S
i
g to an algebraic assertion on V. Astate is a map s
:
V
→
R assigning a real value in R to eachstate variable in V whose value is only changed by algebraic programs. The free variables in V are mapped to the reals by anassignment
ζ
:
V
→
R. These variables are also namedlogical variables. There is no need to distinguish logical variables and state variables except for the clarity of expressions.The semantics of an algebraic program is interpreted as a transition relation consisting of pairs of states, while the satisfaction of anA
D
L formula is interpreted as a Boolean value by a state with respect to an interpretation and an assignment. We begin with the semantics of algebraic programs.Definition 15 (semantics of algebraic programs).
For each algebraic programα
∈
P
r
m
(
V
,
S
i
g
), its semantics, denoted by γ
(
α
), specifies the state w which is reachable from the state v under the operation of α. γ
(
α
) is inductively defined as follows. (i)
γ
(
α
)
=
v
,
w
∣
v
,
w
∈
Z
e
r
o
ψ if α
≝
ψ, where ψ is an algebraic assertion on V
∪
V
′.
(ii)
γ
(
α
)
=
v
,
v
∣
v
∈
Z
e
r
o
ψ if α
≝
ψ
?, where ψ is an algebraic assertion on V.
(iii)
γ
(
α
;
β
)
=
v
,
w
∣
v
,
z
∈
γ
α and z
,
w
∈
γ
β, for some state z.
(iv)
γ
(
α
∪
β
)
=
γ
(
α
)
∪
γ
(
β
).
(v)
(
v
,
w
)
∈
γ
(
α
∗
) if and only if there is a n
∈
N and a state sequence v
=
v
0
,
…
,
v
n
=
w, with (
v
i
,
v
i
+
1
)
∈
γ
(
α
) for all 0
≤
i
<
n.Note that the semantics of an algebraic program is defined according to zero sets of the algebraic assertion. Letα
≝
ψ be an algebraic program with the algebraic assertion ψ
≝
⋀
i
f
i
=
0 on V
∪
V
′; the semantics of α is the common zero set of all f
i. For example, the semantics of (
x
+
1
)
2
-
(
x
′
)
2
=
0 is the set of points lying on the two lines x
′
-
x
-
1
=
0 and x
′
+
x
+
1
=
0 in the x
-
x
′ plane. There may exist more than one successive state for the current state. In most cases, the successive states of a given state are uniquely determined by algebraic programs. The guards in the form of ψ
? are associated with those states which satisfy the algebraic assertion ψ for triggering the next program. An iteration α
∗ points out all states reachable from the state v by successively executing α nondeterministically many times (zero or more).The satisfaction of anA
D
L formula ϕ involves an interpretation I, an assignment ζ, and a state v. For a formula ϕ, we write I
,
ζ
,
v
⊨
ϕ and say that v and ζ satisfy ϕ in I or that ϕ is true in state v with respect to I and ζ. We omit I, ζ and write v
⊨
ϕ when I and ζ are understood in the context. The notation v
⊭
ϕ means that v does not satisfy ϕ. We use ζ
[
x
↦
c
] to denote themodification of the assignment ζ that agrees with ζ except for the variable x which is amended to c
∈
R.Definition 16 (satisfaction of formulas).
For twoA
D
L formulas ϕ and φ, the satisfaction is inductively defined according to the syntactic structure of ϕ and φ. (1)
I
,
ζ
,
v
⊨
f
(
x
1
,
…
,
x
n
)
=
0 if and only if v
∈
Z
e
r
o
(
f
).
(2)
I
,
ζ
,
v
⊨
¬
ϕ if and only if I
,
ζ
,
v
⊭
ϕ.
(3)
I
,
ζ
,
v
⊨
ϕ
∧
φ if and only if I
,
ζ
,
v
⊨
ϕ and I
,
ζ
,
v
⊨
φ. Similarly, for ϕ
∨
φ, ϕ
→
φ.
(4)
I
,
ζ
,
v
⊨
∀
x
ϕ if and only if I
,
ζ
[
x
↦
c
]
,
v
⊨
ϕ for all c
∈
R.
(5)
I
,
ζ
,
v
⊨
∃
x
ϕ if and only if I
,
ζ
[
x
↦
c
]
,
v
⊨
ϕ for some c
∈
R.
(6)
I
,
ζ
,
v
⊨
[
α
]
ϕ if and only if I
,
ζ
,
w
⊨
ϕ for all states w with (
v
,
w
)
∈
γ
(
α
).
(7)
I
,
ζ
,
v
⊨
〈
α
〉
ϕ if and only if I
,
ζ
,
w
⊨
ϕ for some state w with (
v
,
w
)
∈
γ
(
α
).A formulaϕ isvalid in I and written as I
⊨
ϕ if ϕ is true on all states and all assignments in interpretation I. If I
⊨
ϕ for all interpretations I, we write ⊨
ϕ and say that ϕ isvalid.After giving the semantics of algebraic dynamic logic, in order to prove the validity ofA
D
L formulas, such as (17), we construct a proof system for A
D
L in the next section.


## 4.1. Syntax

The formulas ofA
D
L are strings built over a finite set V
=
{
x
1
,
…
,
x
n
} of real-valued variables and a signature S
i
g consisting of function symbols, predicate symbols, and constant symbols. In algebraic dynamic logic, modalities are extended toalgebraic programs which are the combination of algebraic assertions and operational connectives.Definition 12 (algebraic programs).
The set ofalgebraic programs
P
r
m
(
V
,
S
i
g
) is defined inductively as follows. (i)
Ifψ is an algebraic assertion on V
∪
V
′ defined in Definition 8, then theassignment
ψ
∈
P
r
m
(
V
,
S
i
g
) is an algebraic program.
(ii)
Ifψ is an algebraic assertion on V, then theguard
ψ
?
∈
P
r
m
(
V
,
S
i
g
) is an algebraic program.
(iii)
Ifα and β are algebraic programs, then thesequential composition
α
;
β
∈
P
r
m
(
V
,
S
i
g
).
(iv)
Ifα and β are algebraic programs, then thenondeterministic choice
α
∪
β
∈
P
r
m
(
V
,
S
i
g
).
(v)
Ifα is an algebraic program, then theiteration
α
∗
∈
P
r
m
(
V
,
S
i
g
).As previously mentioned, the effect of an assignmentψ
≝
⋀
i
f
i
x
1
,
…
,
x
n
,
x
1
′
,
…
,
x
n
′
=
0 is specified as a transition relation of algebraic transition systems. Furthermore, each f
i of ψ simultaneously takes place to change the current state. Assignments in computer programming languages are special cases of algebraic assertions since each next-state variable can easily be written as a unique polynomial in current-state variables according to assignment statements. The guard ψ
? is used to check whether the subsequent transition is possible. For the guard of (
ψ
?
;
α
), the program α is allowed to happen, only when ψ is satisfied in the current state. Not all programs need a guard. Any program without a guard always takes place. The program α
;
β says that β is executed after doing α. The program α
∪
β means that one of α and β is nondeterministically chosen and executed, and the program α
∗ says that α is executed some finite number of times.Due to the operational structure of programs in standard dynamic logic [15], an algebraic transition system can be translated into an algebraic program without effort. Algebraic programs encode algebraic transition systems into modalities of A
D
L formulas, which specify properties of algebraic transition systems according to the following definition.Definition 13 (formulas).
The set ofA
D
L formulas F
r
m
(
V
,
S
i
g
) is obtained inductively as follows. (i)
Iff
(
x
1
,
…
,
x
n
)
∈
R
[
x
1
,
…
,
x
n
] is a polynomial defined over V, then f
(
x
1
,
…
,
x
n
)
=
0
∈
F
r
m
(
V
,
S
i
g
) is anatomic formula.
(ii)
Ifϕ
,
φ
∈
F
r
m
(
V
,
S
i
g
), then ¬
ϕ
,
(
ϕ
∧
φ
)
,
(
ϕ
∨
φ
)
,
(
ϕ
→
φ
)
∈
F
r
m
(
V
,
S
i
g
).
(iii)
Ifϕ
∈
F
r
m
(
V
,
S
i
g
) and x
∈
V, then ∀
x
ϕ, ∃
x
ϕ
∈
F
r
m
(
V
,
S
i
g
).
(iv)
Ifϕ
∈
F
r
m
(
V
,
S
i
g
) and α
∈
P
r
m
(
V
,
S
i
g
), then [
α
]
ϕ
,
α
ϕ
∈
F
r
m
(
V
,
S
i
g
).The existential quantification can be defined with universal quantification and∃
x
ϕ is abbreviated to ¬
∀
x
¬
ϕ. The relation between [
α
]
ϕ and α
ϕ is α
ϕ
≝
¬
α
¬
ϕ. The formula [
α
]
φ expresses that all runs of program α lead to the states on which the formula φ holds. Likewise, α
ϕ means that there exists at least a run of program α after which the formula φ holds. As for [
α
]
ϕ and α
ϕ, the algebraic program α plays the role of encoding an algebraic transition system, while ϕ claims that behavior of the algebraic transition system satisfies the property specified by ϕ. For example, the formula x
′
=
0
;
(
x
′
=
x
+
1
)
∗  (
x
-
3
=
0
) asserts that there exists a run during the loop of x
′
=
x
+
1 such that x reaches 3 eventually.Variables occurring in the scope of the quantifiers∀ and ∃ arebound to quantifiers, and variables of V
′ occurring in modalities arebound to modalities. Variables arefree if they are not in the scope of quantifiers and modalities. We assume that all variables are not bound to both of quantifiers and modalities at the same time. The interaction of quantifiers ∀, ∃ and modalities ·, · makes the formulas subtle. Particularly, the order of quantifiers occurring before and after modalities makes the understanding of formulas slightly different. For instance, ∀
x
x
′
=
x
ϕ means that all the choices of the parameter x valued to x
′ keep ϕ true. However, for x
′
=
x
∀
x
ϕ, the variable x in x
′
=
x is free and different from x in ∀
x
ϕ which is a parameter and can be substituted with another variable symbol not occurring in ϕ. The way of unifying quantification and modalities in [15] is using a specialwildcard assignment to redefine quantification such that ∀
x
ϕ
↔
x
′
=
?
ϕ and ∃
x
ϕ
↔
x
′
=
?
ϕ, where the wildcard assignment x
′
=
? indicates an arbitrary assignment to x.Example 14.
We formalize the train control system shown in Figure1 into the following algebraic program:(15)
t
r
a
i
n
≝
A
c
∪
D
c
;
d
r
i
v
e
∗
,where(16)
A
c
≝
m
o
d
e
-
A
c
c
=
0
?
;
v
-
10
=
0
?
;
a
′
+
a
=
0
∧
m
o
d
e
′
-
D
e
c
=
0
D
c
≝
m
o
d
e
-
D
e
c
=
0
?
;
v
-
5
=
0
?
;
a
′
+
a
=
0
∧
m
o
d
e
′
-
A
c
c
=
0
d
r
i
v
e
≝
v
′
-
v
-
a
Δ
t
=
0
∧
s
′
-
s
-
v
Δ
t
=
0
.
We use nondeterministic choice∪ to join A
c and D
c together. In the phase of A
c, it tests whether the current mode is A
c
c and then checks whether the current velocity reaches 10. If so, the mode switches to D
e
c and the acceleration power a is inverted. The subsequent action is executing d
r
i
v
e in which the velocity v and the position z evolve along v
′
-
v
-
a
Δ
t
=
0 and s
′
-
s
-
v
Δ
t
=
0, respectively. The phase of D
c is similar to A
c. The control system repeats (
A
c
∪
D
c
;
d
r
i
v
e
) for indefinitely many times (or forever).
Furthermore, we express properties of the train control system asA
D
L formulas. For instance, the following statement about the train control system “the velocity of the train never reaches 11” is equivalently expressed as the formula(17)
t
r
a
i
n
¬
v
-
11
=
0
.


## 4.2. Semantics

The semantics ofA
D
L is defined in the fashion of Kripke [25], where possible worlds represent states of algebraic transition systems and transition relations along the runs of algebraic transition systems are represented as the accessibility relation.For the setV and signature S
i
g, aninterpretation
I is a map, which maps each function symbol in S
i
g to an algebraic assertion on V
∪
V
′ and each predicate symbol in S
i
g to an algebraic assertion on V. Astate is a map s
:
V
→
R assigning a real value in R to eachstate variable in V whose value is only changed by algebraic programs. The free variables in V are mapped to the reals by anassignment
ζ
:
V
→
R. These variables are also namedlogical variables. There is no need to distinguish logical variables and state variables except for the clarity of expressions.The semantics of an algebraic program is interpreted as a transition relation consisting of pairs of states, while the satisfaction of anA
D
L formula is interpreted as a Boolean value by a state with respect to an interpretation and an assignment. We begin with the semantics of algebraic programs.Definition 15 (semantics of algebraic programs).
For each algebraic programα
∈
P
r
m
(
V
,
S
i
g
), its semantics, denoted by γ
(
α
), specifies the state w which is reachable from the state v under the operation of α. γ
(
α
) is inductively defined as follows. (i)
γ
(
α
)
=
v
,
w
∣
v
,
w
∈
Z
e
r
o
ψ if α
≝
ψ, where ψ is an algebraic assertion on V
∪
V
′.
(ii)
γ
(
α
)
=
v
,
v
∣
v
∈
Z
e
r
o
ψ if α
≝
ψ
?, where ψ is an algebraic assertion on V.
(iii)
γ
(
α
;
β
)
=
v
,
w
∣
v
,
z
∈
γ
α and z
,
w
∈
γ
β, for some state z.
(iv)
γ
(
α
∪
β
)
=
γ
(
α
)
∪
γ
(
β
).
(v)
(
v
,
w
)
∈
γ
(
α
∗
) if and only if there is a n
∈
N and a state sequence v
=
v
0
,
…
,
v
n
=
w, with (
v
i
,
v
i
+
1
)
∈
γ
(
α
) for all 0
≤
i
<
n.Note that the semantics of an algebraic program is defined according to zero sets of the algebraic assertion. Letα
≝
ψ be an algebraic program with the algebraic assertion ψ
≝
⋀
i
f
i
=
0 on V
∪
V
′; the semantics of α is the common zero set of all f
i. For example, the semantics of (
x
+
1
)
2
-
(
x
′
)
2
=
0 is the set of points lying on the two lines x
′
-
x
-
1
=
0 and x
′
+
x
+
1
=
0 in the x
-
x
′ plane. There may exist more than one successive state for the current state. In most cases, the successive states of a given state are uniquely determined by algebraic programs. The guards in the form of ψ
? are associated with those states which satisfy the algebraic assertion ψ for triggering the next program. An iteration α
∗ points out all states reachable from the state v by successively executing α nondeterministically many times (zero or more).The satisfaction of anA
D
L formula ϕ involves an interpretation I, an assignment ζ, and a state v. For a formula ϕ, we write I
,
ζ
,
v
⊨
ϕ and say that v and ζ satisfy ϕ in I or that ϕ is true in state v with respect to I and ζ. We omit I, ζ and write v
⊨
ϕ when I and ζ are understood in the context. The notation v
⊭
ϕ means that v does not satisfy ϕ. We use ζ
[
x
↦
c
] to denote themodification of the assignment ζ that agrees with ζ except for the variable x which is amended to c
∈
R.Definition 16 (satisfaction of formulas).
For twoA
D
L formulas ϕ and φ, the satisfaction is inductively defined according to the syntactic structure of ϕ and φ. (1)
I
,
ζ
,
v
⊨
f
(
x
1
,
…
,
x
n
)
=
0 if and only if v
∈
Z
e
r
o
(
f
).
(2)
I
,
ζ
,
v
⊨
¬
ϕ if and only if I
,
ζ
,
v
⊭
ϕ.
(3)
I
,
ζ
,
v
⊨
ϕ
∧
φ if and only if I
,
ζ
,
v
⊨
ϕ and I
,
ζ
,
v
⊨
φ. Similarly, for ϕ
∨
φ, ϕ
→
φ.
(4)
I
,
ζ
,
v
⊨
∀
x
ϕ if and only if I
,
ζ
[
x
↦
c
]
,
v
⊨
ϕ for all c
∈
R.
(5)
I
,
ζ
,
v
⊨
∃
x
ϕ if and only if I
,
ζ
[
x
↦
c
]
,
v
⊨
ϕ for some c
∈
R.
(6)
I
,
ζ
,
v
⊨
[
α
]
ϕ if and only if I
,
ζ
,
w
⊨
ϕ for all states w with (
v
,
w
)
∈
γ
(
α
).
(7)
I
,
ζ
,
v
⊨
〈
α
〉
ϕ if and only if I
,
ζ
,
w
⊨
ϕ for some state w with (
v
,
w
)
∈
γ
(
α
).A formulaϕ isvalid in I and written as I
⊨
ϕ if ϕ is true on all states and all assignments in interpretation I. If I
⊨
ϕ for all interpretations I, we write ⊨
ϕ and say that ϕ isvalid.After giving the semantics of algebraic dynamic logic, in order to prove the validity ofA
D
L formulas, such as (17), we construct a proof system for A
D
L in the next section.


## 5. Proof System

In this section, we construct a sequent calculus for algebraic dynamic logic. In a sequent calculus asequent is an expression of the form Γ
⊢
Δ, where theantecedent
Γ
=
ϕ
1
,
…
,
ϕ
m and thesuccedent
Δ
=
φ
1
,
…
,
φ
n are finite sequences of formulas. The meaning of Γ
⊢
Δ is equivalently expressed as the following formula:(18)
ϕ
1
∧
⋯
∧
ϕ
m
⟶
φ
1
∨
⋯
∨
φ
n
.That is to say, a sequent Γ
⊢
Δ is satisfied by a state v if and only if v
⊨
ϕ
1
∧
⋯
∧
ϕ
m
→
φ
1
∨
⋯
∨
φ
n. Equivalently, v makes the sequent false if v makes ϕ
1
,
…
,
ϕ
m all true and φ
1
,
…
,
φ
n all false.Aninference rule is of the form(19)
S
1
⋯
S
i
S
′
,where both S
1
⋯
S
i and S
′ are sequents. The upper sequents S
1
⋯
S
i are calledpremises and the lower sequent S
′ is calledconclusion. The semantics of an inference rule is that each state satisfying all premises also makes the conclusion true. The direction of entailment is top-down which means that premises logically imply the conclusion, while the direction of applying rules is bottom-up. That means that the procedure of reasoning about a sequent starts from the conclusion at the bottom to the premises at the top.The proof system, calledA
D
L calculus, is constructed by customizing inference rules which manipulate A
D
L formulas in an algebraic fashion. The basic idea is evaluating the effects of algebraic programs with algebraic methods mentioned in Section 2 and transforming A
D
L formulas into first-order formulas without algebraic programs. A
D
L calculus consists of axiom rules, rules for logical operators, rules for quantifier, rules for modalities, and programs.


### 5.1. Rules for Axioms

In this and the following sections, the symbolsΓ, Δ denote arbitrary sequences of A
D
L formulas and ϕ, φ denote A
D
L formulas unless otherwise noted.Four basic rulesA
1
–
A
4 listed in T
1, namedaxiom rules, are composed for closing a proof search. Rules A
1
–
A
3 are the same as in many other sequent calculus. The axiom rule A
1 treats a sequent with a common formula in the antecedent and the succedent as an axiom, which can be inferred from nothing (denoted by ⊥):T
1
A
1
⊥
Γ
,
ϕ
⊢
Δ
,
ϕ
A
2
⊥
Γ
⊢
T
r
u
e
,
Δ
A
3
⊥
Γ
,
F
a
l
s
e
⊢
Δ
A
4
⊥
Γ
,
ϕ
⊢
φ
,
Δ
.In A
4, ϕ and φ are atomic formulas which are expressed as polynomials in variables of V, and Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
).RuleA
4 is customized to coordinate mathematical procedures on ideal theory implemented by computer algebra systems, such as REDUCE, Maple, Mathematica, AXIOM, and SINGULAR. Rule A
4 reveals that any sequent whose antecedent has a formula ϕ with its zero set included by the zero set of one formula φ of the succedent can be applied as an axiom. By Theorems 5 and 6, the inclusion Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
) can be transformed into the radical membership problem which is decided byradical membership algorithm on polynomial ideals [5, 24]. That is to say, if there is an atomic formula φ in the succedent such that φ belongs to the radical of the ideal generated by polynomials in ϕ in the antecedent, that is, φ
∈
ϕ, then the sequent can be applied as an axiom. The radical membership algorithm is implemented in most computer algebra systems, such as theRadicalMembership command in Maple. The discussion on computer algebra systems is not in the scope of this paper.


### 5.2. Rules for Logical Operators

The rules inT
2 are used to handle standard logical operators. There are two cases for the appearance of each logical operator, and each logical operator needs dual rules (left rule and right rule):T
2
L
1
Γ
⊢
ϕ
,
Δ
Γ
,
¬
ϕ
⊢
Δ
L
2
Γ
,
ϕ
⊢
Δ
Γ
⊢
¬
ϕ
,
Δ
L
3
Γ
,
ϕ
,
φ
⊢
Δ
Γ
,
ϕ
∧
φ
⊢
Δ
L
4
Γ
⊢
ϕ
,
Δ
Γ
⊢
φ
,
Δ
Γ
⊢
ϕ
∧
φ
,
Δ
L
5
Γ
,
ϕ
⊢
Δ
Γ
,
φ
⊢
Δ
Γ
,
ϕ
∨
φ
⊢
Δ
L
6
Γ
⊢
ϕ
,
φ
,
Δ
Γ
⊢
ϕ
∨
φ
,
Δ
L
7
Γ
,
φ
⊢
Δ
Γ
⊢
ϕ
,
Δ
Γ
,
ϕ
⟶
φ
⊢
Δ
L
8
Γ
,
ϕ
⊢
φ
,
Δ
Γ
⊢
ϕ
⟶
φ
,
Δ
.RulesL
1
–
L
8 are standard for propositional dynamic logic. These rules decompose formulas with propositional structures into smaller formulas with less logical operators. Rules L
1 and L
2 are dual and aim to reduce the negative operator ¬. Rule L
3 just replaces the symbol ∧ with a comma, since formulas are combined conjunctively in antecedents of sequents by the definition of sequents. Rule L
4 branches the sequent containing the operator ∧ in the succedent into two sequents, since conjuncts in the succedent can be proved separately due to the semantics of sequents. Dually, rule L
5 is similar to L
4 and L
6 is similar to L
3 according to the semantics of sequents. Rule L
7 derives from rules L
5 and L
1 by the logical equivalence of (
ϕ
→
φ
) and (
¬
ϕ
∨
φ
). Similarly, rule L
8 is derived from rules L
6 and L
2.


### 5.3. Rules for Quantifiers

Recall that variables ofV
′ occurring in an algebraic program arebound to modalities. We assume that each modality-bound variable is not bound to any quantifier. A variable is free if it is not bound to modalities and quantifiers.Definition 17 (substitution).
Asubstitution of an algebraic assertion or a formula for a free variable is defined as a function which maps each object variable to a designated polynomial. Let f be a polynomial; the result of substituting f in an algebraic assertion ψ for a variable x is denoted by ψ
[
x
↦
f
]. The result of substituting f in a formula ϕ for a variable x is denoted by ϕ
[
x
↦
f
].A substitution with the resultϕ
[
x
↦
f
] isadmissible for the formula ϕ if no variables y in f are bound in the formula ϕ
[
x
↦
f
]. That is to say, free variables in f are still free in the formula ϕ
[
x
↦
f
] after applying an admissible substitution.RuleQ
1 and rule Q
4 are the usual γ-rule in [7, 26], while Q
2 and Q
3 correspond to the δ
+-rule in [26]. Rules Q
1
–
Q
4 are complete for quantifiers of classic first-order logic. That is to say, everything about quantifiers of first-order logic can be derived with Q
1
–
Q
4 [7]:T
3
Q
1
Γ
,
ϕ
x
⟼
X
,
∀
x
ϕ
⊢
Δ
Γ
,
∀
x
ϕ
⊢
Δ
Q
2
Γ
⊢
ϕ
x
⟼
f
X
1
,
…
,
X
n
,
Δ
Γ
⊢
∀
x
ϕ
,
Δ
Q
3
Γ
,
ϕ
x
⟼
f
X
1
,
…
,
X
n
⊢
Δ
Γ
,
∃
x
ϕ
⊢
Δ
Q
4
Γ
⊢
ϕ
x
⟼
X
,
∃
x
ϕ
,
Δ
Γ
⊢
∃
x
ϕ
,
Δ
.In Q
1
–
Q
4, the variable x is only bound to ∀
x or ∃
x. In Q
1 and Q
4, X is a new free variable. In Q
2 and Q
3, f is a new function symbol and X
1
,
…
,
X
n are all free variables in ∀
x
ϕ and ∃
x
ϕ.


### 5.4. Rules for Modalities and Programs

The rules for modalities and programs are obtained from the rule schemata shown inT
4, which can be applied in both sides of a sequent. Rule schemata in T
4 analyze the effect of modalities by reducing algebraic programs into simpler ones.If(20)
ϕ
1
ϕ
0is an instance of one rule schema in T
4, then(21)
Γ
,
ϕ
1
⊢
Δ
Γ
,
ϕ
0
⊢
Δ
,
Γ
⊢
ϕ
1
,
Δ
Γ
⊢
ϕ
0
,
Δare two inference rules of the A
D
L calculus. There is one rule schema for each program structure (;
,
?
,
∪
,
∗) and modalities (·, ·).As mentioned previously, algebraic programs are defined onV
∪
V
′. A
D
L formulas, which are defined on V, only assert properties on the final states of the runs of algebraic programs. Confusions about variable may emerge when an algebraic program needs to be lifted to a formula by rules in T
4. For eliminating the confusion, variables of algebraic programs need be renumbered by thevariable numbering procedure defined by the following definition when an algebraic program is lifted to a formula with rule M
1 and rule M
2.Definition 18 (variable numbering procedure).
For each sequentΓ
⊢
Δ, there always exists a procedure such that a sequent, which does not produce any confusion about variable, is obtained from Γ
⊢
Δ by numbering all occurrences of variables.Since every sequent is assumed to contain finite variables, numbering finite variables is easy and immediately leads to a variable numbering procedure. We assume that each sequent, which produces variable confusions, is implicitly numbered by the variable numbering procedure. For the sake of succinctness, the description of this procedure is not shown in detail. However, the effect of this procedure is illustrated by Example19:T
4
M
1
∀
X
Ψ
Ψ
⟶
ϕ
Ψ
ϕ
M
2
∃
X
Ψ
Ψ
∧
ϕ
Ψ
ϕ
M
3
Ψ
⟶
ϕ
Ψ
?
ϕ
M
4
Ψ
∧
ϕ
Ψ
?
ϕ
P
1
α
β
ϕ
α
;
β
ϕ
P
2
α
β
ϕ
α
;
β
ϕ
P
3
α
ϕ
∧
β
ϕ
α
∪
β
ϕ
P
4
α
ϕ
∨
β
ϕ
α
∪
β
ϕ
P
5
ϕ
∧
α
;
α
∗
ϕ
α
∗
ϕ
P
6
ϕ
∨
α
;
α
∗
ϕ
α
∗
ϕ
.InM
1 and M
2, Ψ denotes an algebraic assertion on V
∪
V
′. In M
3 and M
4,   Ψ denotes an algebraic assertion on V. Variables bound to Ψ are denoted by X
Ψ.Example 19.
Consider the sequent(22)
⊢
x
2
-
x
′
2
-
4
=
0
;
x
2
-
x
′
2
-
2
=
0
x
-
2
=
0
.It would have produced confusion of the variables x and x
′ if we applied rules M
1 and M
2 directly. After doing the variable numbering procedure, we get the following sequent:(23)
⊢
x
0
2
-
x
1
2
-
4
=
0
;
x
1
2
-
x
2
2
-
2
=
0
x
2
-
2
=
0
,which produces no confusions when applying M
1 and M
2.RulesM
1 and M
2 are used to deal with assignment programs in [
·
] and ·. The basic idea of M
1 and M
2 is transforming an A
D
L formula with assignment programs into a standard first-order formula by lifting assignment programs to logical formulas. M
1 expresses that the formula ϕ always holds after executing the assignment program Ψ, if Ψ implies ϕ for all values of variables bound to Ψ while M
2 expresses that ϕ holds for some execution of Ψ, if both Ψ and ϕ hold for some value for variables bound to Ψ. Both M
1 and M
2 properly reflect the underlying logical principle that A
D
L formulas with assignment programs can be transformed into quantified formulas. The rules M
3 and M
4 can be understood in the same way as in [15], except that the logical formula of test is replaced with a guard specified by an algebraic assertion Ψ on V.RulesP
1
–
P
6 are used to decompose the structure of programs into simpler programs. In order to prove the sequential compositions of programs, nested modalities, which are obtained by decomposing sequential compositions, have to be proved by P
1-P
2. Nondeterministic choices are proved by proving the conjunction by P
3 or disjunction by P
4 of its alternatives. P
5 and P
6 are the usual iteration rules in dynamic logic [15], which unfold loops.


### 5.5. Miscellaneous Rules

Besides the rules mentioned previously, some miscellaneous rules are necessary to our proof system. There are several types of rules listed inT
5. The first type is the usual generalization rules (G
1 and G
2) which allow to derive α
ϕ
⊢
[
α
]
φ and α
ϕ
⊢
α
φ from ⊢
ϕ
→
φ.C
1 is the usual cut rule [27] which does not make our proof system prove more theorems but just allows the proofs to be shorter and simpler. C
1 states that when a formula ϕ can be concluded in the context and ϕ can also serve as a premise for concluding other formulas, then the formula ϕ can be cut out from the context. However, when searching a proof bottom-up with the cut rule, it requires one to guess the auxiliary formula ϕ.RuleI
1 is a variant of the usual induction rule with theinductive invariant
ϕ [15]. It expresses that the invariant ϕ will be true after any number of iterations of α, if ϕ is true in the current state and ϕ is still true after the execution of α when ϕ holds for all bound variables of α. Rule O
1 transforms a finite set of atomic formulas with an empty zero set into the Boolean value F
a
l
s
e. Whether atomic formulas have an empty zero set is decided by Theorem 7. ConsiderT
5
G
1
⊢
ϕ
⟶
φ
α
ϕ
⊢
α
φ
G
2
⊢
ϕ
⟶
φ
α
ϕ
⊢
α
φ
C
1
Γ
⊢
ϕ
,
Δ
Γ
,
ϕ
⊢
Δ
Γ
⊢
Δ
I
1
ϕ
∧
∀
X
α
ϕ
⟶
α
ϕ
α
∗
ϕ
O
1
F
a
l
s
e
⊢
Γ
,
ϕ
1
,
…
,
ϕ
n
⊢
X
α in I
1 denotes all variables bound to the algebraic program α. In rule O
1 formulas ϕ
1
,
…
,
ϕ
n are atomic such that they have an empty zero set.


## 5.1. Rules for Axioms

In this and the following sections, the symbolsΓ, Δ denote arbitrary sequences of A
D
L formulas and ϕ, φ denote A
D
L formulas unless otherwise noted.Four basic rulesA
1
–
A
4 listed in T
1, namedaxiom rules, are composed for closing a proof search. Rules A
1
–
A
3 are the same as in many other sequent calculus. The axiom rule A
1 treats a sequent with a common formula in the antecedent and the succedent as an axiom, which can be inferred from nothing (denoted by ⊥):T
1
A
1
⊥
Γ
,
ϕ
⊢
Δ
,
ϕ
A
2
⊥
Γ
⊢
T
r
u
e
,
Δ
A
3
⊥
Γ
,
F
a
l
s
e
⊢
Δ
A
4
⊥
Γ
,
ϕ
⊢
φ
,
Δ
.In A
4, ϕ and φ are atomic formulas which are expressed as polynomials in variables of V, and Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
).RuleA
4 is customized to coordinate mathematical procedures on ideal theory implemented by computer algebra systems, such as REDUCE, Maple, Mathematica, AXIOM, and SINGULAR. Rule A
4 reveals that any sequent whose antecedent has a formula ϕ with its zero set included by the zero set of one formula φ of the succedent can be applied as an axiom. By Theorems 5 and 6, the inclusion Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
) can be transformed into the radical membership problem which is decided byradical membership algorithm on polynomial ideals [5, 24]. That is to say, if there is an atomic formula φ in the succedent such that φ belongs to the radical of the ideal generated by polynomials in ϕ in the antecedent, that is, φ
∈
ϕ, then the sequent can be applied as an axiom. The radical membership algorithm is implemented in most computer algebra systems, such as theRadicalMembership command in Maple. The discussion on computer algebra systems is not in the scope of this paper.


## 5.2. Rules for Logical Operators

The rules inT
2 are used to handle standard logical operators. There are two cases for the appearance of each logical operator, and each logical operator needs dual rules (left rule and right rule):T
2
L
1
Γ
⊢
ϕ
,
Δ
Γ
,
¬
ϕ
⊢
Δ
L
2
Γ
,
ϕ
⊢
Δ
Γ
⊢
¬
ϕ
,
Δ
L
3
Γ
,
ϕ
,
φ
⊢
Δ
Γ
,
ϕ
∧
φ
⊢
Δ
L
4
Γ
⊢
ϕ
,
Δ
Γ
⊢
φ
,
Δ
Γ
⊢
ϕ
∧
φ
,
Δ
L
5
Γ
,
ϕ
⊢
Δ
Γ
,
φ
⊢
Δ
Γ
,
ϕ
∨
φ
⊢
Δ
L
6
Γ
⊢
ϕ
,
φ
,
Δ
Γ
⊢
ϕ
∨
φ
,
Δ
L
7
Γ
,
φ
⊢
Δ
Γ
⊢
ϕ
,
Δ
Γ
,
ϕ
⟶
φ
⊢
Δ
L
8
Γ
,
ϕ
⊢
φ
,
Δ
Γ
⊢
ϕ
⟶
φ
,
Δ
.RulesL
1
–
L
8 are standard for propositional dynamic logic. These rules decompose formulas with propositional structures into smaller formulas with less logical operators. Rules L
1 and L
2 are dual and aim to reduce the negative operator ¬. Rule L
3 just replaces the symbol ∧ with a comma, since formulas are combined conjunctively in antecedents of sequents by the definition of sequents. Rule L
4 branches the sequent containing the operator ∧ in the succedent into two sequents, since conjuncts in the succedent can be proved separately due to the semantics of sequents. Dually, rule L
5 is similar to L
4 and L
6 is similar to L
3 according to the semantics of sequents. Rule L
7 derives from rules L
5 and L
1 by the logical equivalence of (
ϕ
→
φ
) and (
¬
ϕ
∨
φ
). Similarly, rule L
8 is derived from rules L
6 and L
2.


## 5.3. Rules for Quantifiers

Recall that variables ofV
′ occurring in an algebraic program arebound to modalities. We assume that each modality-bound variable is not bound to any quantifier. A variable is free if it is not bound to modalities and quantifiers.Definition 17 (substitution).
Asubstitution of an algebraic assertion or a formula for a free variable is defined as a function which maps each object variable to a designated polynomial. Let f be a polynomial; the result of substituting f in an algebraic assertion ψ for a variable x is denoted by ψ
[
x
↦
f
]. The result of substituting f in a formula ϕ for a variable x is denoted by ϕ
[
x
↦
f
].A substitution with the resultϕ
[
x
↦
f
] isadmissible for the formula ϕ if no variables y in f are bound in the formula ϕ
[
x
↦
f
]. That is to say, free variables in f are still free in the formula ϕ
[
x
↦
f
] after applying an admissible substitution.RuleQ
1 and rule Q
4 are the usual γ-rule in [7, 26], while Q
2 and Q
3 correspond to the δ
+-rule in [26]. Rules Q
1
–
Q
4 are complete for quantifiers of classic first-order logic. That is to say, everything about quantifiers of first-order logic can be derived with Q
1
–
Q
4 [7]:T
3
Q
1
Γ
,
ϕ
x
⟼
X
,
∀
x
ϕ
⊢
Δ
Γ
,
∀
x
ϕ
⊢
Δ
Q
2
Γ
⊢
ϕ
x
⟼
f
X
1
,
…
,
X
n
,
Δ
Γ
⊢
∀
x
ϕ
,
Δ
Q
3
Γ
,
ϕ
x
⟼
f
X
1
,
…
,
X
n
⊢
Δ
Γ
,
∃
x
ϕ
⊢
Δ
Q
4
Γ
⊢
ϕ
x
⟼
X
,
∃
x
ϕ
,
Δ
Γ
⊢
∃
x
ϕ
,
Δ
.In Q
1
–
Q
4, the variable x is only bound to ∀
x or ∃
x. In Q
1 and Q
4, X is a new free variable. In Q
2 and Q
3, f is a new function symbol and X
1
,
…
,
X
n are all free variables in ∀
x
ϕ and ∃
x
ϕ.


## 5.4. Rules for Modalities and Programs

The rules for modalities and programs are obtained from the rule schemata shown inT
4, which can be applied in both sides of a sequent. Rule schemata in T
4 analyze the effect of modalities by reducing algebraic programs into simpler ones.If(20)
ϕ
1
ϕ
0is an instance of one rule schema in T
4, then(21)
Γ
,
ϕ
1
⊢
Δ
Γ
,
ϕ
0
⊢
Δ
,
Γ
⊢
ϕ
1
,
Δ
Γ
⊢
ϕ
0
,
Δare two inference rules of the A
D
L calculus. There is one rule schema for each program structure (;
,
?
,
∪
,
∗) and modalities (·, ·).As mentioned previously, algebraic programs are defined onV
∪
V
′. A
D
L formulas, which are defined on V, only assert properties on the final states of the runs of algebraic programs. Confusions about variable may emerge when an algebraic program needs to be lifted to a formula by rules in T
4. For eliminating the confusion, variables of algebraic programs need be renumbered by thevariable numbering procedure defined by the following definition when an algebraic program is lifted to a formula with rule M
1 and rule M
2.Definition 18 (variable numbering procedure).
For each sequentΓ
⊢
Δ, there always exists a procedure such that a sequent, which does not produce any confusion about variable, is obtained from Γ
⊢
Δ by numbering all occurrences of variables.Since every sequent is assumed to contain finite variables, numbering finite variables is easy and immediately leads to a variable numbering procedure. We assume that each sequent, which produces variable confusions, is implicitly numbered by the variable numbering procedure. For the sake of succinctness, the description of this procedure is not shown in detail. However, the effect of this procedure is illustrated by Example19:T
4
M
1
∀
X
Ψ
Ψ
⟶
ϕ
Ψ
ϕ
M
2
∃
X
Ψ
Ψ
∧
ϕ
Ψ
ϕ
M
3
Ψ
⟶
ϕ
Ψ
?
ϕ
M
4
Ψ
∧
ϕ
Ψ
?
ϕ
P
1
α
β
ϕ
α
;
β
ϕ
P
2
α
β
ϕ
α
;
β
ϕ
P
3
α
ϕ
∧
β
ϕ
α
∪
β
ϕ
P
4
α
ϕ
∨
β
ϕ
α
∪
β
ϕ
P
5
ϕ
∧
α
;
α
∗
ϕ
α
∗
ϕ
P
6
ϕ
∨
α
;
α
∗
ϕ
α
∗
ϕ
.InM
1 and M
2, Ψ denotes an algebraic assertion on V
∪
V
′. In M
3 and M
4,   Ψ denotes an algebraic assertion on V. Variables bound to Ψ are denoted by X
Ψ.Example 19.
Consider the sequent(22)
⊢
x
2
-
x
′
2
-
4
=
0
;
x
2
-
x
′
2
-
2
=
0
x
-
2
=
0
.It would have produced confusion of the variables x and x
′ if we applied rules M
1 and M
2 directly. After doing the variable numbering procedure, we get the following sequent:(23)
⊢
x
0
2
-
x
1
2
-
4
=
0
;
x
1
2
-
x
2
2
-
2
=
0
x
2
-
2
=
0
,which produces no confusions when applying M
1 and M
2.RulesM
1 and M
2 are used to deal with assignment programs in [
·
] and ·. The basic idea of M
1 and M
2 is transforming an A
D
L formula with assignment programs into a standard first-order formula by lifting assignment programs to logical formulas. M
1 expresses that the formula ϕ always holds after executing the assignment program Ψ, if Ψ implies ϕ for all values of variables bound to Ψ while M
2 expresses that ϕ holds for some execution of Ψ, if both Ψ and ϕ hold for some value for variables bound to Ψ. Both M
1 and M
2 properly reflect the underlying logical principle that A
D
L formulas with assignment programs can be transformed into quantified formulas. The rules M
3 and M
4 can be understood in the same way as in [15], except that the logical formula of test is replaced with a guard specified by an algebraic assertion Ψ on V.RulesP
1
–
P
6 are used to decompose the structure of programs into simpler programs. In order to prove the sequential compositions of programs, nested modalities, which are obtained by decomposing sequential compositions, have to be proved by P
1-P
2. Nondeterministic choices are proved by proving the conjunction by P
3 or disjunction by P
4 of its alternatives. P
5 and P
6 are the usual iteration rules in dynamic logic [15], which unfold loops.


## 5.5. Miscellaneous Rules

Besides the rules mentioned previously, some miscellaneous rules are necessary to our proof system. There are several types of rules listed inT
5. The first type is the usual generalization rules (G
1 and G
2) which allow to derive α
ϕ
⊢
[
α
]
φ and α
ϕ
⊢
α
φ from ⊢
ϕ
→
φ.C
1 is the usual cut rule [27] which does not make our proof system prove more theorems but just allows the proofs to be shorter and simpler. C
1 states that when a formula ϕ can be concluded in the context and ϕ can also serve as a premise for concluding other formulas, then the formula ϕ can be cut out from the context. However, when searching a proof bottom-up with the cut rule, it requires one to guess the auxiliary formula ϕ.RuleI
1 is a variant of the usual induction rule with theinductive invariant
ϕ [15]. It expresses that the invariant ϕ will be true after any number of iterations of α, if ϕ is true in the current state and ϕ is still true after the execution of α when ϕ holds for all bound variables of α. Rule O
1 transforms a finite set of atomic formulas with an empty zero set into the Boolean value F
a
l
s
e. Whether atomic formulas have an empty zero set is decided by Theorem 7. ConsiderT
5
G
1
⊢
ϕ
⟶
φ
α
ϕ
⊢
α
φ
G
2
⊢
ϕ
⟶
φ
α
ϕ
⊢
α
φ
C
1
Γ
⊢
ϕ
,
Δ
Γ
,
ϕ
⊢
Δ
Γ
⊢
Δ
I
1
ϕ
∧
∀
X
α
ϕ
⟶
α
ϕ
α
∗
ϕ
O
1
F
a
l
s
e
⊢
Γ
,
ϕ
1
,
…
,
ϕ
n
⊢
X
α in I
1 denotes all variables bound to the algebraic program α. In rule O
1 formulas ϕ
1
,
…
,
ϕ
n are atomic such that they have an empty zero set.


## 6. Verification Example

Reasoning about the safety property of the train control system, which is formulated by (17), is shown in Figures 2–4. Remark that we have assumed the parameter Δ
t is constant; that is, the time is discrete and modelled by Δ
t. In addition, the train evolves its velocity per Δ
t and keeps the velocity fixed in each Δ
t. We start by writing the safety property [
t
r
a
i
n
]
¬
(
v
-
11
=
0
) into the proof obligation:(24)
⊢
t
r
a
i
n
¬
v
-
11
=
0
.We use the rule I
1 to eliminate the iteration operator and split the sequent into two branches by applying rule L
4. The left branch derives the open sequent v
-
11
=
0
⊢ from ⊢
¬
(
v
-
11
=
0
) by applying L
2. Recall that by the semantics of sequent the proof obligation is valid if all premises are valid. Hence (24) is not valid if (
v
-
11
=
0
)
⊢ is not valid. In other words,(25)
v
≠
11which makes (
v
-
11
=
0
)
⊢ valid must be initially guaranteed in order to make (24) valid.Figure 2
Verification of the train control system.Figure 3
Proof of the right branch.Figure 4
The rest of proof.The proof of the right branch (Π) goes on as shown in Figure 2. Since there are no free variables in ∀
X
α
(
¬
(
v
-
11
=
0
)
→
[
A
c
∪
D
c
;
d
r
i
v
e
]
¬
(
v
-
11
=
0
)
), we replace each bound variable v with a constant v when the rule Q
2 is applied. Proving the sequent ¬
v
-
11
=
0
⊢
A
c
∪
D
c
d
r
i
v
e
¬
(
v
-
11
=
0
) is to prove both ¬
v
-
11
=
0
⊢
A
c
d
r
i
v
e
¬
(
v
-
11
=
0
) and ¬
v
-
11
=
0
⊢
D
c
d
r
i
v
e
¬
(
v
-
11
=
0
) (denoted by Π
1 in Figure 2).The proof of the sequent¬
v
-
11
=
0
⊢
A
c
[
d
r
i
v
e
]
¬
(
v
-
11
=
0
) (Π
2) is shown in Figure 3. For notional convenience, the notions Γ
0, Γ
1, are Γ
2 are introduced as follows: (26)
Γ
0
≝
v
=
10
,
m
o
d
e
=
A
c
c
Γ
1
≝
a
′
=
-
a
,
m
o
d
e
′
=
D
e
c
Γ
2
≝
s
′
=
s
+
v
Δ
t
,
v
′
=
v
+
a
′
Δ
t
ϕ
0
≝
v
=
10
?
;
a
′
=
-
a
∧
m
o
d
e
′
=
D
e
c
d
r
i
v
e
¬
v
-
11
=
0
ϕ
1
≝
a
′
=
-
a
∧
m
o
d
e
′
=
D
e
c
d
r
i
v
e
¬
v
-
11
=
0
ϕ
2
≝
a
′
=
-
a
∧
m
o
d
e
′
=
D
e
c
⟶
d
r
i
v
e
¬
v
-
11
=
0
ϕ
3
≝
v
′
=
v
+
a
′
Δ
t
∧
s
′
=
s
+
v
Δ
t
⟶
¬
v
′
=
11
.At the end of the proof in Figure 3, we obtain the sequent(27)
Γ
0
,
Γ
1
,
Γ
2
,
v
′
=
11
⊢
v
-
11
=
0
,where v denotes the initial velocity and v
′ denotes the final velocity after executing program [
A
c
∪
D
c
;
d
r
i
v
e
]. Since we have known that the initial velocity v does not equal 11 according to (25), the right side of (27) is false. Hence the left side of (27) should be unsatisfiable to make sequent (27) valid. If we treat a
,
v, and Δ
t as parameters of the train, then v
-
a
Δ
t
-
11
=
0 is concluded from Γ
0
∧
Γ
1
∧
Γ
2
∧
v
′
=
11 by eliminating variables except a
,
v
,
Δ
t. If the assertion v
-
a
Δ
t
-
11
=
0 is not satisfied, sequent (27) will be valid. That means(28)
v
-
a
Δ
t
≠
11implies ¬
v
-
11
=
0
⊢
A
c
d
r
i
v
e
¬
(
v
-
11
=
0
).The proof of the sequentΠ
1 is similar to Π
2. In the same way, we get the same assertion:(29)
v
-
a
Δ
t
≠
11which implies ¬
v
-
11
=
0
⊢
D
c
d
r
i
v
e
¬
v
-
11
=
0. Hence, the safety property on the train control system specified by (17) is valid if the requirements specified by (25), (28), and (29) are satisfied; that is,(30)
v
≠
11
∧
v
-
a
Δ
t
≠
11
⟹
t
r
a
i
n
¬
v
-
11
=
0
.


## 7. Soundness and Incompleteness

### 7.1. Soundness

In this section, we prove that theA
D
L calculus is sound; that is, verification with the A
D
L calculus always produces correct results.Lemma 20.
Given a formulaϕ, two interpretations I, J, assignments ζ, η, and states v, w, if I, ζ, v and J, η, w agree on all free variables of ϕ, then I
,
ζ
,
v
⊨
ϕ if and only if J
,
η
,
w
⊨
ϕ.Proof.
This lemma can be proved by a simple induction principle [28] on the structures of algebraic programs and A
D
L formulas as in Section 4.2 using the semantics of algebraic programs and A
D
L formula satisfaction.The soundness of theA
D
L calculus is shown by the following theorem, which says that all rules preserve the validity of sequents.Theorem 21.
For all rules and rule schemata listed inT
1–T
5, if all premises of a rule are valid sequents which are true in all states for all interpretations, then the conclusion is a valid sequent.Proof.
We start by giving the proof of special rules forA
D
L calculus such as A
4, M
1, M
2, O
1, and I
1. The rest of the rules are proved in an immediate way which can be easily found in [15, 26, 28] and thus are skipped over here. (i)
RuleA
4 is a sound rule for axioms. Let I be an interpretation, ζ an assignment, and v a state with I
,
ζ
,
v
⊨
ϕ
∧
Γ. Since the zero set of ϕ in the antecedent of the conclusion is a subset of the zero set of φ in the succedent, that is, Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
), we can conclude that v
∈
Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
). Then we conclude that v
⊨
φ
∨
Δ by the definition of ⊨. According to the semantics of sequents Γ
,
ϕ
⊢
φ
,
Δ is true for all I
,
ζ
,
v and can be applied as an axiom.
(ii)
RuleQ
4 is sound. For any I, ζ, v with I
,
ζ
,
v
⊨
ϕ
[
x
↦
X
], we choose ζ
(
X
) as the witness of ∃
x
ϕ such that the value of X in ζ is assigned to the bound variable x in ∃
x
ϕ. Then I
,
ζ
,
v
⊨
∃
x
ϕ can be concluded. The proof of Q
1 is trivial since the premise and the conclusion contain the common formula ∀
x
ϕ.
(iii)
The soundness proof ofQ
3 is shown as follows. Assume that there are I, v such that for some ζ the formula ϕ
[
x
↦
f
(
X
1
,
…
,
X
n
)
] is true; that is, I
,
ζ
,
v
⊨
ϕ
[
x
↦
f
(
X
1
,
…
,
X
n
)
]. We can conclude that I
,
ζ
,
v
⊨
∃
x
ϕ by choosing the value ζ
(
f
(
X
1
,
…
,
X
n
)
) of f
(
X
1
,
…
,
X
n
) as the witness of ∃
x
ϕ. The soundness proof of Q
2 is dual.
(iv)
M
1 is sound. Assume that there are I, v such that for all assignments ζ the formula Ψ implies ϕ; that is, I
,
ζ
,
v
⊨
∀
X
Ψ
(
Ψ
→
ϕ
). Since all bound variables in the modality [
Ψ
] are denoted by X
Ψ, we can conclude that I
,
ζ
,
w
⊨
ϕ for all w with (
v
,
w
)
∈
γ
(
Ψ
) by the definition of semantics of · and Lemma 20. Then I
,
ζ
,
v
⊨
[
Ψ
]
ϕ is concluded.
(v)
M
2 is sound. Assume that there are I, v such that for some assignment ζ the formula Ψ
∧
ϕ is true; that is, I
,
ζ
,
v
⊨
∃
X
Ψ
(
Ψ
∧
ϕ
). We can conclude that (
v
,
w
)
∈
γ
(
Ψ
) with w
=
v
[
X
Ψ
↦
ζ
(
X
Ψ
)
] by the definition of γ
(
Ψ
). Then I
,
ζ
,
w
⊨
ϕ is concluded by Lemma 20. Hence we can conclude that I
,
ζ
,
v
⊨
Ψ
ϕ.
(vi)
O
1 is sound. Since the zero set of atomic formulas ϕ
1
,
…
,
ϕ
n is empty, there does not exist a state v such that v
⊨
Γ
∧
ϕ
1
∧
⋯
∧
ϕ
n by the satisfaction of formulas. So we can conclude that the antecedent is unsatisfiable and is equivalent to F
a
l
s
e.
(vii)
Rule schemaI
1 is sound. For any I, ζ, v with I
,
ζ
,
v
⊨
ϕ
∧
∀
X
α
(
ϕ
→
[
α
]
ϕ
), we conclude that I
,
ζ
,
w
⊨
ϕ for all states w with (
v
,
w
)
∈
γ
(
α
∗
) by Lemma 20. Hence we can further conclude that I
,
ζ
,
v
⊨
[
α
∗
]
ϕ by the semantics of [
α
∗
].


### 7.2. Incompleteness

The following theorem shows the inherent incompleteness ofA
D
L calculus.Theorem 22.
TheA
D
L calculus is inherently incomplete.Proof.
This theorem is proved by showing that the Peano arithmetic producing natural numbers is definable inA
D
L. Natural numbers are definable in modalities using iterations:(31)
N
a
t
n
≡
x
′
=
0
;
x
′
=
x
+
1
∗
x
=
n
.Hence the incompleteness theorem of Gödel [29] can be applied in A
D
L calculus. Hence we immediately conclude that the A
D
L calculus is incomplete.


## 7.1. Soundness

In this section, we prove that theA
D
L calculus is sound; that is, verification with the A
D
L calculus always produces correct results.Lemma 20.
Given a formulaϕ, two interpretations I, J, assignments ζ, η, and states v, w, if I, ζ, v and J, η, w agree on all free variables of ϕ, then I
,
ζ
,
v
⊨
ϕ if and only if J
,
η
,
w
⊨
ϕ.Proof.
This lemma can be proved by a simple induction principle [28] on the structures of algebraic programs and A
D
L formulas as in Section 4.2 using the semantics of algebraic programs and A
D
L formula satisfaction.The soundness of theA
D
L calculus is shown by the following theorem, which says that all rules preserve the validity of sequents.Theorem 21.
For all rules and rule schemata listed inT
1–T
5, if all premises of a rule are valid sequents which are true in all states for all interpretations, then the conclusion is a valid sequent.Proof.
We start by giving the proof of special rules forA
D
L calculus such as A
4, M
1, M
2, O
1, and I
1. The rest of the rules are proved in an immediate way which can be easily found in [15, 26, 28] and thus are skipped over here. (i)
RuleA
4 is a sound rule for axioms. Let I be an interpretation, ζ an assignment, and v a state with I
,
ζ
,
v
⊨
ϕ
∧
Γ. Since the zero set of ϕ in the antecedent of the conclusion is a subset of the zero set of φ in the succedent, that is, Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
), we can conclude that v
∈
Z
e
r
o
(
ϕ
)
⊆
Z
e
r
o
(
φ
). Then we conclude that v
⊨
φ
∨
Δ by the definition of ⊨. According to the semantics of sequents Γ
,
ϕ
⊢
φ
,
Δ is true for all I
,
ζ
,
v and can be applied as an axiom.
(ii)
RuleQ
4 is sound. For any I, ζ, v with I
,
ζ
,
v
⊨
ϕ
[
x
↦
X
], we choose ζ
(
X
) as the witness of ∃
x
ϕ such that the value of X in ζ is assigned to the bound variable x in ∃
x
ϕ. Then I
,
ζ
,
v
⊨
∃
x
ϕ can be concluded. The proof of Q
1 is trivial since the premise and the conclusion contain the common formula ∀
x
ϕ.
(iii)
The soundness proof ofQ
3 is shown as follows. Assume that there are I, v such that for some ζ the formula ϕ
[
x
↦
f
(
X
1
,
…
,
X
n
)
] is true; that is, I
,
ζ
,
v
⊨
ϕ
[
x
↦
f
(
X
1
,
…
,
X
n
)
]. We can conclude that I
,
ζ
,
v
⊨
∃
x
ϕ by choosing the value ζ
(
f
(
X
1
,
…
,
X
n
)
) of f
(
X
1
,
…
,
X
n
) as the witness of ∃
x
ϕ. The soundness proof of Q
2 is dual.
(iv)
M
1 is sound. Assume that there are I, v such that for all assignments ζ the formula Ψ implies ϕ; that is, I
,
ζ
,
v
⊨
∀
X
Ψ
(
Ψ
→
ϕ
). Since all bound variables in the modality [
Ψ
] are denoted by X
Ψ, we can conclude that I
,
ζ
,
w
⊨
ϕ for all w with (
v
,
w
)
∈
γ
(
Ψ
) by the definition of semantics of · and Lemma 20. Then I
,
ζ
,
v
⊨
[
Ψ
]
ϕ is concluded.
(v)
M
2 is sound. Assume that there are I, v such that for some assignment ζ the formula Ψ
∧
ϕ is true; that is, I
,
ζ
,
v
⊨
∃
X
Ψ
(
Ψ
∧
ϕ
). We can conclude that (
v
,
w
)
∈
γ
(
Ψ
) with w
=
v
[
X
Ψ
↦
ζ
(
X
Ψ
)
] by the definition of γ
(
Ψ
). Then I
,
ζ
,
w
⊨
ϕ is concluded by Lemma 20. Hence we can conclude that I
,
ζ
,
v
⊨
Ψ
ϕ.
(vi)
O
1 is sound. Since the zero set of atomic formulas ϕ
1
,
…
,
ϕ
n is empty, there does not exist a state v such that v
⊨
Γ
∧
ϕ
1
∧
⋯
∧
ϕ
n by the satisfaction of formulas. So we can conclude that the antecedent is unsatisfiable and is equivalent to F
a
l
s
e.
(vii)
Rule schemaI
1 is sound. For any I, ζ, v with I
,
ζ
,
v
⊨
ϕ
∧
∀
X
α
(
ϕ
→
[
α
]
ϕ
), we conclude that I
,
ζ
,
w
⊨
ϕ for all states w with (
v
,
w
)
∈
γ
(
α
∗
) by Lemma 20. Hence we can further conclude that I
,
ζ
,
v
⊨
[
α
∗
]
ϕ by the semantics of [
α
∗
].


## 7.2. Incompleteness

The following theorem shows the inherent incompleteness ofA
D
L calculus.Theorem 22.
TheA
D
L calculus is inherently incomplete.Proof.
This theorem is proved by showing that the Peano arithmetic producing natural numbers is definable inA
D
L. Natural numbers are definable in modalities using iterations:(31)
N
a
t
n
≡
x
′
=
0
;
x
′
=
x
+
1
∗
x
=
n
.Hence the incompleteness theorem of Gödel [29] can be applied in A
D
L calculus. Hence we immediately conclude that the A
D
L calculus is incomplete.


## 8. Conclusions and Future Work

In this paper, we present a deductive approach for reasoning about algebraic transition system. This approach models algebraic transition systems as algebraic programs ofA
D
L, which is obtained by allowing algebraic assertions in dynamic logic. The properties of algebraic transition systems are formalized as A
D
L formulas with our method. We explain the semantics of algebraic programs in A
D
L as transition relations of algebraic transition systems and define the satisfaction of A
D
L formulas zero sets of polynomials. A proof system for A
D
L, called A
D
L calculus, is constructed for reasoning about algebraic transition systems. The A
D
L calculus is proved to be sound and is illustrated by the verification of the safety property of the train control system.Our approach combines mathematical procedures on polynomial ideal theory with the deductive verification by customizing special rules for handling algebraic programs. The introduction of mathematical procedures enhances the reasoning power of our proof system. However proofs of properties related to iterations and quantifiers may be tedious and ineffective in complex cases. Future work includes a closer investigation for effective rules of iterations and quantifiers, for example, the invariant method [4, 30–32] and quantifiers elimination [33–35]. On the other hand, there are properties which cannot be formalized as the A
D
L formulas such as properties with inequalities, since A
D
L formulas are defined with algebraic assertions which actually are polynomial equations. In addition to the future work, more general A
D
L formulas should include inequalities and more complex structures, such as differential equations for specifying hybrid systems.



---

*Source: 607013-2015-10-25.xml*