11institutetext: Collage of Software, Nanjing University of Aeronautics and
Astronautics, China
11email<EMAIL_ADDRESS><EMAIL_ADDRESS>

# Parameterized Dynamic Logic — Towards A Cyclic Logical Framework for Program
Verification via Operational Semantics

Yuanrui Zhang  11 0000-0002-0685-6905

###### Abstract

Dynamic logic and its variations, because of their good expressive forms
capturing program specifications clearly by isolating programs from logical
formulas, have been used as a formalism in program reasoning for decades and
have many applications in different areas. The program models of traditional
dynamic logics are in explicit forms. With a clearly-defined syntactic
structure, compositional verification is made possible, in which a deduction
step transfers proving a program into proving its sub-programs. This
structure-based reasoning forms the basis of many dynamic logics and popular
Hoare-style logics. However, structural rules induce a major drawback that for
different target programs, different rules have to be proposed to adapt
different program structures. Moreover, there exist programs that does not
support (or not entirely support) a structure-based reasoning. In this paper,
we propose a parameterized ‘dynamic-logic-like’ logic called $\mathit{DL}_{p}$
with general forms of program models and formulas, and propose a cyclic proof
system for this logic. Program reasoning in $\mathit{DL}_{p}$ is directly
based on symbolic executions of programs according to their operational
semantics. This reduces the burden of designing a large set of rules when
specializing a logic theory to a specific domain, and facilitates verifying
programs without a suitable structure for direct reasoning. Without reasoning
by dissolving program structures, $\mathit{DL}_{p}$ can cause an infinite
proof structure. To solve this, we build a cyclic preproof structure for the
proof system of $\mathit{DL}_{p}$ and prove its soundness. Case studies are
analyzed to show how $\mathit{DL}_{p}$ works for reasoning about different
types of programs.

###### Keywords:

Logical Framework Dynamic Logic Program Verification Operational Semantics
Cyclic Proof Theorem Proving

##  1 Introduction

Dynamic logic is an extension of modal logic by enriching modal formulas with
explicit program models. It is one of popular formal languages for specifying
and reasoning about different types of programs or systems, such as process
algebras [6], programming languages [5], synchronous systems [43, 42], hybrid
systems [31, 33] and probabilistic systems [30, 32, 24, 14]. Like a Hoare-
style logic, dynamic logic consists of two parts: program models and formulas.
A _dynamic formula_ is of the form: $[\alpha]\psi$, expressing that after all
executions of program $\alpha$, formula $\psi$ holds. Formula
$\phi\to[\alpha]\psi$ exactly captures partial correctness of programs
expressed by triple $\\{\phi\\}\alpha\\{\psi\\}$ in Hoare logic [21]. This
separation of program structures ($\alpha$) and logical formulas ($\phi$) by
the modal operator $[\cdot]$ allows a clear observation of program behaviours
throughout the whole deduction processes. Compared to Hoare-style logics, one
advantage of dynamic logics is that with $[\alpha]\phi$ itself a logical
formula, it is able to also express the negation $\neg[\alpha]\phi$ of
$[\alpha]\phi$, or in its dual form: $\langle\alpha\rangle\neg\phi$, meaning
that there exists an execution of $\alpha$ after which $\phi$ is not
satisfied. Operator $\langle\cdot\rangle$ is helpful to express “incorrectness
properties”, which are crucial for nowadays program analysis and verification,
and which has been addressed recently with the new development of
incorrectness Hoare logic [29, 44].

In dynamic logics, program models $\alpha$ are usually regular programs with
tests (e.g. in propositional dynamic logic [15]), programs tailored from
regular programs with tests (e.g. in differential dynamic logic [31]), or
actual computer programs from reality (e.g. in Java dynamic logic [5]).
Deductions of dynamic logics are based on the syntactic structure of a
program. This makes _compositional verification_ possible, in which a
deduction step transfers proving a property of a program into proving a
property of its sub-programs. For example, in propositional dynamic logic
[15], proving $[\alpha\cup\beta]\phi$ relies on proving both $[\alpha]\phi$
and $[\beta]\phi$, where $\alpha$ and $\beta$ are sub-programs of program
$\alpha\cup\beta$. This also-called ‘divide-and-conquer’ way of verifying have
brought many benefits, among which the most is avoiding state-explosion
problem, as opposed to other verification technologies such as traditional
model checking [2].

However, as the development of programs and computer systems nowadays,
especially as the emergence of real-time systems and AI systems [38], this
traditional structure-based reasoning supported by dynamic logics and many
Hoare-style logics is challenged, because of the two main drawbacks:

Firstly, structure-based reasoning requires explicit program syntactic
structures. So, for a new type of programs, one needs to define a new program
model ($\alpha$) and carefully design a set of particular structural rules to
adapt their semantics. This often demands a large amount of work. For example,
Verifiable C [1], a famous program verifier for C programming language based
on Hoare logic, used nearly 40,000 lines of Coq code to define the logic
theory. Secondly, and importantly as well, some (parts of) programs or system
models do not directly support structural rules. These programs either do not
have a syntactic structure, like neural networks [18] for example, or have
semantics that do not support independent executions based on their syntax. In
the latter case, usually, additional processes are required to re-formalize
their program structures so that structure-based reasoning is possible. A
typical example is the synchronous programming language Esterel [7], where in
a sequential program $\alpha;\beta$, as fully illustrated in [17], the
executions in $\alpha$ cannot be analyzed independently from $\beta$ unless
$\alpha$ and $\beta$ are executed at different instances.

In this paper, we present an abstract dynamic-logic-like formalism, which aims
at compensating for the above two shortcomings in traditional dynamic logics.
We call this proposed formalism _parameterized dynamic logic_ , denoted by
$\mathit{DL}_{p}$. Strictly speaking, $\mathit{DL}_{p}$ is not a dynamic logic
in traditional sense, but of a more general formalism, in which we assume
programs and formulas are in general forms as ‘parameters’, and only keep the
modal operator $[\cdot]$ in traditional dynamic logics to express program
properties. In order to capture the executions of general programs, we also
introduce _program configurations_ in general forms as the _labels_ of
$\mathit{DL}_{p}$ formulas. So, a $\mathit{DL}_{p}$ dynamic formula is of the
form: $\sigma:[\alpha]\phi$, where program $\alpha$, formula $\phi$ and
configuration $\sigma$ come from interested domains. $(\alpha,\sigma)$ is thus
a structure containing all information about an execution state of a program.
Formula $\sigma:[\alpha]\phi$ has the meaning that from $(\alpha,\sigma)$, all
terminal execution paths end by satisfying formula $\phi$.

To see how this labelled form of a $\mathit{DL}_{p}$ formula actually works,
let us see a simple example. We prove a formula $\phi=_{df}(x\geq
0\Rightarrow{}[x:=x+1]x>0)$ in first-order dynamic logic [19] expressed as a
sequent (see Section 3), where $x$ is a variable ranging over the set of
natural numbers. $\phi$ intuitively means that if $x\geq 0$ holds, then $x>0$
holds after the execution of $x:=x+1$. By applying the structural rule
$(x:=e)$ for assignment: $\begin{aligned} [x:=e]\psi\psi[x/e]\end{aligned}$ on
formula $[x:=x+1]x>0$, we substitute $x$ of $x>0$ by $x+1$, and obtain
$x+1>0$. So formula $\phi$ becomes $\phi^{\prime}=_{df}x\geq
0\Rightarrow{}x+1>0$, which is always true for any natural number
$x\in\mathbb{N}$.

In $\mathit{DL}_{p}$, on the other hand, formula $\phi$ can be expressed as a
labelled form: $\psi=_{df}(\\{x\mapsto t\\}:x\geq 0\Rightarrow{}\\{x\mapsto
t\\}:[x:=x+1]x>0)$, where $\\{x\mapsto t\\}$ is a program configuration with
$t$ a free variable, meaning “mapping $x$ to an arbitrary value $t$”. This
form may seem tedious at first sight. But one soon can find out that with a
configuration explicitly showing up, we can skip the assignment rule $(x:=e)$
and directly base on the symbolic execution of program $x:=x+1$ as:
$(x:=x+1,\\{x\mapsto t\\})\longrightarrow(\downarrow,\\{x\mapsto t+1\\})$ to
derive formula $\psi$. Here $\downarrow$ indicates a program termination. Then
formula $\psi$ becomes $\psi^{\prime}=_{df}(\\{x\mapsto t\\}:x\geq
0\Rightarrow{}\\{x\mapsto t+1\\}[\downarrow]:x>0)$ after the execution of
$x:=x+1$, which is actually $\psi^{\prime\prime}=_{df}(\\{x\mapsto t\\}:x\geq
0\Rightarrow{}\\{x\mapsto t+1\\}:x>0)$ since $\downarrow$ contributes nothing.
By defining the applications of $\\{x\mapsto t\\}$ and $\\{x\mapsto t+1\\}$ on
formulas $x\geq 0$ and $x>0$ respectively in a usual way: i.e. replacing every
free occurrence of $x$ by $t$ (or $t+1$), we obtain the same valid formula
$\phi^{\prime}$: $t\geq 0\Rightarrow{}t+1>0$.

$\mathit{DL}_{p}$ formulas benefit from that no structural rules special for a
target program are needed, but only a program operational semantics and a
definition of how a configuration applies to a non-dynamical formula.
Normally, for existing programs and system models, formalizing a program’s
operational semantics (like $(x:=x+1,\\{x\mapsto
t\\})\longrightarrow(\downarrow,\\{x\mapsto t+1\\})$) is easier and more
direct than designing an inference rule (like rule $(x:=e)$). As will be
illustrated in Section 4.2, in some case, for a target program with a certain
structure, there might exist no structural rules, or, designing such a rule
can be complex.

To give the semantics of $\mathit{DL}_{p}$, we follow the way of traditional
dynamic logics by defining a special Kripke structure based on the target
programs’ operational semantics. After linking evaluations and configurations
through the Kripke structures (Definition 6), we manage to define the validity
of a $\mathit{DL}_{p}$ formula in normal sense based on evaluations
(Definition 8).

After building the theory of $\mathit{DL}_{p}$, in this paper, we propose a
proof system for $\mathit{DL}_{p}$, which provides a set of rules to support
reasoning via programs’ operational semantics. Unlike traditional dynamic
logics which base on structural rules to dissolve program structures, the
derivations of a $\mathit{DL}_{p}$ formula may result in an infinite proof
structure. To solve this problem, we adopt the _cyclic proof_ approach (cf.
[10]), a technique to ensure that a certain proof structure, called _preproof_
, is a correct proof if it satisfies some _soundness condition_. We propose a
cyclic preproof structure for $\mathit{DL}_{p}$ (Definitions 11 and 12) and
prove that the proof system of $\mathit{DL}_{p}$ is sound.

To summarize, our contributions are mainly three folds:

  * •

We give the syntax and semantics of $\mathit{DL}_{p}$ formulas.

  * •

We build a cyclic proof system for $\mathit{DL}_{p}$.

  * •

We prove the soundness of the proof system of $\mathit{DL}_{p}$.

The rest of the paper is organized as follows. Section 2 defines the syntax
and semantics of $\mathit{DL}_{p}$ formulas. In Section 3 we propose a cyclic
proof system for $\mathit{DL}_{p}$, whose soundness is analyzed and proved in
Section 3.4. We show two case studies in Section 4. Section 5 introduces some
previous work that is closely related to ours, while Section 6 makes some
discussions and talks about future work.

##  2 Dynamic Logic $\mathit{DL}_{p}$

In this section, we build the theory of $\mathit{DL}_{p}$. What mostly
distinguishes $\mathit{DL}_{p}$ from other dynamic logics is that its program
models and formulas are not in particular forms, but instead can be of any
forms, only provided that their structures and operational semantics of the
programs respect some restrictions (see Definition 1). The so-called “labels”
are introduced in $\mathit{DL}_{p}$, which dynamically associate a formula
with a configuration, enabling reasoning directly via program symbolic
executions.

Below, Section 2.1 introduces the syntax of $\mathit{DL}_{p}$, while Section
2.2 gives the semantics of $\mathit{DL}_{p}$.

###  2.1 Definition of $\mathit{DL}_{p}$

Our construction relies on several assumptions of general structures and
constructions as below without formal definitions, which depend on specific
discussed domains.

#### Programs, Configurations and Program Behaviours

