\section{Introduction}

Their prevalence in safety-critical applications and ample technical subtleties make both cyber-physical systems (CPS) verification \cite{Alur1993, Henzinger1996, DBLP:journals/jar/Platzer08, Alur2011} and parallel program verification \cite{OwickiGries1976, LevinGries1981, deRoever2001, AptdeBoerOlderog10} important challenges.
CPS verification complexity stems from subtle interactions of their discrete control decisions and differential equations.
Parallel program verification complexity comes from intricate interactions caused by synchronization via state or communication interdependencies between parallel components.
But their combination becomes intrinsically complicated because parallel CPS are \emph{always} interdependent as they \emph{always} synchronize implicitly by sharing the same global time.
Moreover, many real-world CPS have heterogeneous subsystems
whose controllers do not operate in lock-step, and their communication is potentially unreliable (see \rref{fig:interaction}).
Unlike hybrid systems model checking \cite{Alur1993,Lynch2003,Frehse2004,Benvenuti2014}---which needs to compute products of communicating parallel automata of significant size even when reducing the size of the subautomata---deductive approaches can be truly compositional.
Existing deductive verification approaches, however, fail to properly tackle the above challenges, since they are restricted to homogeneous subsystems \cite{DBLP:conf/csl/Platzer10},
specific component shapes and interaction patterns \cite{Lunel2019,DBLP:journals/sttt/MullerMRSP18, Kamburjan2020},
do not support symbolic execution \cite{Liu2010,Wang2012,Guelev2017},
or are non-compositional \cite{Liu2010,Wang2012,Guelev2017},
where even explicit attempts on compositionality \cite{Wang2012,Guelev2017} turn out to be non-compostional~again.

\begin{wrapfigure}[19]{R}{.43\textwidth}
	\vspace{-.5\baselineskip}
	\centering
	\input{interaction.tex}
	\vspace*{-1.5em}
	\caption{
		The interaction of $\progtt{CPS}_1$ and $\progtt{CPS}_2$ has (delayed) (\usebox{\communication}),
		lossy (\usebox{\lossy}), and
		noisy (\usebox{\noisy}) communication.
		Discrete change (\usebox{\disc}) is independent of discrete change in parallel unless synchronization takes place.
		Continuous evolution (\usebox{\continuous}) is not interrupted by parallel discrete behavior.
 	}
	\label{fig:interaction}
\end{wrapfigure}

Neither compositionality to tame complexity by reasoning separately about discrete, continuous, and communication behavior,
nor generality in expressing models, nor symbolic execution to boost the feasibility of deductive reasoning are dispensable for a practical approach.
Thus, to tackle all three of these challenges, this paper presents $\dLCHP$,
a \emph{dynamic logic for communicating hybrid programs} (\emph{CHPs}),
that extends differential dynamic logic \dL for hybrid programs of differential equations
\ifblind
\cite{DBLP:journals/jar/Platzer17}
\else
\cite{DBLP:journals/jar/Platzer08,Platzer10,DBLP:journals/jar/Platzer17,Platzer18}
\fi
with CSP-style operators for parallel composition and message passing communication \cite{Hoare1978, Hoare85} as well as assumption-commitment (ac) reasoning \cite{Misra1981, AcHoare_Zwiers}.
Parallel CHPs cannot share state but can communicate.
They run synchronously in global time and their communication is instantaneous.

There are two fundamental approaches to reasoning about parallelism.
Parallelism can either be understood via unfolding its explicit operational semantics,
or via its denotational semantics implicitly characterizing parallel behavior by matching behavior of the subprograms on their respective part of the state.
Verification based on the operational semantics unrolls the exponentially many possible interleavings,
as in hybrid automata \cite{Alur1993} or hybrid CSP \cite{Wang2012,Guelev2017}.
Such approaches admit superficial mitigation of the state space explosion but always resorts to product automata after reducing the size of the subautomata \cite{Frehse2004,Henzinger2001,Benvenuti2014},
or merely postpone the burden of reasoning about exponentially many trace interleavings \cite{Wang2012,Guelev2017} since it reveals the internal structure of subprograms \cite{Wang2012}.
In contrast, verification based on the denotational semantics is compositional for discrete programs with ac-reasoning \cite{AcHoare_Zwiers, AcSemantics_Zwiers}, \emph{if} the semantics is compositional and aligns well with the intended reasoning.
This paper generalizes ac-reasoning for the purpose of integration with a compositional hybrid systems logic
\ifblind
\cite{DBLP:journals/jar/Platzer17}.
\else
\cite{DBLP:journals/jar/Platzer08,Platzer10,DBLP:journals/jar/Platzer17,Platzer18}.
\fi

Our central contribution is a sound \emph{compositional} proof calculus for \dLCHP.
For compositional verification of parallel communication,
it embeds ac-reasoning into dynamic logic via the explicit ac-modality $[ \alpha ] \ac \psi$.
The ac-modality expresses that for all runs of~$\alpha$ whose incoming communication meets assumption $\A$ the outgoing communication fulfills commitment $\C$ and that $\psi$ holds in the final state.
Formulas $\A$ and $\C$ specify the communication behavior of $\alpha$,
and enable parallel composition if they mutually agree for the contracts of subprograms.
Crucially, these formulas directly interface the communication history via history variables such that communication can remain implicit in the parallel composition axiom just as in the underlying denotational semantics.
Since we prove that \dLCHP is a conservative extension of \dL,
it inherits \dL's complete axiomatization of differential equation invariants \cite{DBLP:conf/lics/PlatzerT18}.

Unlike approaches built on Hoare-logics \cite{Liu2010, Wang2012,Guelev2017},
our calculus supports statement-by-statement symbolic execution
instead of executing them backward.
Since executing communication primitives extends the former history,
the new history state requires a fresh name.
As a consequence, it is unsound to adopt Hoare-style ac-reasoning \cite{AcHoare_Zwiers} verbatim with a distinguished variable for the communication history.
Instead, \dLCHP reconciles ac-reasoning and symbolic execution via recorder variables whose evolution is maintainable, as done by our communication axiom along the way.

In summary, we provide the first truly \emph{compositional} approach to the verification of communicating parallel hybrid system models and prove its soundness.
Our logical treatment separates the essentials of discrete, continuous, and communication reasoning into axioms that are simple and modular compared to earlier approaches \cite{Liu2010, Wang2012}.
Even though the technical development is challenging because of a prefix-closed dynamic semantics,
a subtle static semantics due to the global time and recorder variables,
and the mutual dependency of formulas and programs in dynamic logic
it remains finally under the hood.
We demonstrate the flexibility of \dLCHP and its proof calculus with an example in autonomous driving considering the challenge of lossy communication,
where a $\progtt{follower}$ and $\progtt{leader}$ car communicate to form a convoy.

\section{Dynamic Logic of Communicating Hybrid Programs}

We introduce \dLCHP,
a \emph{dynamic logic} to reason about \emph{communicating hybrid programs} (CHPs).
CHPs combine \dL's hybrid programs
\ifblind
\cite{DBLP:journals/jar/Platzer08,DBLP:journals/jar/Platzer17}
\else
\cite{DBLP:journals/jar/Platzer08,DBLP:journals/jar/Platzer17,Platzer18}
\fi
with communication primitives and a parallel operator similar to CSP \cite{Hoare1978,Hoare85}.
On the logical side,
$\dLCHP$ introduces ac-reasoning \cite{Misra1981,AcHoare_Zwiers,AcSemantics_Zwiers} into the dynamic logic setup \cite{Harel1979} of \dL,
allowing compositional reasoning about communication in a way that preserves symbolic execution as an intuitive reasoning principle.

\subsection{Syntax}

The syntax uses channel names $\Chan$ and variables $\V = \RVar \cup \NVar \cup \TVar$ with pairwise disjoint sets of real variables $\RVar$, integer variables $\NVar$, and trace variables $\TVar$.
The variable $\globalTime \in \RVar$ is designated to reflect the global time.
By convention $x, y, t \in \RVar$, $\intVar, \intVar_i \in \NVar$, $\historyVar, \historyVar_i \in \TVar$, $ch, ch_i \in \Chan$, and $\arbitraryVar, \arbitraryVar_i \in \V$.
Notions $\FV(\cdot)$ of free and $\BV(\cdot)$ of bound variables in formulas and programs are defined as usual by simultaneous induction with the syntax (see \rref{app:staticSemantics}).
$\V(\cdot)=\FV(\cdot)\cup\BV(\cdot)$ is the set of all variables,
whether read or written.

All real variables $\RVar$ can be read \emph{and} written in programs but the global time~$\globalTime$ is \emph{not meant} to be written manually.%
\footnote{Programs writing the global time $\globalTime$ manually are likely to be meaningless such as $\globalTime \ceq 0 \parOp \globalTime \ceq 1$ that sets $\globalTime$ to $0$ and $1$ in parallel, which fortunately has no runs.}
Instead, the built-in evolution of~$\globalTime$ with every continuous behavior makes it represent the global flow of time.
Trace variables are bound by programs when they record communication.
For a program $\alpha$,
we call the remaining set $(\BV(\alpha) \cap \RVar) \setminus \{ \globalTime \}$ the state of $\alpha$ and say that $\alpha$ operates over a real state.
In parallel compositions $\alpha \parOp \beta$,
the programs $\alpha$ and $\beta$ may communicate explicitly but do \emph{not} share state.

The logical language of $\dLCHP$ features trace algebra to reason about communication behavior following the approach of Zwiers~\emph{et~al}.\@\xspace \cite{AcSemantics_Zwiers, Zwiers_Phd}.
During symbolic program execution,
communication events are collected syntactically in logical trace variables that were explicitly designated to record the history.
This way, the communication behavior of a program can be specified using recorder variables as interface.
In analogy to a distinguished history variable, this interface is crucial to obtain a compositional proof rule for parallel composition \cite{AcSemantics_Zwiers, Hooman1992, deRoever2001}.

\begin{definition}[Terms] \label{def:syntax_terms}
	Real terms $\Rtrm$, integer terms $\Itrm$, channel terms $\Ctrm$, and trace terms $\Ttrm$ are defined by the grammar below,
	where $c \in \rationals$ is a rational constant, $\ch{} \in \Chan$ a channel name, $\rp_1, \rp_2 \in \polynoms{\rationals}{\RVar}$ are polynomials in $\RVar$, and $\cset \subseteq \Chan$ is a finite set of channel names.
	The set of all terms is denoted by $\Trm$.
	\begin{align*}
		\Rtrm: &&\re_1, \re_2 & \cceq x \mid \rationalConst \mid \re_1 + \re_2 \mid \re_1 \cdot \re_2 \mid \val{\at{\te}{\ie}} \mid \stamp{\at{\te}{\ie}} \\
		\Itrm: &&\ie_1, \ie_2 & \cceq \intVar \mid 0 \mid 1 \mid \ie_1 + \ie_2 \mid \len{\te}\\
		\Ctrm: &&\ce_1, \ce_2 &  \cceq \ch{} \mid \chan{\at{\te}{\ie}}\\
		\Ttrm: &&\te_1, \te_2 & \cceq \historyVar \mid \epsilon \mid \comItem{ch, \rp_1, \rp_2} \mid \te_1 \cdot \te_2 \mid \te \downarrow \cset
	\end{align*}
\end{definition}

Real terms $\Rtrm$ are formed by arithmetic operators, variables $x$ (including $\globalTime$), and rational constants $\rationalConst$.
Additionally, $\val{\at{\te}{\ie}}$ accesses the value and $\stamp{\at{\te}{\ie}}$ the timestamp of the $\ie$-th communication in trace $\te$.
In CHPs only polynomials $\rp \in \polynoms{\rationals}{\RVar} \subset \Rtrm$ in $\RVar$ over rational coefficients occur,
i.e.,\@\xspace without trace terms,
since CHPs operate over a real state.
By convention,~$\rp, \rp_i$ denote terms from $\polynoms{\rationals}{\RVar}$.

