text:
# Proving correctness of Timed Concurrent Constraint Programs

## 1 Introduction

Many “real-life” computer applications maintain some ongoing interaction with external physical processes and involve time-critical aspects. Characteristic of such applications, usually called real-time embedded systems, is the specification of timing constraints such as, for example, that an input is required within a bounded period of time. Typical examples of such systems are process controllers and signal processing systems.

In  tccp, a timed extension of the pure formalism of concurrent constraint programming(), is introduced. This extension is based on the hypothesis of bounded asynchrony (as introduced in ): Computation takes a bounded period of time rather than being instantaneous as in the concurrent synchronous languages ESTEREL , LUSTRE , SIGNAL  and Statecharts . Time itself is measured by a discrete global clock, i.e, the internal clock of the tccp process. In  we also introduced timed reactive sequences which describe at each moment in time the reaction of a tccp process to the input of the external environment. Formally, such a reaction is a pair of constraints $`c,d`$, where $`c`$ is the input given by the environment and $`d`$ is the constraint produced by the process in response to the input $`c`$ (such a response includes always the input because of the monotonicity of ccp computations).

In this paper we introduce a temporal logic for describing and reasoning about timed reactive sequences. The basic assertions of the temporal logic describe the reactions of such a sequence in terms of modalities which express either what a process assumes about the inputs of the environment and what a process commits to, i.e., has itself produced at one time-instant. These modalities thus provide a kind of assumption/commitment style of specification of the reactive behavior of a process. The main result of this paper is a sound and complete compositional proof system for reasoning about the correctness of tccp programs as specified by formulas in this temporal logic.

The remainder of this paper is organized as follows. In the next section we introduce the language tccp and its operational semantics. In Section 3 we introduce the temporal logic and the compositional proof system. In Section 4 we discuss soundness and completeness of the proof system. Section 5 concludes by discussing related work and indicating future research. A preliminary, short version of this paper appeared in .

## 2 The programming language

In this section we first define the tccp language and then we define formally its operational semantics by using a transition system.

Since the starting point is ccp, we introduce first some basic notions related to this programming paradigm. We refer to  for more details. The ccp languages are defined parametrically wrt to a given constraint system. The notion of constraint system has been formalized in  following Scott’s treatment of information systems. Here we only consider the resulting structure.

###### Definition 2.1

A constraint system is a complete algebraic lattice $`𝒞,,,\mathrm{𝑡𝑟𝑢𝑒},\mathrm{𝑓𝑎𝑙𝑠𝑒}`$ where $``$ is the lub operation, and $`\mathrm{𝑡𝑟𝑢𝑒}`$, $`\mathrm{𝑓𝑎𝑙𝑠𝑒}`$ are the least and the greatest elements of $`𝒞`$, respectively.

Following the standard terminology and notation, instead of $``$ we will refer to its inverse relation, denoted by $``$ and called entailment. Formally, $`c,dC.cddc.`$ In order to treat the hiding operator of the language a general notion of existential quantifier is introduced which is formalized in terms of cylindric algebras . Moreover, in order to model parameter passing, diagonal elements  are added to the primitive constraints. This leads to the concept of a cylindric constraint system. In the following, we assume given a (denumerable) set of variables $`\mathrm{𝑉𝑎𝑟}`$ with typical elements $`x,y,z,\mathrm{}`$.

###### Definition 2.2

Let $`𝒞,,,\mathrm{𝑡𝑟𝑢𝑒},\mathrm{𝑓𝑎𝑙𝑠𝑒}`$ be a constraint system. Assume that for each $`x\mathrm{𝑉𝑎𝑟}`$ a function $`_x:𝒞𝒞`$ is defined such that for any $`c,d𝒞`$:

$$\begin{array}{cc}(\mathrm{i})c_x(c),\hfill & (\mathrm{ii})\text{ if }cd\text{ then }_x(c)_x(d),\hfill \\ (\mathrm{iii})_x(c_x(d))=_x(c)_x(d),\hfill & (\mathrm{iv})_x(_y(c))=_y(_x(c)).\hfill \end{array}$$

Moreover assume that for $`x,y`$ ranging in $`\mathrm{𝑉𝑎𝑟}`$, $`𝒞`$ contains the constraints $`d_{xy}`$ (so called diagonal elements) which satisfy the following axioms:

$$\begin{array}{cc}(\mathrm{v})trued_{xx},\hfill & (\mathrm{vi})\text{ if }zx,y\text{ then }d_{xy}=_z(d_{xz}d_{zy}),\hfill \\ (\mathrm{vii})\text{ if }xy\text{ then }d_{xy}_x(cd_{xy})c.\hfill & \end{array}$$

Then C = $`𝒞,,,\mathrm{𝑡𝑟𝑢𝑒},\mathrm{𝑓𝑎𝑙𝑠𝑒},\mathrm{𝑉𝑎𝑟},_x,d_{xy}`$ is a cylindric constraint system.

Note that if $`𝐂`$ models the equality theory, then the elements $`d_{xy}`$ can be thought of as the formulas $`x=y`$. In the sequel we will identify a system C with its underlying set of constraints $`𝒞`$ and we will denote $`_x(c)`$ by $`_xc`$ with the convention that, in case of ambiguity, the scope of $`_x`$ is limited to the first constraint sub-expression (so, for instance, $`_xcd`$ stands for $`_x(c)d`$).

The basic idea underlying ccp is that computation progresses via monotonic accumulation of information in a global store. Information is produced by the concurrent and asynchronous activity of several agents which can add (tell) a constraint to the store. Dually, agents can also check (ask) whether a constraint is entailed by the store, thus allowing synchronization among different agents. Parallel composition in ccp is modeled by the interleaving of the basic actions of its components.

When querying the store for some information which is not present (yet) a ccp agent will simply suspend until the required information has arrived. In timed applications however often one cannot wait indefinitely for an event. Consider for example the case of a bank teller machine. Once a card is accepted and its identification number has been checked, the machine asks the authorization of the bank to release the requested money. If the authorization does not arrive within a reasonable amount of time, then the card should be given back to the customer. A timed language should then allow us to specify that, in case a given time bound is exceeded (i.e. a time-out occurs), the wait is interrupted and an alternative action is taken. Moreover in some cases it is also necessary to abort an active process $`A`$ and to start a process $`B`$ when a specific event occurs (this is usually called preemption of $`A`$). For example, according to a typical pattern, $`A`$ is the process controlling the normal activity of some physical device, the event indicates some abnormal situation and $`B`$ is the exception handler.

In order to be able to specify these timing constraints in ccp we introduce a discrete global clock and assume that $`ask`$ and $`tell`$ actions take one time-unit. Computation evolves in steps of one time-unit, so called clock-cycles. We consider action prefixing as the syntactic marker which distinguishes a time instant from the next one. Furthermore we make the assumption that parallel processes are executed on different processors, which implies that at each moment every enabled agent of the system is activated. This assumption gives rise to what is called maximal parallelism. The time in between two successive moments of the global clock intuitively corresponds to the response time of the underlying constraint system. Thus essentially in our model all parallel agents are synchronized by the response time of the underlying constraint system.

Furthermore, on the basis of the above assumptions we introduce a timing construct of the form now $`c`$ then $`A`$ else $`B`$ which can be interpreted as follows: If the constraint $`c`$ is entailed by the store at the current time $`t`$ then the above agent behaves as $`A`$ at time $`t`$, otherwise it behaves as $`B`$ at time $`t`$. As shown in  this basic construct allows one to derive such timing mechanisms as time-out and preemption. Thus we end up with the following syntax of timed concurrent constraint programming.

###### Definition 2.3

\[tccp Language \] Assuming a given cylindric constraint system C the syntax of agents is given by the following grammar:

$$\begin{array}{c}A::=\text{tell}(c)|_{i=1}^n\text{ask}(c_i)A_i|\mathrm{𝐧𝐨𝐰}c\mathrm{𝐭𝐡𝐞𝐧}A\mathrm{𝐞𝐥𝐬𝐞}B|AB|xA|p(x)\hfill \end{array}$$

where the $`c,c_i`$ are supposed to be finite constraints (i.e. algebraic elements) in $`𝒞`$. A tccp process $`P`$ is then an object of the form $`D.A`$, where $`D`$ is a set of procedure declarations of the form $`p(x)::A`$ and $`A`$ is an agent.

Action prefixing is denoted by $``$, non-determinism is introduced via the guarded choice construct $`_{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i`$, parallel composition is denoted by $``$, and a notion of locality is introduced by the agent $`xA`$ which behaves like $`A`$ with $`x`$ considered local to $`A`$, thus hiding the information on $`x`$ provided by the external environment. In the next subsection we describe formally the operational semantics of tccp. In order to simplify the notation, in the following we will omit the $`_{i=1}^n`$ whenever $`n=1`$ and we will use $`\text{tell}(c)`$ A as a shorthand for $`\text{tell}(c)(\mathrm{𝐚𝐬𝐤}(true)A)`$. In the following we also assume guarded recursion, that is we assume that each procedure call is in the scope of an $`\mathrm{𝐚𝐬𝐤}`$ construct. This assumption, which does not limit the expressive power of the language, is needed to ensure a proper definition of the operational semantics.

### 2.1 Operational semantics

The operational model of tccp can be formally described by a transition system $`T=(\mathrm{𝐶𝑜𝑛𝑓},)`$ where we assume that each transition step takes exactly one time-unit. Configurations (in) Conf are pairs consisting of a process and a constraint in $`𝒞`$ representing the common store. The transition relation $`\mathrm{𝐶𝑜𝑛𝑓}\times \mathrm{𝐶𝑜𝑛𝑓}`$ is the least relation satisfying the rules R1-R10 in Table 1 and characterizes the (temporal) evolution of the system. So, $`A,cB,d`$ means that if at time $`t`$ we have the process $`A`$ and the store $`c`$ then at time $`t+1`$ we have the process $`B`$ and the store $`d`$.

Let us now briefly discuss the rules in Table 1. In order to represent successful termination we introduce the auxiliary agent $`\mathrm{𝐬𝐭𝐨𝐩}`$: it cannot make any transition. Rule R1 shows that we are considering here the so called “eventual” tell: The agent $`\text{tell}(c)`$ adds $`c`$ to the store $`d`$ without checking for consistency of $`cd`$ and then stops. Note that the updated store $`cd`$ will be visible only starting from the next time instant since each transition step involves exactly one time-unit. According to rule $`\mathrm{𝐑𝟐}`$ the guarded choice operator gives rise to global non-determinism: The external environment can affect the choice since $`\mathrm{𝐚𝐬𝐤}(c_j)`$ is enabled at time $`t`$ (and $`A_j`$ is started at time $`t+1`$) iff the store $`d`$ entails $`c_j`$, and $`d`$ can be modified by other agents. The rules $`\mathrm{𝐑𝟑}`$-$`\mathrm{𝐑𝟔}`$ show that the agent now $`c`$ then $`A`$ else $`B`$ behaves as $`A`$ or $`B`$ depending on the fact that $`c`$ is or is not entailed by the store. Differently from the case of the ask, here the evaluation of the guard is instantaneous: If $`A,d`$ ($`B,d`$) can make a transition at time $`t`$ and $`c`$ is (is not) entailed by the store $`d`$, then the agent now $`c`$ then $`A`$ else $`B`$ can make the same transition at time $`t`$. Moreover, observe that in any case the control is passed either to $`A`$ (if $`c`$ is entailed by the current store $`d`$) or to $`B`$ (in case $`d`$ does not entail $`c`$). Rules R7 and R8 model the parallel composition operator in terms of maximal parallelism: The agent $`AB`$ executes in one time-unit all the initial enabled actions of $`A`$ and $`B`$. Thus, for example, the agent $`A:(\mathrm{𝐚𝐬𝐤}(c)\mathrm{𝐬𝐭𝐨𝐩})(\text{tell}(c)\mathrm{𝐬𝐭𝐨𝐩})`$ evaluated in the store $`c`$ will (successfully) terminate in one time-unit, while the same agent in the empty store will take two time-units to terminate. The agent $`xA`$ behaves like $`A`$, with $`x`$ considered local to $`A`$, i.e. the information on $`x`$ provided by the external environment is hidden to $`A`$ and, conversely, the information on $`x`$ produced locally by $`A`$ is hidden to the external world. To describe locality in rule R9 the syntax has been extended by an agent $`^dxA`$ where $`d`$ is a local store of $`A`$ containing information on $`x`$ which is hidden in the external store. Initially the local store is empty, i.e. $`xA=^{\mathrm{𝑡𝑟𝑢𝑒}}xA`$.