Assume a set of programs $\mathbf{Prog}$ and a set of program configurations
$\mathbf{Conf}$. Their elements belongs to a term algebra
$\mathbf{TA}(\Sigma,\mathit{Var})$ — a freely generated algebraic structure
built upon a signature $\Sigma$ with a set of variables $\mathit{Var}$. For
example, we can have terms like $f(x)$, $f(x,y)$, $g(f(c),x)$, if
$f,g\in\Sigma$ are functions, $c\in\Sigma$ is a constant (function), and
$x,y\in\mathit{Var}$ are variables. $\mathbf{TA}(\Sigma,\mathit{Var})$ is an
assumed structure depending on interested domains. It is commonly known that
many interested structures in computer programs and system models can be
captured as a term algebra (cf. [37]). Variables in $\mathit{Var}$ are usually
denoted by $x,y,z$. Terms without variables in term algebra
$\mathbf{TA}(\Sigma,\emptyset)$ (simply $\mathbf{TA}(\Sigma)$) are called
_closed terms_ of algebra $\mathbf{TA}(\Sigma,\mathit{Var})$. Other terms of
algebra $\mathbf{TA}(\Sigma,\mathit{Var})$ are called _open terms_. An
evaluation $\rho:\mathit{Var}\to\mathbf{TA}(\Sigma)$ maps a variable to a
closed term. Given a term $t$, $\rho(t)$ means the closed term obtained by
substituting each free variable $x$ with value $\rho(x)$ in usual sense. We
use $t_{1}\equiv t_{2}$ to denote that two terms $t_{1}$ and $t_{2}$ are
identical. Two terms $t_{1}$ and $t_{2}$ are _equivalent_ , denoted by
$t_{1}=t_{2}$, if $\rho(t_{1})\equiv\rho(t_{2})$ for any $\rho$. Usually, we
use $\mathbf{Cl}(A)$ to represent the set of closed terms of set $A$, use
$\mathbf{Cl}(t)$ to express the set of closed _instances_ of term $t$:
$\mathbf{Cl}(t)=_{df}\\{u\ |\ \mbox{there is an evaluation $\rho$ such that
$\rho(t)=u$}\\}$.

We distinguish two special closed terms in $\mathbf{Prog}$, namely
$\downarrow$ and $\uparrow$. $\downarrow$ indicates a termination of a
program, while $\uparrow$ means an abortion of a program. A _program state_ is
defined as a pair $(\alpha,\sigma)$ of closed terms over
$\mathbf{Cl}(\mathbf{Prog})\times\mathbf{Cl}(\mathbf{Conf})$.

A _program transition_ between two program states $(\alpha,\sigma)$ and
$(\alpha^{\prime},\sigma^{\prime})$ is a binary relation
$(\alpha,\sigma)\longrightarrow(\alpha^{\prime},\sigma^{\prime})$. We use
$\longrightarrow^{*}$ (resp. $\longrightarrow^{+}$) to denote the reflexive
and transitive (resp. transitive) closure of $\longrightarrow$. The
_structural operational semantics_ [34] (also called _small-step semantics_)
of programs is a (possibly infinite) set $\Lambda$ of program transitions.
Usually, $\Lambda$ can be expressed by a finite set of rules (or more strictly
speacking, rule schemata) according to the syntactic structure of the programs
in $\mathbf{Prog}$, in a manner that a transition
$((\alpha,\sigma)\longrightarrow(\alpha^{\prime},\sigma^{\prime}))\in\Lambda$
if $(\alpha,\sigma)\longrightarrow(\alpha^{\prime},\sigma^{\prime})$ can be
inferred based on these rules in a finite number of steps (see the example
below in Table 1 for rule schemata). An _execution path_ over $\Lambda$ is a
finite or infinite sequence of program transitions
$(\alpha_{1},\sigma_{1})\longrightarrow...\longrightarrow(\alpha_{n},\sigma_{n})\longrightarrow...$
($n\geq 1$), with each transition
$((\alpha_{i},\sigma_{i})\longrightarrow(\alpha_{i+1},\sigma_{i+1}))\in\Lambda$
($1\leq i\leq n$). A path is _terminal_ , or can terminate, if it ends with a
program $\downarrow$. We call an execution path _minimum_ , in the sense that
in it there is no two equivalent program states.

In this paper, we confine our discussion to a certain type of programs whose
operational semantics satisfy the following properties, we simply call
_program properties_.

######  Definition 1 (Program Properties)

The operational semantics $\Lambda$ of programs in $\mathbf{Prog}$ satisfies
that for each program $\alpha\in\mathbf{Cl}(\mathbf{Prog})$, the following
properties hold:

  1. I.

Well-definedness. For any program state $(\alpha,\sigma)$, there exists at
least one transition
$(\alpha,\sigma)\longrightarrow(\alpha^{\prime},\sigma^{\prime})\in\Lambda$
for some $\alpha^{\prime}$ and $\sigma^{\prime}$, unless $\alpha$ is either
$\downarrow$ or $\uparrow$, when there is no transitions from
$(\alpha,\sigma)$ in $\Lambda$.

  2. II.

Branching Finiteness. From any program state $(\alpha,\sigma)$, there exists
only a finite number of transitions in $\Lambda$.

  3. III.

Termination Finiteness. From any program state $(\alpha,\sigma)$, there is
only a finite number of minimum terminal execution paths.

These restrictions are crucial for the soundness of $\mathit{DL}_{p}$
discussed in Section 3.4. Our current discussion domain of programs actually
includes a rich set of programs with discrete behaviours. Among them are, for
example, all deterministic programs (i.e., there is only one transition from
any program state) and programs with finite behaviours (i.e., starting from a
program state, only a finite number of program states can be reached).
However, there exist types of programs that do not satisfy some of the program
properties I — III. For example, hybrid programs (cf. [31]) with continuous
behaviours do not satisfy branching finiteness. Some non-deterministic
programs, like probabilistic programs [3], do not satisfy termination
finiteness.

While programs: $\begin{aligned} \textit{WP}&=_{df}x:=e\ |\ \textit{WP}\
;\textit{WP}\ |\ \textit{if}\ b\ \textit{then}\ \textit{WP}\ \textit{else}\
\textit{WP}\ \textit{end}\ |\ \textit{while}\ b\ \textit{do}\ \textit{WP}\
\textit{end}\\\ \sigma&=_{df}\mbox{a set of assignments of the form: $x\mapsto
e$}\end{aligned}$ $(x:=e,\sigma)\longrightarrow(\downarrow,\sigma[x\mapsto
e(\sigma)])$
$(\textit{WP}_{1};\textit{WP}_{2},\sigma)\longrightarrow(\textit{WP'}_{1};\textit{WP}_{2},\sigma^{\prime})(\textit{WP}_{1},\sigma)\longrightarrow(\textit{WP'}_{1},\sigma^{\prime})$
$(\textit{WP}_{1};\textit{WP}_{2},\sigma)\longrightarrow(\textit{WP}_{2},\sigma^{\prime})(\textit{WP}_{1},\sigma)\longrightarrow(\downarrow,\sigma^{\prime})$
$(\textit{while}\ \phi\ \textit{do}\ \textit{WP}_{1}\
\textit{end},\sigma)\longrightarrow(\textit{WP'}_{1};\ \textit{while}\ \phi\
\textit{do}\ \textit{WP}_{1}\
\textit{end},\sigma^{\prime})\lx@proof@logical@and(\textit{WP}_{1},\sigma)\longrightarrow(\textit{WP'}_{1},\sigma^{\prime})\mbox{${\phi}\rhd{\sigma}$
is true}$ $(\textit{while}\ \phi\ \textit{do}\ \textit{WP}_{1}\
\textit{end},\sigma)\longrightarrow(\textit{while}\ \phi\ \textit{do}\
\textit{WP}_{1}\
\textit{end},\sigma^{\prime}),\Delta\lx@proof@logical@and(\textit{WP}_{1},\sigma)\longrightarrow(\downarrow,\sigma^{\prime})\mbox{${\phi}\rhd{\sigma}$
is true}$ $(\textit{while}\ \phi\ \textit{do}\ \textit{WP}_{1}\
\textit{end},\sigma)\longrightarrow(\downarrow,\sigma)\mbox{${\phi}\rhd{\sigma}$
is false}$ Esterel programs: $\begin{aligned} E=_{df}&\ \textit{nothing}\ |\
\textit{pause}\ |\ E\ ;E\ |\ E\parallel E\ |\ \textit{loop}\ E\ \textit{end}\
|\ \textit{signal}\ S\ \textit{in}\ E\ \textit{end}\ |\ \textit{emit}\ S\ |\\\
&\textit{present}\ S\ \textit{then}\ E\ \textit{else}\ E\ \textit{end}\ |\
\textit{suspend}\ E\ \textit{when}\ S\ |\ \textit{trap}\ T\ \textit{in}\ E\
\textit{end}\ |\ \textit{exit}\ T\\\ \sigma=_{df}&\ \mbox{a stack of
assignments of the form: $x\mapsto e$}\end{aligned}$

Table 1: Examples of programs, configurations and operational semantics

Table 1 shows examples of particular $\mathbf{Prog},\mathbf{Conf}$ and
$\Lambda$. Both while programs and Esterel programs are deterministic programs
(for Esterel programs, cf. [7]), thus satisfy the program properties in
Definition 1. However, while programs and Esterel programs have different
syntax and configurations. The operational semantics of while programs is
given by a finite set of inference rules. We do not give the operational
semantics of Esterel programs here due to its complexity. One can refer to
[35] for more details.

#### Syntax of $\mathit{DL}_{p}$

In $\mathit{DL}_{p}$, we assume a set of logical formulas $\mathbf{Form}$,
where each formula is composed by the terms in
$\mathbf{TA}(\Sigma,\mathit{Var})$ using a set L of predicates and logical
connectives distinguished from $\Sigma$. For example, formulas can be
$p(t_{1},t_{2}),p_{1}(t_{1})\to p_{2}(t_{2}),p_{1}\wedge p_{2}$ or $p_{1}\vee
p_{2}$, where $p,p_{1},p_{2},\to,\wedge,\vee\in\textbf{L}$. A formula that has
only closed terms is called a _closed formula_ , otherwise it is called
_open_. Given an evaluation $\rho$, $\rho(\phi)$ represents the formula in
which all terms $t$ of $\phi$ are replaced by $\rho(t)$. Similar to terms, we
use $\phi_{1}\equiv\phi_{2}$ to express that two formulas are identical.

A closed formula in $\mathbf{Form}$ has a boolean semantics of either true or
false. A formula $\phi$ is _satisfied_ by an evaluation $\rho$, denoted by
$\rho\models\phi$, is defined such that $\rho(\phi)$ is true. A formula $\phi$
is _valid_ , denoted by $\models\phi$, if $\rho(\phi)$ is true for any $\rho$.

A configuration is assumed to be applied to a formula through a function:
${\cdot}\rhd{\cdot}:\mathbf{Form}\times\mathbf{Conf}\to\mathbf{Form}$. In
other words, for a formula $\phi\in\mathbf{Form}$ and a configuration
$\sigma\in\mathbf{Conf}$, ${\phi}\rhd{\sigma}$ returns a formula in
$\mathbf{Form}$ w.r.t. $\phi$ and $\sigma$.

Based on the assumed sets $\mathbf{Prog},\mathbf{Conf}$ and $\mathbf{Form}$,
we give the syntax of $\mathit{DL}_{p}$. We firstly define a general dynamic
logical (GDL) formulas in Definition 2, then we define $\mathit{DL}_{p}$ in
Definition 3.

######  Definition 2 (Syntax of GDL)

A general dynamic logical (GDL) formula is inductively defined as follows: 1\.
Any formula in $\mathbf{Form}$ is a GDL formula. 2\. $\neg\phi$ and
$\phi_{1}\wedge\phi_{2}$ are GDL formulas if $\phi$, $\phi_{1}$ and $\phi_{2}$
are GDL formulas. 3\. $[\alpha]\phi$ is a GDL formula if $\alpha$ is a program
in $\mathbf{Prog}$ and $\phi$ is a GDL formula.

We also call $[\alpha]$ the _dynamic part_ of a GDL formula. Call a formula
having a dynamic part a _dynamic formula_. Intuitively, formula $[\alpha]\phi$
means that after all executions of program $\alpha$, formula $\phi$ holds.
$\langle\cdot\rangle$ is the dual operator of $[\cdot]$. Formula
$\langle\alpha\rangle\phi$ can be expressed by $\neg[\alpha]\neg\phi$. Other
formulas with logical connectives such as $\vee$ and $\to$ can be expressed by
formulas with $\neg$ and $\wedge$ accordingly.