For integers, we use Presburger arithmetic (no multiplication) since it is decidable \cite{Presburger1931} and sufficient for our purposes.%
\footnote{Presburger arithmetic is the subset of $\Itrm$ without length computations $\len{\te}$.}
The integer term $\len{\te}$ denotes the length of trace $\te$.
In analogy to $\val{\at{\te}{\ie}}$, the term $\chan{\at{\te}{\ie}}$ accesses the channel name of the $\ie$-th communication in trace $\te$.
The trace term $\epsilon$ represents empty communication, $\te_1 \cdot \te_2$ is the concatenation of trace terms $\te_1$ and $\te_2$, and $\te \downarrow \cset$ the projection of $\te$ onto the set of channel names $\cset \subseteq \Chan$.
The tuple $\comItem{\ch{}, \rp_1, \rp_2}$ represents communication of $\rp_1$ along channel $\ch{}$ at time $\rp_2$,
where~$\rp_1, \rp_2 \in \polynoms{\rationals}{\RVar}$ since communication is between programs over a real state.

A trace variable $\historyVar$ refers to a sequence of communication events.
By symbolic execution,
proofs collect communication items in trace variables designated to record the history.
Then, communication behavior is specified against these recorder variables using projections onto the channels of interest (see \rref{ex:historyAssertion} below).
This allows specifications to hide the internal structure of programs leading to compositional reasoning in the presence of communication \cite{AcSemantics_Zwiers, Hooman1992, deRoever2001}.

\begin{notation}
	We write $\val{\te}$ to abbreviate $\val{\at{\te}{\len{\te} - 1}}$, i.e.,\@\xspace access to the value of the last item on trace $\te$.
	Likewise, we use $\stamp{\te}$ and $\chan{\te}$.
\end{notation}

\begin{example} \label{ex:historyAssertion}
	The formula $\len{\historyVar \downarrow \ch{}} > 0 \rightarrow \val{\historyVar \downarrow \ch{}} > 0$ expresses that the last value sent along channel $\ch{}$ recorded by $\historyVar$ is positive.
	The precondition $\len{\historyVar \downarrow \ch{}} > 0$ ensures that the value is accessed only for a non-empty history.
\end{example}

\begin{definition}[Communicating hybrid programs] \label{def:syntax_chps}
	The set $\Chp$ of \emph{communicating hybrid programs} is defined by the grammar below,
	where $x \in \RVar$ for $x, x'$,
	and $\rp \in \polynoms{\rationals}{\RVar}$ is a polynomial in $\RVar$,
	and $\chi \in \FolRA$ is a formula of first-order real-arithmetic.
	In the parallel composition $\alpha \parOp \beta$, the constituents must not share state, i.e.,\@\xspace $\V(\alpha) \cap \BV(\beta) = \V(\beta) \cap \BV(\alpha) \subseteq \{\globalTime\} \cup \TVar$.
	\begin{align*}
		\alpha, \beta \cceq \;
		& x \ceq \rp \mid x \ceq * \mid \evolution{}{} \mid \test{} \mid \alpha \seq \beta \mid \alpha \cup \beta \mid \repetition{\alpha} \mid \tag*{\nonrelevant{(standard \dL)}}\\
		& \send{}{}{} \mid \receive{}{}{} \mid \alpha \parOp \beta \tag*{\nonrelevant{(CSP extension)}}
	\end{align*}
\end{definition}

The statement $x \ceq \rp$ instantly changes $x$ to $\rp$ and nondeterministic assignment $x \ceq *$ sets $x$ to an arbitrary value.
Assignment to the global time $\globalTime$ is only meant to be used by axioms.
As in $\dL$ \cite{DBLP:journals/jar/Platzer08},
continuous evolution \mbox{$\evolution{}{}$} follows the differential equation $x' = \rp$ for a nondeterministically chosen duration but only as long as the domain constraint $\chi$ is fulfilled.%

In \dLCHP, the global time $\globalTime$ always evolves during a continuous evolution according to $\globalTime' = 1$ even if it does not occur syntactically.
Hence, an evolution $\globalTime' = \rp$
is considered ill-formed if $\rp \not\equiv 1$ just like an ODE $x' = 1, x' = 2$ is considered ill-formed.
Since programs operate over a real state,
terms $\rp \in \polynoms{\rationals}{\RVar}$ are polynomials in $\RVar$ and $\chi \in \FolRA$ is a formula of first-order real-arithmetic.

The test $\test{}$ passes if formula $\chi$ is satisfied.
Otherwise, execution is aborted.
The sequential composition $\alpha \seq \beta$ executes $\beta$ after $\alpha$.
The choice $\alpha \cup \beta$ follows~$\alpha$ or $\beta$ nondeterministically,
and $\repetition{\alpha}$ repeats $\alpha$ zero or more times.

Communication and parallelism are inspired by CSP \cite{Hoare1978}.
The primitive $\send{}{}{}$ sends the value of term $\rp$ along channel $\ch{}$ and $\receive{}{}{}$ receives a value from $\ch{}$ binding it to variable $x$.
For both statements, $\historyVar$ is the trace variable designated to record the communication.
In an ongoing symbolic execution,
this variable can be renamed to refer to the variable keeping the most recent communication history.
In system models,
all recorder variables are meant to be the same.
In this case,
we also write $\send{}{non}{}$ and $\receive{}{non}{}$ instead of $\send{}{}{}$ and $\receive{}{}{}$.

Finally, $\alpha \parOp \beta$ executes $\alpha$ and $\beta$ in parallel for equal duration,
i.e.,\@\xspace their final states agree on the value of the global time $\globalTime$.
If $\globalTime$ is not manipulated manually,
its increase equals the duration of continuous behavior.
As in CSP,~$\alpha$ and $\beta$ can perform synchronous message passing but cannot share state.%
\footnote{The global time $\globalTime$ and trace variables $\TVar$ are not considered as program state.}
All programs participating in communication over a channel must agree on all communication along that channel and share the same values and recorder variables at the same time,
i.e.,\@\xspace message passing does not consume time.
Since shared recorder variables agree on the communication for all subprograms,
they provide the interface that allows for decomposition of parallel behavior.
If the recorders are not the same as in $\send{}{\historyVar_0}{} \parOp \receive{}{\historyVar_1}{}$,
there are no runs.
The need for matching recorders in parallel composition must not be confused with renaming of the history by symbolic execution along the sequential structure of programs.

As usual in CSP \cite{Hoare1978},
the syntax does not enforce unidirectional communication such that several programs may send and receive on the same channel at the same time as long as they agree on the recorder variables and values.
For example, $\receive{}{}{x} \parOp \receive{}{}{y}$ is a well-formed program.
Its semantics has all runs where $x$ and $y$ receive the same values.
Likewise, $\send{}{}{\rp_1} \parOp \dots \parOp \send{}{}{\rp_n}$ has terminating runs if the values of all $\rp_i$ agree.
Consequently, a receive statement $\receive{}{}{}$ can be replaced with the semantical equivalent $x \ceq * \seq \send{}{}{x}$.

\begin{notation}
	As usual $\ifstat{\varphi}{\{ \alpha \}}$ is short for $(\test{\varphi} \seq \alpha) \cup \test{\neg\varphi}$.
\end{notation}

\begin{example} \label{ex:followerLeader}
	\rref{fig:followerLeader} models two cars in a convoy safely adjusting their speed.
	From time to time,
	the $\progtt{leader}$ changes its speed $v_l$ in the range $0$ to $V$ and notifies the $\progtt{follower}$ about the change.
	The communication, however, is lossy ($\ch{vel} ! v_l \cup \skipProg$).
	%
	%
	%
	Sending position updates by $\progtt{updt}$ succeeds at least every $\epsilon$ time units.
	On such an update, the $\progtt{follower}$'s controller $\progtt{dist}$ awakes.
	%
	If the distance~$d$ fell below $\epsilon \maxvelo$, the $\progtt{follower}$ slows down to avoid collision before the next position update.

	Regularly, the $\progtt{follower}$ adopts the speed update in $\progtt{velo}$, but crucially refuses to do so
	%
	if the last known distance was not safe ($d > \epsilon \maxvelo$).
	If the $\progtt{leader}$ could overwrite the $\progtt{follower}$'s speed, it could cause a future collision (see \rref{fig:convoyPlot} below) even though obeying would be perfectly fine at the moment.
	This is because a subsequent notification of the leader slowing down could be lost.
	%
	%
	%
\end{example}