Rule $`\mathrm{𝐑𝟏𝟎}`$ treats the case of a procedure call when the actual parameter equals the formal parameter. We do not need more rules since, for the sake of simplicity, here and in the following we assume that the set D of procedure declarations is closed wrt parameter names: That is, for every procedure call p(y) appearing in a process D.A we assume that if the original declaration for p in D is p(x):: A then D contains also the declaration $`p(y)::x(\text{tell}(d_{\mathrm{𝑥𝑦}})A)`$333Here the (original) formal parameter is identified as a local alias of the actual parameter. Alternatively, we could have introduced a new rule treating explicitly this case, as it was in the original ccp papers..

Using the transition system described by (the rules in) Table 1 we can now define our notion of observables which associates with an agent a set of timed reactive sequences of the form

$$c_1,d_1\mathrm{}c_n,d_nd,d$$

where a pair of constraints $`c_i,d_i`$ represents a reaction of the given agent at time i: Intuitively, the agent transforms the global store from $`c_i`$ to $`d_i`$ or, in other words, $`c_i`$ is the assumption on the external environment while $`d_i`$ is the contribution of the agent itself (which includes always the assumption). The last pair denotes a “stuttering step” in which no further information can be produced by the agent, thus indicating that a “resting point” has been reached.

Since the basic actions of tccp are monotonic and we can also model a new input of the external environment by a corresponding tell operation, it is natural to assume that reactive sequences are monotonically increasing. So in the following we will assume that each timed reactive sequence $`c_1,d_1\mathrm{}c_{n1},d_{n1}c_n,c_n`$ satisfies the following condition: $`d_ic_i\text{ and }c_jd_{j1},`$ for any $`i[1,n1]`$ and $`j[2,n]`$. Since the constraints arising from the reactions are finite, we also assume that a reactive sequence contains only finite constraints444Note that here we implicitly assume that if $`c`$ is a finite element then also $`_xc`$ is finite..

The set of all reactive sequences is denoted by $`𝒮`$ and its typical elements by $`s,s_1\mathrm{}`$, while sets of reactive sequences are denoted by $`S,S_1\mathrm{}`$ and $`\epsilon `$ indicates the empty reactive sequence. Furthermore, $``$ denotes the operator which concatenates sequences. Operationally the reactive sequences of an agent are generated as follows.

###### Definition 2.4

We define the semantics $`R\mathrm{𝐴𝑔𝑒𝑛𝑡}𝒫(𝒮)`$ by

$$\begin{array}{cc}R(A)=\hfill & \{c,dw𝒮A,cB,d\text{ and }wR(B)\}\hfill \\ & \hfill \\ & \{c,cw𝒮A,c\to ̸\text{ and }wR(A)\{\epsilon \}\}.\hfill \end{array}$$

Note that $`R(A)`$ is defined as the union of the set of all reactive sequences which start with a reaction of $`A`$ and the set of all reactive sequences which start with a stuttering step of $`A`$. In fact, when an agent is blocked, i.e., it cannot react to the input of the environment, a stuttering step is generated. After such a stuttering step the computation can either continue with the further evaluation of $`A`$ (possibly generating more stuttering steps) or it can terminate, as a “resting point” has been reached. These two case are reflected in the second part of the definition of $`R(A)`$ by the two conditions $`wR(A)`$ and $`w\{\epsilon \}`$, respectively. Note also that, since the stop agent used in the transition system cannot make any move, an arbitrary (finite) sequence of stuttering steps is always appended to each reactive sequence.

Formally $`R`$ is defined as the least fixed-point of the corresponding operator $`\mathrm{\Phi }(\mathrm{𝐴𝑔𝑒𝑛𝑡}𝒫(𝒮))\mathrm{𝐴𝑔𝑒𝑛𝑡}𝒫(𝒮)`$ defined by

$$\begin{array}{cc}\mathrm{\Phi }(I)(A)=\hfill & \{c,dw𝒮A,cB,d\text{ and }wI(B)\}\hfill \\ & \hfill \\ & \{c,cw𝒮A,c\to ̸\text{ and }wI(A)\{\epsilon \}\}.\hfill \end{array}$$

The ordering on $`\mathrm{𝐴𝑔𝑒𝑛𝑡}𝒫(𝒮)`$ is that of (point-wise extended) set-inclusion (it is straightforward to check that $`\mathrm{\Phi }`$ is continuous).

## 3 A calculus for tccp

In this section we introduce a temporal logic for reasoning about the reactive behavior of tccp programs. We first define temporal formulas and the related notions of truth and validity in terms of timed reactive sequences. Then we introduce the correctness assertions that we consider and a corresponding proof system.

### 3.1 Temporal logic

Given a set $`M`$, with typical element $`X,Y,\mathrm{}`$, of monadic constraint predicate variables, our temporal logic is based on atomic formulas of the form $`X(c)`$, where $`c`$ is a constraint of the given underlying constraint system. The distinguished predicate $`I`$ will be used to express the “assumptions” of a process about its inputs, that is, $`I(c)`$ holds if the process assumes the information represented by $`c`$ is produced by its environment. On the other hand, the distinguished predicate $`O`$ represents the output of a process, that is, $`O(c)`$ holds if the information represented by $`c`$ is produced by the process itself (recall that the produced information includes always the input, as previously mentioned). More precisely, these formulas $`I(c)`$ and $`O(c)`$ will be interpreted with respect to a reaction which consists of a pair of constraints $`c,d`$, where $`c`$ represents the input of the external environment and $`d`$ is the contribution of the process itself (as a reaction to the input $`c`$) which always contains $`c`$ (i.e. such that $`dc`$ holds).

An atomic formula in our temporal logic is a formula as described above or an atomic formula of the form $`cd`$ which ‘imports’ information about the underlying constraint system, i.e., $`cd`$ holds if $`dc`$. Compound formulas are constructed from these atomic formulas by using the (usual) logical operators of negation, conjunction and (existential) quantification and the temporal operators $``$ (the next operator) and $`𝒰`$ (the until operator). We have the following three different kinds of quantification:

* quantification over the variables $`x,y,\mathrm{}`$ of the underlying constraint system;
* quantification over the constraints $`c,d,\mathrm{}`$ themselves;
* quantification over the monadic constraint predicate variables $`X,Y,\mathrm{}`$.

Variables $`p,q,\mathrm{}`$ will range over the constraints. We will use $`V,W,\mathrm{}`$, to denote a variable $`x`$ of the underlying constraint system, a constraint variable $`p`$ or a constraint predicate $`X`$.

###### Definition 3.1

\[Temporal formulas\] Given an underlying constraint system with set of constraints $`𝒞`$, formulas of the temporal logic are defined by

$$\varphi ::=pqX(c)\neg \varphi \varphi \psi V\varphi |\varphi \varphi 𝒰\psi $$

In the sequel we assume that the temporal operators have binding priority over the propositional connectives. We introduce the following abbreviations: $`c=d`$ stands for $`cddc`$, $`\mathrm{}\varphi `$ for $`\mathrm{𝑡𝑟𝑢𝑒}𝒰\varphi `$ and $`\mathrm{}\varphi `$ for $`\neg \mathrm{}\neg \varphi `$. We also use $`\varphi \psi `$ as a shorthand for $`\neg (\neg \varphi \neg \psi )`$ and $`\varphi \psi `$ as a shorthand for $`\neg \varphi \psi `$. Finally, given a temporal formula $`\varphi `$, we denote by $`FV(\varphi )`$ ($`FV_{constr}(\varphi )`$) the set of the free (constraint) variables of $`\varphi `$.

###### Definition 3.2

Given an underlying constraint system with set of constraints $`𝒞`$, the truth of an atomic formula $`X(c)`$ is defined with respect to a predicate assignment $`vMC`$ which assigns to each monadic predicate $`X`$ a constraint. We define

$`vX(c)`$ if $`v(X)c`$.
Thus $`X(c)`$ holds if $`c`$ is entailed by the constraint represented by $`X`$. In other words, a monadic constraint predicate $`X`$ denotes a set $`\{ddc\}`$ for some $`c`$. We restrict to constraint predicate assignments which are monotonic in the following sense: $`v(O)v(I)`$. In other words, the output of a process contains its input.

The temporal operators are interpreted with respect to finite sequence $`\rho =v_1,\mathrm{},v_n`$ of constraint predicate assignments in the standard manner: $`\varphi `$ holds if $`\varphi `$ holds in the next time-instant and $`\varphi 𝒰\psi `$ holds if there exists a future moment (possibly the present) in which $`\psi `$ holds and until then $`\varphi `$ holds. We restrict to sequences $`\rho =v_1,\mathrm{},v_n`$ which are monotonic in the following sense: for $`1i<n`$, we have

* $`v_{i+1}(X)v_i(X)`$, for every predicate $`X`$;
* $`v_{i+1}(I)v_i(O)`$.

The latter condition requires that the input of a process contains its output at the previous time-instant. Note that these conditions corresponds with the monotonicity of reactive sequences as defined above.

In order to define the truth of a temporal formula we introduce the following notions: given a finite sequence $`\rho =v_1,\mathrm{},v_n`$ of predicate assignments, we denote by $`l(\rho )=n`$ the length of $`\rho `$ and $`\rho _i=v_i`$, $`1in`$. We also define $`\rho <\rho ^{}`$ if $`\rho `$ is a proper suffix of $`\rho ^{}`$ ($`\rho \rho ^{}`$ if $`\rho <\rho ^{}`$ or $`\rho =\rho ^{}`$). Given a variable $`x`$ of the underlying constraint systems and a predicate assignment $`v`$ we define the predicate assignment $`xv`$ by $`xv(X)=_xd`$, where $`d=v(X)`$. Given a sequence $`\rho =v_1,\mathrm{},v_n`$, we denote by $`x\rho `$ the sequence $`xv_1,\mathrm{},xv_n`$. Moreover, given a monadic constraint predicate $`X`$ and a predicate assignment $`v`$ we denote by $`Xv`$ the restriction of $`v`$ to $`M\{X\}`$. Given a sequence $`\rho =v_1,\mathrm{},v_n`$, we denote by $`X\rho `$ the sequence $`Xv_1,\mathrm{},Xv_n`$. Furthermore, by $`\gamma `$ we denote a constraint assignment which assigns to each constraint variable $`p`$ a constraint $`\gamma (p)`$. Finally, $`\gamma \{c/p\}`$ denotes the result of assigning in $`\gamma `$ the constraint $`c`$ to the variable $`p`$.

Moreover, we assume that time does not stop, so actually a finite sequence $`v_1\mathrm{}v_n`$ represents the infinite sequence $`v_1\mathrm{}v_n,v_n,v_n\mathrm{}`$ with the last element repeated infinitely many times. Formally, this assumption is reflected in the following definition in the interpretation of the $``$. By a slight abuse of notation, given a sequence $`\rho =v_1\mathrm{}v_n`$ with $`n1`$ we define $`\rho `$ as follows

$$\begin{array}{cc}(n=1)\hfill & v_1=v_1\hfill \\ (n>1)\hfill & \rho =v_2\mathrm{}v_n.\hfill \end{array}$$

The truth of a temporal formula is then defined as follows.

###### Definition 3.3

Given a sequence of predicate assignments $`\rho =v_1,v_2,\mathrm{},v_n`$, a constraint assignment $`\gamma `$ and $`\varphi `$ a temporal formula, we define $`\rho _\gamma \varphi `$ by:

by:

$$\begin{array}{ccc}\rho _\gamma pq\hfill & \text{if}\hfill & \gamma (q)\gamma (p)\hfill \\ \rho _\gamma X(c)\hfill & \text{if}\hfill & \rho _1X(c)\hfill \\ \rho _\gamma \neg \varphi \hfill & \text{if}\hfill & \rho \vDash ̸_\gamma \varphi \hfill \\ \rho _\gamma \varphi _1\varphi _2\hfill & \text{if}\hfill & \rho _\gamma \varphi _1\text{ and }\rho _\gamma \varphi _2\hfill \\ \rho _\gamma x\varphi \hfill & \text{if}\hfill & \rho ^{}_\gamma \varphi \text{, for some }\rho ^{}\text{ s.t. }x\rho =x\rho ^{}\hfill \\ \rho _\gamma X\varphi \hfill & \text{if}\hfill & \rho ^{}_\gamma \varphi \text{, for some }\rho ^{}\text{ s.t. }X\rho =X\rho ^{}\hfill \\ \rho _\gamma p\varphi \hfill & \text{if}\hfill & \rho _\gamma ^{}\varphi \text{, for some }c\text{ s.t. }\gamma ^{}=\gamma \{c/p\}\hfill \\ \rho _\gamma \varphi \hfill & \text{if}\hfill & \rho _\gamma \varphi \hfill \\ \rho _\gamma \varphi 𝒰\psi \hfill & \text{if}\hfill & \text{for some }\rho ^{}\rho \text{}\rho ^{}_\gamma \psi \text{ and for all }\rho ^{}<\rho ^{\prime \prime }\rho \text{}\rho ^{\prime \prime }_\gamma \varphi .\hfill \end{array}$$

Moreover $`\rho \varphi `$ iff $`\rho _\gamma \varphi `$ for every constraint assignment $`\gamma `$.

###### Definition 3.4

A formula $`\varphi `$ is valid, notation $`\varphi `$, iff $`\rho \varphi `$ for every sequence $`\rho `$ of predicate assignments.

We have the validity of the usual temporal tautologies. Monotonicity of the constraint predicates wrt the entailment relation of the underlying constraint system is expressed by the formula

$$pqX(pq(X(q)X(p))).$$

Monotonicity of the constraint predicates wrt time implies the validity of the following formula

$$pX(X(p)\mathrm{}X(p)).$$

The relation between the distinguished constraint predicates $`I`$ and $`O`$ is logically described by the laws

$$p(I(p)O(p))\mathrm{and}p(O(p)I(p)),$$

that is, the output of a process contains its input and is contained in the inputs of the next time-instant.

### 3.2 The proof-system

We introduce now a proof-system for reasoning about the correctness of tccp programs. We first define formally the correctness assertions and their validity.

###### Definition 3.5

Correctness assertions are of the form $`A\mathrm{𝑠𝑎𝑡}\varphi `$, where $`A`$ is a tccp process and $`\varphi `$ is a temporal formula. The validity of an assertion $`A\mathrm{𝑠𝑎𝑡}\varphi `$, denoted by $`A\mathrm{𝑠𝑎𝑡}\varphi `$, is defined as follows

$$A\mathrm{𝑠𝑎𝑡}\varphi \text{ iff }\rho \varphi ,\text{ for all }\rho R^{}(A),$$

where

$$R^{}(A)=\{v_1,\mathrm{},v_n\begin{array}{cc}v_1(I),v_1(O)\mathrm{}v_n(I),v_n(O)R(A)\hfill & \}.\hfill \end{array}$$

Roughly, the correctness assertion $`A\mathrm{𝑠𝑎𝑡}\varphi `$ states that every sequence $`\rho `$ of predicate assignments such that its ‘projection’ onto the distinguished predicates $`I`$ and $`O`$ generates a reactive sequence of $`A`$, satisfies the temporal formula $`\varphi `$.

Table 2 presents the proof-system.

Axiom T1 states that the execution of $`\text{tell}(c)`$ consists of the output of $`c`$ (as described by $`O(c)`$) together with any possible input (as described by $`I(q)`$). Moreover, at every time-instant in the future no further output is generated, which is expressed by the formula

$$p(O(p)I(p)),$$

which we abbreviate by stut (since it represents stuttering steps).

In rule T2 $`I_i`$ stands for $`I(c_i)`$. Given that $`A_i`$ satisfies $`\varphi _i`$, rule T2 allows the derivation of the specification for $`\mathrm{\Sigma }_{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i`$, which expresses that either eventually $`c_i`$ is an input and, consequently, $`\varphi _i`$ holds in the next time-instant (since the evaluation of the ask takes one time-unit), or none of the guards is ever satisfied.

Rule T3 simply states that if $`A`$ satisfies $`\varphi `$ and $`B`$ satisfies $`\psi `$ then every computation of now $`c`$ then $`A`$ else $`B`$ satisfies either $`\varphi `$ or $`\psi `$, depending on the fact that $`c`$ is an input or not.

Hiding of a local variable $`x`$ is axiomatized in rule T4 by first existentially quantifying $`x`$ in $`\varphi \mathrm{𝑙𝑜𝑐}(x)`$, where $`\mathrm{𝑙𝑜𝑐}(x)`$ denotes the following formula which expresses that $`x`$ is local, i.e., the inputs of the environment do not contain new information on $`x`$:

$$p(_xpp(\neg I(p)\mathrm{}(I(p)r(O(r)_xpr=p)))).$$

This formula literally states that the initial input does not contain information on $`x`$ and that everywhere in the computation if in the next state an input contains information on $`x`$ then this information is already contained by the previous output. Finally, the following formula $`\mathrm{𝑖𝑛𝑣}(x)`$

$$p\mathrm{}(_xpp(O(p)r(I(r)_xpr=p)))$$

states that the process does not provide new information on the global variable $`x`$.

Rule T5 gives a compositional axiomatization of parallel composition. The ‘fresh’ constraint predicates $`X`$ and $`Y`$ are used to represent the outputs of $`A`$ and $`B`$, respectively ($`\varphi [X/O]`$ and $`\psi [Y/O]`$ denote the result of replacing $`O`$ by $`X`$ and $`Y`$). Additionally, the formula

$$p\mathrm{}(O(p)(q_1,q_2(X(q_1)Y(q_2)q_1q_2=p))),$$

denoted by $`\mathrm{𝑝𝑎𝑟}(X,Y)`$, expresses that every output of $`AB`$ can be decomposed into outputs of $`A`$ and $`B`$.

Rule T6, where $`_p`$ denotes derivability within the proof system, describes recursion in the usual manner by using a meta-rule (Scott-induction, see also ): we can conclude that the agent $`p(x)`$ satisfies a property $`\varphi `$ whenever the body of $`p(x)`$ satisfies the same property assuming the conclusion of the rule. In this rule $`x`$ is assumed to be both the formal and the actual parameter. We do not need more rules since, as previously mentioned, we can assumed that the set D of procedure declarations is closed wrt parameter names.

Note also that, for the sake of simplicity, we do not mention explicitly the declarations in the proof system. In fact, the more precise formulation of this rule, that will be needed in the proofs, would be the following:

$$\frac{D\{p\}.p(x)\mathrm{𝑠𝑎𝑡}\varphi _pD\{p\}.A\mathrm{𝑠𝑎𝑡}\varphi }{D.p(x)\mathrm{𝑠𝑎𝑡}\varphi }.$$

Rule T7 allows to weaken the specification.

As an example of a sketch of a derivation consider the agent $`xA`$ where

$$\begin{array}{cc}A::\hfill & \mathrm{𝐚𝐬𝐤}(x=a)\text{tell}(true)\hfill \\ & +\hfill \\ & \mathrm{𝐚𝐬𝐤}(true)\text{tell}(y=b).\hfill \end{array}$$

(constraints are equations on the Herbrand universe). By T1 and T7 we derive

$$\text{tell}(y=b)\mathrm{𝑠𝑎𝑡}O(y=b)and\text{tell}(true)\mathrm{𝑠𝑎𝑡}O(true).$$

By T2 and T7 we subsequently derive

$$A\mathrm{𝑠𝑎𝑡}I(x=a)O(y=b)$$

(note that $`\neg I(\mathrm{𝑡𝑟𝑢𝑒})`$ is logically equivalent to $`\mathrm{𝑓𝑎𝑙𝑠𝑒}`$ and $`\mathrm{𝑓𝑎𝑙𝑠𝑒}𝒰\varphi `$ is equivalent to $`\varphi `$). Using rule T4, we derive the correctness assertion

$$xA\mathrm{𝑠𝑎𝑡}x((I(x=a)O(y=b))\mathrm{𝑙𝑜𝑐}(x)).$$

It is easy to see that $`I(x=a)\mathrm{𝑙𝑜𝑐}(x)`$ implies false. So we have that $`x((I(x=a)O(y=b))\mathrm{𝑙𝑜𝑐}(x))`$ implies $`x(\mathrm{𝑙𝑜𝑐}(x)O(y=b))`$. Clearly this latter formula implies $`O(y=b)`$. Summarizing the above, we obtain a derivation of the correctness assertion $`xA\mathrm{𝑠𝑎𝑡}O(y=b)`$ which states that in every reactive sequence of $`xA`$ the constraint $`y=b`$ is produced in the next (wrt the start of the sequence) time instant.

## 4 Soundness and completeness

We investigate now soundness and completeness of the above calculus. Here and in the following, in order to clarify some technical details, we consider processes of the form $`D.A`$ rather than agents of the form $`A`$ with a separate set of declarations $`D`$. All the previous definitions can be extended to processes in the obvious way. We also denote by $`_pD.A\mathrm{𝑠𝑎𝑡}\varphi `$ the derivability of the correctness assertion $`D.A\mathrm{𝑠𝑎𝑡}\varphi `$ in the proof system introduced in the previous section (assuming as additional axioms in rule T7 all valid temporal formulas).

Soundness means that every provable correctness assertion is valid: whenever $`_pD.Asat\varphi `$, i.e. $`D.Asat\varphi `$ is derivable, then $`D.Asat\varphi `$. Completeness on the other hand consists in the derivability of every valid correctness assertion: whenever $`D.Asat\varphi `$ then $`_pD.Asat\varphi `$ (in $`T`$).

At the heart of the soundness and completeness results that we are going to prove lies the compositionality of the semantics $`R^{}`$, which follows from the compositionality of the underlying semantics $`R`$. In order to prove such a compositionality, we first introduce a denotational semantics $`[[D.A]](e)`$ where, for technical reasons, we represent explicitly the environment $`e`$ which associate a denotation to each procedure identifier. More precisely, assuming that Pvar denotes the set of procedure identifier, $`\mathrm{𝐸𝑛𝑣}=\mathrm{𝑃𝑣𝑎𝑟}\mathrm{}(𝒮)`$, with typical element $`e`$, is the set of environments.

Given a process $`D.A`$, the denotational semantics $`[[D.A]]:\mathrm{𝐸𝑛𝑣}\mathrm{}(𝒮)`$ is defined by the equations in Table 3, where $`\mu `$ denotes the least fixpoint wrt subset inclusion of elements of $`\mathrm{}(𝒮)`$. The semantic operators appearing in Table 3 are formally defined as follows. Intuitively they reflect, in terms of reactive sequences, the operational behaviour of their syntactic counterparts.

###### Definition 4.1

 Let $`S,S_i`$ be sets of reactive sequences and $`c,c_i`$ be constraints. Then we define the operators $`\stackrel{~}{}`$, $`\stackrel{~}{}`$, $`\stackrel{~}{now}`$ and $`\stackrel{~}{}x`$ as follows:

Guarded Choice