######  Definition 3 ($\mathit{DL}_{p}$ Formulas)

A parameterized dynamic logical ($\mathit{DL}_{p}$) formula is a formula of
the form $\sigma:\phi$, where $\sigma\in\mathbf{Conf}$ is a configuration,
$\phi$ is a GDL formula.

In order to reason about termination of programs in $\mathit{DL}_{p}$ and to
prove the soundness of the proof system of $\mathit{DL}_{p}$ as shown later in
Section 3, the concept of _well-founded relation_ is introduced.

######  Definition 4 (Well-foundedness)

A set is ‘well-founded’ w.r.t. a partially-ordered relation $<$, if for any
element $a$ in this set, there is no infinite descent sequence:
$a>a_{1}>a_{2}>...$ in this set. Relation $<$ is also called a _well-founded
relation_.

In $\mathit{DL}_{p}$, we assume a partial function
$\mathcal{T}:\mathbf{Conf}\to\mathbf{TA}(\Sigma)$ that assigns a configuration
$\sigma\in\mathbf{Conf}$ with a sub-term $t$ appeared in $\sigma$, called
_termination factor_. And we assume a well-founded relation $\prec$ between
these termination factors. A termination factor measures how close a program
is from terminations. Usually, we write $\sigma\\{t\\}$ if
$t\equiv\mathcal{T}(\sigma)$. $\mathcal{T}$ is a function as usually we only
care about one such factor. $\mathcal{T}$ is partial as in a configuration
there might not exist such a factor.

###  2.2 Semantics of $\mathit{DL}_{p}$

Traditionally, the semantics of a dynamic logic is denotational and is given
as a Kripke structure [20]. Following a similar manner, to give the semantics
of $\mathit{DL}_{p}$ formulas, we firstly build a special Kripke structure
consisting of closed configurations as worlds, and operational semantics of
programs as relations between worlds. This structure allows us to define a
satisfaction relation of GDL formulas by evaluations and configurations, based
on which, the semantics of $\mathit{DL}_{p}$ is given.

######  Definition 5 (Kripke Structure of GDL)

Given $\mathbf{Prog},\mathbf{Conf}$ and $\Form$, the Kripke structure of GDL
is a triple $M=_{df}(\mathbf{Cl}(\mathbf{Conf}),\to,\mathcal{I})$, where
$\mathbf{Cl}(\mathbf{Conf})$ is the set of closed configurations as ‘worlds’,
$\to\subseteq\mathbf{Cl}(\mathbf{Conf})\times(\mathbf{Cl}(\mathbf{Prog})\times\mathbf{Cl}(\mathbf{Prog}))\times\mathbf{Cl}(\mathbf{Conf})$
is a set of labelled transitions, $\mathcal{I}:\mathbf{Cl}(\mathbf{Form})\to
2^{\mathbf{Cl}(\mathbf{Conf})}$ is an interpretation of closed formulas in
$\mathbf{Form}$ on the set of worlds, satisfying the following conditions:

  1. 1\.

For each world $\sigma$,
$\sigma\xrightarrow{\alpha/\alpha^{\prime}}\sigma^{\prime}$ iff
$((\alpha,\sigma)\longrightarrow(\alpha^{\prime},\sigma^{\prime}))\in\Lambda$.

  2. 2\.

For each formula $\phi\in\mathbf{Cl}(\mathbf{Form})$,
$\sigma\in\mathcal{I}(\phi)$ iff ${\phi}\rhd{\sigma}$ is true.

Different from the traditional Kripke structure (cf. [20]), in the Kripke
structure of GDL, the transitions between worlds are defined according to the
operational semantics, rather than the syntactic structures of programs.

Below we do not distinguish
$\sigma\xrightarrow{\alpha/\alpha^{\prime}}\sigma^{\prime}$ from
$(\alpha,\sigma)\longrightarrow(\alpha^{\prime},\sigma^{\prime})$ and also
call it a ‘transition’, and call
$\sigma_{1}\xrightarrow{\alpha_{1}/\alpha_{2}}\sigma_{2}\xrightarrow{\alpha_{2}/\alpha_{3}}...\xrightarrow{\alpha_{n-1}/\alpha_{n}}\sigma_{n}...$
an “execution path”.

######  Definition 6 (Satisfaction Relation of GDL Formulas on Kripke
Structure)

Given the Kripke structure $M=(\mathbf{Cl}(\mathbf{Conf}),\to,\mathcal{I})$ of
GDL, the satisfaction of a GDL formula $\phi$ w.r.t. an evaluation $\rho$ and
a configuration $\sigma\in\mathbf{Conf}$, denoted by
$\rho,\sigma\models_{M}\phi$ (or simply $\rho,\sigma\models\phi$), is
inductively defined as follows:

  1. 1\.

$\rho,\sigma\models_{M}\phi$ where $\phi\in\mathbf{Form}$, if
$\rho(\sigma)\in\mathcal{I}(\rho(\phi))$.

  2. 2\.

$\rho,\sigma\models_{M}\neg\phi$, if $\rho,\sigma\not\models_{M}\phi$.

  3. 3\.

$\rho,\sigma\models_{M}\phi_{1}\wedge\phi_{2}$, if both
$\rho,\sigma\models_{M}\phi_{1}$ and $\rho,\sigma\models_{M}\phi_{2}$.

  4. 4\.

$\rho,\sigma\models_{M}[\alpha]\phi$, if (1) $\rho(\alpha)$ is $\downarrow$
and $\rho,\sigma\models_{M}\phi$, or (2) for all execution paths
$\sigma\xrightarrow{\rho(\alpha)/\alpha_{1}}...\xrightarrow{\alpha_{n}/\downarrow}\sigma^{\prime}$,
$\rho,\sigma^{\prime}\models_{M}\phi$.

Note that $\rho,\sigma\models_{M}\phi$ differs from $\rho\models\phi$
introduced in Section 2.1 as $\sigma$ has an impact on formula $\phi$ through
operator ${\cdot}\rhd{\cdot}$. The satisfaction relation
$\rho,\sigma\models_{M}\langle\alpha\rangle\phi$ can be formally defined as:
$\rho,\sigma\models_{M}\langle\alpha\rangle\phi$, if (1) $\rho(\alpha)$ is
$\downarrow$ and $\rho,\sigma\models_{M}\phi$, or (2) there exists an
execution path
$\sigma\xrightarrow{\rho(\alpha)/\alpha_{1}}...\xrightarrow{\alpha_{n}/\downarrow}\sigma^{\prime}$
such that $\rho,\sigma^{\prime}\models_{M}\phi$.

We define the semantics of a $\mathit{DL}_{p}$ formula naturally based on the
Kripke structure of GDL and the satisfaction of GDL formulas on the Kripke
structure.

######  Definition 7 (Semantics of $\mathit{DL}_{p}$ Formulas)

The semantics of a $\mathit{DL}_{p}$ formula $\sigma:\phi$ is given as the
satisfaction relation by an evaluation $\rho$ as follows:
$\rho\models\sigma:\phi\mbox{, if $\rho,\sigma\models\phi$}.$

The satisfiability and validity of $\mathit{DL}_{p}$ formulas are introduced
as follows. They are defined in a standard way.

######  Definition 8 (Satisfiability and Validity)

A $\mathit{DL}_{p}$ formula $\sigma:\phi$ is ‘satisfiable’, if there exists an
evaluation $\rho$ such that $\rho\models\sigma:\phi$. A $\mathit{DL}_{p}$
formula $\sigma:\phi$ is ‘valid’, if $\rho\models\phi$ for all evaluations
$\rho$, denoted by $\models\sigma:\phi$.

##  3 A Cyclic Proof System for $\mathit{DL}_{p}$

#### Sequent Calculus

In this paper, we adopt _sequents_ [16] as the derivation form of the logic.
Sequent is a convenient structure for derivation, as it can describe both top-
down and bottom-up natural deductions as bottom-up deductions on the left and
right sides of the arrow ‘$\Rightarrow$’ of a sequent. By using sequents, the
implementation of $\mathit{DL}_{p}$ would become nature in theorem provers
like Coq or Isabelle, whose deduction structure is actually in the form of a
sequent.

A sequent is a logical argumentation of the form: $\Gamma\Rightarrow\Delta,$
where $\Gamma$ and $\Delta$ are finite multisets of formulas.
$\Gamma\Rightarrow\Delta$ expresses the formula
$(\bigwedge_{\phi\in\Gamma}\phi)\to(\bigvee_{\phi\in\Delta}\phi)$. In this
paper, we do not distinguish a sequent and its corresponding formula.

An inference rule in a sequent calculus is of the form $\begin{aligned}
\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma_{1}\Rightarrow\Delta_{1}...\Gamma_{n}\Rightarrow\Delta_{n},\end{aligned}$
where $\Gamma_{1}\Rightarrow\Delta_{1}$,…,$\Gamma_{n}\Rightarrow\Delta_{n}$
are called _premises_ , $\Gamma\Rightarrow\Delta$ is called a _conclusion_.
The semantics of the rule is that the validity of sequents
$\Gamma_{1}\Rightarrow\Delta_{1}$,…,$\Gamma_{n}\Rightarrow\Delta_{n}$ implies
the validity of sequent $\Gamma\Rightarrow\Delta$.

A _proof tree_ is a tree structure formed by deducing a sequent as a
conclusion backwardly by consecutively applying a set of proof rules. In a
proof tree, each node is a sequent of an instance of a proof rule. The root
node of the tree is the conclusion. Each leaf node of the tree is called
_terminal_ , if it is a sequent of an instance of an axiom.

###  3.1 A Proof System for $\mathit{DL}_{p}$

As shown in Table 2, the proof system of $\mathit{DL}_{p}$ consists of a set
of rules for deriving $\mathit{DL}_{p}$ labeled dynamic formulas based on
program executions according to their operational semantics. These rules forms
the core part of a general verification framework in which to prove the
validity of a $\mathit{DL}_{p}$ formula, we transform it into proof
obligations of the formulas in $\mathbf{Form}$. Notice that in practical
deductions, additional rules in special domains may be needed for constructing
suitable labelled formulas in order to obtain a preproof structure. See
Section 4.1 for an example.

$\begin{aligned}
\Gamma\Rightarrow\sigma:[\alpha]\phi,\Delta\\{\Gamma\Rightarrow\sigma^{\prime}:[\alpha^{\prime}]\phi,\Delta\\}_{(\alpha^{\prime},\sigma^{\prime})\in\Phi}\end{aligned}$,
where $\par\Phi=\left\\{(\alpha^{\prime},\sigma^{\prime})\ \left|\
\begin{aligned} &\mbox{for any $\rho$, if $\rho\models\Gamma$,}\\\ &\mbox{then
$((\rho(\alpha),\rho(\sigma))\longrightarrow(\rho(\alpha^{\prime}),\rho(\sigma^{\prime})))\in\Lambda$}\end{aligned}\right.\right\\}$
$\begin{aligned}
\Gamma\Rightarrow\sigma\\{t\\}:\langle\alpha\rangle\phi,\Delta\Gamma\Rightarrow\sigma^{\prime}\\{t^{\prime}\\}:\langle\alpha^{\prime}\rangle\phi,\Delta\end{aligned}$,
for any $\rho$, if $\rho\models\Gamma$, then $\begin{aligned}
((\rho(\alpha),\rho(\sigma))\longrightarrow(\rho(\alpha^{\prime}),\rho(\sigma^{\prime})))\in\Lambda,\end{aligned}$
$t^{\prime}\preceq t$ $\Gamma\Rightarrow\Delta$
$\Gamma\Rightarrow\sigma:[\downarrow]\phi,\Delta\Gamma\Rightarrow\sigma:\phi,\Delta$
$\Gamma\Rightarrow\sigma:\langle\downarrow\rangle\phi,\Delta\Gamma\Rightarrow\sigma:\phi,\Delta$
$\Gamma\Rightarrow\sigma:[\uparrow]\phi,\Delta$
$\Gamma\Rightarrow\sigma:(\neg\phi),\Delta\Gamma,\sigma:\phi\Rightarrow\Delta$
$\Gamma,\sigma:(\neg\phi)\Rightarrow\Delta\Gamma\Rightarrow\sigma:\phi,\Delta$
$\Gamma\Rightarrow\sigma:(\phi\wedge\psi),\Delta\lx@proof@logical@and\Gamma\Rightarrow\sigma:\phi,\Delta\Gamma\Rightarrow\sigma:\psi,\Delta$
$\Gamma\Rightarrow\sigma:(\phi\vee\psi),\Delta\Gamma\Rightarrow\sigma:\phi,\sigma:\psi,\Delta$
$\Gamma\Rightarrow\sigma:\phi,\Delta\Gamma\Rightarrow{\phi}\rhd{\sigma},\Delta$
1 (1) for each formula $\phi$ in $\Gamma$ or $\Delta$, $\phi\in\mathbf{Form}$;
(2) $\Gamma\Rightarrow\Delta$ is valid. 2
$\alpha\notin\\{\downarrow,\uparrow\\}$. 3 $\phi\in\mathbf{Form}$.