\begin{figure}[h!tb]
	\vspace*{-3em}
	\begin{small}
		\begin{minipage}{.55\textwidth}
			\begin{align*}
				\progtt{velo} \equiv\;
					& \ch{vel} ? v_{tar} \seq
					\ifstat{d > \epsilon V}{v_f \ceq v_{tar}} \\
				\progtt{dist} \equiv\;
					& \ch{pos} ? m \seq
					d \ceq m - x_f \seq \\
					& \ifstat{d \le \epsilon V}{%
						\{v_f \ceq * \seq \test{\orange{0}{v_f}{\safevelo{d}}}\}
					} \\
				\Plant_f \equiv\;
					& \evolution{x_f' = v_f}{non} \\
				\progtt{follower} \equiv\;
					& \big( (\progtt{velo} \cup \progtt{dist}) \seq \Plant_f \big)^*
			\end{align*}
		\end{minipage}%
		\begin{minipage}{.45\textwidth}
			\begin{align*}
				\chi_{vel} & \equiv \range{0}{v_l}{V} \\
				\progtt{noti} & \equiv v_l \ceq * \seq \test{\chi_{vel}} \seq (\ch{vel} ! v_l \cup \skipProg) \\
				\progtt{updt} & \equiv \ch{pos} ! x_l \seq w \ceq 0 \\
				\Plant_l & \equiv \evolution{w' = 1, x_l' = v_l}{w \le \epsilon} \\
				\progtt{leader} & \equiv \big( (\progtt{noti} \cup \progtt{updt}) \seq \Plant_l \big)^*
			\end{align*}
		\end{minipage}
	\end{small}
	\caption{Models of two moving cars ($\progtt{follower}$ and $\progtt{leader}$) intended to form the convoy $\progtt{follower} \parOp \progtt{leader}$ by parallel composition, communicating target speed.}
	\label{fig:followerLeader}
	\vspace*{-1.5em}
\end{figure}

\begin{wrapfigure}[24]{R}{.45\textwidth}
	\vspace*{-.5\baselineskip}
	\centering
	\input{convoy.tex}
	\vspace*{-1.5em}
	\caption{
		Plot of example positions $x_f$ and $x_l$ of the cars over time.
		%
		First, speed update is accepted (\textcolor{OliveGreen}{$\checkmark$}).
		The next update is lost (\usebox{\lossy}).
		%
		After position update (\textcolor{MidnightBlue}{$\distpicto$}),
		the $\progtt{follower}$ adjusts its speed.
		%
		Crucially, it conservatively rejects the speed update (\textcolor{BrickRed}{$\notcheckmark$})
		%
		when a crash ($\lightning$) with a slowing $\progtt{leader}$ is possible since speed communication may fail (\usebox{\lossy}) until the next reliable position update is expected, see dashed trajectory (\usebox{\crash}).
		}
	\label{fig:convoyPlot}
\end{wrapfigure}

\begin{definition}[Formulas] \label{def:syntax_formulas}
	The set of \emph{$\dLCHP$ formulas} $\Fml$ is defined by the following grammar,
	where $\arbitraryVar \in \V$, terms $\expr_1, \expr_2 \in \Trm$ are of equal sort, $\re_i \in \Rtrm$, $\ie_i \in \Itrm$, $\te_i \in \Ttrm$, and the ac-formulas $\A$ and $\C$ do not refer to state and time of~$\alpha$,
	i.e.,\@\xspace $(\FV(\A) \cup \FV(\C)) \cap \BV(\alpha) \subseteq \TVar$.
	\begin{align*}
		\varphi, \psi, \A, \C \cceq \;
			& \expr_1 = \expr_2 \mid \re_1 \ge \re_2 \mid \ie_1 \ge \ie_2 \mid \te_1 \preceq \te_2 \mid \neg \varphi \mid \varphi \wedge \psi \mid \varphi \vee \psi \mid \\
			& \varphi \rightarrow \psi \mid \fa{\arbitraryVar} \varphi \mid \ex{\arbitraryVar} \varphi \mid [ \alpha ] \psi \mid [\alpha] \ac \psi
	\end{align*}
\end{definition}

For specifying the (communication) behavior of CHPs, we combine first-order dynamic logic \cite{Harel1979} with ac-reasoning \cite{AcHoare_Zwiers}.
Equality is defined on each sort of terms.
On real and integer terms, $\ge$ has the usual meaning.
On trace terms, $\te_1 \preceq \te_2$ means that $\te_1$ is a prefix of $\te_2$.
There is no order on channel terms.
Quantified variables $\arbitraryVar \in \V$ are of arbitrary sort.
Since our primary interest is safety, we omit the dynamic modality $\langle \alpha \rangle \psi$ and give no dual $\langle \alpha \rangle \ac \psi$ for $[ \alpha ] \ac \psi$.

Besides the dynamic modality $[ \alpha ] \psi$, $\dLCHP$ prominently features the ac-box $[ \alpha ] \ac \psi$
that reshapes Hoare-style ac-reasoning \cite{AcHoare_Zwiers} into the modal approach of dynamic logic.
In an ac-contract $\varphi \rightarrow [ \alpha ] \ac \psi$,
assumption $\A$ and commitment~$\C$ specify $\alpha$'s communication behavior along the interface of recorder variables but without access to $\alpha$'s state and time as required by $(\FV(\A) \cup \FV(\C)) \cap \BV(\alpha) \subseteq \TVar$,
whereas formulas $\varphi$ and $\psi$
act as pre- and postcondition as usual.
Formula $[ \alpha ] \ac \psi$  promises that $\C$ holds after each communication event of $\alpha$ assuming $\A$ held before each event.
Moreover, if the program terminated \emph{and} $\A$ held before and after each communication event, %
the final state satisfies $\psi$.

\begin{example} \label{ex:convoy_safety}
	The safety condition about $\progtt{follower}$ and $\progtt{leader}$ below expresses:
	If they start driving with a distance of at least $d$ and a speed ${\le}\nicefrac{d}{\epsilon}$ that prevents the $\progtt{follower}$ from reaching the $\progtt{leader}$ within $\epsilon$ time units,
	then the cars do never collide.
	\rref{sec:example} shows a proof of this formula.
	\begin{equation*}
		\epsilon \ge 0 \wedge
			\range{0}{v_f}{\safevelo{d}} \wedge
			v_f \le V \wedge
			x_f + d < x_l
		\rightarrow [ \progtt{follower} \parOp \progtt{leader} ]
		\, x_f < x_l
	\end{equation*}
\end{example}

Closed systems,
where communication has an internal partner,
can be specified using boxes $[ \cdot ] \psi$ (see \rref{ex:convoy_safety}) since their safety does not depend on the environment.
Ac-boxes $[ \cdot ] \ac \psi$ come into play when such systems are decomposed since the constituents $\progtt{follower}$ and $\progtt{leader}$ are each other's environment.

\subsection{Semantics} \label{sec:semantics}

CHPs have a denotational linear history semantics merging ideas from \dL \cite{DBLP:journals/jar/Platzer08} and ac-reasoning \cite{AcSemantics_Zwiers} and adding synchronization in the global time.
The basic domains are traces $\traces$ and states $\states$.
A \emph{trace} $\trace \in \traces$ is a finite sequence $(\trace_1, ..., \trace_n)$ of communication events $\trace_i = \comItem{\ch{}_i, a_i, \duration_i}$ with channel $\ch{}_i \in \Chan$, value $a_i \in \reals$, and timestamp $\duration_i \in \reals$ that is \emph{chronological}, i.e.,\@\xspace $\duration_i \le \duration_j$ for all $1 \le i < j \le n$.
The empty trace is denoted $\epsilon$, the concatenation of traces $\trace_1$ and $\trace_2$ is $\trace_1 \cdot \trace_2$, and for $\cset \subseteq \Chan$, the projection $\trace \downarrow \cset$ is the subsequence of $\trace$ consisting exactly of those $\comItem{\ch{}, a, \duration}$ and $\comItem{\historyVar, \ch{}, a, \duration}$ with $\ch{} \in \cset$.%
\footnote{We use the same operators for corresponding syntax and semantics, i.e.,\@\xspace $\te \downarrow \cset$ and $\trace \downarrow \cset$ are the projection on $\cset$ for trace term $\te$ and semantic trace $\trace$, respectively.}
By $\trace[pre] \preceq \trace$ and $\trace[pre] \prec \trace$,
we express that $\trace[pre]$ is a prefix or proper prefix of $\trace$, respectively.
A \emph{recorded trace} $\trace \in \recTraces$ is a trace that has an additional recorder variable $\historyVar_i \in \TVar$ for each communication event such that $\trace_i = \comItem{\historyVar_i, \ch{}_i, a_i, \duration_i}$.
Raw traces $\traces$ represent trace terms in a state, whereas
recorded traces originate from programs.

A \emph{state} is a map $\pstate{v} : \V \rightarrow \reals \cup \naturals \cup \traces$ that assigns a value from $\type(\arbitraryVar)$ to each variable $\arbitraryVar \in \V$,
where $\type(\expr) = \mathbb{M}$ if $\expr \in \SortedTrm{\mathbb{M}}$ for $\mathbb{M} \in \{\reals, \naturals, \traces\}$.
The \emph{updated state} $\pstate{v} \subs{\arbitraryVar}{d}$ is defined by $\pstate{v} \subs{\arbitraryVar}{d} = \pstate{v}$ on $\{ \arbitraryVar \}^\complement$ and $\pstate{v} \subs{\arbitraryVar}{d}(\arbitraryVar) = d$.
\emph{State-trace concatenation} $\pstate{v} \cdot \trace$ appends recorded communication $\trace \in \recTraces$ to the corresponding trace variable in $\pstate{v} \in \states$.
It is defined by $\pstate{v} \cdot \trace = \pstate{v}$ on $\TVar^\complement$ and $(\pstate{v} \cdot \trace)(\historyVar) = \pstate{v}(\historyVar) \cdot \trace(\historyVar)$ for all $\historyVar \in \TVar$,
where $\trace(\historyVar)$ denotes the subtrace of $\trace$ consisting of the raw versions $\comItem{\ch{}, a, \duration}$ of communication events $\comItem{\historyVar, \ch{}, a, \duration}$ in $\trace$ recorded by $\historyVar$.

\subsubsection{Term Semantics}

The value $\sem{\expr} \pstate{v} \in \type(\expr)$ of term $\expr$ at state $\pstate{v} \in \states$ is according to its sort $\type(\expr)$ (see \rref{app:semantics}).
The evaluation of real and integer terms is as usual.
Additionally, $\val{\at{\te}{\ie}}$ evaluates to the value, $\stamp{\at{\te}{\ie}}$ to the timestamp, and $\chan{\at{\te}{\ie}}$ to the channel name of the $\ie$-th communication event in $\te$ with indices from $0$ to $\len{\te} - 1$.
Moreover, $\len{\te}$ evaluates to the length of $\te$.
The evaluation of trace terms is aligned with the semantic operators on traces \cite{AcSemantics_Zwiers, Zwiers_Phd}, e.g.,\@\xspace $\sem{\te \downarrow \cset} \pstate{v} = (\sem{\te} \pstate{v}) \downarrow \cset$ and $\sem{\comItem{\ch{}, \rp_1, \rp_2}} \pstate{v} = \comItem{\ch{}, \sem{\rp_1} \pstate{v}, \sem{\rp_2} \pstate{v}}$.

\subsubsection{Domain of Computation}

The denotational semantics $\sem{\alpha} \subseteq \pDomain$ of a CHP~$\alpha$ has domain $\pDomain = \states \times \recTraces \times \botop{\states}$ with $\botop{\states} = \states \cup \{\bot\}$,
i.e.,\@\xspace the observables of a CHP started from a state are communication and a final state.
The marker $\bot$ indicates an unfinished execution that either can be continued or was aborted due to a failing test.
Since communication can even be observed from unfinished computations,
a meaningful semantics of communicating programs is prefix-closed and total (see \rref{def:prefixClosedAndTotal} below).
Totality captures that every program can at least start computation even if it aborts immediately like $\test{\false}$ and has not emitted communication initially.
For \rref{def:prefixClosedAndTotal}, we extend the prefix relation $\preceq$ on traces $\recTraces$ to a partial order $\preceq$ on observable behavior $\recTraces \times \botop{\states}$ expressing that $\observable[pre]$ is a prefix of $\observable$ if
$\big( (w = \pstate[pre]{w} \text{ and } \trace = \trace[pre])$ or $(\pstate[pre]{w} = \bot \text{ and } \trace[pre] \preceq \trace) \big)$.

\begin{definition}[Prefix-closedness and totality] \label{def:prefixClosedAndTotal}
	A set $U \subseteq \pDomain$ is \emph{prefix-closed} if $\computation \in U$ and $\observable[pre] \preceq \observable$ implies $\computation[pre] \in U$.
	The set is \emph{total} if $\pLeast \subseteq U$ with $\pLeast = \states \times \{\epsilon\} \times \{\bot\}$,
	i.e.,\@\xspace $\leastComputation \in U$ for every $\pstate{v} \in \states$.
\end{definition}

\subsubsection{Program Semantics}

The semantics of compound programs is compositionally defined in terms of semantical operators:
For $U, M \subseteq \pDomain$,
we define $\botop{U} = \{ (\pstate{v}, \trace, \bot) \mid \computation \in U \}$
and $\computation \in U \continuation M$ if $(\pstate{v}, \trace_1, \pstate{u}) \in U$ and $\pstate{u} \neq \bot$ and $(\pstate{u}, \trace_2, \pstate{w}) \in M$ exists such that $\trace = \trace_1 \cdot \trace_2$.
The operator $\closedComposition$ is for sequential composition.
For $U, M \subseteq \pDomain$, we define $U \closedComposition M = \botop{U} \cup (U \continuation M)$.
Semantic iteration $U^m$ is defined by $U^0 = \pIdentity = \pLeast \cup (\states \times \{ \epsilon \} \times \states)$ and $U^{n+1} = U \closedComposition U^n$ for $n > 0$.
Accordingly, $\alpha^0 \equiv{} \test{\true}$ and $\alpha^{n+1} \equiv \alpha \seq \alpha^n$ defines syntactic iteration.

Parallel composition $\alpha \parOp \beta$ requires that $\alpha$ and $\beta$ have disjoint bound variables (\rref{def:syntax_chps}) except for $\{\globalTime\} \cup \TVar$,
where they will always agree.
Thus, the merged state $\pstate{w}_\alpha \merge \pstate{w}_\beta \in \botop{\states}$ for states $\pstate{w}_\alpha, \pstate{w}_\beta \in \botop{\states}$ can be unambiguously determined as follows:
$\pstate{w}_\alpha \merge \pstate{w}_\beta = \bot$ if at least one of the states is $\bot$.
Otherwise, define $(\pstate{w}_\alpha \merge \pstate{w}_\beta)(\arbitraryVar) = \pstate{w}_\alpha(\arbitraryVar)$ if $\arbitraryVar \in \BV(\alpha)$ and $(\pstate{w}_\alpha \merge \pstate{w}_\beta)(\arbitraryVar) = \pstate{w}_\beta(\arbitraryVar)$ if $\arbitraryVar \not\in \BV(\alpha)$.%
\footnote{The alternative condition $\arbitraryVar \in \BV(\beta)$ leads to an equivalent definition when $\pstate{w}_\alpha = \pstate{w}_\beta$ on $(\BV(\alpha) \cup \BV(\beta))^\complement$, which is the case for the final states in parallel composition.}
For program $\alpha$,
the set $\CN(\alpha) \subseteq \Chan$ consists of all channel names occurring in $\alpha$,
i.e.,\@\xspace in send $\send{}{}{}$ and receive $\receive{}{}{}$ statements.
The projection $\trace \downarrow \CN(\alpha)$ is abbreviated as $\trace \downarrow \alpha$.
The \emph{semantic parallel operator} is defined as follows for programs $\alpha, \beta \in \Chp$:
\begin{equation*}
	\sem{\alpha} \parOp \sem{\beta}
	= \Bigg\{ (\pstate{v}, \trace, \pstate{w}_\alpha \merge \pstate{w}_\beta) \in \pDomain
	\;\bigg\vert\;
	\begin{aligned}
		&\computation[proj=\alpha] \in \sem{\alpha},
		\computation[proj=\beta] \in \sem{\beta}, \\
		&\statetime{\pstate{w}_\alpha} = \statetime{\pstate{w}_\beta},
		\trace = \trace \downarrow (\alpha \parOp \beta)
	\end{aligned}
	\Bigg\}
\end{equation*}

Instead of computing explicit interleavings,
the parallel operator $\parOp$ characterizes the joint communication $\trace$ implicitly via any order that
the subprograms can agree on.
Thereby $\trace \in \recTraces$ rules out non-chronological ordering of communication events that are exclusive to either $\trace \downarrow \alpha$ or $\trace \downarrow \beta$.
Moreover, by $\trace = \trace \downarrow (\alpha \parOp \beta)$,
the trace $\trace$ must not contain any junk,
i.e.,\@\xspace communication not caused by $\alpha$ or~$\beta$.
Communication along joint channels of $\alpha$ and $\beta$ must agree in its recorder variable, value, and timestamp as it occurs in $\trace \downarrow \alpha$ and $\trace \downarrow \beta$.
By $\statetime{\pstate{w}_\alpha} = \statetime{\pstate{w}_\beta}$ both computations need to meet at the same point in global time.%
\footnote{We consider $\statetime{\pstate{w}_\alpha} = \statetime{\pstate{w}_\beta}$ fulfilled if $\pstate{w}_\alpha = \bot$ or $\pstate{w}_\beta = \bot$.}

\begingroup
\allowdisplaybreaks
\begin{definition}[Program semantics]\label{def:programsemantics}
	The semantics $\sem{\alpha} \subseteq \pDomain$ of a program $\alpha \in \Chp$ is inductively defined as follows,
	where $\pLeast = \states \times \{\epsilon\} \times \{\bot\}$
	and~$\vDash$ is the satisfaction relation for formulas (\rref{def:formulaSemantics}):
	\begingroup
	\begin{align*}%
		%
		%
		%
		&\sem{x \ceq \rp}
		= \pLeast \cup \{ (\pstate{v}, \epsilon, \pstate{w}) \mid \pstate{w} = \pstate{v} \subs{x}{\sem{\rp} \pstate{v}} \} \\
		&\sem{x \ceq *}
		= \pLeast \cup \{ (\pstate{v}, \epsilon, \pstate{w}) \mid \pstate{w} = \pstate{v} \subs{x}{a} \text{ where } a \in \reals \} \\
		&\sem{\test{}}
		= \pLeast \cup \{ (\pstate{v}, \epsilon, \pstate{v}) \mid \pstate{v} \vDash \chi \} \\
		&\sem{\evolution{}{}}
		= \pLeast \cup \big\{ (\odeSolution(0), \epsilon, \odeSolution(\duration)) \mid
		%
			 \odeSolution(\zeta) \vDash \globalTime' = 1 \wedge x' = \rp \wedge \chi
			 \text{ and } \\
		%
			&\qquad
			\odeSolution(\zeta) = \odeSolution(0) \text{ on } \{ x, \globalTime\}^\complement
			\text{ for all } \zeta \in [0, \duration]
			\text{ and a solution }\\
		%
			&\qquad
			\odeSolution : [0, \duration] \rightarrow \states \text{ with } \odeSolution(\zeta)(\arbitraryVar') = \solutionDerivative{\odeSolution}{\arbitraryVar}(\zeta) \text{ for } \arbitraryVar \in \{x,\globalTime\} \big\} \\
		%
		%
		%
		&\sem{\send{}{}{}}
		= \{ \computation \mid \observable \preceq ( \comItem{\historyVar, \ch{}, \sem{\rp} \pstate{v}, \statetime{\pstate{v}}}, \pstate{v} ) \} \\
		&\sem{\receive{}{}{}}
		= \{ \computation \mid \observable \preceq ( \comItem{\historyVar, \ch{}, a, \statetime{\pstate{v}}}, \pstate{v} \subs{x}{a} ) \text{ where } a \in \reals \} \\
		%
		%
		%
		&\sem{\alpha \cup \beta}
		= \sem{\alpha} \cup \sem{\beta}\\
		%
		&\sem{\alpha \seq \beta}
		= \sem{\alpha} \closedComposition \sem{\beta} = \botop{\sem{\alpha}} \cup (\sem{\alpha} \continuation \sem{\beta})\\
		%
		&\sem{\repetition{\alpha}}
		= \bigcup_{n \in \naturals} \sem{\alpha}^n
		= \bigcup_{n \in \naturals} \sem{\alpha^n} \\
		%
		&\sem{\alpha \parOp \beta}
		= \sem{\alpha} \parOp \sem{\beta}
	\end{align*}
	\endgroup
\end{definition}
\endgroup

In the semantics of continuous evolution,
the solution for the ODE gives meaning to the primed variable $x'$ as in \dL \cite{DBLP:journals/jar/Platzer17}.
By $\globalTime' = 1$,
the global time $\globalTime$ always evolves with slope $1$ with every continuous evolution.

The semantics $\sem{\alpha} \subseteq \pDomain$ is prefix-closed and total (\rref{def:prefixClosedAndTotal}) for every program $\alpha$ (see \rref{app:semantics}).
For atomic non-communicating programs,
$\pLeast = \states \times \{\epsilon\} \times \{\bot\}$ ensures prefix-closedness.
If $\test{}$ or $\evolution{}{}$ abort, $\pLeast$ also guarantees totality.
Keeping the unfinished computations $\botop{\sem{\alpha}}$ preserves prefix-closedness of $\alpha \seq \beta$.

\subsubsection{Formula Semantics}

The semantics of the first-order fragment is as usual.
Like in dynamic logic \cite{Harel1979},
the box $[ \alpha ] \psi$ means that $\psi$ is true after all finished computations,
i.e.,\@\xspace the final state and communication of $\computation \in \sem{\alpha}$ with $\pstate{w} \neq \bot$.
The ac-box $[ \alpha ] \ac \psi$ additionally means that
the communication of (un)finished computations fulfills commitment $\C$.
In our modal treatment of ac-reasoning \cite{AcHoare_Zwiers},
assumption $\A$ and program $\alpha$ determine the reachable worlds together,
i.e.,\@\xspace only computations need to be considered whose incoming communication meets $\A$.

\begin{definition}[Formula semantics]\label{def:formulaSemantics}
	The semantics $\sem{\varphi} \subseteq \states$ of a formula $\varphi \in \Fml$ is defined as \(\sem{\varphi} = \{\pstate{v} \mid \pstate{v} \vDash \varphi\}\) using the \emph{satisfaction relation}~$\vDash$.
	The relation $\vDash$ is defined by induction on the structure of $\varphi$ as follows:
	\begin{enumerate}
		\item $\pstate{v} \vDash \expr_1 {=} \expr_2$ if $\sem{\expr_1} \pstate{v} = \sem{\expr_2} \pstate{v}$. Accordingly, for $\re_1 {\ge} \re_2$, $\ie_1 {\ge} \ie_2$, $\te_1 {\preceq} \te_2$
		\item $\pstate{v} \vDash \varphi \wedge \psi$ if $\pstate{v} \vDash \varphi$ and $\pstate{v} \vDash \psi$. Accordingly, for $\neg, \vee, \rightarrow$
		\item $\pstate{v} \vDash \fa{\arbitraryVar} \varphi$ if $\pstate{v} \subs{\arbitraryVar}{d} \vDash \varphi$ for all $d \in \type(\arbitraryVar)$
		\item $\pstate{v} \vDash \ex{\arbitraryVar} \varphi$ if $\pstate{v} \subs{\arbitraryVar}{d} \vDash \varphi$ for some $d \in \type(\arbitraryVar)$
		%
		\item \label{itm:dynBoxSem}
		%
		$\pstate{v} \vDash [ \alpha ] \psi$ if $\pstate{w} \cdot \trace\vDash \psi$ for all $\computation \in \sem{\alpha}$ with $\pstate{w} \neq \bot$
		%
		\item \label{itm:acBoxSem}
		%
		$\pstate{v} \vDash [ \alpha ] \ac \psi$ if for all $\computation \in \sem{\alpha}$ the following conditions hold:
		\begin{align}
			\vspace{-.7em}
			&\proppre{\pstate{v}}{\trace} \vDash \A \text{ implies } \pstate{v} \cdot \trace \vDash \C \tag{commit} \label{eq:commit}\\
			&\big( \preeq{\pstate{v}}{\trace} \vDash \A \text{ and } \pstate{w} \neq \bot \big) \text{ implies } \pstate{w} \cdot \trace \vDash \psi \tag{post} \label{eq:post}
		\end{align}%
		%
		Where $U \vDash \varphi$ for a set of states $U \subseteq \states$ and any formula $\varphi \in \Fml$ if $\pstate{v} \vDash \varphi$ for all $\pstate{v} \in U$.
		In particular, $\emptyset \vDash \varphi$.
	\end{enumerate}
\end{definition}

In \rref{itm:acBoxSem}, \acCommit is checked after each communication event as desired since \emph{all} communication prefixes are reachable worlds by prefix-closedness of the program semantics $\sem{\alpha}$ (\rref{def:prefixClosedAndTotal}).
Via state-trace concatenation $\pstate{v} \cdot \trace$ and $\pstate{w} \cdot \trace$ in \rref{itm:dynBoxSem} and \rref{itm:acBoxSem},
the communication events recorded in $\trace$ become observable.
This follows the realization that the reachable worlds of a CHP consist of the final state and the communication trace.

\begin{remark} \label{rem:unsoundCommit}
	In \acCommit, assumptions are only available about the communication \emph{strictly} before to prevent unsound circular reasoning \cite{AcHoare_Zwiers, Hooman1992}.
	With a non-strict definition, the formula $y = 0 \rightarrow [ \send{}{}{y} ] \ac \true$,
	where $\A \equiv \C \equiv \len{\historyVar \downarrow \ch{}} > 0 \rightarrow \val{\historyVar \downarrow \ch{}} = 1$, would get valid.
	Locally, we are aware of the contradiction between the precondition $y = 0$ and what is assumed by $\A$, whereas
	the environment is not and would trust in the promise $\C$.
	%
	%
	%
	%
\end{remark}

\newcommand{\FmlSet{\dL}{}}{\FmlSet{\dL}{}}

\begin{proposition}[Conservative extension] \label{prop:conservative}
	The logic $\dLCHP$ is a conservative extension of $\dL$. That is, a formula $\varphi \in \Fml \cap \FmlSet{\dL}{}$ is valid in $\dLCHP$ iff it is valid in $\dL$, where $\FmlSet{\dL}{}$ is the set of $\dL$ formulas (see \rref{app:semantics}).
\end{proposition}

\subsection{Calculus}

This section develops a sound (see \rref{thm:soundness}) proof calculus for \dLCHP, summarized in \rref{fig:calculus} on page~\pageref{fig:calculus}.
In \rref{fig:derived} on page \pageref{fig:derived}, we provide common derived rules.
Since $\dLCHP$ is a conservative extension of $\dL$ (\rref{prop:conservative}), the entire $\dL$ sequent calculus
\ifblind
\cite{DBLP:journals/jar/Platzer17,DBLP:journals/jacm/PlatzerT20}
\else
\cite{DBLP:journals/jar/Platzer17,Platzer18,DBLP:journals/jacm/PlatzerT20}
\fi
can be used soundly for reasoning about $\dLCHP$ formulas.
A \emph{sequent} $\Gamma \vdash \Delta$ with finite lists of formulas $\Gamma$, $\Delta$ is short for $\bigwedge_{\varphi \in \Gamma} \varphi \rightarrow \bigvee_{\psi \in \Delta} \psi$.

Each program statement is axiomatized by a dynamic box $[\cdot] \psi$ or an ac-box $[\cdot] \ac \psi$.
Axioms \RuleName{acNoCom} and \RuleName{boxesDual} for switching between dynamic and ac-boxes mediate between them.
The dynamic axioms are as usual in differential \cite{DBLP:journals/jar/Platzer17} dynamic logic \cite{Harel1979}.
The ac-axioms re-express Hoare-style ac-reasoning \cite{AcHoare_Zwiers} as a dynamic logic.
However, we design more atomic axioms for parallel composition and communication from which the proof rule \RuleName{acParCompRight} for parallel composition and proof rules for communication derive.

Noninterference (\rref{def:noninterference}) identifies valid instances of the formula $[ \alpha ] \ac \psi \rightarrow [ \alpha \parOp \beta ] \ac \psi$,
which we introduce as axiom \RuleName{acDropComp} in \rref{fig:calculus}.
For formula~$\chi$, the accessed channels $\CN(\chi) \subseteq \Chan$ are those channels whose communication may influence the truth value of $\chi$, e.g.,\@\xspace $\ch{}$ in $\len{\historyVar \downarrow \ch{}} > 0$.
That is, $\CN(\chi)$ plays a similar role for the communication traces $\restrict{\pstate{v}}{\TVar}$ (the state restricted to $\TVar$) with $\pstate{v} \in \states$ as $\FV(\chi)$ does for the overall state $\pstate{v}$.
For program $\alpha$, the set $\CN(\alpha)$ denotes the communication channels used.

\begin{definition}[Noninterference] \label{def:noninterference}
	Given an ac-box $[ \alpha \parOp \beta ] \ac \psi$ the CHP $\beta$ \emph{does not interfere} with its surrounding contract if the following conditions hold:%
	\footnote{The definition only restricts $\beta$'s influence on formulas $\A$, $\C$, $\psi$ but not on program~$\alpha$ because in parallel composition $\alpha \parOp \beta$, the subprograms must not share state anyway.}
	\begin{align}
		&\FV(\psi) \cap \BV(\beta) \subseteq \{ \globalTime \} \cup \TVar \label{eq:noninterference_0}\\
		&\FV(\chi) \cap \BV(\beta) \subseteq \TVar \sidecondition{for $\chi \in \{\A, \C\}$} \label{eq:noninterference_1}\\
		&\CN(\chi) \cap \CN(\beta) \subseteq \CN(\alpha) \sidecondition{for $\chi \in \{ \A, \C, \psi \}$} \label{eq:noninterference_2}
	\end{align}%
\end{definition}

Clearly, state variables bound by $\beta$ and free in $\chi \in \{ \A, \C, \psi \}$ would influence~$\chi$'s truth in $[ \alpha \parOp \beta ] \ac \psi$.
But \rref{eq:noninterference_0} and \rref{eq:noninterference_1} do not capture trace variables $\TVar$ since they are also $\alpha$'s interface with communication that might be joint with~$\beta$.
However, \rref{eq:noninterference_2} restricts access to trace variables in~$\chi$ to those
channels whose communication can be observed either exclusively from $\alpha$ or as joint communication between $\alpha$ and $\beta$,
thus prevents influence of~$\beta$ on~$\chi$ beyond what is already caused by $\alpha$.
Still \rref{def:noninterference} allows full access to~$\alpha$'s communication including the joint communication with $\beta$.

\subsubsection{Dynamic ac-reasoning}

In Hoare-style ac-reasoning~\cite{AcHoare_Zwiers},
a distinguished history variable records communication globally.
Assuming that $\historyVar$ is such a variable in $\dLCHP$,
a tempting but \emph{wrong} axiomatization of the send statement would be
\begin{equation*} \tag{$\lightning$} \label{eq:wrongComAxiom}
	[ \send{}{non}{} ] \psi(\historyVar) \leftrightarrow \fa{\historyVar_0} \big( \historyVar_0 = \historyVar \cdot \comItem{\ch{}, \rp, \globalTime} \rightarrow \psi(\historyVar_0) \big) \text{.}
\end{equation*}
Applying it to
\begin{equation}
	\label{eq:toexecute}
	\vdash [ \send{\ch{}_1}{non}{\rp_1} ][ \send{\ch{}_2}{non}{\rp_2} ] \psi(\historyVar)
\end{equation}
results in $\historyVar_0 = \historyVar \cdot \comItem{\ch{}_1, \rp_1, \globalTime} \vdash [ \send{\ch{}_2}{non}{\rp_2} ] \psi(\historyVar_0)$.
After this step,
the ongoing history is $\historyVar_0$.
However, another application leads to
$\historyVar_0 = \historyVar \cdot \comItem{\ch{}_1, \rp_1, \globalTime}, \historyVar_1 = \historyVar \cdot \comItem{\ch{}_2, \rp_2, \globalTime} \vdash \psi(\historyVar_0)$.
Incorrectly, communication is appended to $\historyVar$ again and $\psi(\historyVar_0)$ still refers to $\historyVar_0$.
Problematically, the substitution $( [ \send{\ch{}_2}{non}{\rp_2} ] \psi(\historyVar) ) \synsubs{\historyVar}{\historyVar_0}$ during the first application does not guide $\ch{}_2 ! \rp_2$ to append its communication to $\historyVar_0$.
Without $\historyVar$ occurring syntactically but being free in $\send{\ch{}_2}{non}{\rp_2}$ the substitution does not even have a meaningful definition.
For a similar reason, axiom
\begin{equation*}
	[ \send{}{non}{} ] \psi(\historyVar) \leftrightarrow \psi(\historyVar \cdot \comItem{\ch{}, \rp, \globalTime}) \tag{$\lightning$}
\end{equation*}
is unsound as applying it twice to \rref{eq:toexecute} leads to $\vdash \psi(\historyVar \cdot \comItem{\ch{}_2, \rp_2, \globalTime} \cdot \comItem{\ch{}_1, \rp_1, \globalTime})$ with the communication items in wrong order.
Here the axiom is not able to append the second item at the right position because there is no symbolic name for the state $\historyVar \cdot \comItem{\ch{}_1, \rp_1, \globalTime}$ of history after the first application.

To enable symbolic execution,
we drop the assumption of a distinguished history variable and annotate each communication statement $\send{}{}{}$ and $\receive{}{}{}$ with an explicit recorder variable $\historyVar$.
Now, substitution $\alpha \synsubs{\historyVar}{\historyVar_0}$ is defined easily as $\send{}{\historyVar_0}{}$ for $\alpha \equiv \send{}{}{}$, and as $\receive{}{\historyVar_0}{}$ for $\alpha \equiv \receive{}{}{}$, and as $\alpha$ for other atomic programs, and by recursive application otherwise.

\begin{figure}[h!tb]
	%
	\begin{small}
		\begin{minipage}{\textwidth}
			\begin{calculus}
				\startAxiom{assign}
					$[ x \ceq \rp] \psi(x) \leftrightarrow \psi(\rp)$
				\stopAxiom
				\startAxiom{nondetAssign}
					$[ x \ceq *] \psi \leftrightarrow \fa{x} \psi$
				\stopAxiom
				\startAxiom{test}
					$[ \test{} ] \psi \leftrightarrow (\chi \rightarrow \psi)$
				\stopAxiom
				\startAxiom{boxesDual}
					$[ \alpha ] \psi \leftrightarrow [ \alpha ] \acpair{\true, \true} \psi$
				\stopAxiom
			\end{calculus}%
			\hspace*{1em}%
			\begin{calculus}
				\startAxiom{acComposition}
					$[\alpha \seq \beta] \ac \psi \leftrightarrow [\alpha] \ac [\beta] \ac \psi$
				\stopAxiom
				\startAxiom{acChoice}
					$[\alpha \cup \beta] \ac \psi \leftrightarrow [\alpha] \ac \psi \wedge [\beta] \ac \psi$
				\stopAxiom
				\startAxiom{acIteration}
					$[ \repetition{\alpha }] \ac \psi \leftrightarrow [\alpha^0] \ac \psi \wedge [\alpha] \ac [ \repetition{\alpha} ] \ac \psi$%
					%
					\footnote{\label{ft:ind-base}Note that $[\alpha^0] \ac \psi \leftrightarrow \C \wedge (\A \rightarrow \psi)$ by \RuleName{acNoCom} and \RuleName{test} since $\alpha^0 \equiv \test{\true}$.}
				\stopAxiom
				\startAxiom{acInduction}
					$[ \repetition{\alpha} ] \ac \psi \leftrightarrow [\alpha^0] \ac \psi \wedge [ \repetition{\alpha} ] \acpair{\A, \true} (\psi \rightarrow [\alpha] \ac \psi)$%
					%
					\footnoteref{ft:ind-base}%
				\stopAxiom
			\end{calculus}

			\begin{calculus}
				\startAxiom{gtime}
					$[\evolution{x' = \rp}{\chi}] \psi \leftrightarrow [\evolution{\globalTime' = 1, x' = \rp}{\chi}] \psi$%
				\stopAxiom
				\startAxiom{solution}
					$[x' = \rp(x)] \psi(x) \leftrightarrow \fa{t {\ge} 0} [ x \ceq y(t) ] \psi(x)%
					%
					\sidecondition{$y'(t) = \rp(y)$ and $\globalTime \in x$}$%
					%
					\footnote{Conservative extension only applies if $\globalTime' = 1$ is part of $x' = \rp$, which holds if $\globalTime \in x$ since every right-hand side for $\globalTime$ other than $1$ in an evolution is considered ill-formed.}
				\stopAxiom
				\startAxiom{send}
					$[ \send{}{}{} ] \psi(\historyVar)
					\leftrightarrow \fa{\historyVar_0}
						\big(
							\historyVar_0 = \historyVar \cdot \comItem{\ch{}, \rp, \globalTime} \rightarrow \psi(\historyVar_0)
						\big)$
					\sidecondition{$\historyVar_0$ fresh}
				\stopAxiom
				\startAxiom{acCom}
					$[ \send{}{}{} ] \ac \psi \leftrightarrow \C \wedge \Big( \A \rightarrow [ \send{}{}{} ] \big( \C \wedge (\A \rightarrow \psi ) \big)\Big)$
				\stopAxiom
				\startAxiom{comDual}
					$[ \receive{}{}{} ] \ac \psi \leftrightarrow [ x \ceq * ] [ \send{}{}{x} ] \ac \psi$
				\stopAxiom
				\startAxiom{K}
					$(\universal \K) \wedge [ \alpha ] \acpair{\A_1 \wedge \A_2, \C_1 \wedge \C_2} \psi \rightarrow [ \alpha ] \acpair{\A, \C_1 \wedge \C_2} \psi$%
					%
					\footnote{$\K$ is the compositionality condition $\Kexpanded$.
					The universal closure $\universal \varphi$ of $\varphi$ is defined by $\fa{\arbitraryVar_1, ..., \arbitraryVar_n} \varphi$, where $\FV(\varphi) = \{ \arbitraryVar_1, ..., \arbitraryVar_n \}$.}%
					%
					\footnoteref{ft:well-formed}%
				\stopAxiom
				\startAxiom{acDropComp}
					$[ \alpha ] \ac \psi \rightarrow [ \alpha \parOp \beta ] \ac \psi$%
					%
					\sidecondition{$\beta$ does not interfere with $[ \alpha ] \ac \psi$ (\rref{def:noninterference})}
				\stopAxiom
			\end{calculus}

			\begin{calculus}
				\startAxiom{acNoCom}
					$[ \alpha ] \ac \psi \leftrightarrow \C \wedge (\A \rightarrow [ \alpha ] \psi)$%
					%
					\sidecondition{$\CN(\alpha) = \emptyset$}%
					%
					\footnote{\label{ft:well-formed}Care must be taken, for example, when \RuleName{acNoCom} is applied from right to left, that resulting ac-boxes are well-formed, i.e.,\@\xspace $(\FV(\A) \cup \FV(\C)) \cap \BV(\alpha) \subseteq \TVar$ for $[ \alpha ] \ac \psi$.}
				\stopAxiom
				\startAxiom{acWeak}
					$[ \alpha ] \ac \psi \leftrightarrow \C \wedge [ \alpha ] \ac ( \C \wedge ( \A \rightarrow \psi ) )$
				\stopAxiom

				%
				%
				%
				\startAxiom{acBoxesDist}
					$[\alpha] \acpair{\A, \C_1 \wedge \C_2} (\psi_1 \!\wedge\! \psi_2) \leftrightarrow \bigwedge_{j=1}^2 [\alpha] \acpair{\A, \C_j} \psi_j$
				\stopAxiom
			\end{calculus}
			\begin{calculus}
				\startRule{acMono}
					\Axiom{$\A_2 \rightarrow \A_1$}
					\Axiom{$\C_1 \rightarrow \C_2$}
					\Axiom{$\psi_1 \rightarrow \psi_2$}
					\TrinaryInf{$[ \alpha ] \acj{1} \psi_1 \rightarrow [ \alpha ] \acj{2} \psi_2$}
				\stopRule
				\startRule{acG}
					\Axiom{$\C \wedge \psi$}
					\UnaryInf{$[ \alpha ] \ac \psi$}
				\stopRule
			\end{calculus}
		\end{minipage}
	\end{small}
	\vspace{-.2em}
	\caption{\dLCHP proof calculus}
	\label{fig:calculus}
	\vspace{-1em}
\end{figure}

\begin{figure}[h!tb]
	\vspace{.5em}
	\begin{small}
		\begin{minipage}{\textwidth}
			\begin{calculus}
				\startRule{CG}
					\Axiom{$\Gamma, \historyVar_0 = \historyVar \cdot \comItem{\ch{}, \rp, \globalTime} \vdash [ \alpha(\historyVar_0) ] \psi, \Delta$}

					\RightLabel{\sidecondition{$\historyVar \not \in \FV(\psi)$ and $\historyVar_0$ fresh}}
					\UnaryInf{$\Gamma, \vdash [ \alpha(\historyVar) ] \psi, \Delta$}
				\stopRule
			\end{calculus}

			\begin{calculus}
				\startRule{acLoop}
					\Axiom{$\Gamma \vdash \C \wedge \inv, \Delta$}
					\Axiom{$\C, \inv \vdash [ \alpha ] \ac \inv$}
					\Axiom{$\A, \C, \inv \vdash \psi$}
					\TrinaryInf{$\Gamma \vdash [ \repetition{\alpha} ] \ac \psi, \Delta$}
				\stopRule
			\end{calculus}
			\begin{calculus}
				\startRule{if}
					\Axiom{$\Gamma, \varphi \vdash [ \alpha ] \psi, \Delta$}

					\Axiom{$\Gamma, \neg \varphi \vdash \psi, \Delta$}

					\BinaryInf{$\Gamma \vdash [ \ifstat{\varphi}{\{\alpha\}} ] \psi, \Delta$}
				\stopRule
			\end{calculus}

			\begin{calculus}
				\startRule{acParCompRight}
					\Axiom{$\vdash \K$}

					\Axiom{$\Gamma \vdash [ \alpha_j ] \acj{j} \psi_j, \Delta$ \sidecondition{$j = 1, 2$}}

					\RightLabel{%
						\parbox{.45\textwidth}{\;\;\textnormal{\textcolor{gray}{(%
							$\alpha_{3-j}$ does not interfere with \\
							\hspace*{2em}$[ \alpha_j ] \acj{j} \psi_j$ for $j = 1, 2$ (\rref{def:noninterference})%
						)}%
						\footnote{$\K$ is the compositionality condition $\Kexpanded$.}%
						}}%
					}
					\BinaryInf{$\Gamma \vdash [ \alpha_1 \parOp \alpha_2  ] \acpair{\A, \C_1 \wedge \C_2} (\C_1 \wedge \C_2), \Delta$}
				\stopRule

				\startRule{acSendRight}
					\Axiom{$\Gamma \vdash \C(\historyVar), \Delta$}

					\Axiom{$\Gamma, H_0 \vdash \C(\historyVar_0), \Delta$}

					\Axiom{$\Gamma, H_0, \A(\historyVar_0) \vdash \psi(\historyVar_0), \Delta$}

					\RightLabel{%
						\sidecondition{$\historyVar_0$ fresh}%
						%
						\footnote{Formula $H_0$ is short for $\historyVar_0 = \historyVar \cdot \comItem{\ch{}, \rp, \globalTime}$ recording the global time $\globalTime$ as timestamp.}%
					}
					\TrinaryInf{$\Gamma \vdash [ \send{}{}{} ] \acpair{\A(\historyVar), \C(\historyVar)} \psi(\historyVar), \Delta$}
				\stopRule
			\end{calculus}
		\end{minipage}
	\end{small}
	\caption{
		Derived \dLCHP proof rules
	}
	\label{fig:derived}
	\vspace{-1em}
\end{figure}

\subsubsection{Atomic Hybrid Programs}

For an (atomic) non-communicating program $\alpha$,
we can flatten $[ \alpha ] \ac \psi$ by axiom \RuleName{acNoCom}to a dynamic formula because $\A$ and $\C$ only refer to the initial state when $\CN(\alpha) = \emptyset$.
Subsequently, we can execute the program by its dynamic axiom (\RuleName{assign}, \RuleName{nondetAssign}, \RuleName{test}, \RuleName{solution}).
Note that by conservative extension (\rref{prop:conservative}) axiom \RuleName{solution} only applies to $[ \evolution{}{} ] \psi$ if the ODE $x' = \rp$ matches the underlying semantics,
i.e.,\@\xspace if $\globalTime \in x$,
which has right-hand side $1$ for well-formed continuous evolution $x' = \rp$.
Therefore, axiom \RuleName{gtime} allows to materialize the flow of global time $\globalTime$ as evolution $\globalTime' = 1$ whenever necessary.

\subsubsection{Compound Hybrid Programs}

Compound CHPs in an ac-box cannot be handled by axiom \RuleName{acNoCom} if they communicate.
Instead, they have the axioms \RuleName{acComposition}, \RuleName{acChoice}, \RuleName{acIteration}, and \RuleName{acInduction}.
Compound programs in a dynamic box can be repackaged into an ac-box using axiom \RuleName{boxesDual}.
The ac-induction axiom \RuleName{acInduction} carefully generalizes that of dynamic logic \cite{Harel1979}.
Importantly, the reachable worlds,
where the induction step needs to hold,
only depend on program $\alpha$ and assumption $\A$ about incoming communication,
whereas commitment $\C$ is proven inductively.
In \rref{fig:derived}, we give the useful derived loop invariant proof rule \RuleName{acLoop}.
As usual, it derives from axiom \RuleName{acInduction} and the ac-version \RuleName{acG} of the Gödel-generalization rule,
which confirms that the embedding into dynamic logic is correct.

If we were to neglect the communication of aborting runs in the semantics of $\alpha \seq \beta$, axiom \RuleName{acComposition} would not be sound.
Proving $[ \alpha ] \ac [ \beta ] \ac \psi$ requires to show the commitment $\C$ after each communication of $\alpha$ even if $\beta$ aborts.
To obtain this from $[ \alpha \seq \beta ] \ac \psi$ the semantics $\sem{\alpha \seq \beta} = \botop{\sem{\alpha}} \cup (\sem{\alpha} \continuation \sem{\beta})$ contains all respective runs of $\alpha$ up to $\beta$ with $\botop{\sem{\alpha}}$.

\subsubsection{Communication Statements}

Axiom \RuleName{acCom} unfolds \acCommit for an ac-box of a single send statement into a dynamic box.
The effect on the recorder variable~$\historyVar$ of executing sending $\send{}{}{}$ is captured by axiom \RuleName{send}.
It records the event $\comItem{\ch{}, \rp, \globalTime}$ using the current global time $\globalTime$ as timestamp and renames the history in the postcondition for subsequent proof steps.
Axiom \RuleName{comDual} allows to execute a receive statement by its duality with send.
Derived rule \RuleName{acSendRight} combines \RuleName{acNoCom} and \RuleName{send}, and decomposes the statement into two premises for \acCommit and one for \acPost.
Derived rule \RuleName{CG} is useful as it eliminates the need for case distinction about empty history by prefixing the history with additional ghost communication.

\subsubsection{Parallel Composition}

A non-interfering program $\beta$ (\rref{def:noninterference}) can be dropped from parallel composition $[ \alpha \parOp \beta ] \ac \psi$ by axiom \RuleName{acDropComp} because it has no influence on the surrounding contract $[ \alpha \parOp \!\raisebox{.1em}{\underline{\hspace{.5em}}}\, ] \ac \psi$.
Since $\parOp$ is associative and commutative (see \rref{app:calculus}),
axiom \RuleName{acDropComp} can drop any subprogram in a chain of parallel statements.
In parallel composition of $[ \alpha_j ] \acj{j} \psi_j$ for $j = 1, 2$,
the commitments mutually contribute to the assumptions.
This can weaken the assumption of $\alpha_1 \parOp \alpha_2$ about its environment to $\A$ by axiom \RuleName{K} if the compositionality condition $\K \equiv \Kexpanded$ is valid.

The derived rule \RuleName{acParCompRight} combines axioms \RuleName{acDropComp} and \RuleName{K} for full decomposition of parallelism.
Reasoning about a parallel $[ \alpha_1 \parOp \alpha_2 ] \ac \psi$
with arbitrary $\A$, $\C$, and $\psi$ is the task of constructing $\A_j$, $\C_j$, and $\psi_j$ for $j = 1, 2$ such that $\C_1 \wedge \C_2 \rightarrow \C$, and $\psi_1 \wedge \psi_2 \rightarrow \psi$ are valid, and such that \RuleName{acParCompRight} is applicable.
Since the side condition of \RuleName{acParCompRight} about noninterference still allows~$\C_j$ and~$\psi_j$ for $j = 1, 2$ to access $\alpha_j$'s communication including the joint communication with~$\alpha_{3-j}$, the formulas can cover the complete communication of $\alpha_1 \parOp \alpha_2$.

\subsubsection{Miscellaneous}
Ac-boxes distribute over conjunctions
by axiom \RuleName{acBoxesDist} except for assumptions
just like preconditions $\varphi_j$ do not distribute in $\varphi_1 \wedge \varphi_2 \rightarrow [ \alpha ] \psi$.
Rule \RuleName{acMono} generalizes monotonicity from dynamic to ac-boxes.
Ac-weakening \RuleName{acWeak} exploits totality of the program semantics $\sem{\alpha}$ to add or drop $\C$ in the initial state.
Moreover, adding or dropping $\C$ and $\A \rightarrow \psi$ by \RuleName{acWeak} in the final state is due to \acCommit and \acPost, respectively.
Rule \RuleName{acG} is the ac-version of the G\"odel-generalization rule.

First-order formulas $\FolPA$ over $\Itrm$ without length computations $\len{\te}$, can be handled by an effective oracle proof rule (called \RuleName{PA}) since Presburger arithmetic is decidable \cite{Presburger1931}.
Likewise, first-order real arithmetic $\FolRA$ is decidable \cite{Tarski1951}, and we use an oracle rule for it (called \RuleName{real}) as in \dL \cite{DBLP:journals/jar/Platzer08}.
However, the full first-order fragment $\Fol$ of $\dLCHP$ is not decidable because of alternating quantifiers of trace and integer variables \cite{Bradley2006}.

Instead, reasoning about trace terms is by simple algebraic laws for successive simplification (see \rref{app:calculus}) \cite{Zwiers_Phd}.
For applicability of rules \RuleName{real} and \RuleName{PA} trace subterms can be rewritten with fresh variables.
For example, $\val{\te_1[\ie]} < \val{\te_2[\ie]} \rightarrow \val{\te_1[\ie]} + \rp < \val{\te_2[\ie]} + \rp$ is valid since $x < y \rightarrow x + \rp < y + \rp$ is valid in $\FolRA$.
Ultimately, we use \RuleName{PA} and \RuleName{real} modulo trace terms, i.e.,\@\xspace perform rewritings silently.
\\

Our central contribution is the soundness theorem about the compositional \dLCHP proof calculus.
The proof rules given in \rref{fig:derived} derive (see \rref{app:calculus}).

\begin{theorem} \label{thm:soundness}
	The $\dLCHP$ calculus (see \rref{fig:calculus}) is sound (see \rref{app:calculus}).
\end{theorem}

\section{Demonstration of \dLCHP} \label{sec:example}

We demonstrate our calculus outlining a proof of the safety condition from \rref{ex:convoy_safety} on page \pageref{ex:convoy_safety} about the convoy in \rref{fig:followerLeader} on page \pageref{fig:followerLeader}.
After decomposing the parallel statement, the proof proceeds purely mechanical by statement-by-statement symbolic execution.
It starts in \rref{fig:pardecomp} using a standard pattern for decomposing a parallel statement:
First, introduce commitments and postconditions (see \rref{fig:postconditions}) by axiom \RuleName{boxesDual} and rule \RuleName{acMono}, which relate the subprograms, such that second, rule \RuleName{acParCompRight} becomes applicable.
The latter also makes the commitments mutual assumptions.

The formulas in \rref{fig:postconditions} relating the subprograms clearly reduce their complex interior and only depend on the small communication interface and local variables,
thus are independent of any knowledge about the internal structure of the respective other car.
Adding initial ghost communication (rule \RuleName{CG}) exploits the flexibility of explicit history variables and dynamic logic to avoid cumbersome case distinction about empty history.

\begin{figure}[ht]
	\vspace*{-1em}
	\begin{align}
		\!\!\varphi \equiv\;
			& \epsilon \ge 0 \wedge
			\range{0}{v_f}{\safevelo{d}} \wedge
			v_f \le V \wedge
			x_f + d < x_l \tag{precond.\ convoy} \\
		\!\!\psi_f \equiv\;
			& 0 \le \safevelo{d} \wedge
			x_f + (\epsilon - \timespan{\globalTime}{\historyVar \downarrow \ch{pos}}) \safevelo{d} < \val{\historyVar \downarrow \ch{pos}}\! \tag{postcond.\ $\progtt{follower}$} \\
		\!\!\psi_l \equiv\;
			& \val{\historyVar \downarrow \ch{pos}} \le x_l \wedge
			\timespan{\globalTime}{\historyVar \downarrow \ch{pos}} \le \epsilon \tag{postcond.\ $\progtt{leader}$} \\
		\!\!\A \equiv \C \equiv\;
			& \range{0}{\val{\historyVar \downarrow \ch{vel}}}{V} \tag{ac-formulas}
	\end{align}
	\vspace{-1.5em}
	\caption{
		For $\ch{} \in \{ \ch{vel}, \ch{pos} \}$,
		the term $\timespan{\globalTime}{\historyVar \downarrow \ch{}}$ is short for $\globalTime - \stamp{\historyVar \downarrow \ch{}}$,
		i.e.,\@\xspace the time elapsed since last communication along $\ch{}$ recorded by $\historyVar$.
		The commitment $\C$ given by the $\progtt{leader}$,
		assumption $\A$ made by the $\progtt{follower}$,
		and the postconditions $\psi_f$ and $\psi_l$ are used in the proof in \rref{fig:pardecomp}.
	}
	\label{fig:postconditions}
\end{figure}

\begin{figure}[ht]
	\begin{prooftree}
		\Axiom{$\triangleleft_1\, \text{\RuleName{trueR}}\hspace{-1em}$}

		\Axiom{$\triangleleft_2\, \text{\RuleName{real}}\hspace{-1em}$}

		\Axiom{$*$}

		\UnaryInf{$\vdash \C \rightarrow \A$}

		\Axiom{$\triangleright$ \rref{fig:follower_in_dist_safe}}

		\UnaryInf{$\Gamma \vdash [ \progtt{follower}(\historyVar) ] \acpair{\A, \true} \psi_f$}

		\Axiom{$\triangleright$ \rref{fig:leader_vel_send}}

		\UnaryInf{$\Gamma \vdash [ \progtt{leader}(\historyVar) ] \acpair{\true, \C} \psi_l$}

		\RuleNameRight{acParCompRight}
		\TrinaryInf{$\Gamma \vdash [ \progtt{follower}(\historyVar) \parOp \progtt{leader}(\historyVar) ] \acpair{\true, \C} (\psi_f \wedge \psi_l)$}

		\RuleNameRight{acMono}
		\BinaryInf{$\Gamma \vdash [ \progtt{follower}(\historyVar) \parOp \progtt{leader}(\historyVar) ] \acpair{\true, \C} x_f < x_l$}

		\RuleNameRight{acMono}
		\BinaryInf{$\Gamma \vdash [ \progtt{follower}(\historyVar) \parOp \progtt{leader}(\historyVar) ] \acpair{\true, \true} x_f < x_l$}

		\RuleNameRight{boxesDual}
		\UnaryInf{$\Gamma \vdash [ \progtt{follower}(\historyVar) \parOp \progtt{leader}(\historyVar) ] x_f < x_l$}

		\RightLabel{$2 \times$\RuleName{CG}}
		\UnaryInf{$\varphi \vdash [ \progtt{follower}(\historyVar_0) \parOp \progtt{leader}(\historyVar_0) ] x_f < x_l$}

		\RuleNameRight{implR}
		\UnaryInf{$\vdash \varphi \rightarrow [ \progtt{follower}(\historyVar_0) \parOp \progtt{leader}(\historyVar_0) ] x_f < x_l$}
	\end{prooftree}
	\vspace{-1em}
	\caption{
		Safety proof for the convoy from \rref{ex:followerLeader},
		where $\Gamma$ is the formula list $\varphi, \historyVar_1 = \historyVar_0 \cdot \comItem{\ch{vel}, 0, \globalTime}, \historyVar = \historyVar_1 \cdot \comItem{\ch{pos}, x_l, \globalTime}$.
		The open premises $\C \vdash \true$ ($\triangleleft_1$) and $\psi_f \wedge \psi_l \vdash x_f < x_l$ ($\triangleleft_2$) close by rules \RuleName{trueR} and \RuleName{real}, respectively.
	}
	\label{fig:pardecomp}
\end{figure}

\rref{fig:pardecomp} decomposes $x_f < x_l$ into $\psi_f$ and $\psi_l$
since $\progtt{follower}$ stays behind $\progtt{leader}$'s last known position $\val{\historyVar_\ch{pos}}$,
whereas $\progtt{leader}$ never drives backward by $\psi_l$.
Indeed, $\progtt{follower}$ stores the last known distance $\val{\historyVar_\ch{pos}} - x_f$ in $d$
and $\epsilon - \timespan{\globalTime}{\historyVar_\ch{pos}}$ bounds the waiting time till the next position update along channel $\ch{pos}$.
Thus, $\progtt{follower}$ stays behind $\progtt{leader}$ when driving with speed~$\nicefrac{d}{\epsilon}$.

\rref{fig:follower_in_dist_safe} continues from \rref{fig:pardecomp}
and demonstrates the reasoning along one execution path of $\progtt{follower}$.
The invariant $\invariant{f}$ for induction \RuleName{acLoop} bounds $\progtt{follower}$'s speed by $\safevelo{d}$ such that it stays behind $\progtt{leader}$ before the next position update.
\RuleName{TA} indicates trace algebra reasoning.
The remaining proof is mechanical symbolic execution.
In particular, combining \RuleName{acNoCom} and \RuleName{acWeak} swallows the ac-formulas $\{\A, \true\}$ and using duality axiom \RuleName{comDual} allows to execute the communication by rule \RuleName{acSendRight}.
Axiom \RuleName{gtime} materializes the flow of the global time $\globalTime$ making the solution axiom \RuleName{solution} applicable.
Weakening \RuleName{WL} drops irrelevant premises,
\RuleName{forallR} introduces fresh for quantified variables,
and \RuleName{subsL} and \RuleName{subsR} perform substitution on the left and right, respectively.
Trace algebra \RuleName{TA} evaluates the assumption~$\A$.
Finally, the proof concludes by real arithmetic \RuleName{real} modulo trace terms.

\newcommand{\UnaryText}[1]{\UnaryInf{%
	\hspace*{-2em}\vbox{\vspace*{.2em}%
	#1%
	\vspace*{.3em}%
}}}

\begin{figure}[ht!]
	\begin{small}
		\begin{prooftree}[shape=justified, JustifiedScoresWidth=.9\textwidth]
			\Axiom{$*$}

			\RuleNameRight{real}
			\UnaryInf{$\begin{aligned}
				& \invariant{f}, \A, \range{0}{v_{tar}}{V}, d > \epsilon \maxvelo, t \ge 0 \vdash \range{0}{v_{tar}}{\safevelo{d}} \\
				&\qquad \wedge v_f \le V \wedge x_f + (\epsilon - \timespan{\globalTime + t}{\historyVar \downarrow \ch{pos}}) \safevelo{d} < \val{\historyVar \downarrow \ch{pos}}
			\end{aligned}$}

			\RuleNameRight{TA}
			\UnaryInf{$\begin{aligned}
				& \invariant{f}, \A, \A(\historyVar \cdot \comItem{\ch{}, v_{tar}, \globalTime}), d > \epsilon \maxvelo, t \ge 0 \vdash \invariant{f} \parameters{v_{tar}, x_f + t \cdot v_{tar}, \globalTime + t, \historyVar_\ch{vel}}
			\end{aligned}$}

			\RuleNameRight{subsL}
			\UnaryInf{$\begin{aligned}
				\invariant{f}, \A, H_\ch{vel}, \A \parameters{\historyVar_\ch{vel}}, d > \epsilon \maxvelo, t \ge 0 \vdash \invariant{f}\parameters{v_{tar}, x_f + t \cdot v_{tar}, \highlight{\globalTime + t, \historyVar_\ch{vel}}}
			\end{aligned}$}

			\RuleNameRight{forallR}
			\UnaryInf{$\begin{aligned}
				\nonrelevant{\invariant{f}, \A, H_\ch{vel}, \A \parameters{\historyVar_\ch{vel}}, d > \epsilon \maxvelo} \vdash \fa{t{\ge}0} \invariant{f} \parameters{v_{tar}, \highlight{x_f + t \cdot v_{tar}}, \highlight{\globalTime + t, \historyVar_\ch{vel}}}
			\end{aligned}$}

			\RuleNameRight{solution, assign}
			\UnaryInf{$\nonrelevant{\invariant{f}, \A, H_\ch{vel}, \A \parameters{\historyVar_\ch{vel}}, d > \epsilon \maxvelo} \vdash [ \evolution*{\globalTime' = 1, x_f' = v_{tar}}{non} ] \invariant{f} \parameters{v_{tar}, x_f, \globalTime, \historyVar_\ch{vel}}$}

			\RuleNameRight{gtime}
			\UnaryInf{$\nonrelevant{\invariant{f}, \A, H_\ch{vel}, \A \parameters{\historyVar_\ch{vel}}, d > \epsilon \maxvelo} \vdash [ \Plant_f \parameters{\highlight{v_{tar}}} ] \invariant{f} \parameters{\highlight{v_{tar}}, x_f, \globalTime, \historyVar_\ch{vel}}$}

			\SideAx$\triangleright \text{\rref{fig:follower_in_dist_unsafe}}$
			\RuleNameRight{assign}
			\UnaryInf{$\invariant{f}, \A, H_\ch{vel}, \A \parameters{\historyVar_\ch{vel}}, d > \epsilon \maxvelo \vdash [ v_f \ceq v_{tar}
			] [ \Plant_f \parameters{v_f} ] \invariant{f} \parameters{v_f, x_f, \globalTime, \historyVar_\ch{vel}}$}

			\SideAx$\triangleright\RuleName{trueR}$
			\RuleNameRight{if}
			\UnaryInf{$\invariant{f}, \A, H_\ch{vel}, \A \parameters{\historyVar_\ch{vel}} \vdash [ \ifstat{\text{safe}_d}{v_f \ceq v_{tar}}
			] [ \Plant_f ] \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar_\ch{vel}}}$}

			\SideAx$\triangleright\RuleName{trueR}$
			%
			%
			%

			\RuleNameRight{acSendRight}
			\UnaryInf{$\invariant{f} \vdash [ \send{\ch{vel}}{\historyVar}{v_{tar}} ] \acpair{\A(\historyVar), \true} [ \ifstat{\text{safe}_d}{v_f \ceq v_{tar}}
			] [ \Plant_f ] \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar}}$}

			\RuleNameRight{forallR}
			\UnaryInf{$\invariant{f} \vdash \fa{v_{tar}} [ \send{\ch{vel}}{\historyVar}{v_{tar}} ] \acpair{\A(\historyVar), \true} [ \ifstat{\text{safe}_d}{v_f \ceq v_{tar}}
			] [ \Plant_f ] \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar}}$}

			\RuleNameRight{nondetAssign}
			\UnaryInf{$\invariant{f} \vdash [ v_{tar} \ceq * ] [ \send{\ch{vel}}{\historyVar}{v_{tar}} ] \acpair{\A(\historyVar), \true} [ \ifstat{\text{safe}_d}{v_f \ceq v_{tar}}
			] [ \Plant_f ] \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar}}$}

			\RuleNameRight{comDual}
			\UnaryInf{$\invariant{f} \vdash [ \receive{\ch{vel}}{\historyVar}{v_{tar}} ] \acpair{\A(\historyVar), \true} [ \ifstat{\text{safe}_d}{v_f \ceq v_{tar}}
			] [ \Plant_f ] \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar}}$}

			\RuleNameRight{acNoCom, acWeak}
			\UnaryInf{$\invariant{f} \vdash [ \receive{\ch{vel}}{\historyVar}{v_{tar}} ] \acpair{\A(\historyVar), \true} [ \ifstat{\text{safe}_d}{v_f \ceq v_{tar}}
			] \acpair{\A(\historyVar), \true} [ \Plant_f ] \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar}}$}

			\SideAx$\triangleright \text{\rref{fig:follower_mes_dist_safe}}$
			\RuleNameRight{acComposition}
			\UnaryInf{$\invariant{f} \vdash [ \progtt{velo}(\historyVar) ] \acpair{\A(\historyVar), \true} [ \Plant_f ] \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar}}$}

			%
			%
	%
			%
			%
			%
			%

			\UnaryText{Execution by \RuleName{acComposition}, \RuleName{acChoice}, \RuleName{acNoCom}, \RuleName{acWeak}, and \RuleName{andR}}

			\SideAx$\triangleright_1 \text{\RuleName{TA, real}} \;\;\triangleright_2 \text{\RuleName{real}}$
			\UnaryInf{$\invariant{f} \vdash [ (\progtt{velo}(\historyVar) \cup \progtt{dist}(\historyVar)) \seq \Plant_f ] \acpair{\A(\historyVar), \true} \invariant{f} \nonrelevant{\parameters{v_f, x_f, \globalTime, \historyVar}}$}

			\RuleNameRight{acLoop}
			\UnaryInf{$\Gamma \vdash [ \progtt{follower}(\historyVar) ] \acpair{\A(\historyVar), \true} \psi_f$}
		\end{prooftree}
	\end{small}
	\vspace*{-1em}
	\caption{
		Partial proof for $\progtt{follower}$.
		The induction \RuleName{acLoop} uses $\invariant{f} \equiv \range{0}{v_f}{\safevelo{d}} \wedge
		v_f \le V \wedge x_f + (\epsilon - \timespan{\globalTime}{\historyVar \downarrow \ch{pos}}) \safevelo{d} < \val{\historyVar \downarrow \ch{pos}}$ as invariant.
		Formula $H_\ch{vel}$ is short for $\historyVar_\ch{vel} = \historyVar \cdot \comItem{\ch{vel}, v_{tar}, \globalTime}$ and $\text{safe}_d$ is short for $d > \epsilon \maxvelo$.
		The induction base $\Gamma \vdash \invariant{f}$ ($\triangleright_1$) closes by trace algebra \RuleName{TA} and real arithmetic \RuleName{real}.
		Postcondition $\invariant{f} \vdash \psi_f$ ($\triangleright_2$) holds by \RuleName{real}.
		For clarity, we \highlight{highlight} substitutions.
	}
	\label{fig:follower_in_dist_safe}
	\vspace*{-1em}