$$\stackrel{~}{}_{i=1}^nc_iS_i=\begin{array}{c}\{ss^{}𝒮\begin{array}{c}s=d_1,d_1\mathrm{}d_m,d_m,d_j⊬c_i\text{ for each }j[1,m\text{-}1],i[1,n],\hfill \\ d_mc_h\text{ and }s^{}S_h\text{ for an }h[1,n]\}\hfill \end{array}\hfill \\ \hfill \\ \{s𝒮\begin{array}{c}s=d_1,d_1\mathrm{}d_m,d_m,d_j⊬c_i\text{ for each }j[1,m],i[1,n]\},\hfill \end{array}\hfill \end{array}$$

Parallel Composition Let $`\stackrel{~}{}𝒮\times 𝒮𝒮`$ be the (commutative and associative) partial operator defined as follows:

$$\begin{array}{c}c_1,d_1\mathrm{}c_n,d_nd,d\stackrel{~}{}c_1,e_1\mathrm{}c_n,e_nd,d=c_1,d_1e_1\mathrm{}c_n,d_ne_nd,d.\hfill \end{array}$$

We define $`S_1\stackrel{~}{}S_2`$ as the point-wise extension of the above operator to sets.

The Now-Operator

$$\stackrel{~}{now}(c,S_1,S_2)=\{s𝒮s=c^{},ds^{}\text{ and either }\text{}c^{}c\text{ and }sS_1\text{ or }c^{}⊬c\text{ and }sS_2\}.$$

The Hiding Operator We first need the following notions similar to those used in :

Given a sequence $`s=c_1,d_1\mathrm{}c_n,c_n`$, we denote by $`xs`$ the sequence $`xc_1,xd_1\mathrm{}xc_n,xc_n`$.

A sequence $`s^{}=c_1,d_1\mathrm{}c_n,c_n`$ is $`x`$-connected if

* $`_xc_1=c_1`$ (that is, the input constraint of $`s^{}`$ does not contain information on $`x`$) and
* $`_xc_id_{i1}=c_i\text{ for each }i[2,n]`$ (that is, each assumption $`c_i`$ does not contain any information on $`x`$ which has not been produced previously in the sequence by some $`d_j`$).

A sequence $`s`$ is $`x`$-invariant if

* for all computation steps $`c,d`$ of $`s`$, $`d=_xdc`$ holds.

The semantic hiding operator then can be defined as follows:

$$\stackrel{~}{}xS=\{s𝒮\text{there exists }s^{}S\text{ such that }_xs=_xs^{}\text{}s^{}\text{ is }x\text{-connected and }s\text{ is }x\text{-invariant}\}.$$

A few explanations are in order here. Concerning the semantic choice operator, a sequence in $`\stackrel{~}{}_{i=1}^nc_iS_i`$ consists of an initial period of waiting for (a constraint stronger than) one of the constraints $`c_i`$. During this waiting period only the environment is active by producing the constraints $`d_i`$ while the process itself generates the stuttering steps $`d_i,d_i`$. Here we can add several pairs since the external environment can take several time-units to produce the required constraint. When the contribution of the environment is strong enough to entail a $`c_h`$ the resulting sequence is obtained by adding $`s^{}S_h`$ to the initial waiting period.

In the semantic parallel operator defined on sequences we require that the two arguments of the operator agree at each point of time with respect to the contribution of the environment (the $`c_i`$’s) and that they have the same length (in all other cases the parallel composition is assumed being undefined).

In the definition of $`\stackrel{~}{}`$ we say that a sequence is $`x`$-connected if no information on $`x`$ is present in the input constraints which has not been already accumulated by the computation of the agent itself. A sequence is $`x`$-invariant if its computation steps do not provide more information on $`x`$.

If $`D.A`$ is a closed process, that is if all the procedure names occurring in $`A`$ are defined in $`D`$, then $`[[D.A]](e)`$ does not depend on $`e`$ and will be indicated as $`[[D.A]]`$. Environments in general allows us to defined the semantics also of processes which are not closed, and this will be used in the soundness proof.

The following result shows the correspondence between the two semantics we have introduced and therefore the compositionality of $`R(A)`$.

###### Theorem 4.2

 If $`D.A`$ is closed then $`R(A)=[[D.A]]`$ holds.

In order to prove the soundness of the calculus we have to interpret also correctness assertions about arbitrary processes (that is, including processes which do contain undefined procedure variables).

###### Definition 4.3

Given a underlying constraint system $`𝒞`$ and an environment $`e`$, we define $`_eD.Asat\varphi `$ iff

$$\rho \varphi ,\text{ for all }\rho [[D.A]]^{}(e),$$

where

$$[[D.A]]^{}(e)=\{v_1,\mathrm{},v_n\begin{array}{cc}v_1(I),v_1(O)\mathrm{}v_n(I),v_n(O)[[D.A]](e)\hfill & \}.\hfill \end{array}$$

Note that, for closed processes, $`_e`$ coincides with $``$ as previously defined. We first need the following Lemma.

###### Lemma 4.4

Let $`\varphi `$ be a temporal formula, $`\rho `$ and $`\rho ^{}`$ be sequences of predicate assignment and let $`V`$ be a variable such that either $`VM`$ or $`V`$ is a variable $`x`$ of the underlying constraint system. The following holds:

1. Assume that $`\rho \varphi `$. Then $`\rho ^{}V\varphi `$ for each $`\rho ^{}`$ such that $`V\rho =V\rho ^{}`$.
2. Assume that $`\rho V\varphi `$ and $`FV_{constr}(\varphi )=\mathrm{}`$. Then there exists $`\rho ^{}`$ such that $`\rho ^{}\varphi `$ and $`V\rho ^{}=V\rho `$.

Proof

1. Assume that $`\rho \varphi `$. By Definition 3.3, $`\rho _\gamma \varphi `$ for each $`\gamma `$ and then for each $`\rho ^{}`$ such that $`V\rho =V\rho ^{}`$, we have that $`\rho ^{}_\gamma V\varphi `$ for each $`\gamma `$. Therefore, by Definition 3.3, $`\rho ^{}V\varphi `$.
2. Assume that $`\rho V\varphi `$ and $`FV_{constr}(\varphi )=\mathrm{}`$. By Definition 3.3, $`\rho _\gamma V\varphi `$ for each $`\gamma `$. Then by Definition 3.3, for each $`\gamma `$ there exists $`\rho ^{}`$ such that $`V\rho =V\rho ^{}`$ and $`\rho ^{}_\gamma \varphi `$. Since by hypothesis $`FV_{constr}(\varphi )=\mathrm{}`$, whenever $`\rho ^{}_\gamma \varphi `$ we also have that $`\rho ^{}\varphi `$ and then the thesis holds.

The following Theorem is the core of the soundness result.

###### Theorem 4.5

Let us denote $`D_i.A_i`$ by $`P_i`$ for $`1in`$ and $`D.A`$ by $`P`$. If

$$P_1sat\varphi _1,\mathrm{},P_nsat\varphi _n_pPsat\varphi \text{ and }_eP_isat\varphi _i,$$

for $`i=1,\mathrm{},n`$, then

$$_ePsat\varphi .$$

Proof The proof is by induction on the length $`l`$ of the derivation.

In this case $`A=\text{tell}(c)`$ and $`_pD.\text{tell}(c)\mathrm{𝑠𝑎𝑡}O(c)p(O(p)q(I(q)qc=p))\mathrm{}\mathrm{𝑠𝑡𝑢𝑡}`$. By Definition 4.3, we have to prove that for any $`e`$, $`\rho O(c)p(O(p)q(I(q)qc=p))\mathrm{}\mathrm{𝑠𝑡𝑢𝑡}`$, for all $`\rho [[D.\text{tell}(c)]]^{}(e).`$ By equation E2 of Table 3 and Definition 4.3,

$$[[D.\text{tell}(c)]]^{}(e)=\{\rho \rho _1(O)=\rho _1(I)c\text{ and }\rho _i(O)=\rho _i(I)\text{ for }i[2,l(\rho )]\}.$$

The remaining of the proof for this case is straightforward.

We distinguish various cases according to the last rule applied in the derivation.

In this case $`_pD._{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i\mathrm{𝑠𝑎𝑡}\chi `$, where $`\chi `$ is the formula

$$\underset{i=1}{\overset{n}{}}\left((\underset{j=1}{\overset{n}{}}\neg I(c_j)stut)𝒰(I(c_i)stut\varphi _i)\right)\mathrm{}(\underset{j=1}{\overset{n}{}}\neg I(c_j)stut).$$

Since for each $`i[1,n]`$ the proof $`D.A_i\mathrm{𝑠𝑎𝑡}\varphi _i`$ is shorter than the current one, from the inductive hypothesis follows that, for every environment $`e`$ and for each $`i[1,n]`$, $`_eD.A_i\mathrm{𝑠𝑎𝑡}\varphi _i`$, that is $`\rho \varphi _i`$, for all $`\rho [[D.A_i]]^{}(e).`$

Let us take a particular $`e`$. By Definition 4.3, we have to prove that $`\rho \chi `$, for all $`\rho [[D._{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i]]^{}(e).`$

By equation E3 of Table 3 and Definitions 4.1 and 4.3, $`[[D._{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i]]^{}(e)=D_1D_2`$, where

$$\begin{array}{ccc}D_1=\hfill & \{\rho \rho ^{}\hfill & \rho _j(O)=\rho _j(I)\text{ and }\rho _j(I)⊬c_i\text{ for each }j[1,l(\rho )1],i[1,n]\hfill \\ & & \rho _{l(\rho )}(I)c_h,\rho _{l(\rho )}(O)=\rho _{l(\rho )}(I)\text{ and }\rho ^{}[[D.A_h]]^{}(e)\text{ for an }h[1,n]\}\text{ and }\hfill \\ D_2=\hfill & \{\rho \hfill & \rho _j(O)=\rho _j(I)\text{ and }\rho _j(I)⊬c_i\text{ for each }j[1,l(\rho )],i[1,n]\}\hfill \end{array}$$

Now, it is straightforward to prove that if $`\rho D_2`$ then $`\rho \mathrm{}(_{j=1}^n\neg I(c_j)stut)`$. Moreover, since by inductive hypothesis for each $`i[1,n]`$, $`_eD.A_i\mathrm{𝑠𝑎𝑡}\varphi _i`$, we have that if $`\rho D_1`$ then $`\rho _{i=1}^n\left((_{j=1}^n\neg I(c_j)stut)𝒰(I(c_i)stut\varphi _i)\right)`$ and then the thesis.

In this case $`_p\text{now }c\text{ then }A\text{ else }B\mathrm{𝑠𝑎𝑡}(I(c)\varphi )(\neg I(c)\psi )`$. Since the proofs $`A\mathrm{𝑠𝑎𝑡}\varphi `$ and $`B\mathrm{𝑠𝑎𝑡}\psi `$ are shorter than the current one, the induction hypothesis says that for every environment $`e`$, we have that $`_eD.A\mathrm{𝑠𝑎𝑡}\varphi `$ and $`_eD.B\mathrm{𝑠𝑎𝑡}\psi `$ i.e. $`\rho \varphi `$ and $`\rho ^{}\psi `$ for all $`\rho [[D.A]]^{}(e)`$ and $`\rho ^{}[[D.B]]^{}(e).`$

Let us take a particular $`e`$. By Definition 4.3, we have to prove that $`\rho (I(c)\varphi )(\neg I(c)\psi )`$ for all $`\rho [[D.\text{now }c\text{ then }A\text{ else }B]]^{}(e)`$. Now the proof is immediate, by observing that by equation E4 of Table 3 and Definitions 4.1 and 4.3, $`[[D.\text{now }c\text{ then }A\text{ else }B]]^{}(e)=D_1D_2`$, where

$$\begin{array}{ccc}D_1=\hfill & \{\rho \rho _1(I)c\text{ and }\rho [[D.A]]^{}(e)\}\text{ and }\hfill & \\ D_2=\hfill & \{\rho ^{}\rho _1^{}(I)⊬c\text{ and }\rho ^{}[[D.B]]^{}(e)\}.\hfill & \end{array}$$