Table 2: A Proof System for $\mathit{DL}_{p}$

Rules $([\alpha]\sigma)$ and $(\langle\alpha\rangle\sigma)$ deal with dynamic
parts of $\mathit{DL}_{p}$ formulas based on the operational semantics of
programs. In rule $([\alpha]\sigma)$,
$\\{...\\}_{(\alpha^{\prime},\sigma^{\prime})\in\Phi}$ represents the
collection of premises for all $(\alpha^{\prime},\sigma^{\prime})\in\Phi$.
$\Phi$ is a set consisting of distinct elements w.r.t. equivalence $=$ between
terms. In other words, for any $t_{1},t_{2}\in\Phi$, $t_{1}\neq t_{2}$. By II
of Definition 1, set $\Phi$ is finite. So rule $([\alpha]\sigma)$ has a finite
number of premises. We write ‘$\rho\models\Gamma$’ to mean that
$\rho\models\phi$ for each $\phi\in\Gamma$. Intuitively, rule
$([\alpha]\sigma)$ says that to prove that $[\alpha]\phi$ holds under
configuration $\sigma$ in the context $\Gamma$, we prove that for any
execution from $(\alpha,\sigma)$ to $(\alpha^{\prime},\sigma^{\prime})$
(w.r.t. a $\rho$), $[\alpha^{\prime}]\phi$ holds under configuration
$\sigma^{\prime}$ in the context $\Gamma$. Compared to rule
$([\alpha]\sigma)$, rule $(\langle\alpha\rangle\sigma)$ only has one premise
for some pair $(\alpha^{\prime},\sigma^{\prime})$. Termination factor $t$ is
required by partial function $\mathcal{T}$ in $\sigma$ to indicate program
terminations. Intuitively, rule $(\langle\alpha\rangle\sigma)$ says that to
prove $\langle\alpha\rangle\phi$ holds under configuration $\sigma$ in the
context $\Gamma$, after some execution from $(\alpha,\sigma)$ to
$(\alpha^{\prime},\sigma^{\prime})$ (w.r.t. a $\rho$),
$\langle\alpha^{\prime}\rangle\phi$ holds under configuration
$\sigma^{\prime}$ in the context $\Gamma$. At the same time, the termination
factor $t^{\prime}$ is forbidden to grow larger than $t$ w.r.t. the well-
founded relation $\prec$. Note that in both rules $([\alpha]\sigma)$ and
$(\langle\alpha\rangle\sigma)$, we assume that there always exists an
execution from $(\alpha,\sigma)$ to $(\alpha^{\prime},\sigma^{\prime})$
(w.r.t. a $\rho$) since $\alpha$ is neither $\downarrow$ nor $\uparrow$. This
is guaranteed by the well-definedness of the operational semantics, as stated
in I of Definition 1.

Note that in practice, form $(\alpha^{\prime},\sigma^{\prime})$ in rule
$(\sigma[\alpha]\phi)$, $(\sigma\langle\alpha\rangle)$ can be easily obtained
by the program’s operational semantics. Check Section 4.1 for an example.

Rule $(\sigma\textit{Ter})$ declares a termination of a proof branch. When
each formula in $\Gamma$ and $\Delta$ is a formula in $\mathbf{Form}$. We can
conclude the proof branch if sequent $\Gamma\Rightarrow\Delta$ is valid.

Rules $([\downarrow]\sigma)$, $(\langle\downarrow\rangle\sigma)$ and
$([\uparrow]\sigma)$ deal with the situations when program $\alpha$ is either
a termination $\downarrow$ or an abortion $\uparrow$. Note that there is no
rules for formula $\sigma:\langle\uparrow\rangle\phi$. Intuitively, it is not
hard to see that $\langle\uparrow\rangle\phi$ is false under any configuration
because $\uparrow$ never terminates.

Rules $(\neg\sigma R)$, $(\neg\sigma L)$, $(\wedge\sigma)$ and $(\vee\sigma)$
deal with logic connectives $\neg$, $\wedge$ and $\vee$ in a labelled
$\mathit{DL}_{p}$ formula. They correspond to the rules in traditional
propositional logic (without labels) for $\neg$, $\wedge$ and $\vee$. Note
that rule $(\vee\sigma)$ is primitive, as rule $(\wedge\sigma)$ only expresses
the deduction on the right side of the sequent for connective $\wedge$.

Rule $(\sigma\textit{Int})$ is an introduction rule for labels, used when
$\phi$ is a formula in $\mathbf{Form}$ without any dynamic parts. To prove
that $\phi$ holds under configuration $\sigma$, we prove that
${\phi}\rhd{\sigma}$ is a valid formula.

In the above rules, we often call the formulas distinguished from $\Gamma$ and
$\Delta$ that are changed from the conclusion to the premise the _target
formulas_ of the rule.

###  3.2 Infiniteness of $\mathit{DL}_{p}$ Proof System and Well-founded
Relations

Based on the semantics of $\mathit{DL}_{p}$ given in Section 2.2, it is not
hard to prove that each proof rule of Table 2 is sound. When each branch of a
proof tree terminates with a valid sequent in $\mathbf{Form}$, the whole proof
is sound.

However, a branch of a proof tree in $\mathit{DL}_{p}$ system does not always
terminate, since the process of symbolically executing a program via rule
$([\alpha]\sigma)$ or/and rule $(\langle\alpha\rangle\sigma)$ might not stop.
This is well known when a program has a loop structure that may runs
infinitely, for example, a while program $\textit{while}\ \textit{true}\
\textit{do}\ x:=x+1\ \textit{end}$.

To avoid potentially infinite derivations in $\mathit{DL}_{p}$, in this paper,
we adopt the so-called _cyclic proof_ approach (cf. [10]), a technique to
insure a sound conclusion even when its proof tree contains infinite
derivations. A _preproof_ is a proof tree with a finite structure (which means
having a finite number of nodes) but containing infinite derivation paths. A
preproof structure can lead to a sound conclusion if a certain soundness
condition is met. This condition guarantees that any counterexamples from an
invalid conclusion would cause an infinite descent sequence w.r.t. a well-
founded relation (Definition 4) that is related to the semantics of
$\mathit{DL}_{p}$, which, however, is a contradiction to the definition of the
well-foundedness itself. We will expand it in detail in Section 3.3.

To apply the cyclic proof approach, we need 3 critical well-founded relations
that are related to the semantics of $\mathit{DL}_{p}$. One of them, relation
$\prec$, has already been introduced in Section 2.1. With these relations, in
Section 3.3, we will define a preproof structure, and give the soundness
condition in which a preproof is a sound proof.

In the following, we introduce another 2 well-founded relations. The first
relation $\prec_{s}$ is the suffix relation between two execution paths; while
the second relation $\prec_{m}$ is between two finite sets of execution paths.

######  Definition 9 (Relation $\prec_{s}$)

Given two execution paths $tr_{1}$ and $tr_{2}$, relation
$tr_{1}\prec_{s}tr_{2}$ is defined if $tr_{2}$ is a proper suffix of $tr_{1}$.
Write $tr_{1}\preceq_{s}tr_{2}$ if $tr_{1}$ is a suffix of $tr_{2}$.

It is trivial that in a set of finite paths, relation $\prec_{s}$ is well-
founded. Because every finite path has only a finite number of suffixes.

Relation $\prec_{m}$ is based on the definition of relation $\prec_{s}$.

######  Definition 10 (Relation $\prec_{m}$)

Given two finite sets $\mathit{C}_{1}$ and $\mathit{C}_{2}$ of finite paths,
$\mathit{C}_{1}\prec_{m}\mathit{C}_{2}$ is defined if set $\mathit{C}_{1}$ can
be obtained from $\mathit{C}_{2}$ by replacing (or removing) one or more
elements of $\mathit{C}_{2}$ with a finite number of elements, such that for
each replaced element $tr\in\mathit{C}_{2}$, its replacements
$tr_{1},...,tr_{n}$ ($n\geq 1$) in $\mathit{C}_{1}$ satisfies that
$tr_{i}\prec_{s}tr$ for any $i$, $1\leq i\leq n$.

Write $\mathit{C}_{1}\preceq_{m}\mathit{C}_{2}$ if
$\mathit{C}_{1}=\mathit{C}_{2}$ or $\mathit{C}_{1}\prec_{m}\mathit{C}_{2}$.

Note that in Definition 10 it is not hard to see that
$\mathit{C}_{1}\prec_{m}\mathit{C}_{2}$ implies
$\mathit{C}_{1}\neq\mathit{C}_{2}$.

For example, let $C_{1}=\\{tr_{1},tr_{2},tr_{3}\\}$, where
$tr_{1}=_{df}(\alpha,\sigma)\longrightarrow(\alpha_{1},\sigma_{1})\longrightarrow(\alpha_{2},\sigma_{2})\longrightarrow(\alpha_{3},\sigma_{3})\longrightarrow(\downarrow,\sigma_{4}),tr_{2}=_{df}(\alpha,\sigma)\longrightarrow(\alpha_{1},\sigma_{1})\longrightarrow(\beta_{1},\delta_{1})\longrightarrow(\beta_{2},\delta_{2})\longrightarrow(\downarrow,\delta_{3})$
and $tr_{3}=_{df}(\alpha,\sigma)\longrightarrow(\downarrow,\tau)$;
$C_{2}=\\{tr^{\prime}_{1},tr^{\prime}_{2}\\}$, where
$tr^{\prime}_{1}=_{df}(\alpha_{1},\sigma_{1})\longrightarrow(\alpha_{2},\sigma_{2})\longrightarrow(\alpha_{3},\sigma_{3})\longrightarrow(\downarrow,\sigma_{4}),tr^{\prime}_{2}=_{df}(\alpha_{1},\sigma_{1})\longrightarrow(\beta_{1},\delta_{1})\longrightarrow(\beta_{2},\delta_{2})\longrightarrow(\downarrow,\delta_{3})$.
We see that $tr^{\prime}_{1}\prec_{s}tr_{1}$ and
$tr^{\prime}_{2}\prec_{s}tr_{2}$. $C_{2}$ can be obtained from $C_{1}$ by
replacing $tr_{1}$ and $tr_{2}$ with $tr^{\prime}_{1}$ and $tr^{\prime}_{2}$
respectively, and removing $tr_{3}$. Hence $C_{2}\prec_{m}C_{1}$.

Relation $\prec_{m}$ is in fact a special case of the “multiset ordering”
introduced in [12], where it has shown that multiset ordering is well-founded.
Therefore, $\prec_{m}$ is well-founded.

###  3.3 Construction of A Cyclic Preproof Structure in $\mathit{DL}_{p}$

A _preproof_ is a finite proof tree in which each non-terminal node is
identical to one of its ancestors in the tree. Such a non-terminal node is
called a _bud_ (cf. [10]). The ancestor equivalent to a bud $N$ is called a
_companion of $N$_. A bud and one of its companions is together called a
_back-link_.

A _derivation path_ in a preproof is a possibly infinite sequence of nodes
$n_{1}n_{2}...n_{m}...$ ($m\geq 1$) starting from the root $n_{1}$, where each
pair of nodes $(n_{i},n_{i+1})$ $(i\geq 1)$ is either a conclusion-premise
pair of the instance of a proof rule, or a back-link of the preproof. A
_derivation trace_ is a possibly infinite sequence
$\tau_{1}\tau_{2}...\tau_{m}...$ of formulas over a derivation path
$n_{1}n_{2}...n_{m}...$ ($m\geq 1$) such that each $\tau_{i}$ is a formula
appeared in node $n_{i}$ ($i\geq 1$).

We introduce the notion of _(progressive) derivation traces_ (cf. [10]) in a
preproof of $\mathit{DL}_{p}$, which is critical for a preproof structure to
be a sound proof. The key idea is that if each derivation trace of a preproof
structure is progressive, then it is impossible for the conclusion of the
preproof to be invalid. Otherwise, an infinite descent sequence of
counterexamples of finite sets of execution traces of a program can be
constructed, contradicting the fact that the relation $\prec_{s}$ or
$\prec_{m}$ mentioned in Section 3.2 is well-founded.