\end{figure}

\section{Related Work}

Unlike CHPs, Hybrid CSP (HCSP) \cite{Jifeng1994} extends CSP \cite{Hoare1978} with \emph{eager} continuous evolution
terminating on violation of the evolution constraint.
This reduced nondeterminism leaves negligible room for parallel programs to agree on a duration,
which easily results in empty behavior and vacuous proofs,
Non-eager evolution in CHPs subsumes eager runs.
Instead of exploiting their compositional models as in \dLCHP,
other hybrid process algebras are verified non-compositionally by translation to model checking \cite{Man2005, Cong2013, Song2005}.
Unlike CHPs, which demonstrated to model and reason about loss of communication out of the box,
meta-level components \cite{Lunel2019,DBLP:journals/sttt/MullerMRSP18,Kamburjan2020,Benvenuti2014,Frehse2008,Henzinger2001,Lynch2003} would need to be rethought to integrate lossy communication as for every other new application as well.

Hybrid Hoare-logic (HHL) for HCSP \cite{Liu2010} is non-compositional \cite{Wang2012}.
Wang~\emph{et~al}.\@\xspace \cite{Wang2012} extend it with assume-guarantee reasoning (AGR)
in a way that, unlike \dLCHP, becomes non-compositional again.
Unfortunately, their rule for parallel composition still explicitly unrolls all interleavings in the postcondition for communication traces reflecting the structure of the subprograms.
Assumptions and guarantees in HHL cannot specify the communication history but consider readiness for reasoning about deadlock freedom for future work \cite{Wang2012}.
Externalizing the complete observable behavior (and program structure) in this way devalues the whole point of
compositionality \cite[Section 1.6.2]{deRoever2001} but only postpones reasoning about the exponentially many interleavings.
Similarly, Guelev~\emph{et~al}.\@\xspace encode the semantics of the parallel composition into the postcondition \cite{Guelev2017}.