In this case $`_pxA\mathrm{𝑠𝑎𝑡}x(\varphi \mathrm{𝑙𝑜𝑐}(x))\mathrm{𝑖𝑛𝑣}(x)`$. Since the proof $`A\mathrm{𝑠𝑎𝑡}\varphi `$ is shorter than the current one, the induction hypothesis says that for every environment $`e`$, $`_eD.A\mathrm{𝑠𝑎𝑡}\varphi `$ i.e. $`\rho ^{}\varphi `$ for all $`\rho ^{}[[D.A]]^{}(e)`$. Let us consider a particular $`e`$. By Definition 4.3, we have to prove that $`\rho x(\varphi \mathrm{𝑙𝑜𝑐}(x))\mathrm{𝑖𝑛𝑣}(x)`$, for all $`\rho [[D.xA]]^{}(e).`$ By equation E6 of Table 3 and Definitions 4.1 and 4.3, $`\rho [[D.xA]]^{}(e)`$ if and only if there exists $`\rho ^{}[[D.A]]^{}(e)`$ such that $`l(\rho )=l(\rho ^{})`$ and the following conditions hold

1. for each $`i[1,l(\rho )]`$, $`x\rho _i(I)=x\rho _i^{}(I)`$ and $`x\rho _i(O)=x\rho _i^{}(O)`$,
2. $`x\rho _1^{}(I)=\rho _1^{}(I)`$ and for each $`i[2,l(\rho )]`$, $`x\rho _i^{}(I)\rho _{i1}^{}(O)=\rho _i^{}(I)`$,
3. for each $`i[1,l(\rho )]`$, $`\rho _i(O)=x\rho _i(O)\rho _i(I)`$.

Since for any sequence $`\rho `$ of predicate assignments and for any tccp process $`D.A`$, $`\rho [[D.A]]^{}(e)`$ if and only if its ‘projection’ onto the distinguished predicates $`I`$ and $`O`$ generates a reactive sequence of $`D.A`$, by 1. we can assume without loss of generality that $`x\rho =x\rho ^{}`$. From 2., the definition of $`loc(x)`$ and the inductive hypothesis follows that $`\rho ^{}\varphi \mathrm{𝑙𝑜𝑐}(x)`$. Therefore, by the previous equality and case 1 of Lemma 4.4 imply that $`\rho x(\varphi \mathrm{𝑙𝑜𝑐}(x))`$ holds. Moreover by 3. and by definition of $`inv(x)`$ we obtain that $`\rho inv(x)`$ thus proving the thesis for this case.

In this case $`_pAB\mathrm{𝑠𝑎𝑡}\chi `$, where $`\chi `$ is the formula

$$X,Y(\varphi [X/O]\psi [Y/O]\mathrm{𝑝𝑎𝑟}(X,Y)),$$

$`X,YM`$, $`XY`$ and $`X,YFV(\varphi )FV(\psi )`$. Since the proofs $`A\mathrm{𝑠𝑎𝑡}\varphi `$ and $`B\mathrm{𝑠𝑎𝑡}\psi `$ are shorter than the current one, the induction hypothesis says that for every environment $`e`$, we have that $`_eD.A\mathrm{𝑠𝑎𝑡}\varphi `$ and $`_eD.B\mathrm{𝑠𝑎𝑡}\psi `$ i.e. $`\rho ^{}\varphi `$ and $`\rho ^{\prime \prime }\psi `$ for all $`\rho ^{}[[D.A]]^{}(e)`$ and $`\rho ^{\prime \prime }[[D.B]]^{}(e).`$

Let us take a particular $`e`$. By Definition 4.3, we have to prove that $`\rho \chi `$, for all $`\rho [[D.AB]]^{}(e).`$ Assume that $`\rho [[D.AB]]^{}(e)`$. By equation E5 of Table 3 and Definitions 4.1 and 4.3, there exist $`\rho ^{}[[D.A]]^{}(e)`$ and $`\rho ^{\prime \prime }[[D.B]]^{}(e)`$ such that $`l(\rho )=l(\rho ^{})=l(\rho ^{\prime \prime })`$ and for each $`i[1,l(\rho )]`$, $`\rho _i(I)=\rho _i^{}(I)=\rho _i^{\prime \prime }(I)`$ and $`\rho _i(O)=\rho _i^{}(O)\rho _i^{}(O).`$ Since for any sequence $`\rho `$ of predicate assignments and for any tccp process $`D.A`$, $`\rho [[D.A]]^{}(e)`$ if and only if its ‘projection’ on the distinguished predicates $`I`$ and $`O`$ generates a reactive sequence of $`D.A`$, by previous observation we can assume without loss of generality that $`\rho _i(Z)=\rho _i^{}(Z)=\rho _i^{\prime \prime }(Z)`$ for each $`i[1,n]`$ and for each $`ZM`$ such that $`ZO`$. Now we can construct a new sequence $`\overline{\rho }`$ of predicate assignments, of the same length of $`\rho `$, such that $`\overline{\rho }_i(X)=\rho _i^{}(O)`$ $`\overline{\rho }_i(Y)=\rho _i^{\prime \prime }(O)`$ $`\overline{\rho }_i(Z)=\rho _i(Z)`$ for each $`i[1,l(\rho )]`$ and for each $`ZM`$ such that $`ZX,Y`$. Since $`X`$ and $`Y`$ are not free in $`\varphi `$ and $`\psi `$ and by inductive hypothesis $`\rho ^{}\varphi `$ and $`\rho ^{\prime \prime }\psi `$ holds, by construction we obtain that $`\overline{\rho }\varphi [X/O]`$ and $`\overline{\rho }\psi [Y/O]`$. Moreover, by construction $`\overline{\rho }\mathrm{𝑝𝑎𝑟}(X,Y)`$ holds. Therefore $`\overline{\rho }\varphi [X/O]\psi [Y/O]\mathrm{𝑝𝑎𝑟}(X,Y)`$ and the thesis follows from case 1 of Lemma 4.4 by observing that $`X,Y\rho =X,Y\overline{\rho }`$.

In this case $`_pD.p(x)\mathrm{𝑠𝑎𝑡}\varphi `$. Since the proof $`D\{p\}.p(x)sat\varphi _pD\{p\}.Asat\varphi `$ is shorter than the current one, the induction hypothesis says that for every environment $`e`$ such that $`_eD\{p\}.p(x)sat\varphi `$ we also have that $`_eD\{p\}.Asat\varphi `$. Let us take a particular $`e`$. We have to show that $`_eD.p(x)\mathrm{𝑠𝑎𝑡}\varphi `$ holds or, in other words, that if $`\rho [[D.p(x)]](e)`$ then we have that $`\rho \varphi `$.

Now $`[[D.p(x)]](e)=\mu \mathrm{\Psi }`$, where $`\mu \mathrm{\Psi }=_if_i`$, with $`f_0=\mathrm{}`$ and $`f_{i+1}=[[D\{p\}.A]](e\{f_i/p\})`$. Thus it suffices to prove by induction that for all $`n`$, if $`\rho f_n`$ then, $`\rho \varphi `$. The base case is obvious. Suppose that the thesis holds for $`f_n`$, so for $`e^{}=e\{f_n/p\}`$ we have that $`_e^{}D\{p\}.p(x)\mathrm{𝑠𝑎𝑡}\varphi `$, holds. Thus we infer that $`_e^{}D\{p\}.A\mathrm{𝑠𝑎𝑡}\varphi `$. Since by definition $`f_{n+1}=[[D\{p\}.A]](e\{f_n/p\})`$, we have that if $`\rho f_{n+1}`$ then $`\rho \varphi `$ which completes the proof.

The proof is immediate.

Since $`R(A)=[[D.A]](e)`$ holds for any closed process $`D.A`$ with $`e`$ arbitrary, whenever $`_eD.Asat\varphi `$ we also have $`D.Asat\varphi `$. Hence from the above result, with $`n=0`$, we can derive immediately the soundness of the system.

###### Corollary 4.6 (Soundness)

The proof system consisting of the rules C0-C7 is sound, that is, given a closed process $`D.A`$, if $`_pAsat\varphi `$ then $`D.Asat\varphi `$ holds, for every correctness assertion $`D.Asat\varphi `$.

Following the standard notion of completeness for Hoare-style proof systems as introduced by  we consider here a notion of relative completeness. We assume the existence of a property which describes exactly the denotation of a process, that is, we assume that for any process $`D.A`$ there exists a formula, that for the sake of simplicity we denote by $`\psi (A)`$, such that $`\rho R^{}(A)`$ iff $`\rho \psi (A)`$ holds555In order to describe recursion, the syntax of the temporal formulas has to be extended with a fixpoint operator of the form $`\mu p(x).\varphi `$, where $`p(x)`$ is supposed to occur positively in $`\varphi `$ and the variable $`x`$ denotes the formal parameter associated with the procedure $`p`$ (see ). The meaning of $`\mu p(x).\varphi `$ is given by a least fixpoint-construction which is defined in terms of the lattice of sets of sequences of predicate assignements ordered by set-inclusion.. This is analogous to assume the expressibility of the strongest postcondition of a process $`P`$, as with standard Hoare-like proof systems. Furthermore, we assume as additional axioms all the valid temporal formulas, (for use in the consequence rule). Also this assumption, in general, is needed to obtain completeness of Hoare logics.

Analogously to the previous case, the completeness of the system is a corollary of the following Theorem.

###### Theorem 4.7

Let $`D=\{p_1(x_1)::A_1,\mathrm{},p_n(x_n)::A_n\}`$ be a set of declarations and $`A`$ an agent which involves only calls to procedures declared in $`D`$. Then we have

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pAsat\psi (A).$$

where, for $`i=1,\mathrm{},n`$, $`\mathrm{\Phi }_i=p_i(x_i)sat\psi (p_i(x_i));`$.

Proof First observe that, for $`i=1,\mathrm{},n`$, we can assume $`FV_{constr}(\psi (p_i(x_i)))=\mathrm{}`$. In fact, from the definition of $``$ it follows that $`\rho R^{}(p_i(x_i))`$ if and only if $`\rho _\gamma \psi (p_i(x_i))`$, for each constraint assignment $`\gamma `$, and this holds if and only if $`\rho _{constr}\psi (p_i(x_i))`$, where $`_{constr}\psi (p_i(x_i))`$ is the universal closure over constraint variables of the formula $`\psi (p_i(x_i))`$. Therefore we can assume that all the constraint variables in $`\psi (p_i(x_i))`$ are universally quantified, thus there are no free constraint variables.

We prove now, by induction on the complexity of $`A`$, that $`\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pAsat\psi (A)`$ and $`FV_{constr}(\psi (A))=\mathrm{}`$.

In this case, since $`FV_{constr}(O(c)p(O(p)q(I(q)qc=p))\mathrm{}\mathrm{𝑠𝑡𝑢𝑡})=\mathrm{}`$, we have only to prove that

$$\psi (\text{tell}(c))=O(c)p(O(p)q(I(q)qc=p))\mathrm{}\mathrm{𝑠𝑡𝑢𝑡}.$$

The proof is straightforward, since Definition 3.5, Theorem 4.2 and equation E2 of Table 3 imply that the following equalities hold

$$R^{}(\text{tell}(c))=\{\rho \rho _1(O)=\rho _1(I)c\text{ and }\rho _i(O)=\rho _i(I)\text{ for }i[2,l(\rho )]\}.$$

By inductive hypothesis we obtain that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pA_isat\psi (A_i)\text{ and }FV_{constr}(\psi (A_i))=\mathrm{},$$

for $`i=1,2,\mathrm{},n`$. Then by rule T2 we obtain also that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pAsat\beta $$

where

$$\beta =\underset{i=1}{\overset{n}{}}\left((\underset{j=1}{\overset{n}{}}\neg I_jstut)𝒰(I_istut\psi (A_i))\right)\mathrm{}(\underset{j=1}{\overset{n}{}}\neg I_jstut),$$

.

The inductive hypothesis implies that that