######  Definition 11 (Progressive Step/Progressive Derivation Trace in
$\mathit{DL}_{p}$)

In a preproof of $\mathit{DL}_{p}$, given an infinite derivation trace
$\tau_{1}\tau_{2}...\tau_{m}...$ along a derivation path
$n_{1}n_{2}...n_{m}...$ ($m\geq 1$), a formula pair $(\tau_{i},\tau_{i+1})$
($1\leq i\leq m$) of the derivation trace is called a “progressive step”, if
$\tau_{i},\tau_{i+1}$ are the formulas appeared in the sequent pair
$(n_{i},n_{i+1})$ respectively, as:

$\begin{gathered}n_{i}:\Gamma\Rightarrow\sigma:[\alpha]\phi,\Delta,\\\
n_{i+1}:\Gamma\Rightarrow\sigma^{\prime}:[\alpha^{\prime}]\phi,\Delta,\end{gathered}$

which is in an instance of rule $([\alpha]\sigma)$ and where $\tau_{i}$ is
formula $\sigma:[\alpha]\phi$, $\tau_{i+1}$ is formula
$\sigma^{\prime}:[\alpha^{\prime}]\phi$;

Or as:

$\begin{gathered}n_{i}:\Gamma\Rightarrow\sigma\\{t\\}:\langle\alpha\rangle\phi,\Delta,\\\
n_{i+1}:\Gamma\Rightarrow\sigma^{\prime}\\{t^{\prime}\\}:\langle\alpha^{\prime}\rangle\phi,\Delta,\end{gathered}$

which is in an instance of rule $(\langle\alpha\rangle\sigma)$ and where
$\tau_{i}$ is formula $\sigma\\{t\\}:\langle\alpha\rangle\phi$, $\tau_{i+1}$
is formula
$\sigma^{\prime}\\{t^{\prime}\\}:\langle\alpha^{\prime}\rangle\phi$, and
termination factors $t,t^{\prime}$ satisfy $t^{\prime}\prec t$.

If a derivation trace has an infinite number of progressive steps, we say that
the trace is ‘progressive’, or it is a “progressive trace”.

Note that when $(n_{i},n_{i+1})$ is in an instance of rule
$(\langle\alpha\rangle\sigma)$, the execution from $(\alpha,\sigma)$ to
$(\alpha^{\prime},\sigma^{\prime})$ observes a termination factor $t^{\prime}$
strictly less than $t$ w.r.t. relation $\prec$. This, as will be seen later in
Section 3.4, actually indicates the termination of a counter-example path of
program $\alpha$, which is the key to prove Theorem 3.1.

Now we give the soundness condition for a preproof structure to lead a sound
conclusion in $\mathit{DL}_{p}$.

######  Definition 12 (A Cyclic Preproof of $\mathit{DL}_{p}$)

In $\mathit{DL}_{p}$, a preproof is a ‘cyclic’ one, if there exists a
progressive trace along any infinite derivation path.

The following theorem is the main result of this section.

######  Theorem 3.1 (Soundness of A Cyclic Preproof of $\mathit{DL}_{p}$)

A cyclic preproof of $\mathit{DL}_{p}$ always has a valid conclusion.

#### About the Completeness of $\mathit{DL}_{p}$

Since $\mathit{DL}_{p}$ is not a specific logic in traditional sense, its
completeness relies on specific structures of programs, configurations and
formulas given as $\mathbf{Prog},\mathbf{Conf}$ and $\mathbf{Form}$
respectively. The completeness of $\mathit{DL}_{p}$ depends on whether we can
build a cyclic preproof for every valid formula in this logic by constructing
suitable configurations so that every infinite derivation path has a
progressive derivation trace.

###  3.4 Soundness of the Cyclic Proof System for $\mathit{DL}_{p}$

In this subsection, we analyze and prove Theorem 3.1. We only focus on the
case when the conclusion is of the form $\Gamma\Rightarrow\sigma:[\alpha]\phi$
or $\Gamma\Rightarrow\sigma:\langle\alpha\rangle$, where dynamic
$\mathit{DL}_{p}$ formulas $\sigma:[\alpha]\phi$ and
$\sigma:\langle\alpha\rangle\phi$ are the only formula on the right side of
the sequent. Other cases are trivial.

To prove Theorem 3.1 we need to show that if a preproof is cyclic (Definition
12), that is, if any infinite derivation path is followed by a progressive
trace, then the conclusion is valid. The proof is carried out by contradiction
following the main idea behind [8]. Suppose the conclusion is invalid, that
is, $\Gamma\Rightarrow\sigma:[\alpha]\phi$ (resp.
$\Gamma\Rightarrow\sigma:\langle\alpha\rangle\phi$) is invalid. Then we show
that it induces an infinite descent sequence of elements ordered by well-
founded relation $\prec_{m}$ introduced in Section 3.2, which is contradict to
Definition 4.

Before proving Theorem 3.1, we need some preparations stated as the following
lemmas and definitions.

###### Definition 13

A “counter-example” $F(\rho,\alpha,\sigma,\phi)$ of a formula
$\tau\in\\{\sigma:[\alpha]\phi,\sigma:\langle\alpha\rangle\phi\\}$ is a set of
minimum terminal execution paths defined as: $\begin{aligned}
F(\rho,\alpha,\sigma,\phi)=_{df}\\{(\rho(\alpha),\rho(\sigma))\longrightarrow^{*}(\downarrow,\sigma^{\prime})\
|\ \rho,\sigma^{\prime}\not\models\phi\\}.\end{aligned}$

Recall that a path being minimum is defined in Section 2.1.

Intuitively, a _corresponding path_ is a result of symbolic executions by the
instances of rules $(\sigma[\alpha])$ and $(\sigma\langle\sigma\rangle)$ along
a derivation trace.

###### Definition 14

Given a derivation trace $\tau_{1}\tau_{2}...\tau_{m}...$ over a derivation
path $n_{1}n_{2}...n_{m}...$ ($m\geq 1$), where
$\tau_{1}\in\\{\sigma:[\alpha]\phi,\sigma:\langle\alpha\rangle\phi\\}$, each
pair $(\tau_{i},\tau_{i+1})$ ($i\geq 1$) either satisfies
$\tau_{i}\equiv\tau_{i+1}$ or $(n_{i},n_{i+1})$ is a conclusion-premise pair
of an instance of rule $(\sigma[\alpha])$ or $(\sigma\langle\alpha\rangle)$, a
“corresponding path”
$(\alpha_{1},\sigma_{1})\longrightarrow...\longrightarrow(\alpha_{n},\sigma_{n})\longrightarrow...$
($n\geq 1$) of the derivation trace $\tau_{1}\tau_{2}...\tau_{m}...$ satisfies
that $\alpha_{1}\in\mathbf{Cl}(\alpha),\sigma_{1}\in\mathbf{Cl}(\sigma)$, and
for any $(\alpha_{k},\sigma_{k})\longrightarrow(\alpha_{k+1},\sigma_{k+1})$
($k\geq 1$) of the path and formula
$\tau_{i}=_{df}\sigma_{i}:[\alpha_{i}]\phi$ (resp.
$\tau_{i}=_{df}\sigma_{i}:\langle\alpha_{i}\rangle\phi$, $i\geq 1$) such that
$\alpha_{k}\in\mathbf{Cl}(\alpha_{i})$ and
$\sigma_{k}\in\mathbf{Cl}(\sigma_{i})$, there is a pair
$(\tau_{j},\tau_{j+1})$ over $(n_{j},n_{j+1})$ ($i\leq j$) such that
$\tau_{i}\equiv...\equiv\tau_{j}$, $(n_{i},n_{i+1})$ is a conclusion-premise
pair of an instance of rule $(\sigma[\alpha])$ (resp. rule
$(\sigma\langle\alpha\rangle)$), and
$\tau_{j+1}=_{df}\sigma_{j+1}[\alpha_{j+1}]\phi$ (resp.
$\tau_{j+1}=_{df}\sigma_{j+1}\langle\alpha_{j+1}\rangle\phi$) such that
$\alpha_{k+1}\in\mathbf{Cl}(\alpha_{i})$ and
$\sigma_{k+1}\in\mathbf{Cl}(\sigma_{i})$.

###### Lemma 1

In a cyclic preproof of sequent
$\Gamma\Rightarrow\sigma:\langle\alpha\rangle\phi$, given an evaluation $\rho$
satisfying $\rho\models\Gamma$, any corresponding path $tr$ starting from
$(\rho(\alpha),\rho(\sigma))$ of an infinite derivation trace
$\tau_{1}\tau_{2}...$ starting from
$\tau_{1}=_{df}\sigma:\langle\alpha\rangle\phi$ eventually terminates.

###### Proof

Since every derivation trace is progressive, according to rule
$(\sigma\langle\alpha\rangle)$ and Definition 14, if path $tr$ does not
terminate, then along the path there exists an infinite sequence of
configurations $\sigma_{1}\\{t_{1}\\},...,\sigma_{n}\\{t_{n}\\}...$ where
their termination factors satisfy $t_{1}\succ...\succ t_{n}\succ...$. This
violates the well-foundedness of relation $\prec$ (see below Definition 4).
$\Box$

###### Lemma 2

In a cyclic preproof, let
$\tau\in\\{\sigma:[\alpha]\phi,\sigma:\langle\alpha\rangle\phi\\}$ be a
formula in an invalid node $n=_{df}(\Gamma\Rightarrow\tau)$,
$\rho\models\Gamma$, and $F(\rho,\alpha,\sigma,\phi)$ is a finite counter-
example of $\tau$. Then there exists a formula pair $(\tau,\tau^{\prime})$
appeared in the node pair $(n,n^{\prime})$ and a set
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$ such that $n^{\prime}$ is
invalid, $F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$ is a finite counter-
example of $\tau^{\prime}$, and
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)\preceq_{m}F(\rho,\alpha,\sigma,\phi)$.
Moreover, if $(\tau,\tau^{\prime})$ is a progressive step, then
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)\prec_{m}F(\rho,\alpha,\sigma,\phi)$.

###### Proof

Consider the rule application from node $n$, actually the only non-trivial
cases are when it is an instance of rule $([\alpha]\sigma)$ (namely “case 1”)
or rule $(\langle\alpha\rangle\sigma)$ (namely “case 2”).

Case 1:  If from node $n$ rule $([\alpha]\sigma)$ is applied with
$\tau=_{df}\sigma:[\alpha]\phi$ the target formula in $n$, by
$\rho\models\Gamma$ and the invalidity of $n$,
$\rho\not\models\sigma:[\alpha]\phi$. By the semantics of
$\sigma:[\alpha]\phi$, there is a pair $(\alpha^{\prime},\sigma^{\prime})$ and
a transition
$(\rho(\alpha),\rho(\sigma))\longrightarrow(\rho(\alpha^{\prime}),\rho(\sigma^{\prime}))\in\Lambda$
such that $\rho\not\models\sigma^{\prime}:[\alpha^{\prime}]\phi$. This means
that there exists an invalid sequent
$n^{\prime}=_{df}\Gamma\Rightarrow\tau^{\prime}$ as a premise of $n$, in which
formula $\tau^{\prime}=_{df}\sigma^{\prime}:[\alpha^{\prime}]\phi$ is invalid.
And because of this, $F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$ is non-
empty. We observe that by the transition
$(\rho(\alpha),\rho(\sigma))\longrightarrow(\rho(\alpha^{\prime}),\rho(\sigma^{\prime}))$,
each path in $F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$ is actually a
proper suffix of a path in $F(\rho,\alpha,\sigma,\phi)$. So from the
finiteness of $F(\rho,\alpha,\sigma,\phi)$, we obtain the finiteness of
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$, and by Definition 10, we have
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)\prec_{m}F(\rho,\alpha,\sigma,\phi)$.