Hoare-style ac-reasoning \cite{AcHoare_Zwiers,AcSemantics_Zwiers,Hooman1987} including Hoare-style reasoning for HCSP \cite{Liu2010,Wang2012,Guelev2017} lacks symbolic execution as intuitive reasoning principle but manages with a distinguished history variable since multiple Hoare-triples cannot be considered together.
\dLCHP makes symbolic execution possible despite communication through explicit trace variables referring to the different possible states of the history in a proof.
The resulting combination of ac-reasoning and dynamic logic allows flexible switch between first-order, dynamic, and ac-reasoning while the axioms are simple capturing discrete, continues, or communication behavior.
Unlike \dLCHP, which has a global flow of time due to continuous evolution,
calculi for distributed real-time computation \cite{Hooman1987,Hooman1992} need to consider the waiting for termination of time-consuming discrete statements.

Unlike other \dL approaches \cite{Lunel2019,DBLP:journals/sttt/MullerMRSP18,Kamburjan2020},
\dLCHP has a parallel operator with built-in time-synchronization as first-class citizen in hybrid programs that can be arbitrarily nested with other programs,
rather than parallel composition of meta-level components with a explicit time model.
Modeling of parallelism by nondeterministic choice additionally requires extra care to ensure execution periodicity \cite{Lunel2019}.
In contrast to first-order constraints relating at most consecutive I/O events \cite{Lunel2019,DBLP:journals/sttt/MullerMRSP18,Kamburjan2020},
\dLCHP can reason about invariants of the whole communication history.
Different from our integrated reasoning about discrete, hybrid, and communication behavior,
Kamburjan~\emph{et~al}.\@\xspace \cite{Kamburjan2020} separate reasoning about communication from hybrid systems reasoning.