$$FV_{constr}(\beta )=\mathrm{}.$$

Then, in order to prove the thesis we have to show that

$$\beta =\psi (\mathrm{\Sigma }_{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i)$$

holds, that is, we have to prove that $`\rho R^{}(\mathrm{\Sigma }_{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i)`$ if and only if $`\rho \beta `$.

(Only if). Assume that $`\rho R^{}(\mathrm{\Sigma }_{i=1}^n\mathrm{𝐚𝐬𝐤}(c_i)A_i)`$. By Theorem 4.2, equation E4 in Table 3 and Definition 4.1 it follows that $`\rho D_1D_2`$ where

$$\begin{array}{ccc}D_1=\hfill & \{\rho \rho ^{}\hfill & \rho _j(O)=\rho _j(I)\text{ and }\rho _j(I)⊬c_i\text{ for each }j[1,l(\rho )1],i[1,n]\hfill \\ & & \rho _{l(\rho )}(I)c_h,\rho _{l(\rho )}(O)=\rho _{l(\rho )}(I)\text{ and }\rho ^{}[[D.A_h]]^{}\text{ for an }h[1,n]\}\text{ and }\hfill \\ D_2=\hfill & \{\rho \hfill & \rho _j(O)=\rho _j(I)\text{ and }\rho _j(I)⊬c_i\text{ for each }j[1,l(\rho )],i[1,n]\}\hfill \end{array}$$

By definition of $`\psi (A)`$ and Definition 3.5, if $`\rho ^{}[[D.A_h]]^{}`$ then $`\rho ^{}\psi (A_h)`$. Therefore, if $`\rho D_1`$ then $`\rho (_{j=1}^n\neg I_jstut)𝒰(I_istut\psi (A_h))`$ for an $`h[1,n]`$ which implies $`\rho \beta `$ by definition of disjunction and of $`\beta `$.

If $`\rho D_2`$ then clearly $`\rho \mathrm{}(_{j=1}^n\neg I(c_j)stut)`$ and therefore $`\rho \beta `$. This complete the proof of the “Only if” part. The proof of the other implication is analogous (by using $`D_1`$ and $`D_2`$ above) and hence omitted.

By inductive hypothesis we obtain

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pAsat\psi (A),\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pBsat\psi (B)\text{ and }FV_{constr}(\psi (A))=FV_{constr}(\psi (B))=\mathrm{}.$$

Therefore rule T3 implies that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_p\text{now }c\text{ then }A\text{ else }Bsat(I(c)\psi (A))(\neg I(c)\psi (B)).$$

Since the inductive hypothesis implies also that $`FV_{constr}((I(c)\psi (A))(\neg I(c)\psi (B)))=\mathrm{}`$, to prove the thesis we have only to show that

$$(I(c)\psi (A))(\neg I(c)\psi (B))=\psi (\text{now }c\text{ then }A\text{ else }B)$$

hold, that is, we have to show that $`\rho R^{}(\text{now }c\text{ then }A\text{ else }B)`$ if and only if $`\rho (I(c)\psi (A))(\neg I(c)\psi (B))`$. The proof is straightforward, by observing that from the definition of $`\psi (A)`$ and $`\psi (B)`$, from Definition 3.5, Theorem 4.2, equation E4 of Table 3 and Definition 4.1 it follows the following equality

$$\begin{array}{ccc}R^{}(\text{now }c\text{ then }A\text{ else }B)=\hfill & \{\rho \rho _1(I)c\text{ and }\rho \psi (A)\}\hfill & \\ & \{\rho ^{}\rho _1^{}(I)⊬c\text{ and }\rho ^{}\psi (B)\}.\hfill & \end{array}$$

The inductive hypothesis implies that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pAsat\psi (A)\text{ and }FV_{constr}(\psi (A))=\mathrm{}$$

and therefore, by rule T4, we obtain that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pAsatx(\psi (A)\mathrm{𝑙𝑜𝑐}(x))\mathrm{𝑖𝑛𝑣}(x).$$

From the inductive hypothesis and the definitions of $`\mathrm{𝑙𝑜𝑐}(x)`$ and of $`\mathrm{𝑖𝑛𝑣}(x)`$, we obtain that

$$FV_{constr}(x(\psi (A)\mathrm{𝑙𝑜𝑐}(x))\mathrm{𝑖𝑛𝑣}(x))=\mathrm{}.$$
(1)
In order to prove the thesis, we have then to show that

$$x(\psi (A)\mathrm{𝑙𝑜𝑐}(x))\mathrm{𝑖𝑛𝑣}(x)=\psi (xA),$$

holds, that is, we have to prove that $`\rho R^{}(xA)`$ if and only if $`\rho x(\psi (A)\mathrm{𝑙𝑜𝑐}(x))\mathrm{𝑖𝑛𝑣}(x)`$.

Assume now that $`\rho R^{}(xA)`$. Definition 3.5, Theorem 4.2, equation E6 of Table 3, Definition 4.1 and the definition of $`\psi (A)`$ imply that there exists $`\rho ^{}`$ such that $`\rho ^{}\psi (A)`$, $`l(\rho )=l(\rho ^{})`$ and the following conditions hold:

1. for each $`i[1,l(\rho )]`$, $`x\rho _i(I)=x\rho _i^{}(I)`$ and $`x\rho _i(O)=x\rho _i^{}(O)`$;
2. $`x\rho _1^{}(I)=\rho _1^{}(I)`$ and for each $`i[2,l(\rho )]`$, $`x\rho _i^{}(I)\rho _{i1}^{}(O)=\rho _i^{}(I)`$;
3. for each $`i[1,l(\rho )]`$, $`\rho _i(O)=x\rho _i(O)\rho _i(I)`$.

Now the proof is analogous to that one already given for the case of Rule T4 of Theorem 4.5.

Conversely, assume that $`\rho x(\psi (A)\mathrm{𝑙𝑜𝑐}(x))\mathrm{𝑖𝑛𝑣}(x)`$. Then the following facts hold:

1. $`\rho \mathrm{𝑖𝑛𝑣}(x)`$. Therefore, by definition of $`\mathrm{𝑖𝑛𝑣}(x)`$, for each $`i[1,l(\rho )]`$ the following holds

$$\rho _i(O)=x\rho _i(O)\rho _i(I);$$
(2)
2. $`\rho x(\psi (A)\mathrm{𝑙𝑜𝑐}(x))`$. Then, from case 2 of Lemma 4.4 and (1) we obtain that $`\rho ^{}\psi (A)\mathrm{𝑙𝑜𝑐}(x)`$ for some $`\rho ^{}`$ such that

$$x\rho ^{}=x\rho .$$
(3)
Since $`\rho ^{}\psi (A)\mathrm{𝑙𝑜𝑐}(x)`$, from the definition of $`\psi (A)`$ and of $`\mathrm{𝑙𝑜𝑐}(x)`$ it follows that

$`\rho ^{}R^{}(A)\text{and}`$ (4)
$`x\rho _1^{}(I)=\rho _1^{}(I)\text{ and for each }i[2,l(\rho )],x\rho _i^{}(I)\rho _{i1}^{}(O)=\rho _i^{}(I).`$ (5)

From Definition 3.5, Theorem 4.2, equation E6 of Table 3, Definition 4.1, (2), (3), 4) and (5), it follows that $`\rho R^{}(xA)`$ and therefore the thesis holds.

By inductive hypothesis we obtain that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pA_isat\psi (A_i)\text{ and }FV_{constr}(\psi (A_i))=\mathrm{},$$

for $`i=1,2`$. Then by rule T5 we obtain also that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pAsatX,Y(\psi (A_1)[X/O]\psi (A_2)[Y/O]par(X,Y)),$$

where $`X,YFV(\psi (A_1))FV(\psi (A_2))`$ and $`XY`$.

The inductive hypothesis and the definition of $`par(X,Y)`$ imply that