Case 2:  If from node $n$ rule $(\langle\alpha\rangle\sigma)$ is applied with
$\tau=_{df}\sigma:\langle\alpha\rangle\phi$ the target formula in $n$, let
$n^{\prime}=_{df}\Gamma\xRightarrow{}\tau^{\prime}$ and
$\tau^{\prime}=_{df}\sigma^{\prime}:\langle\alpha^{\prime}\rangle\phi$. By
Lemma 1, any path
$(\rho(\alpha),\rho(\sigma))\longrightarrow(\rho(\alpha^{\prime}),\rho(\sigma^{\prime}))\longrightarrow^{*}(\downarrow,\sigma^{\prime\prime})$
that corresponds to an infinite derivation trace $\tau_{1}\tau_{2}...$
starting from $\tau_{1}=_{df}\sigma:\langle\alpha\rangle\phi$ and
$\tau_{2}=_{df}\sigma^{\prime}:\langle\alpha^{\prime}\rangle\phi$ in the sense
of Definition 14 eventually terminates. And since
$\rho\not\models\sigma:\langle\alpha\rangle\phi$,
$\rho,\sigma^{\prime\prime}\not\models\phi$. As there must exist an infinite
derivation trace $\tau_{1}\tau_{2}...$ as described above (otherwise violating
the assumption that $n$ is invalid),
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$ is non-empty. By the transition
$(\rho(\alpha),\rho(\sigma))\longrightarrow(\rho(\alpha^{\prime}),\rho(\sigma^{\prime}))$,
each path in $F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$ is a proper suffix
of $F(\rho,\alpha,\sigma,\phi)$. So the finiteness of
$F(\rho,\alpha,\sigma,\phi)$ implies the finiteness of
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$, and we have
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)\prec_{m}F(\rho,\alpha,\sigma,\phi)$.
$\Box$

From the “case 2” of the above proof, we see that it does not have to be a
progressive step in order to obtain a strictly-smaller-than relation
$F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)\prec_{m}F(\rho,\alpha^{\prime},\sigma^{\prime},\phi)$.
However, progressive steps are still required for proving the termination of
paths in Lemma 1.

As the end of this subsection, we give the proof of Theorem 3.1 as follows.

######  Proof (Proof of Theorem 3.1)

As stated previously we only focus on the cases where the conclusion of a
cyclic preproof is either of the form $\Gamma\Rightarrow\sigma:[\alpha]\phi$
or $\Gamma\Rightarrow\sigma:\langle\alpha\rangle\phi$.

Let $\tau\in\\{\sigma:[\alpha]\phi,\sigma:\langle\alpha\rangle\phi\\}$.
Suppose $\Gamma\Rightarrow\tau$ is invalid. If the counter-example set
$F(\rho,\alpha,\sigma,\phi)$ of $\tau$ is finite, according to Lemma 2, we can
obtain an infinite derivation trace $\tau_{1}\tau_{2}...\tau_{m}...$ over a
derivation path $n_{1}n_{2}...n_{m}...$ ($m\geq 1$) and each set $F_{i}$ (with
$F_{1}=_{df}F(\rho,\alpha,\sigma,\phi)$) as a finite counter-example of
formula $\tau_{i}$ ($i\geq 1$). Note that there must exist at least one
infinite derivation trace, otherwise, $\Gamma\xRightarrow{}\tau$ is valid. By
Lemma 2, from these counter-examples we obtain an infinite relation chain:
$F_{1}\succeq_{m}F_{2}\succeq_{m}...\succeq_{m}F_{m}\succeq_{m}...$. Moreover,
since $\tau_{1}\tau_{2}...\tau_{m}...$ is progressive (Definition 12), there
must be an infinite number of relation $\succ_{m}$ among these relations. This
thus forms an infinite descent sequence w.r.t. relation $\succ_{m}$, violating
the well-foundedness of relation $\succ_{m}$ (cf. Section 3.2).

It remains to show that $F(\rho,\alpha,\sigma,\phi)$ is finite in different
cases of $\tau$. However, this is direct by III of Definition 1. $\Box$

##  4 Case Studies

In this section, we give two case studies from different types of programs as
described in Table 1, showing how the proposed $\mathit{DL}_{p}$ can be used
to derive different types of programs step by step according to their
operational semantics and how it lifts other rules in specific domains.

###  4.1 Example One: A While Program

The first example is a traditional while program:

$\textit{WP}_{1}=_{df}\\{s:=0;\ \textit{while}\ (n>0)\ \textit{do}\ s:=s+n;\
n:=n-1\ \textit{end}\ \\}.$

Given an initial value of variables $n$, this program computes the sum from
$n$ to $1$ stored in variable $s$. We prove a property described in a sequent
of $\mathit{DL}_{p}$ formulas as follows:

$P_{1}=_{df}\sigma_{1}:(n\geq
0)\Rightarrow\sigma_{1}:[\textit{WP}_{1}](s=\frac{(n+1)n}{2}),$

where $\sigma_{1}=_{df}\\{n\mapsto v,s\mapsto u\\}$ with $v,u$ free variables.
$P_{1}$ says that given an initial value of $n$, after executing $E_{1}$, $s$
equals to $((n+1)n)/2$, which is the sum of $1+2+...+n$.

A configuration $\sigma$ of a while program is a storage that maps some
variable to a value of the integer domain $\mathbb{Z}$. For example,
$\\{n\mapsto 100,s\mapsto 0\\}$ denotes a configuration that maps $n$ to $100$
and $s$ to $0$. Part of the operation semantics of Program $\textit{WP}_{1}$
are described as inference rules in Table 1. ${\phi}\rhd{\sigma}$ is defined
as the formula after the variable assignments according to configuration
$\sigma$ in $\phi$. For example, ${(n\geq 0)}\rhd{\\{n\mapsto 1,s\mapsto
0\\}}$ assigns $n$ to $1$ in $n\geq 0$ and thus we get $1\geq 0$.

$123\lx@proof@logical@and 491011125678$ 1: $\sigma_{1}(v,u):(n\geq
0)\Rightarrow\sigma_{1}(v,u):[s:=0;\ \alpha_{1}]\phi_{1}$ 2:
$\sigma_{1}(v,u):(n\geq 0)\Rightarrow\sigma_{2}(v):[\textit{while}\ (n>0)\
\textit{do}\ \beta_{1}\ \textit{end}\ ]\phi_{1}$ 3: $\sigma_{1}(v,u):(n\geq
0)\Rightarrow\mbox{\textul{$\sigma_{3}(v):[\textit{while}\ (n>0)\ \textit{do}\
\beta_{1}\ \textit{end}\ ]\phi_{1}$}}$ 4:
$\sigma_{1}(v,u):(n>0)\Rightarrow\mbox{\textul{$\sigma_{3}(v):[\textit{while}\
(n>0)\ \textit{do}\ \beta_{1}\ \textit{end}\ ]\phi_{1}$}}$ 5:
$\sigma_{1}(v,u):(n=0)\Rightarrow\sigma_{3}(v):[\textit{while}\ (n>0)\
\textit{do}\ \beta_{1}\ \textit{end}\ ]\phi_{1}$ 6:
$\sigma_{1}(v,u):(n=0)\Rightarrow\sigma_{3}(v):[\downarrow]\phi_{1}$ 7:
$\sigma_{1}(v,u):(n=0)\Rightarrow\sigma_{3}(v):(s=((n+1)n)/2)$ 8:
$\sigma_{1}(v,u):(n=0)\Rightarrow{(s=((n+1)n)/2)}\rhd{\sigma_{3}(v)}$ 9:
$\sigma_{1}(v,u):(n>0)\Rightarrow\mbox{\textul{$\sigma_{4}(v):[n:=n-1;\
\alpha_{1}]\phi_{1}$}}$ 10:
$\sigma_{1}(v,u):(n>0)\Rightarrow\mbox{\textul{$\sigma_{5}(v):[\textit{while}\
(n>0)\ \textit{do}\ \beta_{1}\ \textit{end}\ ]\phi_{1}$}}$ 11:
$\sigma_{1}(v^{\prime},u):(n\geq
0)\Rightarrow\mbox{\textul{$\sigma_{3}(v^{\prime}):[\textit{while}\ (n>0)\
\textit{do}\ \beta_{1}\ \textit{end}\ ]\phi_{1}$}}$ 12:
$\sigma_{1}(v,u):(n\geq
0)\Rightarrow\mbox{\textul{$\sigma_{3}(v):[\textit{while}\ (n>0)\ \textit{do}\
\beta_{1}\ \textit{end}\ ]\phi_{1}$}}$ $\alpha_{1}=_{df}\textit{while}\ (n>0)\
\textit{do}\ \beta_{1}\ \textit{end}$ $\beta_{1}=_{df}s:=s+n;\ n:=n-1$
$\phi_{1}=_{df}(s=((n+1)n)/2)$ $\sigma_{1}(v,u)=_{df}\\{n\mapsto v,s\mapsto
u\\}$ $\sigma_{2}(v)=_{df}\\{n\mapsto v,s\mapsto 0\\}$
$\sigma_{3}(v)=_{df}\left\\{\begin{array}[]{l}n\mapsto v,\\\
s\mapsto((n+v+1)(n-v))/2\end{array}\right\\}$
$\sigma_{4}(v)=_{df}\left\\{\begin{array}[]{l}n\mapsto v,\\\
s\mapsto((n+v)(n-v+1))/2\end{array}\right\\}$
$\sigma_{5}(v)=_{df}\left\\{\begin{array}[]{l}n\mapsto v-1,\\\
s\mapsto((n+v)(n-v+1))/2\end{array}\right\\}$

Figure 1: Derivations of Example 1

Figure 1 shows the derivation of this formula. The inferences with no names
aside do not belong to Table 2, but are the additional rules for constructing
proper labelled formulas. The derivation from sequent 2 to 3 is according to
the fact that $\sigma_{2}(v)=\sigma_{3}(v)$. Configuration $\sigma_{3}(v)$
constructed in sequent 3 is crucial, as starting from it, we can find a bud
node — 12 — that is identical to it. The derivation from sequent 3 to {4, 5}
is dividing sequent 3 into two cases: $n>0$ and $n=0$. Sequent 11 is obtained
by substituing $v$ with $v^{\prime}+1$ from sequent 10. We observe that
$\sigma_{5}(v)$ is just $\sigma_{3}(v-1)$. The left side of 11 comes from the
fact that $\\{u\mapsto v^{\prime}+1,s\mapsto u\\}:(n>0)$ is logically
equivalent to $\\{u\mapsto v^{\prime},s\mapsto u\\}:(n\geq 0)$, which is the
left side of sequent 11. From sequent 11 to sequent 12, we simply replace the
free variable name $v^{\prime}$ with $v$, which does not change the validity
of the sequent.

The whole proof tree is a cyclic preproof because the only infinite derivation
path:
1,2,$\dot{3}$,$\dot{4}$,$\dot{9}$,$\dot{10}$,$\dot{11}$,$\dot{12}$,$\dot{3}$,
$\dot{4}$,$\dot{9}$,… has a progressive derivation trace consisting of the
target formulas underlined in Figure 1.

Readers may notice that if we choose the configuration as a free variable $X$
and try to prove $X:(n\geq
0)\Rightarrow{}X:[\textit{WP}_{1}](s=\frac{(n+1)n}{2})$, then our approach is
no different from using the ‘update’ structure in previous work like [4]. In
this way, a configuration has no explicit structure itself, but just a
variable carrying updates, for example, $X[s\mapsto 0]$, which updates the
value of $s$ to $0$ in $X$. One of the advantages of the configurations in
$\mathit{DL}_{p}$ compared to the ‘update’ approach is that it allows explicit
forms of programs’ or system models’ structures.

###  4.2 Example Two: A Synchronous Loop Program

The second example we consider is a synchronous program written in Esterel
language [7]:

$E_{2}=_{df}A\parallel B,$

where

$\begin{aligned} A=\ &\textit{trap}\ \textit{loop}\underbrace{\
\left\\{\begin{aligned} &\ \ \textit{if}\ x>0\ \textit{then}\\\ &\ \ \
x:=x-1;\ \textit{emit}\ T;\ \textit{pause}\\\ &\ \ \textit{else}\\\ &\ \ \
\textit{emit}\ S;\ \textit{exit}\\\ &\ \ \textit{end}\ \end{aligned}\right\\}\
}_{A_{l}}\ \textit{end}\ \textit{end}\end{aligned},\begin{aligned} B=\
&\textit{trap}\ \textit{loop}\underbrace{\ \left\\{\begin{aligned} &\ \
\textit{present}\ S\ \textit{then}\\\ &\ \ \ \textit{exit}\\\ &\ \
\textit{else}\\\ &\ \ \ \textit{pause}\\\ &\ \ \textit{end}\ \end{aligned}\
\right\\}\ }_{B_{l}}\textit{end}\ \textit{end}\end{aligned}$

are two programs running in parallel. Their loop bodies are represented by
$A_{l}$ and $B_{l}$ respectively. Different from while programs, the behaviour
of a synchronous program is characterized by a sequence of _instances_. At
each instance, several (atomic) executions of a program occur. A synchronous
program model guarantees that when some programs run in parallel, the program
state at the end of an instance is unique, regardless of the orders of all
executions during that instance. Therefore, at each instance, the behaviour of
a parallel synchronous program is deterministic.