Quantified differential dynamic logic \QdL \cite{DBLP:conf/csl/Platzer10} allows reasoning about parallel compositions of an unbounded number of distributed CPSs.
Unlike \dLCHP that can reason about interactions of entirely different programs, parallelism in \QdL is restricted to subprograms with a \emph{homogeneous} structure.

Different from the denotational semantics of CHPs,
parallel composition of hybrid automata \cite{Lynch2003, Frehse2004, Henzinger2001, Benvenuti2014}, just like Hoare-style reasoning about HCSP \cite{Wang2012,Guelev2017}, always fall back to the combinatorial exploration of parallelism.
Consequently, even AGR approaches \cite{Lynch2003,Frehse2004,Henzinger1996,Benvenuti2014} for hybrid automata that mitigate the state space explosion for subautomata,
eventually resort to large product automata later.
In contrast, \dLCHP's proof rule for parallel composition exploits the built-in compositionality of its semantics enabling verification of subprograms truly independent of their environment except for the communication interface.
Unlike ac-formulas in \dLCHP,
which can capture change, rate, delay, or noise for arbitrary pairings of communication channels,
overapproximation is limited to coarse abstractions by timed transition systems \cite{Frehse2004},
components completely dropping knowledge about continuous behavior \cite{Henzinger2001},
or static global contracts \cite{Benvenuti2014}.
Where \dLCHP inherits complete reasoning about differential equation invariants from \dL,
automata approaches are often limited to linear continuous dynamics \cite{Frehse2004,Henzinger2001}.