$$FV_{constr}(X,Y(\psi (A_1)[X/O]\psi (A_2)[Y/O]par(X,Y))=\mathrm{}.$$
(6)
Then, in order to prove the thesis we have to show that

$$X,Y(\psi (A_1)[X/O]\psi (A_2)[Y/O]par(X,Y))=\psi (A_1A_2),$$

holds, that is, we have to prove that $`\rho R^{}(A_1A_2)`$ if and only if $`\rho X,Y(\psi (A_1)[X/O]\psi (A_2)[Y/O]par(X,Y))`$.

Assume that $`\rho R^{}(A_1A_2)`$. By Definition 3.5, Theorem 4.2, equation E4 in Table 3 and Definition 4.1 it follows that there exist $`\rho ^{}R^{}(A_1)`$ and $`\rho ^{\prime \prime }R^{}(A_2)`$ such that $`l(\rho )=l(\rho ^{})=l(\rho ^{\prime \prime })`$ and, for each $`i[1,l(\rho )]`$, $`\rho _i(I)=\rho _i^{}(I)=\rho _i^{\prime \prime }(I)`$ and $`\rho _i(O)=\rho _i^{}(O)\rho _i^{}(O)`$ hold. Since $`\rho ^{}R^{}(A_1)`$, the definition of $`\psi (A_1)`$ implies that $`\rho ^{}\psi (A_1)`$. Analogously we have that $`\rho ^{\prime \prime }\psi (A_2)`$. Now the proof is analogous to that one already shown for the case of Rule T5 in the proof of Lemma 4.5.

Conversely, assume that $`\rho X,Y(\psi (A_1)[X/O]\psi (A_2)[Y/O]par(X,Y))`$. We have to prove that $`\rho R^{}(A_1A_2)`$. By case 2 of Lemma 4.4 and (6) there exists a sequence of predicate assignments $`\overline{\rho }`$ such that $`X,Y\overline{\rho }=X,Y\rho `$ and $`\overline{\rho }\psi (A_1)[X/O]\psi (A_2)[Y/O]par(X,Y)`$.

We can now construct two new sequences $`\rho ^{}`$ and $`\rho ^{\prime \prime }`$ of predicate assignments having the same length as $`\overline{\rho }`$, such that, for each $`i[1,l(\overline{\rho })]`$,

$$\rho _i^{}(O)=\overline{\rho }_i(X),\rho _i^{\prime \prime }(O)=\overline{\rho }_i(Y)\text{ and }\rho _i^{}(Z)=\rho _i^{\prime \prime }(Z)=\overline{\rho }_i(Z),\text{ for each }ZM\text{}ZO\text{.}$$
(7)
Since $`X,YFV(\psi (A_1))FV(\psi (A_2))`$ and $`XY`$, by construction it follows that $`\rho ^{}\psi (A_1)`$ and $`\rho ^{\prime \prime }\psi (A_2)`$. Therefore, by definition of $`\psi (A)`$,

$$\rho ^{}R^{}(A_1)\text{ and }\rho ^{\prime \prime }R^{}(A_2).$$
(8)
Moreover, since $`\overline{\rho }par(X,Y)`$, again by construction we obtain that, for $`i[1,l(\overline{\rho })]`$,

$$\overline{\rho }_i(O)=\rho _i^{}(O)\rho _i^{\prime \prime }(O)$$
(9)
holds. From Definition 3.5, Theorem 4.2, equation E4 in Table 3, Definition 4.1, (7), (8) and (9) it follows that $`\overline{\rho }R^{}(A_1A_2)`$. Observe now that, by definition, for any sequence $`\rho `$ of predicate assignments and for any tccp process $`A`$, $`\rho R^{}(A)`$ if and only if its ‘projection’ on the distinguished predicates $`I`$ and $`O`$ generates a reactive sequence of $`R(A)`$. Hence, since $`X,Y\overline{\rho }=X,Y\rho `$ and $`\overline{\rho }R^{}(A_1A_2)`$, we have that $`\rho R^{}(A_1A_2)`$ and therefore the thesis holds.

Immediate.

From the above Theorem we derive the following corollary:

###### Corollary 4.8 (Completeness)

Let $`D=\{p_1(x_1)::A_1,\mathrm{},p_n(x_n)::A_n\}`$ and $`A_{n+1}`$ be an agent such that $`A_i`$, for $`1in+1`$, only involves calls to procedures declared in $`D`$. It follows that $`D.A_{n+1}sat\varphi `$ implies $`_pD.A_{n+1}sat\varphi `$.

Proof By the above lemma we have for $`i=1,\mathrm{},n`$ that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pA_isat\psi (D.p_i(x_i))$$

where $`\mathrm{\Phi }_i=p_i(x_i)sat\psi (D.p_i(x_i))`$ (note that $`\psi (D.A_i)=\psi (D.p_i(x_i))`$). Now a repeated application of the recursion rule gives us $`_pD.p_i(x_i)sat\psi (D.p_i(x_i))`$. Again by the above lemma we have that

$$\mathrm{\Phi }_1,\mathrm{},\mathrm{\Phi }_n_pA_{n+1}sat\psi (D.A_{n+1})$$

It follows by a straightforward induction on the length of the derivation (which does not involve applications of the recursion rule) that

$$\mathrm{\Phi }_1^{},\mathrm{},\mathrm{\Phi }_n^{}_pD.A_{n+1}sat\psi (D.A_{n+1})$$

where $`\mathrm{\Phi }_i^{}=D.p_i(x_i)sat\psi (D.p_i(x_i))`$, $`i=1,\mathrm{},n`$. So, since $`_p\mathrm{\Phi }_i^{}`$, $`i=1,\mathrm{},n`$, we thus derive that $`_pD.A_{n+1}sat\psi (D.A_{n+1})`$. Assume now that $`D.A_{n+1}sat\varphi `$. Then $`\psi (D.A_{n+1})\varphi `$ holds and an application of C7 gives us $`_pD.A_{n+1}sat\varphi `$.

The formula $`\psi (A)`$ (analogous to the strongest postcondition) has been used to prove completeness. However, often to prove a property of a program it is sufficient to deal with some simpler property. The situation can be compared to the problem of finding the suitable invariant when using the standard Hoare systems for imperative programming.

## 5 Related and future work

We introduced a temporal logic for reasoning about the correctness of a timed extension of ccp and we proved the soundness and completeness of a related proof system.

A simpler temporal logic for tccp has been defined in  by considering epistemic operators of “belief” and “knowledge” which corresponds to the operators $`I`$ and $`O`$ considered in the present paper. Even though the intuitive ideas of the two papers are similar, the technical treatment is different. In fact, the logic in  is less expressive than the present one, since it does not allow constraint (predicate) variables. As a consequence, the proof system defined in  was not complete.

Recently, a logic for a different timed extension of ccp, called ntcc, has been presented in . The language ntcc  is a non deterministic extension of the timed ccp language defined in . Its computational model, and therefore the underlying logic, are rather different from those that we considered. Analogously to the case of the ESTEREL language, computation in ntcc (and in the language defined in ) proceeds in “bursts of activity”: in each phase a ccp process is executed to produce a response to an input provided by the environment. The process accumulates monotonically information in the store, according to the standard ccp computational model, until it reaches a “resting point”, i.e. a terminal state in which no more information can be generated. When the resting point is reached, the absence of events can be checked and it can trigger actions in the next time interval. Thus, each time interval is identified with the time needed for a ccp process to terminate a computation. Clearly, in order to ensure that the next time instant is reached, the ccp process has to be always terminating, thus it is assumed that it does not contain recursion (a restricted form of recursion is allowed only across time boundaries). Furthermore, the programmer has to transfer explicitly the all information from a time instant to the next one by using special primitives, since at the end of a time interval all the constraints accumulated and all the processes suspended are discarded, unless they are argument to a specific primitive. These assumptions allow to obtain an elegant semantic model consisting of sequences of sets of resting points (each set describing the behavior at a time instant).

On the other hand, the tccp language that we consider has a different notion of time, since each time-unit is identified with the time needed for the underlying constraint system to accumulate the tell’s and to answer the ask’s issued at each computation step by the processes of the system. This assumption allows us to obtain a direct timed extension of ccp which maintain the essential features of ccp computations. No restriction on recursion is needed to ensure that the next time instant is reached, since at each time instant there are only a finite number of parallel agents which can perform a finite number of (ask and tell) actions. Also, no explicit transfer of information across time boundaries is needed in tccp, since the (monotonic) evolution of the store is the same as in ccp (these differences affects the expressive power of the language, see  for a detailed discussion). Since the store grows monotonically, some syntactic restrictions are needed also in tccp in order to obtain bounded response time, that is, to be able to statically determine the maximal length of each time-unit (see ).

¿From a logical point of view, as shown in  the set of resting points of a ccp process characterizes essentially the strongest post condition of the program (the characterization however is exact only for a certain class of programs). In  this logical view is integrated with (linear) temporal logic constructs which are interpreted in terms of sequences of sets of resting points, thus taking into account the temporal evolution of the system. A proof system for proving the resulting linear temporal properties is also defined in . Since the resting points provide a compositional model (describing the final results of computations), in this approach there is no need for a semantic and logical representation of “assumptions”. On the other hand such a need arises when one wants to describe the input/output behavior of a process, which for generic (non deterministic) processes cannot be obtained from the resting points. Since tccp maintains essentially the ccp computational model, at each time instant rather than a set of final results (i.e. a set of resting points) we have an input/ouput behavior corresponding to the interaction of the environment, which provides the input, with the process, which produces the output. This is reflected in the the logic we have defined.

Related to the present paper is also , where tcc specifications are represented in terms of graph structures in order to apply model checking techniques. A finite interval of time (introduced by the user) is considered in order to obtain a finite behavior of the tcc program, thus allowing the application of existing model checking algorithms.

Future work concerns the investigation of an axiomatization for the temporal logic introduced in this paper and the possibility of obtaining decision procedures, for example considering a semantic tableaux method. Since reactive sequences have been used also in the semantics of several other languages, including dataflow and imperative ones , we plan also to consider extensions of our logic to deal with these different languages.


format: text

text:
# Pseudo-digital quantum bits

## Abstract

Quantum computers are analog devices; thus they are highly susceptible to accumulative errors arising from classical control electronics. Fast operation–as necessitated by decoherence–makes gating errors very likely. In most current designs for scalable quantum computers it is not possible to satisfy both the requirements of low decoherence errors and low gating errors. Here we introduce a hardware-based technique for pseudo-digital gate operation. We perform self-consistent simulations of semiconductor quantum dots, finding that pseudo-digital techniques reduce operational error rates by more than two orders of magnitude, thus facilitating fast operation.

Quantum computation would not be feasible without quantum error correction.preskill98  However fault-tolerant codes can succeed only when error rates fall below a certain threshold.steane02  Error management therefore involves prevention as well as correction. In this letter we focus on the prevention of quantum gate errors. There are two possible approaches: perform the gates slowly (and thus accurately), or quickly (with associated bandwidth noise) using hardware that is relatively noise-tolerant. NMR quantum computers have succeeded in performing some simple quantum computations, by taking the slow approach.vandersypen01  However, promising applications like the factorization of large numbersshor94  involve many quantum gate operations. Indeed, more than $`10^9`$ Toffoli gates are required for factorizing a modest 130-digit number, using fault-tolerant codes.preskill98  Such computations may take years to complete at NMR speeds. Further, NMR qubits cannot be scaled up with current technologies. It is therefore important to develop robust gating techniques for faster, scalable technologies, including spin qubits in semiconductorsloss98 ; kane98  and superconducting qubits.makhlin01

We consider here a specific architecture: silicon-germanium quantum dots containing single electrons.loss98 ; hu00 ; burkard99 ; levy01 ; friesen02  The electrons are confined vertically by a quantum well heterostructure and laterally by repulsive electrostatic interactions with lithographically patterned top-gates. Voltage pulses lower the potential barrier between pairs of quantum dots, moving the electrons towards each other and “turning on” their exchange coupling $`J`$.loss98 ; hu00 ; burkard99  Details of the device are given in Ref. friesen02, .

The analog voltages that control couplings between the spin qubits cannot be produced perfectly, resulting in errors.friesen02  We consider relative uncertainties in the voltage height $`\mathrm{\Delta }V/V`$, arising from classical control electronics. Such control errors are unavoidable–in practice, they increase with the operating speed. The voltage $`V`$ controls two-qubit gate operations by “turning on” the qubit coupling $`J`$. If the dependence of $`J`$ on $`V`$ is strong, then even small voltage uncertainties lead to large coupling errors.

The slope $`J/V`$ determines the susceptibility of a quantum dot device to voltage errors. The dimensionless susceptibility is given by

$$\mathrm{\Omega }=\left|\frac{V}{J}\frac{J}{V}\right|,$$
(1)
where $`V`$ is the pulse height. $`\mathrm{\Omega }`$ is useful because it converts fractional voltage uncertainties into fractional gating errors: $`\mathrm{\Delta }J/J=\mathrm{\Omega }\mathrm{\Delta }V/V`$. For virtually all qubit proposals, $`\mathrm{\Omega }`$ is greater than zero, and it may be quite large for particular designs. Corresponding error rates are large, causing error correction techniques to fail. The requirement for fault tolerant computation is preskill98 ; note1

$$\mathrm{\Omega }\frac{\mathrm{\Delta }V}{V}<10^4.$$
(2)
The solid curve in Fig. 1 shows the dependence of exchange coupling $`J`$ on voltage $`V`$, as computed for the conventionally-gated quantum dot of Ref. friesen02, . From Eq. (1) we obtain $`\mathrm{\Omega }=5`$-10. The reason $`\mathrm{\Omega }`$ is large in this architecture (and other spin qubit architectures) is that the qubit coupling depends exponentially on the spacing between the two electrons, due to the exponential shape of the wavefunction tails. The strong dependence of $`J(V)`$ translates into a large value of $`\mathrm{\Omega }`$. Consequently, small uncertainties in the gate voltage produce substantial coupling errors. Assuming $`\mathrm{\Omega }=5`$-10, at the GHz operation speeds needed to beat decoherence $`\mathrm{\Delta }V/V`$ is so large that Eq. (2) cannot be satisfied.friesen02

A truly digital dependence of $`J`$ on $`V`$ (Fig. 1, dashed curve) would give $`\mathrm{\Omega }0`$, facilitating fault-tolerant computation. Such a response is obviously desirable, but unfeasible in an analog device. Here we propose a pseudo-digital technique, in which the electrons are confined to separate channels (Fig. 1, lower inset), such that they move past each other instead of directly towards each other.leuenberger01  There is a point of minimum separation where the coupling $`J`$ is a maximum and its dependence on $`V`$ is negligible. In other words, $`J(V)`$ becomes flat-topped. It is not immediately obvious that such behavior can be realized. In the following, we propose a specific pseudo-digital design for quantum dot qubits, and demonstrate its feasibility through detailed simulations of a realistic silicon-germanium device.

The main challenge for designing channel qubits is to provide adequate travel for the sliding electrons. Ideally, when the qubit coupling is turned “off,” the electrons should be well separated. In the “on” configuration, the coupling should be large enough to enable fast operation. To meet this challenge we have developed a bistable quantum dot design (Fig. 2). Using opposing plunger gates, an electron is squeezed into either side of a dot. The flattop “on” condition for $`J(V)`$ corresponds to the side-by-side configuration of electrons in neighboring dots.

To determine the feasibility of the channel qubit architecture, we model the double quantum dot device of Fig. 2(b), containing one electron per dot. The heterostructure is the same as in Ref. friesen02, . Precise Poisson and Schrödinger equation simulations are performed using finite element techniques. A basis set of single-electron wavefunctions is computed for each qubit in the Hartree-Fock approximation. A two-electron basis set is obtained in the configuration interaction approach, and exact diagonalization is performed on the corresponding Hamiltonion matrix. Image potentials arising from the various gates, due to the qubit electrons, are computed using Green’s functions techniques. The computations are then iterated until self-consistency is achieved. We do not consider impurities here, or other inevitable imperfections in the crystal lattice. However we note that disorder cannot invalidate the basis of pseudo-digital control–the existence of a minimum in the separation between the two qubits.

Fig. 3 shows the simulation results. As the plungers force the electrons into their side-by-side configuration, the exchange coupling grows, exponentially at first. The coupling reaches a peak as the qubits slide past one another; this is the flattop condition we exploit for pseudo-digital control. The bistable dot design clearly enables the desired range of electronic motion, from an “off” state, where the qubit coupling is exponentially small, to an “on” state, where $`J(V)`$ is flat-topped.

For the device studied here, the exchange coupling achieves a maximum value of $`0.4\mu `$eV, corresponding to gate time of 5 ns for the two-qubit SWAP. Faster operation can be achieved with appropriate modifications to the qubit design. In the present work, we have assumed minimum feature sizes of 30 nm for lithographic patterning, giving a qubit separation of 90 nm for the “on” configuration. Since $`J`$ decreases exponentially with qubit separation, reducing the feature dimensions will increase both $`J`$ and the gating speed.

One of the key features of the qubits in Fig. 2 is that the plunger gates and the channel gates perform very different roles. The channel gates regulate the maximum value of $`J`$. Since the channel gate voltages are held constant, this can be accomplished with arbitrary precision. Switching $`J`$ on and off is the function of the plunger gates, as controlled by classical control electronics. Ideally, plunger gate voltages will be varied quickly, near GHz frequencies. This speed makes them subject to the large uncertainties $`|\mathrm{\Delta }V/V|0.01`$ associated with high-speed electronics.friesen02 ; note2  The key advantage to the shape of $`J(V)`$ in Fig. 3 is that first order uncertainties in $`V`$ translate to second order errors in $`J`$. To estimate the errors in $`J`$, we calculate the RMS deviation of $`J(V)`$ from its mean, assuming a uniform distribution of gate voltages in the range $`\pm \mathrm{\Delta }V`$. This gives $`\mathrm{\Delta }J/J5\times 10^4`$, or $`\mathrm{\Omega }0.05`$. Thus, the channel qubit design decreases coupling errors by two orders of magnitude compared to conventional gating architectures. This improvement is accomplished in spite of the fact that the $`J(V)`$ curve in Fig. 3 is only “flat” at a single point.

With these results, Eq. (2) suggests that coupling errors $`\mathrm{\Delta }J`$ will only need to be reduced by a factor of 5 to meet the $`10^4`$ threshold level for fault tolerance. If $`10^3`$ is more appropriate, then the present scheme will be adequate.steane02  This can be accomplished by improvements in existing pulse generators, emphasizing the dependence of scalable quantum computers on cutting-edge classical technology. However, if enhancements in control electronics are not possible or desirable, $`\mathrm{\Omega }`$ may be further reduced by optimizing quantum dot designs. For example, top-gate patterns can be developed that cause qubit confinement potentials to become steeper. Small voltage fluctuations will then have less of an impact on the electron positions, resulting in smaller fluctuations in $`J`$.

In general, both single and two qubit gates are required for universal quantum computation. So far, we have only demonstrated how to apply pseudo-digital techniques to two-qubit operations. Fortunately, two qubit operations are known to be universal for coded spin qubits.bacon00 ; divincenzo00  Thus, universal quantum gate operations can be controlled pseudo-digitally.

In this paper, we have shown how to construct qubits that enable fast gating by pseudo-digital techniques. For any quantum computer, gate operations must be performed $`10^4`$ times faster than the decoherence rate. However, unless special care is taken, fast operation results in large gate errors. In general, an operational “sweet spot” must exist where two fundamental constraints are satisfied: the quantum gates are fast enough to beat decoherence and slow enough to be robust. Here we have developed a hardware design for quantum dot spin qubits that helps meet these criteria by increasing the speed at which gating remains robust. The concept is general and can be extended to many physical systems.unpub

###### Acknowledgements.

We have benefited from many discussions within the solid-state quantum computing group at the University of Wisconsin. Our work was supported by the U.S. Army Research Office through the ARDA program, and the National Science Foundation through the MRSEC and QuBIC programs.


text:
# Towards the Continuum Limit of the Overlap Quark Propagator in Landau Gauge Presented by J. B. Zhang at Lattice 2002 This work is supported by the Australia Research Council

## 1 Introduction

The quark propagator, is one of the fundamental quantities in QCD. By studying the momentum-dependent quark-mass function in the infrared region we can gain valuable insights into the mechanism of dynamical chiral symmetry breaking and the associated dynamical generation of mass. The ultraviolet behaviour of the propagator at large momentum can be used to extract the running quark mass .

There have been several studies of the momentum space quark propagator  using different gauge fixing and fermion actions. Here we focus on Landau gauge fixing and the overlap-fermion action and extend previous work  to two lattices with different lattice spacings $`a`$ and very similar physical volumes. This allows us to probe the continuum limit of the quark propagator.

## 2 Quark Propagator on the Lattice

In a covariant gauge in the continuum the renormalized Euclidean-space quark propagator must have the form

$`S(\zeta ;p)={\displaystyle \frac{1}{ip/A(\zeta ;p^2)+B(\zeta ;p^2)}}={\displaystyle \frac{Z(\zeta ;p^2)}{ip/+M(p^2)}},`$ (1)
where $`\zeta `$ is the renormalization point.

On the lattice the inverse lattice bare quark propagator takes the general form

$$(S^{\mathrm{bare}})^1(p)i\left(\underset{\mu }{}C_\mu (p)\gamma _\mu \right)+B(p).$$
(2)
We use periodic boundary conditions in the spatial directions and anti-periodic in the time direction. The discrete momentum values for a lattice of size $`N_i^3\times N_t`$, with $`n_i=1,..,N_i`$ and $`n_t=1,..,N_t`$, are

$`p_i={\displaystyle \frac{2\pi }{N_ia}}\left(n_i{\displaystyle \frac{N_i}{2}}\right),p_t={\displaystyle \frac{2\pi }{N_ta}}\left(N_t{\displaystyle \frac{1}{2}}{\displaystyle \frac{N_t}{2}}\right).`$ (3)
Defining the bare lattice quark propagator as

$$S^{\mathrm{bare}}(p)i\left(\underset{\mu }{}𝒞_\mu (p)\gamma _\mu \right)+(p),$$
(4)
we perform a spinor and color trace to identify

$`𝒞_\mu \left(p\right)={\displaystyle \frac{i}{12}}\mathrm{tr}\left[\gamma _\mu S^{\mathrm{bare}}\left(p\right)\right],\left(p\right)={\displaystyle \frac{1}{12}}\mathrm{tr}\left[S^{\mathrm{bare}}\left(p\right)\right].`$ (5)
The $`C_\mu (p)`$ and $`B(p)`$ in Eq.(2) can be written

$$C_\mu \left(p\right)=\frac{𝒞_\mu \left(p\right)}{𝒞^2\left(p\right)+^2\left(p\right)},B\left(p\right)=\frac{\left(p\right)}{𝒞^2\left(p\right)+^2\left(p\right)},$$
(6)
where $`𝒞^2(p)=_\mu (𝒞_\mu (p))^2`$.

We can identify the appropriate kinematic lattice momentum $`q`$ directly from the definition of the tree-level quark propagator,

$`q_\mu C_\mu ^{(0)}(p)`$ $`=`$ $`{\displaystyle \frac{𝒞_\mu ^{(0)}(p)}{(𝒞^{(0)}(p))^2+(^{(0)}(p))^2}}.`$ (7)
Having identified the lattice momentum $`q`$, we can now define the bare lattice propagator as

$`S^{\mathrm{bare}}(p)`$ $``$ $`{\displaystyle \frac{1}{iq/A(p)+B(p)}}={\displaystyle \frac{Z(p)}{iq/+M(p)}}`$ (8)
$`=`$ $`Z_2(\zeta ;a)S(\zeta ;p),`$
where $`S(\zeta ;p)`$ is the lattice version of the renormalized propagator in Eq. (1).

The overlap fermion formalism  realizes an exact chiral symmetry on the lattice and is automatically $`𝒪(a)`$ improved. The massless coordinate-space overlap-Dirac operator can be written in dimensionless lattice units as

$$D(0)=\frac{1}{2}\left[1+\gamma _5ϵ(H_w)\right],$$
(9)
where $`ϵ(H_w)`$ is the matrix sign function, where $`H_w(x,y)=\gamma _5D_w(x,y)`$ is the Hermitian Wilson-Dirac operator and where $`D_w`$ is the usual Wilson-Dirac operator on the lattice. However, in the overlap formalism the Wilson mass parameter $`m_w`$ enters with a negative sign.

The massless overlap quark propagator is given by

$$S^{\mathrm{bare}}(0)=\frac{1}{2m_w}\left[D^1(0)1\right]=\frac{1}{2m_w}\stackrel{~}{D}^1(0).$$
(10)
This definition of the massless overlap quark propagator follows from the overlap formalism  and ensures that the massless quark propagator anticommutes with $`\gamma _5`$, i.e., $`\{\gamma _5,S^{\mathrm{bare}}(0)\}=0`$ just as it does in the continuum . The tree-level momentum-space massless quark propagator defines the kinematic lattice momentum $`q`$,

$$S^{\mathrm{bare}}(0,p)\stackrel{~}{D}_c^1(0,p)S^{(0)}(0,p)=\frac{1}{iq/},$$
(11)
We can obtain $`q`$ numerically and analytically from the tree-level massless quark propagator .

Having identified the massless quark propagator in Eq. (10), we can construct the massive overlap quark propagator by simply adding a bare mass to its inverse, i.e.,

$$(S^{\mathrm{bare}})^1(m^0)(S^{\mathrm{bare}})^1(0)+m^0.$$
(12)
## 3 Numerical results

Here we work on two lattices with different lattice spacing $`a`$ and very similar physical volumes using a tadpole-improved plaquette plus rectangle gauge action. For each lattice size, we use 50 configurations . Lattice parameters are summarized in Table 1.

Our calculations use $`\kappa =0.19`$ for lattice 1 ($`12^3\times 24`$) and $`\kappa =0.1864`$ for lattice 2 ($`8^3\times 16`$) to make $`m_wa=1.661`$ on both lattices. We calculate at ten bare quark masses in physical units of $`m^0=`$ $`126`$, $`147`$, $`168`$, $`210`$, $`252`$, $`315`$, $`420`$, $`524`$, $`629`$, and $`734`$ MeV respectively.

The results of lattice 1 are presented in detail in Ref. . It is satisfying that the results of lattice 2 are similar to those of lattice 1. Here we focus on the comparision of the results on these two lattices. All data has been cylinder cut  and extrapolated to the chiral limit using a simple linear chiral extrapolation . The mass function $`M(p)`$ for the two lattices is plotted in Fig. 1 and the renormalization function $`Z(p)`$ of the two lattices is plotted in Fig. 2. We can see that when the mass function $`M(p)`$ is plotted against the discrete lattice momentum $`p`$ the results of the two lattices are in good agreement, while for the renormalization function $`Z(p)`$, good agreement is reached on the two lattices if it is plotted against the kinematical lattice momentum $`q`$.

## 4 Summary

In this report, we use tadpole-improved quenched lattice configurations, and the overlap fermion operator with the Wilson overlap kernel. The momentum space quark propagator is calculated in Landau gauge on two lattices with different lattice spacing $`a`$ and very similar physical volumes to explore the continuum limit. We calculate the nonperturbative momentum-dependent wavefunction renormalization function $`Z(p)`$ and the nonperturbative mass function $`M(p)`$ for a variety of bare quark masses and perform a simple linear extrapolation to the chiral limit. We have seen that, the continuum limit for, $`Z(p)`$, is most rapidly approached when it is plotted against the kinematical lattice momentum $`q`$, whereas for the quark mass function, $`M(p)`$, we should plot against the discrete lattice momentum $`p`$. The agreement between the two lattices suggests that we are close to the continuum limit.