In this example, program $A$ decreases a variable $x$ by $1$ every instance,
while program $B$ listens to a control signal $S$ from $A$, and only
terminates when program $A$ emits $S$. Key word pause ends the current
instance of a program. “$\textit{present}\ S...$” means “if $S$ is emitted…”.
exit terminates either program $A$ or $B$ by jumping out of a trap statement.
At each instance, when $x>0$, program $A$ executes $x:=x-1$ and
$\textit{emit}\ T$, while program $B$ simply pauses by doing nothing. When
$x\leq 0$, program $A$ emits $S$ and terminates, while program $B$ just
terminates at the same instance. And the whole program $A\parallel B$
terminates. When initializing $x$ as $5$, the state of all variables at the
end of each instance is listed as follows: $(\textit{inst}\
1:x=4,S=\bot,T=\top),(\textit{inst}\ 2:x=3,S=\bot,T=\top),(\textit{inst}\
3:x=2,S=\bot,T=\top),(\textit{inst}\ 4:x=1,S=\bot,T=\top),(\textit{inst}\
5:x=0,S=\top,T=\bot),$ where $\top$ and $\bot$ represent the presence and
absence of a signal respectively.

Different from Example 1, a configuration in Esterel is a stack structure
[35], allowing expressing local variables with same names. For example,
$\\{x\mapsto
5\operatorname{|}T\mapsto\bot\operatorname{|}S\mapsto\top\operatorname{|}T\mapsto\top\\}$
represents a configuration in which there are 4 variables: $x$, $S$ and two
$T$s with different values. We use “$\operatorname{|}$” instead of “,” to
remind that it is a stack structure, with the right-most side as the top of
the stack. In this example, for simplicity, we assume that the 3 variables
$x$, $T$ and $S$ are already declared, so an initial configuration of the
program is always of the form: $\\{x\mapsto
v\operatorname{|}T\mapsto\bot\operatorname{|}S\mapsto\bot\\}$ for an arbitrary
value $v$. ${\phi}\rhd{\sigma}$ has a similar meaning as in Example 1, the
only difference is that, a variable, say $x$, is explained by the top-most
variable $x$ in the stack of $\sigma$. For instance, ${(x>0)}\rhd{\\{x\mapsto
5\operatorname{|}x\mapsto 2\operatorname{|}y\mapsto 1\\}}$ is $2>0$, rather
than $5>0$.

The operational semantics of an Esterel program is quite complex, which can be
understood in two scopes. In micro scope, each transition represents an atomic
execution of a program in an instance. In macro scope, there can be more than
one transitions in an instance. After the last transition, all signals are
reset to “absence” and a new instance starts. During executions in an
instance, auxiliary processes (called ‘Can’ processes [35]) are needed in
order to guarantee the consistency of all variables. In this paper, for
simplicity, we do not list the inference rules for Esterel but only give the
transitions needed for the deductions as below.

Contrast with while programs, Esterel programs do not directly support
structural rules. Intuitively, for a sequence program $\alpha;\beta$ in
Esterel, program $\alpha$ cannot simply proceed independently from program
$\beta$, unless all atomic executions in $\beta$ occur at a different instance
from any execution in $\alpha$. One needs to collect all atomic executions in
$\alpha;\beta$ at current instance together, in order to check that all
variables are consistent. More analysis was given in [17].

We prove the following property

$P_{2}=_{df}\\{x\mapsto
v\operatorname{|}T\mapsto\bot\operatorname{|}S\mapsto\bot\\}:(x>0)\Rightarrow{}\\{x\mapsto
v\operatorname{|}T\mapsto\bot\operatorname{|}S\mapsto\bot\\}:\langle
E_{2}\rangle(x=0),$

which says that under any configuration (with $v$ a free variable), if $x>0$,
then there exists an execution of $E_{2}$ that terminates and satisfies $x=0$.

$1234\lx@proof@logical@and 51112678910$ 1:
$\sigma_{1}(v):(x>0)\Rightarrow\sigma_{1}(v)\\{v\\}:\langle A\parallel
B\rangle(x=0)$ 2:
$\sigma_{1}(v):(x>0)\Rightarrow\sigma_{2}(v)\\{v-1\\}:\langle A_{1}\parallel
B\rangle(x=0)$ 3:
$\sigma_{1}(v):(x>0)\Rightarrow\sigma_{3}(v)\\{v-1\\}:\langle A_{2}\parallel
B_{1}\rangle(x=0)$ 4:
$\sigma_{1}(v):(x>0)\Rightarrow\sigma_{2}(v)\\{v-1\\}:\langle A\parallel
B\rangle(x=0)$ 5:
$\sigma_{1}(v):(x>1)\Rightarrow\sigma_{2}(v)\\{v-1\\}:\langle A\parallel
B\rangle(x=0)$ 6:
$\sigma_{1}(v):(x=1)\Rightarrow\sigma_{2}(v)\\{v-1\\}:\langle A\parallel
B\rangle(x=0)$ 7:
$\sigma_{1}(v):(x=1)\Rightarrow\sigma_{4}(v)\\{v-1\\}:\langle A_{3}\parallel
B_{2}\rangle(x=0)$ 8:
$\sigma_{1}(v):(x=1)\Rightarrow\sigma_{2}(v)\\{v-1\\}:\langle\downarrow\rangle(x=0)$
9: $\sigma_{1}(v):(x=1)\Rightarrow\sigma_{2}(v)\\{v-1\\}:(x=0)$ 10:
$\sigma_{1}(v):(x=1)\Rightarrow{(x=0)}\rhd{\sigma_{2}(v)\\{v-1\\}}$ 11:
$\sigma_{1}(v^{\prime}):(x>0)\Rightarrow\sigma_{1}(v^{\prime})\\{v^{\prime}\\}:\langle
A\parallel B\rangle(x=0)$ 12:
$\sigma_{1}(v):(x>0)\Rightarrow\sigma_{1}(v)\\{v\\}:\langle A\parallel
B\rangle(x=0)$ $\beta_{1}=_{df}s:=s+n;\ n:=n-1$ $A_{1}=_{df}\textit{trap}\
\textit{loop}\ \textit{emit}\ T;\ \textit{pause};A_{l}\ \textit{end}\
\textit{end}$ $A_{2}=_{df}\textit{trap}\ \textit{loop}\ \textit{pause};A_{l}\
\textit{end}\ \textit{end}$ $B_{1}=_{df}\textit{trap}\ \textit{loop}\
\textit{pause};B_{l}\ \textit{end}\ \textit{end}$ $A_{3}=_{df}\textit{trap}\
\textit{loop}\ \textit{exit};A_{l}\ \textit{end}\ \textit{end}$
$B_{2}=_{df}\textit{trap}\ \textit{loop}\ \textit{exit};B_{l}\ \textit{end}\
\textit{end}$ $\sigma_{1}(v)\\{v\\}=_{df}\\{x\mapsto
v\operatorname{|}T\mapsto\bot\operatorname{|}S\mapsto\bot\\}$
$\sigma_{2}(v)\\{v-1\\}=_{df}\\{x\mapsto
v-1\operatorname{|}T\mapsto\bot\operatorname{|}S\mapsto\bot\\}$
$\sigma_{3}(v)\\{v-1\\}=_{df}\\{x\mapsto
v-1\operatorname{|}T\mapsto\top\operatorname{|}S\mapsto\bot\\}$
$\sigma_{4}(v)\\{v-1\\}=_{df}\\{x\mapsto
v-1\operatorname{|}T\mapsto\bot\operatorname{|}S\mapsto\top\\}$

Figure 2: Derivations of Example 2

The derivations of $P_{2}$ is shown in Figure 2. Instances of rule
$(\langle\alpha\rangle\sigma)$ rely on the transitions listed as follows:

  * •

from node 1 to 2: $(A\parallel
B,\sigma_{1}(v)\\{v\\})\longrightarrow(A_{1}\parallel
B,\sigma_{2}(v)\\{v-1\\})$

  * •

from node 2 to 3: $(A_{1}\parallel
B,\sigma_{2}(v)\\{v-1\\})\longrightarrow(A_{2}\parallel
B_{1},\sigma_{3}(v)\\{v-1\\})$

  * •

from node 6 to 7: $(A\parallel
B,\sigma_{2}(v)\\{v-1\\})\longrightarrow(A_{3}\parallel
B_{2},\sigma_{4}(v)\\{v-1\\})$

  * •

from node 7 to 8: $(A_{3}\parallel
B_{2},\sigma_{4}(v)\\{v-1\\})\longrightarrow(\downarrow,\sigma_{2}(v)\\{v-1\\})$

The termination factors in $E_{2}$ are defined as natural numbers, with the
“less-than relation” $<$ between natural numbers as the well-founded relation
($\prec$) between termination factors. $v$ and $v-1$ are the termination
factors in the configurations. From node 4, two situations 5 and 6 are
considered based on the loop condition $x>0$. Node 11 is obtained from node 5
by substituting variable $v$ with $v^{\prime}+1$. Node 12 is a bud with node 2
as its companion, which is obtained by replace the free variable name
$v^{\prime}$ with $v^{\prime}$ in node 11. The whole preproof is progressive
as the derivation step from 1 to 2 is progressive (with $v-1<v$). So all
infinite derivation traces are progressive.

##  5 Related Work

Reasoning about programs directly through their executable semantics is not a
new idea. As far as we know, the first related work was matching logic,
proposed by Rosu and Stefanescu in [36]. Matching logic is based on patterns
and pattern matching. Its basic form, a reachability rule
$\varphi\Rightarrow\varphi^{\prime}$ (note that $\Rightarrow$ means
differently there than in our sequents), captures whether pattern
$\varphi^{\prime}$ is reachable from pattern $\varphi$ in a given pattern
reachability system. One-path reachability logic [37] and all-paths
reachability logic [39] were developed based on matching logic by adding
conditional rules and a all-paths reachability rule
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ respectively. The concept of
‘patterns’ in matching/reachability logics has a wider scope of meaning than
the concepts of ‘programs’, ‘configurations’ and ‘formulas’ in
$\mathit{DL}_{p}$. The program specifications described with modal operator
$[\cdot]$ in $\mathit{DL}_{p}$ cannot be expressed in matching logic and one-
path reachability logic when the program models are non-deterministic, as
$[\cdot]$ captures “the reachability of ALL execution paths”. However, the
semantics of $[\cdot]$ can be captured by the reachability rule
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ in all-paths reachability
logic. A more powerful matching $\mu$-logic [11] was developed by adding a
least fixpoint $\mu$-binder to matching logic. We conjecture that matching
$\mu$-logic can encode $\mathit{DL}_{p}$, as it has been declared in [11] that
it can encode traditional dynamic logics. So compared to reachability logic
and matching-$\mu$ logic, our contribution is not about expressiveness, but
that we propose a different proof theory rooted in cyclic reasoning (rather
than coinduction [37]) and the theory of dynamic logic for program
verification via operational semantics.

Compared to all matching, reachability and matching-$\mu$ logics above, one
advantage of $\mathit{DL}_{p}$ is that $\mathit{DL}_{p}$ comes to program
deductions in a more natural and direct way, in the sense that the concepts of
‘programs’ and ‘configurations’ are explicitly expressed, and programs and
formulas are clearly separated by the modal operator $[\cdot]$. As we put
previously, this brings a benefit that we can observe how program behaviours
evolve independently from the formulas along the whole derivation processes.
On the other hand, to express a $\mathit{DL}_{p}$ specification like
$(\sigma:\phi)\Rightarrow{}(\sigma:\langle\alpha\rangle\psi)$ in matching
logic for example, one needs to ‘mix up’ all structures together to form a
pattern, in a form like: $\varphi=_{df}\alpha\wedge\sigma\wedge\phi$ and
$\varphi^{\prime}=_{df}\downarrow\wedge\sigma^{\prime}\wedge\psi$ for some
configuration $\sigma^{\prime}$, in order to prove the reachability rule
$\varphi\Rightarrow{}\varphi^{\prime}$.