Concurrent dynamic logic (CDL) has no way for parallel programs to interact~\cite{Peleg1987}.
CDL with communication \cite{Peleg1987a} has CSP-style \cite{Hoare1978} communication primitives but lacks continuous behavior and a proof calculus for verification.

\section{Conclusion}

This paper presented a dynamic logic \dLCHP for communicating hybrid programs (CHPs) with synchronous parallel composition in global time.
The \dLCHP proof calculus is the first truly compositional verification approach for communicating parallel hybrid systems.
To this end, \dLCHP exploits the flexibility of dynamic logic by complementing necessity and possibility modalities with assumption-commitment~(ac) modalities.
Crucially, this embedding of ac-reasoning enables compositional specification and verification of parallel hybrid behavior in a way that tames their complexity.
The practical feasibility of \dLCHP increases as it supports reasoning via intuitive symbolic execution in the presence of communication.
All technical subtleties in the semantic construction remain under the hood such that the actual calculus naturally generalizes dynamic logic reasoning.

Future work includes developing a uniform substitution calculus \cite{DBLP:journals/jar/Platzer17} for $\dLCHP$ in order to enable parsimonious theorem prover implementations \cite{DBLP:conf/cade/FultonMQVP15}.

\ifblind\else
\subsubsection{Funding Statement}
This project was funded in part by the Deutsche For\-schungs-gemeinschaft (DFG) -- \href{https://gepris.dfg.de/gepris/projekt/378803395?context=projekt&task=showDetail&id=378803395&}{378803395} (ConVeY) and an Alexander von Humboldt Professorship.
\fi

\let\oldthebibliography\thebibliography
\let\endoldthebibliography\endthebibliography
\renewenvironment{thebibliography}[1]{
  \begin{oldthebibliography}{#1}
    \setlength{\itemsep}{0em}
    \setlength{\parskip}{0em}
}
{
  \end{oldthebibliography}
}

\begingroup
\linespread{.87}
\renewcommand{\doi}[1]{doi: \href{https://doi.org/#1}{\nolinkurl{#1}}}
\bibliographystyle{splncs04}