[28] proposed a general program verification framework based on coinduction,
the theory the reachability logics [37, 39] also rely on. Using the
terminology in this paper, in [28] a program specification can be expressed as
a pair $(c,P)$ with $c$ a program state and $P$ a set of program states,
capturing the exact meaning of formula $\sigma:[\alpha]\phi$ in
$\mathit{DL}_{p}$ if we let $c$ be $(\alpha,\sigma)$ and let set $P$ be the
semantics of formula $\phi$. The authors designed a method to derive a program
specification $(c,P)$ in a coinductive way according to the operational
semantics of $c$. The soundness of the method is proved by using the greatest
fixpoint theory on mathematical sets. Following [28], [26] also proposed a
general framework for program reasoning, but via big-step semantics. Unlike
the frameworks in [28] and [26], which are directly based on set theory,
$\mathit{DL}_{p}$ has an explicit form of logic, which is more suitable in
some cases to catch specifications. The proof system of $\mathit{DL}_{p}$ is
based on the cyclic proof theory (cf. [10]) rather than coinduction, where
especially, the soundness of $\mathit{DL}_{p}$ is proved by contradiction on
the well-foundedness of partial-order relations. Besides, in
$\mathit{DL}_{p}$, one can also express and derive the negation of a dynamic
formula $\sigma:[\alpha]\phi$ as the dual formula
$\sigma:\langle\alpha\rangle\neg\phi$, whose meaning cannot be captured in the
framework of [28].

The structure ‘updates’ in traditional dynamic logics, used in Java dynamic
logic [5], differential dynamic logic [31], dynamic trace logic [4], etc.,
works as a special case of the configurations in this paper. As illustrated at
the end of Section 4.1, a configuration is more than just a calculus for
substitutions of variables and terms.

The proof system of $\mathit{DL}_{p}$ relies on the cyclic proof theory which
firstly arose in [40], and later developed in different logics such as [10],
[8], etc. Traditional dynamic logics’ proof systems are not cyclic ones. In
[23], Jungteerapanich proposed a complete cyclic proof system for
$\mu$-calculus, which subsumes propositional dynamic logic (PDL) [15] in its
expressiveness. In [13], Docherty and Rowe proposed a complete labelled cyclic
proof system for PDL. Both $\mu$-calculus and PDL are logics with regular
expressions with tests as their program models, which are not in a
parameterized form like the program models of $\mathit{DL}_{p}$. The labelled
form of $\mathit{DL}_{p}$ formula $\sigma:[\alpha]\phi$ comes from [13], where
a labelled PDL formula is of the form $s:[\alpha]\phi$, with $s$ a state in
Kripke structure. Rather than just a state, a configuration $\sigma$ in
$\mathit{DL}_{p}$ allow more forms rather than functions mapping variables to
values (see our Example 2). [13] has inspired us to use the well-founded
relation $\prec_{m}$ in the proof of the soundness of $\mathit{DL}_{p}$,
though we take a different proof approach since unlike PDL, $\mathit{DL}_{p}$
formulas do not satisfy the “finite model property” (cf. [13]).

##  6 Some Discussions & Future Work

$\mathit{DL}_{p}$ can be a very powerful logic calculus due to its general
forms. But one should not take $\mathit{DL}_{p}$ as a “unified framework” for
programming and verification, like matching-$\mu$ logic and UTP theory [22].
$\mathit{DL}_{p}$ is more of a second-ordered logic restricted to a particular
form so that it facilitates expressing and reasoning about programs and
systems. Though we only give two examples in this paper, one can easily see
that $\mathit{DL}_{p}$ can be used to reason about many other types of
programs, specially those do not support structural rules, such as neural
networks as done recently in [41], and also many abstract system models, such
as Kleene algebra with tests [25] and CCS [27].

$\mathit{DL}_{p}$ can be taken as a general theory that can subsume the
existed dynamic logic theories in which program models satisfy the program
properties declared in Definition 1. Any rule in a dynamic logic theory can be
lifted as a labelled rule in $\mathit{DL}_{p}$, which is derived without
changing the labels of a formula. For instance, in the example discussed in
Section 1, to derive formula $\psi=_{df}(\\{x\mapsto t\\}:x\geq
0\Rightarrow{}\\{x\mapsto t\\}:[x:=x+1]x>0)$, one can also apply the “lifting
version” of the assignment rule ($x:=e$) as: $\begin{aligned}
\sigma:[x:=e]\psi\sigma:\psi[x/e]\end{aligned}$, and $\psi$ then becomes
$\psi^{\prime\prime\prime}=_{df}(\\{x\mapsto t\\}:x\geq 0)\to(\\{x\mapsto
t\\}:x+1>0)$, which also can be transformed into formula $\phi^{\prime}$:
$t\geq 0\to t+1>0$ after the applications of $\\{x\mapsto t\\}$. This “lifting
ability” provides $\mathit{DL}_{p}$ with a flexible framework in which
different inference rules can be applied to make a trade-off between
structural-based reasoning and symbolic executions in practical deduction
processes. More work will be on analyzing how program verification can be
benefited from this flexibility of the theory of $\mathit{DL}_{p}$.

One future work will focus on implementing a specialized program verifier
based on the theory of $\mathit{DL}_{p}$. The tool is now under development
based on Cyclist [9], a proof engine supported by an efficient cyclic-proof-
search algorithm. To see the full potential of $\mathit{DL}_{p}$, we are also
trying to use $\mathit{DL}_{p}$ to describe and verify more types of programs
or structures.

#### Acknowledgements

This work is partially supported by the Youth Project of National Science
Foundation of China (No. 62102329), the Project of National Science Foundation
of Chongqing (No. cstc2021jcyj-bshX0120), and the Project of National Science
Foundation of China (No. 62272397).

## References

  * [1] Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press (2014)
  * [2] Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (May 2008)
  * [3] Barthe, G., Katoen, J.P., Silva, A.: Foundations of Probabilistic Programming. Cambridge University Press (2020)
  * [4] Beckert, B., Bruns, D.: Dynamic logic with trace semantics. In: Bonacina, M.P. (ed.) Automated Deduction – CADE-24. pp. 315–329. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)
  * [5] Beckert, B., Klebanov, V., Weiß, B.: Dynamic Logic for Java, pp. 49–106. Springer International Publishing, Cham (2016)
  * [6] Benevides, M.R., Schechter, L.M.: A propositional dynamic logic for concurrent programs based on the $\pi$-calculus. Electronic Notes in Theoretical Computer Science 262, 49–64 (2010), proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)
  * [7] Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming 19(2), 87 – 152 (1992)
  * [8] Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. SIGPLAN Not. 43(1), 101–112 (jan 2008). https://doi.org/10.1145/1328897.1328453, https://doi.org/10.1145/1328897.1328453
  * [9] Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) Programming Languages and Systems. pp. 350–367. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)
  * [10] Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). pp. 51–62 (2007). https://doi.org/10.1109/LICS.2007.16
  * [11] Chen, X., Rosu, G.: Matching $mu$-logic. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–13. IEEE Computer Society, Los Alamitos, CA, USA (jun 2019). https://doi.org/10.1109/LICS.2019.8785675, https://doi.ieeecomputersociety.org/10.1109/LICS.2019.8785675
  * [12] Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. In: Maurer, H.A. (ed.) Automata, Languages and Programming. pp. 188–202. Springer Berlin Heidelberg, Berlin, Heidelberg (1979)
  * [13] Docherty, S., Rowe, R.N.S.: A non-wellfounded, labelled proof system for propositional dynamic logic. In: Cerrito, S., Popescu, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. pp. 335–352. Springer International Publishing, Cham (2019)
  * [14] Feldman, Y.A., Harel, D.: A probabilistic dynamic logic. Journal of Computer and System Sciences 28(2), 193–215 (1984)
  * [15] Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)
  * [16] Gentzen, G.: Untersuchungen über das logische Schließen. Ph.D. thesis, NA Göttingen (1934)
  * [17] Gesell, M., Schneider, K.: A hoare calculus for the verification of synchronous languages. In: Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification. p. 37–48. PLPV ’12, Association for Computing Machinery, New York, NY, USA (2012)
  * [18] Goodfellow, I.J., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge, MA, USA (2016), http://www.deeplearningbook.org
  * [19] Harel, D.: First-Order Dynamic Logic, Lecture Notes in Computer Science (LNCS), vol. 68. Springer (1979)
  * [20] Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
  * [21] Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (Oct 1969)
  * [22] Hoare, C., He, J.: Unifying theories of programming, vol. 14. Prentice Hall (1998)
  * [23] Jungteerapanich, N.: A tableau system for the modal $\mu$-calculus. In: Giese, M., Waaler, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. pp. 220–234. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)
  * [24] Kozen, D.: A probabilistic pdl. Journal of Computer and System Sciences 30(2), 162–178 (1985). https://doi.org/https://doi.org/10.1016/0022-0000(85)90012-1, https://www.sciencedirect.com/science/article/pii/0022000085900121
  * [25] Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (may 1997). https://doi.org/10.1145/256167.256195, https://doi.org/10.1145/256167.256195
  * [26] Li, X., Zhang, Q., Wang, G., Shi, Z., Guan, Y.: Reasoning about iteration and recursion uniformly based on big-step semantics. In: Qin, S., Woodcock, J., Zhang, W. (eds.) Dependable Software Engineering. Theories, Tools, and Applications. pp. 61–80. Springer International Publishing, Cham (2021)
  * [27] Milner, R.: A Calculus of Communicating Systems. Springer-Verlag, Berlin, Heidelberg (1982)
  * [28] Moore, B., Peña, L., Rosu, G.: Program verification by coinduction. In: Ahmed, A. (ed.) Programming Languages and Systems. pp. 589–618. Springer International Publishing, Cham (2018)
  * [29] O’Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL) (dec 2019). https://doi.org/10.1145/3371078, https://doi.org/10.1145/3371078
  * [30] Pardo, R., Johnsen, E.B., Schaefer, I., Wąsowski, A.: A specification logic for programs in the probabilistic guarded command language. In: Theoretical Aspects of Computing – ICTAC 2022: 19th International Colloquium, Tbilisi, Georgia, September 27–29, 2022, Proceedings. p. 369–387. Springer-Verlag, Berlin, Heidelberg (2022). https://doi.org/10.1007/978-3-031-17715-6_24, https://doi.org/10.1007/978-3-031-17715-6_24
  * [31] Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: International Conference on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX). Lecture Notes in Computer Science (LNCS), vol. 4548, pp. 216–232. Springer Berlin Heidelberg (2007)
  * [32] Platzer, A.: Stochastic differential dynamic logic for stochastic hybrid programs. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction – CADE-23. pp. 446–460. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)
  * [33] Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018)
  * [34] Plotkin, G.D.: A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, University of Aarhus (1981), http://citeseer.ist.psu.edu/plotkin81structural.html
  * [35] Potop-Butucaru, D., Edwards, S.A., Berry, G.: Compiling Esterel. Springer New York, NY (2010)
  * [36] Roşu, G., Ştefănescu, A.: Towards a unified theory of operational and axiomatic semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) Automata, Languages, and Programming. pp. 351–363. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)
  * [37] Rosu, G., Stefanescu, A., Ciobâcá, S., Moore, B.M.: One-path reachability logic. In: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 358–367 (2013). https://doi.org/10.1109/LICS.2013.42
  * [38] Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46–55 (jun 2022). https://doi.org/10.1145/3503914, https://doi.org/10.1145/3503914
  * [39] Ştefănescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Şerbănută, T.F., Roşu, G.: All-path reachability logic. In: Dowek, G. (ed.) Rewriting and Typed Lambda Calculi. pp. 425–440. Springer International Publishing, Cham (2014)
  * [40] Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theor. Comput. Sci. 89(1), 161–177 (aug 1991). https://doi.org/10.1016/0304-3975(90)90110-4, https://doi.org/10.1016/0304-3975(90)90110-4
  * [41] Zhang, X., Chen, X., Sun, M.: Towards a unifying logical framework for neural networks. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) Theoretical Aspects of Computing – ICTAC 2022. pp. 442–461. Springer International Publishing, Cham (2022)
  * [42] Zhang, Y., Mallet, F., Liu, Z.: A dynamic logic for verification of synchronous models based on theorem proving. Front. Comput. Sci. 16(4) (aug 2022). https://doi.org/10.1007/s11704-022-1374-4, https://doi.org/10.1007/s11704-022-1374-4
  * [43] Zhang, Y., Wu, H., Chen, Y., Mallet, F.: A clock-based dynamic logic for the verification of ccsl specifications in synchronous systems. Science of Computer Programming 203, 102591 (2021)
  * [44] Zilberstein, N., Dreyer, D., Silva, A.: Outcome logic: A unifying foundation for correctness and incorrectness reasoning. Proc. ACM Program. Lang. 7(OOPSLA1) (apr 2023). https://doi.org/10.1145/3586045, https://doi.org/10.1145/3586045