Uniform Substitution for Differential Refinement Logic
Enguerrand Prebet André Platzer











E. Prebet, A. Platzer




  Karlsruhe Institute of Technology, Karlsruhe, Germany
  {enguerrand.prebet,platzer}@kit.edu


Uniform Substitution for
 Differential Refinement Logic
Funding has been provided by an Alexander von Humboldt Professorship and the pilot program Core Informatics (KiKIT) of the Helmholtz Association (HGF).
    Enguerrand Prebet0009-0008-0160-5219 André Platzer0000-0001-7238-5710
    April 29, 2024
===============================================================================================================================================================================================================




This paper introduces a uniform substitution calculus for differential refinement logic .
The logic extends the differential dynamic logic such that one can simultaneously reason about properties of and relations between hybrid systems.
Refinements is useful e.g. for simplifying proofs by relating a concrete hybrid system to an abstract one from which the property can be proved more easily.
Uniform substitution is the key to parsimonious prover microkernels.
It enables the verbatim use of single axiom formulas instead of axiom schemata with soundness-critical side conditions scattered across the proof calculus.
The uniform substitution rule can then be used to instantiate all axioms soundly.
Access to differential variables in enables more control over the notion of refinement, which is shown to be decidable on a fragment of hybrid programs.








§ INTRODUCTION


Hybrid systems modeled by joint discrete dynamics and continuous dynamics are important and subtle systems in need of sound proofs <cit.> on account of their important applications <cit.>.
Since such systems are important to get right, hybrid systems verification techniques themselves should be sound.
Uniform substitution <cit.>, originally phrased by Church for first-order logic <cit.>, has been identified as the key technique reducing the soundness-critical core to a prover microkernel and is behind the prover <cit.>.

This paper designs a corresponding uniform substitution proof calculus for differential refinement logic () <cit.>.
The logic is unique in its capabilities of proving simultaneous hybrid systems properties and hybrid systems refinement relations.
This ability of has been shown to be quite beneficial for establishing refinement relations of system implementations to verification abstractions and for relating time-triggered implementation models to event-triggered verification models <cit.>.
The latter relation overcomes a stark divide in embedded system design principles while combining ease of verification with ease of implementation in ways that neither design paradigm alone supports.
But such proving power only helps practical system verification if the theoretical proof calculi are implemented in a sound way and, in fact, has not yet been implemented at all.
Such an implementation is significantly simplified and significantly easier to get sound by identifying a uniform substitution calculus, which has no axiom schemata with their usual side conditions (and the algorithms implementing them) but merely a finite list of concrete formulas as axioms.
Reasoning directly with these concrete formulas also makes the proofs easier as the conditions are checked only when uniform substitution is used.
This means that a direct consequence of the axioms could have more admissible substitution instances than the axioms themselves, whereas with schemata, the side conditions would pile up and not generalize as well.
Other beneficial side effects include the fact that now acquires a Hilbert-style proof calculus that is significantly more flexible and also more modular than 's previous sequent calculus.

Challenges include the fact that uniform substitution calculi for hybrid systems give a differential-form semantics to differentials and differential symbols <cit.>, which is critical to obtain logic-based decision procedures for differential equation invariants <cit.>, but also renders some sequent calculus proof rules of unsound due to the resulting finer-grained view on differential equations.
The flip side is that this finer view distinguishes widely different classes of differential equations better, thereby making it easier to tell apart different differential equations that merely coincide on the overall reachable set while having different temporal behavior.
This difference is exploited here to obtain a decidability result for refinement for a fragment of hybrid systems.
Other challenges to overcome are the unexpected definition of free variables of refinements, which are required for soundness.
The core of the resulting calculus has been implemented in [<https://github.com/LS-Lab/KeYmaeraX-release/tree/dRL>], extending the prover microkernel in 4 hours with about 300 lines of code, mostly spent on writing down all the new axioms.



§ RELATED WORK


Hybrid programs in form a Kleene algebra with tests <cit.>.
Program equivalence for Kleene algebra with tests is known to be decidable for abstract atomic programs.
Refinement  can be recovered and defined as , but that duplicates reasoning about .
Certain classes of hypotheses can be added to the theory, e.g. Hoare-like triples p;;¬ q 0, without breaking the decidability <cit.>.
This however does not extend when limited commutativity is allowed, which arises even in the discrete fragment: (x2;y3)  (y3;x2) but (x2;x3) ≠ (x3;x2).
KAT with only discrete assignments has been studied as Schematic KAT <cit.>.
can derive the axioms of Schematic KAT, but also allows reasoning with continuous dynamics and differential equations.

The Event-B method <cit.> is a formalism for reasoning about discrete models where the primary mechanism is refinement to check the conformance between abstract models and more detailed ones.
Multiple different formalisms have been proposed. 
Hybrid Event-B <cit.> is an extension with tool support <cit.> for hybrid systems with events corresponding to discrete and continuous evolutions.
These continuous steps are however abstracted by the invariants they are assumed to satisfy.
Event-B can also be extended with theories <cit.>.
By adding some axioms about differential equations, it allows refinement reasoning with some continuous dynamics <cit.>.
In contrast, captures the continuous dynamics directly and proves the invariants as a consequence of the continuous dynamics.

Uniform substitution was proposed by Alonzo Church for first-order logic to capture axioms instead of axiom schemata <cit.>.
Modern uniform substitution originated for to support hybrid systems theorem proving in simple ways <cit.>, extended to hybrid games in differential game logic <cit.>, and 
to communicating parallel programs <cit.>.
This work is complementing the approach by adding refinement reasoning in a uniform substitution calculus for hybrid systems.
Developing uniform substitution calculi are key to the design of small soundness-critical prover microkernels such as <cit.>.




§ DIFFERENTIAL REFINEMENT LOGIC 


Differential refinement logic <cit.> extends the differential dynamic logic for hybrid systems <cit.> with a first-class refinement operator  on hybrid systems.
This section presents differential-form , which prepares for the features needed for 's uniform substitution axiomatization, most notably the inclusion of differential terms alongside function symbols, predicate symbols, and program constant symbols, but also the requisite inclusion of differential variable symbols.
Differential terms  are the fundamental logical device with which to enable sound <cit.> and complete <cit.> reasoning about differential equations.



 §.§ Syntax

This section defines the syntax of the differential refinement logic .
The set of all variables is .
To each variable x ∈ is associated a differential symbol x which is also in .
Its purpose is to use x to refer to the time-derivative of variable x during a differential equation, but also to cleverly relay that information to surrounding formulas in a sound way <cit.>.
It is this (crucial) presence of differential symbols, that gives differential-form a refined notion of refinement, especially of differential equations, compared to its sequent calculus predecessor <cit.>.


	Terms are defined by the grammar below where x ∈ is a variable,  is a function symbol of arity n and ,,1,…,n are terms:

    [              ,                x [1,…,n]  + · ]


Terms have the usual arithmetic operations and function symbols.
They also have differentials of terms  which describe how the value of  changes locally depending on the value of the differential symbols associated to the variables of .


	Formulas are defined by the grammar below where ,,1,…,n are terms,  is a predicate symbol of arity n,, are formulas and , are hybrid programs (def:HP):

    [           ,             ≤[1,…,n] ¬x ]



In addition to the operators of first-order logic of real arithmetic, formulas also contain the modality  which expresses that the formula  holds after all possible runs of the hybrid program .
extends with the refinement operator  which expresses that  refines  as  has more behaviors than : it is true in a state [state] if all states reachable by hybrid program  from [state] can be reached by hybrid program .
The program equivalence  is shorthand for .
This will be made explicit by axiom (leqantisym) in sec:dRL-calculus.

Note the fundamental difference between modal formula , which expresses that all runs of hybrid program  satisfy formula , compared to the refinement formula , which expresses that all runs of hybrid program  are also runs of hybrid program .
Both formulas refer to the runs of a hybrid program , but only the former states a property of the (final) states reached, while only the latter relates the overall transition behavior of hybrid program  to that of another program.
Just like , formula  is a formula and not just a judgment, so it can be true in some states and false in others.
This makes it possible to easily express conditional refinement as  meaning that if  is true initially, then  refines .
The logic is closed under all operators.
For example the formula  expresses that after all runs of  it is the case that all runs of  are also runs of .
Just like in an ordinary implication,   says nothing about what happens when the initial state does not satisfy .
Just like ordinary dynamic logic modalities   says nothing about what happens before program  ran.
Indeed, this extended expressibility that is closed under all operators will add to its expressibility and the eloquence of its uniform substitution proof calculus.


	Hybrid programs are defined by the grammar below where x is a variable,  is a term,  is a program constant,  is a differential-free formula and , are hybrid programs:

    [     ,       xxx=; ]


The test  behaves like a skip if the formula  is true in the current state and blocks the system otherwise.
The assignment x instantaneously updates the value of the variable x to the value of the term .
The nondeterministic assignment x updates the value of the variable x to an arbitrary value.
The differential equation x= behaves like a continuous evolution where both the differential equation x= and the domain  holds.
The nondeterministic choice  can behave like either  or .
The sequence ; behaves like  followed by .
The nondeterministic repetition  behaves like  repeated an arbitrary number of times.
[Modelling safe breaking]
	Let us consider a car that needs to stop before a wall at distance m. It starts from a safe position and can accelerate with acceleration A if some safety condition safe_T(x) is verified or brake with braking force B. The controller is run at most every T seconds. Proving its safety can be achieve by proving the following formula:
	
    [                A ≥ 0  B > 0  x + v^2/2B ≤ m  [car_T] x ≤ m; car_T (a-Bsafe_T(x);aA);t_0t;x = v, v = a, t = 1t - t_0≤ T ]

	Such system, called time-triggered, can be refined to a event-triggered system where the controller is sure to run when an event, E(x) is triggered. Event-triggered systems are easier to verify but less realistic. With and the axiom (boxleq) below, the time-triggered system can be proved safe by proving the safety of the event-triggered system and the refinement between the two systems:
	
    A ≥ 0  B ≥ 0  x + v^2/2B ≤ m  car_T car_E [car_E] x ≤ m

	
    car_E (a-Bsafe_E(x);aA);t_0t;x = v, v = a, t = 1E(x)




 §.§ Semantics

A state [state] is a mapping →.
The state [state]xr agrees with the state [state] except for the variable x whose value is r∈.
State [state] is a U-variation of [state] if [state] and [state] are equal on the complement U of that set of variables U.
For instance, [state]xr is an x-variation of [state].
The set of all states is .
The interpretation of a function symbol of arity n in interpretation [const] is a smooth function f: ^n→.

	The semantics of a term  in interpretation [const] and state [state] is its value ∈ and is defined as follows:
	
		
  * x = x
		
  * [1,…,n] = (1,…,n)
		
  * +  =  +
		
  * · = ·
		
  * = ∑_x∈x[x]θ([state]) = ∑_x∈x[x]
	

The partial derivative [x] corresponds to the derivative of the one-dimensional function X ↦[state]xX at X=x.
Since  denotes a smooth function, the derivative always exists.

Since hybrid programs appear in formulas and vice versa, the interpretation of hybrid programs and formulas is defined by simultaneous induction.
The interpretation of a predicate symbol of arity n in interpretation [const] is an n-ary relation ⊆^n.
The interpretation of a program constant symbol  in interpretation [const] is a state-transition relation ⊆× where [] iff the program constant  can reach the state [state] starting from the state [state].


    The semantics of a formula  for an interpretation [const] is the subset ⊆ of states in which  is true and defined as:
    
        
  * ≤ iff ≤
        
  * [1,…,n] iff (1,…,n)∈
        
  * ¬ iff 
        
  *  iff  and 
        
  * x iff [state]xr for all r∈
        
  *  iff  for all []
        
  *  iff [] for all []
    

A formula  is valid in [const] if =. A formula  is valid if it is valid in all interpretations.

	The semantics of a hybrid program  for an interpretation [const] is the transition relation []⊆× and is defined as follows:
	
		
  * [] =
		
  * [] =  ([state], [state])

		
  * [x] = ([state], [state]xr) for all r∈
		
		
  * [x] = ([state], [state]xr)  r =
		
		
  * [x=] = ([state], [state]) (0)  is a x-variation of [state] and [state] = (r) 
for some function  : [0, r ] → where (t)  is a x,x-variation of [state], 
satisfies x =  and [t]x= for all  t∈[0,r]
		
		
  * [] = []∪[]
		
		
  * [;] = []∘[] = ([state],[state]) : [], [] for some [state]∈
		
		
  * [] = ⋃_n∈[[n]]
	

Most importantly,  is true in a state [state] iff all states [state] reachable from [state] by running program  are also reachable by running  from [state].

The transition for a differential equation x= synchronizes the differential symbol x with the current time-derivative of x, i.e. , and then evolves the system continuously along the solution  of the differential equation x= within the domain .
Differential equations are the only hybrid programs that intrinsically relate variables with their associated differential symbol.

As differential equations effectively change the value of differential symbols, this is taken into account in the semantics of refinements.
The differential equations x = 1 and x = 2 are not equivalent: although both can reach the same values for x, their respective end states will always have a different value for x.
This behavior differs from the original semantics of <cit.>.
Intuitively, this notion of refinement corresponds to assuming that differential equations evolve with a global time t=1.
Other extensions of like <cit.> already assume the presence of such global time.
This property allows to express refinements of differential equations as a formula as shown in the axiom (ode) below.



 §.§ Static Semantics

Uniform substitution relies on the notions of free and bound variables to prevent any unsound substitution attempts.
Static semantics gives a definition for free and bound variables of terms, formulas and hybrid programs based on their (dynamic) semantics, which can be defined as in <cit.>:
 
	The static semantics defines the free variables ,  and , which are the variables whose values the expression depends on, and the bound variables , which are the variables whose values may change during the execution of .
They are defined formally as follows:
	
    = x∈   [const],[state],[state]a x-variation of [state] such that ≠
     = x∈   [const],[state],[state]a x-variation of [state] such that []∌[state]
     = x∈   [const],[state],[state],[state]a x-variation of [state] such that []
       and  [state]x-variation of [state] such that []
     = x∈   [const],[state],[state]such that [] and x≠x


Free and bounds variables are the only information needed about the logic to ensure that the result of uniform substitution is only defined when sound.
The coincidence lemmas <cit.> show that the truth-values of formulas only depend on their free variables and the interpretation of the symbols appearing in them (and similarly for terms and hybrid programs).
The set of function, predicate, and program symbols appearing in a formula, term or hybrid program is denoted ·.

 
	The set  is the smallest set with the coincidence property for : If [state] = [state] on V⊇ and [const] = [const] on , then =.


 
	The set  is the smallest set with the coincidence property for : If [state] = [state] on V⊇ and [const] = [const] on , then  iff .


 
	The set  is the smallest set with the coincidence property for : If [state] = [state] on V⊇ and [const] = [const] on , then [] implies [] for some [state] with [state] = [state] on V.

The proof <cit.> requires a mutual induction on the structure of the formula and hybrid program to show that = and [] = [] which extends to the refinement case.
The rest is done by induction on the set of variables S where the states [state] and [state] can differ.


	The set  is the smallest set with the bound effect property for : If [], then [state] = [state] on .


These sets are the smallest sets with the coincidence property, which means that conservative extensions of these sets can also be used soundly.
We define ,, and  as such overapproximations that can be computed syntactically.
Computing the free variables for a formula  requires the must-bound variables of the hybrid program , written α.
They represent the variables that will be written in all executions of .
These sets are given in app:static and are constructed in a standard way <cit.>, except for the new refinement operator.

Since the behavior of hybrid program  and  only depends on their respective free variables (lem:coincidence-HP), it would be tempting to define = ∪ stating that the refinement depends on the variables for which either program depends on.
Somewhat surprisingly, this would be unsound for reasons that truly touch on the nature of refinement.
Take the refinement formula x1 and a state [state] with x = 0.
Then x1.
However if the initial value of x is 1, then the refinement holds: [state]x1x1, because the assignment x1 has no effect.
In fact x1 = x even though =x1=∅.
To obtain a sound definition of , one needs to take into account the variables that may be written in one program, ∪, but that can also remain unmodified (which makes them depend on their initial values), so not in ∩.
Hence, the (syntactic) free variables of a refinement are defined as follows:

    = ∪∪((∪)∖(∩))

With this definition for refinements as the only but notable outlier to an otherwise standard definition of the syntatic computations for a static semantics  <cit.>, the static semantics  etc. can be proved to be sound overapproximations of the static semantics  from def:static-semantics and thereby enjoy the coincidence lemmas <ref>–<ref> and the bound effect lemma <ref>, respectively.

	For all terms , formulas  and hybrid programs :
	
    ⊇  ⊇  ⊇  ⊇


The proof of ·⊇· for formulas and hybrid programs is the only case affected by the addition of refinement operators compared to prior proofs <cit.>.
It is done by induction on the structure of the formulas and hybrid programs.
For hybrid programs, the property shown for  is stronger than the coincidence property from lem:coincidence-HP, enforcing [state] = [state] on V∪ rather than V.

 For the case of the refinement operator , the main insight is visible when proving that  implies  with [state] = [state] on V and [const] = [const] on .
For any [], we have [], [] and [] for some states [state],[state] by repeated use of the induction hypothesis and the definition of refinement.
Both the induction hypothesis and lem:boundeffect give us information on [state] and [state]. As V ⊇, the definition of  is crucial for ensuring that this knowledge is enough to fully determine [state] and [state] from [state],[state] and [state], and then that [state] = [state].



§ UNIFORM SUBSTITUTION


A uniform substitution σ is a mapping from terms of the form [] to terms σ[], from formulas of the form [] to formulas σ[], and from program constants  to hybrid programs σ.
The reserved 0-ary function symbol  marks the position where the argument, e.g.  in [], will be substituted in the resulting expression.
Soundness of such substitutions requires that the substitution does not introduce new free variables in a context where they are bound <cit.>.



fig:usubst defines the result Uσ of applying a uniform substitution σ with taboo set U⊆ to a formula  (or term , or hybrid programs  respectively) <cit.>.
For hybrid programs , the substitution result VUσ for input taboo U⊆ also outputs a taboo set V⊆, written in subscript notation, that will be tabooed after program .
Taboos U,V are sets of variables that cannot be substituted in free during the application of the substitution, because they have been bound within the context and, thus, potentially changed their meaning compared to the original substitution σ.
The difference is that the input U is already taboo when the substitution σ is applied to  while V is the new output taboo after .
Finally, σ is short for ∅σ started without initial taboos.
The key advantage to working with uniform substitution applications with taboo passing is that they enable an efficient one-pass substitution <cit.> compared to the classical Church-style uniform substitution application mechanism that checks admissibility at every binding operator along the way <cit.>.
One-pass uniform substitution postpones admissibility checks till the actual substitutions of function and predicate symbols according to explicit taboos carried around.

Despite the surprising definition of the free variables of a refinement, defining uniform substitution for the refinement case is standard, the input taboo U is given to both programs except that their output taboos V,W are discarded: 

    Uσ() = VUσWUσ

The reason is two-fold: 

	
  * Unlike quantifiers and modalities, refinements do not subsequently bind any variables.
	
  * The free variables of a refinement introduced by a substitution can only be introduced free in the programs, and thus checking these against the input taboo set U is sufficient.

This last statement is a consequence of σ⊆ and σ⊇, which is proved by a direct induction.





 §.§ Uniform Substitutions and Adjoint Interpretations


The proof of the soundness of uniform substitution follows the same structure as the proof of the uniform substitution lemma for <cit.> but adapted to hybrid programs instead of hybrid games and generalized to the presence of refinements.
The output taboo V of a uniform substitution VUσ will include the original taboo set U and all variables bound in the program .

	If VUσ is defined, then V ⊇ U ∪VUσ.

Whereas uniform substitutions are syntactic transformations on expressions, their semantic counterparts are semantic transformations on interpretations.
The two are related by Lemmas <ref> and <ref>.
Let [const][const]d denote the interpretation that agrees with interpretation [const] except for the constant function symbol  which is interpreted as the constant d∈.

	For an interpretation [const] and a state [state], the adjoint interpretation [const] modifies the interpretation of each function symbol ∈σ, predicate symbol ∈σ and program constant ∈σ as follows:
	
    : →; d ↦[const]dσ[]
       = d∈[const]dσ[]
       = [σ]




	The uniform substitution σ for taboo U ⊆ and its adjoint interpretation [const] for [const],[state] have the same semantics on U-variations [state] for all terms :
	
    Uσ   =




	Uniform substitution σ for taboo U ⊆ and its adjoint interpretation [const] for [const],[state] have the same semantics on U-variations [state] for all formulas  and hybrid programs :
	
    for all U-variations [state] of [state]   :Uσ iff 
    for all states [state] and all U-variations [state] of [state]   :[VUσ] iff []


The proof is done by simultaneous induction on the structure of σ,  and  for all U,[state],[state] and [state] app:sec34.
The use of U-variations is critical when the induction hypothesis needs to be used in a state other than [state], e.g. for quantifiers and modalities.
Without considering the extension of the refinement operator, this result was previously proved in a weaker form (U = ∅) for <cit.> or for more complex semantics like hybrid games <cit.>.




 §.§ Soundness of Uniform Substitution


lem:usubst-fmlprg is essentially all that is required to ensure the sound application of uniform substitution.
First, uniform substitution can be used to have a sound instantiation of the axioms, using the uniform substitution rule (US).
A proof rule is sound if the validity of the premises implies the validity of the conclusion.


	The proof rule (US) is sound.
	
    US


Uniform substitution can also be used on rules or whole inferences, as long as they are locally sound, i.e. the conclusion is valid in any interpretation where the premises are valid.
Locally sound inferences are also sound.


	All locally sound inferences remain locally sound when substituted with a uniform substitution σ with taboo set .

	1   …   n locally sound implies σ1   …   σnσ locally sound.





§ PROOF CALCULUS
 

Most notably, uniform substitution makes it possible to use concrete formulas as axioms instead of axiom schemata that accept infinitely many formulas as axioms.
Axioms are finite syntactic objects, and are thus easy to implement, while axiom schemata are ultimately algorithms accepting certain formulas as input while rejecting others <cit.>.
Figure <ref> lists the axioms of .
also satisfies the axioms of KAT <cit.>, Schematic KAT <cit.> and the axioms of app:axioms.
Some axioms use the reverse implication  instead of  for emphasis.


In the axiom (boxleq), x̅ stands for the (finite) vector of all relevant variables (alternative treatments <cit.> of p(x̅) use quantifier symbols or additional program constants instead, but are not necessary for this paper).
This characteristic axiom of expresses that if formula  holds after all runs of hybrid program , then it also holds after any refinement .
Thus, as long as a proof of the refinement is given, it is possible to replace hybrid programs inside modalities.
In general, axioms are meant to be applied to the axiom key (marked blue).

Refinement is transitive (leqtrans), allowing the introduction of intermediate refinements  similar to the role that cuts play in first-order logic.

Axiom (sequence) helps proving a refinement between two sequences of programs (;;) by proving the refinement of the first programs () and the refinement of the second programs, but only after all executions of  ().
Axioms (testdet) and (assigndet) are particular cases of the axiom (sequence) where the implication can be strengthened to an equivalence.
As such, the implication from right to left is not required for both axioms app:derived.



Axioms (loopl), (loopr) and (unloop) are used to prove refinements of loops. The first two state that if adding a program before or after only leads to less executions, then adding an unbounded number of executions, i.e. a loop, will also lead to less executions. The axiom (unloop) is useful for comparing two loops, as it allows to reduce the problem to comparing the loop bodies. Both axioms (loopl) and (unloop) need a box modality when proving the refinement of the loop body, as it must be proved after any number of iterations of a.

The axiom (ode) describes how to prove refinements between differential equations.
A refinement x=[x][x]x=[x][x] is sound if throughout the execution of the former ODE, it always satisfies the latter differential equation and domain.
Along with the axioms (DWref) and (DEref), these axioms subsume differential cut (DCax), differential weakening (diffweakenax) and differential effect (DEax) from app:axioms.
The equivalence in the axiom (ode) effectively means that refinements of differential equations can always be reduced to standard formulas, which is essential to our decidability result.

The axiom (DX) states that a differential equation always has a solution for the interval [0,0].
In that case, the execution succeeds only if the domain holds, and the correct value [x] is assigned to the differential variable x.

The axiom (ODEidemp) states that following the same differential equation twice in a row is equivalent to following it only once, because the concatenation of solutions of the same differential equation is still a solution of the same differential equation.


Compared to the original sequent calculus for <cit.>, the proof rule schemata matching infinitely many instances are now replaced by a finite number of axioms that are concrete formulas rather than standing for infinitely many instances.
The infinitely many possible instances can then be recovered soundly using the uniform substitution rule (US).
Because of this two-step mechanism, reasoning with the axioms can be done without considering the possible instantiations.
Take for instance the sound equivalence x;xx.
The proof can be done by transitivity (leqtrans) with x;x = ;x as intermediate step app:derived.
But the same proof cannot be done by replacing  by any term : the intermediate program is not always equivalent to the other two (e.g. for = x+1).
On the other hand, by proving the equivalence for  and then using rule (US), the equivalence can be proved for all terms .

The axioms are also more modular than its cast-in-stone sequent calculus rules.
For instance, with rule (Gax) and axiom (Kax), any implication , e.g. (choicer), can be used to prove .
This would not fit the shape of the corresponding sequent rule, which requires  at the top level.
The lack of differential symbols in the original sequent calculus <cit.> changes the soundness of some rules: the match direction field rule (MDF) would allow rescaling the right-hand side of a differential equation, which is unsound here as it would change the resulting differential symbols.
Conversely, only the reverse implication of the axiom (ode) would be sound in the original calculus, again for lack of differential symbols.
The axioms are proved sound app:proofaxioms and <ref>:


	All axioms of are sound.




§ DECIDABILITY OF REFINEMENT FOR A FRAGMENT OF 


This section identifies a subset of hybrid programs for which the refinement problem is decidable.
It is focused on concrete programs, i.e. programs without function symbols, predicate symbols or program constants.
They have the following high-level structure: (ctrl;plant) where a discrete, loop-free program ctrl, modelling a controller that sets some parameters u̅, then a continuous program plant that describes the dynamics of the variables y̅ according to the choice of the parameters u̅.
These steps are then repeated nondeterministically.
The continuous variables y̅ (and by extension y̅) are expected to be distinct from the discrete variables u̅ and also contain a global clock t which follows the differential equation t=1.
The presence of the clock t is not needed for comparing the differential equations, but to distinguish between discrete executions and hybrid executions.

For two such programs, (ctrl_a;plant_a) and (ctrl_b;plant_b), a canonical proof of the refinement has the following shape (omitting uses of MPax for brevity):

    [unloop][Gax][sequence]…ctrl_a  ctrl_b   …ctrl_a(plant_a  plant_b)ctrl_a;plant_a ctrl_b;plant_b(ctrl_a;plant_a)(ctrl_a;plant_a ctrl_b;plant_b)(ctrl_a;plant_a)(ctrl_b;plant_b)


This means that proving the refinement of the whole programs is reduced to proving the refinement of the controllers, ctrl_a  ctrl_b and the refinement of the plants after all ctrl_a executions, ctrl_a(plant_a  plant_b).
With our restrictions on the controllers, the first refinement is always decidable.

	For concrete, discrete and loop-free controllers ctrl_a and ctrl_b, the validity of ctrl_a  ctrl_b is decidable by proof.

Given a controller ctrl_a, it is possible to synthesize a first-order formula _a(x,x^+) that characterizes the behavior of ctrl_a, where x (resp. x^+) corresponds to the variables after (resp. before) the controller <cit.>.
Using the axioms, ctrl_a  ctrl_b is provable from _a(x,x^+) _b(x,x^+). 
The validity of the latter is decidable as it is first-order real arithmetic <cit.>.
The full proof is in app:sec6.

The second refinement, ctrl_a(plant_a  plant_b), is more complex.
Let us write the two plants as plant_a y̅=p(y̅,u̅)Q and plant_b y̅=q(y̅,u̅)R for some polynomials p(y̅,u̅), q(y̅,u̅) and formulas Q,R.
The axiom ode entails that we must prove ctrl_aplant_a(p(y̅,u̅) = q(y̅,u̅)  R), which no longer contains any refinement.
For the decidability result (thm:deciderefine) to hold, we require that the validity of this formula is decidable.

There are two cases which always ensure this.
First, if the differential equation plant_a admits a solution expressible in (e.g. a polynomial), then using standard reasoning, the formula can be reduced to a first-order formula and thus its validity can be decided.
The differential equation from ex:carbrake, x = v,v = a, is such a case.

The second case is when the domain R is algebraic, i.e. of the form _i_j p_ij(x) = 0 for some polynomial p_ij
and Q, the domain of plant_a, is an open set <cit.>.

The remaining question is now to show that the approach presented above is complete, meaning it always succeeds when the refinement holds.
The only additional constraint we require is that the controller ctrl_b is idempotent.

	A controller ctrl is idempotent if it satisfies ctrl;ctrl  ctrl.

An idempotent controller cannot reach more states by executing multiple times without any continuous dynamics happening.
Pure reactive controllers, i.e. controllers for which the parameters' values only depend on the values of the continuous variables, are always idempotent.
This is the case for the controllers in ex:carbrake: x-Bsafe_T(x);xA.
On the other hand, counting the number of times the controller has been executed would not be idempotent.


This derived rule is invertible, if ctrl_b is idempotent.

    ctrl_a;plant_a ctrl_b;plant_b(ctrl_a;plant_a)(ctrl_b;plant_b)


The derivation of the rule is given in the canonical proof.
The converse, that the conclusion implies the premise, is more involved app:sec6.
Showing ctrl_a;plant_a (ctrl_b;plant_b) from (ctrl_a;plant_a)(ctrl_b;plant_b) is done by unfolding the loop on the left.
To get rid of the loop on the right, we use the fact that ctrl_b is idempotent.
It means that if the global time is not modified, then we can assume without loss of generality that the controller (and thus also the plant) is executed only once.
The case when the global time is modified additionally considers the value of the derivative to ensure that there is an execution of the right program that does not require looping.

With the above lemma, we can now state the decidability result. 


	For concrete hybrid programs ctrl_a;plant_a and ctrl_b;plant_b discrete loop-free ctrl_a, ctrl_b and with plant_a y̅=p(y̅,u̅)Q and plant_b y̅=q(y̅,u̅)R, if ctrl_b is idempotent, and the validity of
	ctrl_aplant_a(p(y̅,u̅) = q(y̅,u̅)  R) is decidable,
	then the validity of ctrl_a;plant_actrl_b;plant_b is also decidable.


In particular, the theorem applies to the event-triggered model and the time-triggered model templates used to show how to prove that the latter refines the former <cit.>. Indeed, their controller template is loop-free and idempotent and the differential equation are assumed to be solvable. It strengthens their result by showing the completeness of the approach.



§ CONCLUSION

This paper introduced a uniform substitution proof calculus for differential refinement logic .
This yields a parsimonious prover microkernel for hybrid systems verification that simultaneously works for properties of and relations between hybrid systems.
The handling of refinement relations between hybrid systems is subtle even only in its static semantics, which makes the correctness proofs of this paper particularly interesting.
The uniform substitution is one-pass <cit.> giving it respectable performance advantages compared to Church-style uniform substitutions.
While the joint presence of differential equations reasoning and refinement reasoning causes challenges, a resulting benefit besides soundness is that a finer notion of differential equation refinement is obtained with logical decidability properties on a fragment of hybrid systems.

Future work involves improving the implementation of the uniform substitution calculus in .
Although the prover microkernel was straightforward following the uniform substitution process and list of 's uniform substitution axioms, the prover would benefit from some quality of life features, e.g. using the axioms to rewrite on subprograms.
The more advanced implementation is the refinement decision algorithm for the decidable fragment.
An other axis of research is to combine refinements with hybrid games, with a proper semantics and how to adapt the new axioms of to games, some of which would not be sound as is.


splncs04




§ ADDITIONAL AXIOMS





Axioms of also include the differential axioms, e.g. (x) = x <cit.>, to reason on terms, which are omitted as it is not the main focus of this paper.
Axioms preceded by a star can be derived from other axioms app:derived.



§ SYNTACTIC STATIC SEMANTICS

	The (syntactically) bound variables of a hybrid program  are defined as follows:
	
    = 
       = ∅
    x   = x
    x   = x
    x=   = x,x
       = ∪
    ;   = ∪
       =

	The definition of free variables for formulas requires the definition of must-bound variables for a hybrid program  which are written on all runs of :
	
    = ∅
       = ∅
    x   = x
    x   = x
    x=   = x,x
       = ∩
    ;   = ∪
       = ∅

	The (syntactically) free variables for terms are defined as follows where U{x x∈ U} are the differential variables corresponding to a set U of variables:
	
    x   = x
    [1,…,n]   = 1∪…∪n
     +    = ∪
    ·   = ∪
       = ∪

	The (syntactically) free variables for formulas are defined as follows:
	
    ≤   = ∪
    [1,…,n]   = 1∪…∪n
    ¬   = 
       = ∪
    x   = ∖x
       = ∪ (∖)
       = ∪∪((∪)∖(∩))

	The (syntactically) free variables for hybrid programs are defined as follows:
	
    = 
       = 
    x   = 
    x   = x
    x=   = x∪∪
       = ∪
    ;   = ∪ (∖)
       =




§ PROOFS FOR SEC:DRL AND SEC:USUBST


	We focus on the proof of ·⊇· for formulas and hybrid programs, because it is the only case affected by the addition of refinement operators compared to prior proofs <cit.>.
	We reason by induction on the structure of the formulas and hybrid programs.
	For hybrid programs, the property shown for  is stronger than the coincidence property, it shows that if [state] = [state] on V⊇ and [const] = [const] on , then [] implies [] for some [state] with [state] = [state] on V∪.

	We show the case for the refinement operator .
	Take [state],[state],[const],[const] such that [state] = [state] on V and [const] = [const] on .

	We prove that  implies .
	For [], by induction hypothesis, we have [] for some [state] with [state] = [state] on V∪.
	By definition of the refinement, [] follows from  and [].
	Similarly, we have [] for some state [state] with [state] = [state] on V∪. Thus, [state] = [state] on V∪(∩).
	Additionally, by lem:boundeffect, we also have [state] = [state] = [state] on . This means that in fact [state] = [state] and thus [].

	By a symmetric argument, we have  iff .
	This means that  satisfies the coincidence property for  and thus ⊇ by lem:coincidence.


	We prove the lemma by simultaneous induction on the structure of σ,  and  for all U,[state],[state] and [state].
	Take a U-variation [state] of [state].

	For formulas, we need to prove:
	
    for all U-variations [state] of [state]:Uσ iff

	
		
  * For ≤, we have Uσ(≤) iff Uσ≤Uσ, by lem:usubst-term iff ≤ iff ≤.

		
  *  For [], where  is not substituted by anything else, we have Uσ[] = [Uσ] iff Uσ∈, by lem:usubst-term iff ()∈ = iff [].

		
  * For [], we write d Uσ = by lem:usubst-term.
		We have Uσ[] = ∅Uσσ[], by IH iff [const]dσ[], by lem:coincidence iff
		[const]dσ[], by definition iff d=()∈ iff [].
		The IH for Uσ is used for a potentially bigger σ[] but simpler substitution that does not substitute a predicate so is covered by case:pred.
		lem:coincidence is applicable as [state] is a U-variation of [state] and σ[]∩ U = ∅, so [state] = [state] on σ[].
		
		
  * For ¬, we have Uσ¬ =¬Uσ iff Uσ, by IH iff  iff ¬.

		
  * For , we have Uσ = UσUσ = Uσ∩Uσ, by IH iff ∩ iff .

		
  * For x, we have Uσ(x) = xU∪xσ iff for all d, [state]xdU∪xσ, by IH iff for all d, [state]xd iff x.
		The IH is applicable as [state]xd is a (U∪x)-variation of [state].

		
  *  For , we have Uσ() = VUσVσ iff for all states [state], [VUσ] implies Vσ.
		Since [state] is a U-variation of [state], by IH, [VUσ] iff [].
		Take a state [state] with [VUσ].
		By lem:boundeffect, [state] is a -variation of [state], and thus a (U∪)-variation of [state].
		By lem:taboo, it means that [state] is a V-variation of [state] because VUσ is defined so V⊇ U∪.
		Thus, we can apply the induction hypothesis: Vσ iff .
		Finally, we can conclude VUσVσ iff .

		
  * For , we have by definition  that for all states [state], [] implies [].
		Since [state] is a U-variation of [state], by induction hypothesis for both  and , this is equivalent to having, for all states [state], [VUσ] implies [WUσ].
		This is, by definition, equivalent to VUσWUσ = Uσ().
	
	
	

	For programs, we need to prove:
	
    for all states [state] and all U-variations [state] of [state]:[VUσ] iff []

	 
		
		
  * For , we have [VUσ] = [σ] = [].
		
		
  * For , we have [UUσ] iff Uσ, by IH iff  iff [].

		
  * For x, we have [U∪xUσ(x)] = [xUσ] iff [state] = [state]xd with d = Uσ.
		By lem:usubst-term, this is equivalent to [state] = [state]xd with d =, i.e. [x].
		
		
  * For x, we have [U∪xUσx] = [x] iff [state] = [state]xd for some d iff [x].

		
  * For x=, we have [U∪x,xUσ(x=)] = [x=U∪x,xσU∪x,xσ] iff x = U∪x,xσU∪x,xσ and [t]x=U∪x,xσ for all t∈[0,r] for some function : [0, r ] → where (t)  is a x,x-variation of [state], (0) is a x-variation of [state], and (r) = [state].
		[state] is a (U∪x,x)-variation of [state], so by lem:usubst-term, U∪x,xσ= σω and by IH x = U∪x,xσU∪x,xσ is equivalent to σωx =.
		Thus, we have [U∪x,xUσ(x=)] iff [x=].

		
  * For , we have [V∪ WUσ()] = [VUσWUσ] iff [VUσ]∪[WUσ], by IH iff []∪[] iff [].

		
  *  For ;, we have [WUσ(;)] iff [VUσ]1 and [WVσ]1 for some [state]1.
		By IH, [VUσ]1 iff []1.
		Similarly to case:box, by Lemmas <ref> and <ref>, we have that [state]1 is a V-variation of [state], so by IH, [WVσ]1 iff [].
		Thus, [WUσ(;)] iff [;].
		
		
  * For , we have [VUσ()] = [(VVσ)] iff [(VVσ)^n] for some n.
		By IH, we have that [VVσ]1 iff []1 for all states [state]1.
		By repeated application of case:seq, we obtain by induction that [(VVσ)^n] iff [^n]. Thus [].
		The other direction is similar.
	




§ PROOF OF AXIOMS' SOUNDNESS


The soundness of axioms was done in <cit.>.
The proof of soundness of most axioms is similar to the corresponding ones in the original presentation of <cit.>.
In particular, all KAT axioms in fig:KATaxioms are instances of the KAT axioms from <cit.>, so their soundness follow from the original proof <cit.>.


	
  (leqtrans)
Take  and [].
As , we have [].
Then, as , we have [].
Thus, .


  (boxleq)
Take  and .
We need to show that .
Let us consider a state [state] such that [].
By refinement, it means that [].
Then, as , it implies .
Thus, we can conclude that .


  (test)
By definition, [] is equivalent to [state] = [state] and .
Thus,  holds iff
[] implies [], which by definition is equivalent to  implies  and so .



  (choicel)
Take  and [].
Then, by the semantics of the choice, [] and by refinement, [].
Similarly, if [], we have [].
Thus, .

On the other hand, take .
If [], then either [] or [].
In both cases, by refinement, we have [].
Thus .


  (choicer)
Take .
Then either  or .
If [], then depending on the case above, either [] or [].
In both cases, we have [].
Thus .


  (sequence)
Take  and .
If [;], then there exists  such that [] and [].
Additionally, by semantics of the box operator, .
Thus, by refinement, we have both [] and [].
We can conclude as [;].


  (loopl)
Let us assume that ;.
We show by induction on n that ^n;.

For n = 0, ^0 = by definition and ; by (seqidl).

If ^n;, we show that ^n+1; by (leqtrans), that is^n+1;^n;^n;.
The second part holds by induction hypothesis.
For the first part, by (sequence), we must show ^n ^n ^n;.
By semantics of the loop operator, []⊇[^n] for all n, so ^n holds.
Thus, we can conclude the proof by (leqrefl) for the left part, and by (boxleq) for the right part, as ;.


  (loopr)
Let us assume that ;.
We show by induction on n that ;^n.

For n = 0, ^0 = by definition and ; by (seqidr).

If ;^n, we show that ;^n+1 by (leqtrans), that is ;^n+1;^n ;^n.
The second part holds by induction hypothesis.
For the first part, by (sequence), we must show ;;^n ^n.
We can conclude the proof by assumption for the left part, and by (Gax) and (leqrefl) for the right part.


  (unloop)
Let us assume that .
We show by induction on n that ^n ^n.

For n = 0, ^0 =  = ^0 by definition, so it holds by (leqrefl).

If ^n ^n, then by (sequence), we must show ^n ^n ^n.
As in the proof of (loopl), we have ^n.
Thus, the first part holds by induction hypothesis, and the second part holds by (boxleq) and by assumption.


  (update)
The main insight is that as =  = [state]xr for any r, [state]xrx = iff r =.
As [x] iff [state] = [state]xr for r =, and [x;x = ] iff [state] = [state]xr for some r with x =, the two programs are equivalent.


  (testdet)
Take ;;.
For all [] and [], we need to show [].
As, [;], by refinement, we have [;], which means that there exists [state] such that [] and [].

By definition of [], we have [state] = [state] = [state], so [].
We can conclude that .

The other direction is derivable from (sequence) app:derived.


  (assigndet)
Take x;x;.
For all [x] and [], we need to show [].
As, [x;], by refinement, we have [x;], which means that there exists [state] such that [x] and [].

By definition of [x], we have [state] = [state]xr = [state] for r =, so [].
We can conclude that x.

The other direction is derivable from (sequence) app:derived.


  (stutter)
[xx] iff [state] = [state]xr for r = x.
It means that [state]It = [state].
So [xx] iff [state] = [state].

On the other hand, [] iff  which is always true.
So [] = ([state],[state]) = 
[xx], and the programs are thus equivalent.


  (randtestmerge)
For all states [state], [state], we have [x;[x];x] iff there exists r_1, r_2,[state] with [state] = [state]xr_1, and
, and [state] = [state]xr_2.

This also means that [state] = [state]xr_2 and [state] = [state]xr_1.
Thus it is equivalent to having some r_2 such that [state] = [state]xr_2 and some r_1 such that [state]xr_1, and so [x; y [y]].


  (randtestassignmerge)
For all states [state], [state], we have [x;[x];x[x]] iff there exists r_1, r_2,[state] with [state] = [state]xr_1, and
, and [state] = [state]xr_2 with r_2 = [x].

This also means that [state] = [state]xr_2 and [state] = [state]xr_1.
Thus it is equivalent to having some r_2 such that [state] = [state]xr_2 and some r_1 such that both [state]xr_1 and r_2 = [state]xr_1[x].
The latter can be rewritten as [state]xr_1r_2 = [x] so we can conclude that it is equivalent to [x; y ([y]  y = [y])].



  (DWref)
[x];x=[x][x];[x]x=[x][x] is a consequence of (seqidl), (seqidr), (test) and (sequence).

For the other direction, take [x=[x][x]]. Then there is : [0, r] → with (0) being a x-variation of [state] and [state] = (r) where (t) is a x,x-variation of [state], and satisfies x = [x] [x].
In particular, (0) and (r) = [x].
As (0) = [state] on [x] = x, then [x] by lem:coincidence.
Thus, both ([state],[state]) and [[x]].
This implies [[x];x=[x][x];[x]].
As it holds for all end states [state], we can conclude that x=[x][x][x];x=[x][x];[x].


  (DEref)
Similarly to above, [x=[x][x]] entails x = [x]. Thus [state]xr = [state] for r = [x].
So ([state], [state]xr) = [x=[x][x];x[x]] iff [x=[x][x]].
As it holds for all end states [state], we can conclude that x=[x][x]x=[x][x];x[x].


  (ode)
The forward implication is derivable from (DWref), (DEref), (boxleq).

For the converse implication, take [state] with x=[x][x](x=[x] [x]) and take [state] with [x=[x][x]].
Then there is : [0, r] → with (0) being a x-variation of [state] and [state] = (r) where (t) is a x,x-variation of [state], and satisfies x = [x] [x] and  [t]x= for all t∈[0,r].
This also means that [x=[x][x]] for all t∈[0,r].
By the semantics of the box operator, it implies x=[x] [x] for all t∈[0,r].
Thus [x=[x][x]].
As it holds for all end states [state], we can conclude that x=[x][x]x=[x][x].


  (DX)
Take [x[x];[x]]. We have that [state] = [state]xr and [x] for r = [x].
In particular, it also implies x = [x].
We define : 0→ with (0) = [state]. The function  satisfies that (0) is a x-variation of [state], [state] is a x,x-variation of [state] for t∈[0,0],
x = [x] [x]
for all t∈[0,0].
Thus, ([state],[state]) = [x=[x][x]][0].


  (ODEidemp)
x=[x][x]x=[x][x];x=[x][x] derives from (DX), (DWref) and (DEref).

For the other direction, take any states [state],[state],[state] with [x=[x][x]] and [x=[x][x]].
There is two functions _1 : [0,r_1] and _2 : [0,r_2] with [state] = _1(0) on x, and [state] = _1(r_1), and [state] = _2(0) on x, and [state] = _2(r_2).
Since both _1(r_1)∈x = [x] [x] and 
_2(0)∈x = [x] [x], this means that _1(r_1) = _2(0). By defining : [0, r_1+r_2] with (t) = _1(t) on [0,r_1] and (t) = _2(t-r_1) on [r_1,r_2], we have that ([state], (r_1+r_2)) = [x=[x][x]].



  (randcomm)
If [x;y], then there is [state], r_1, r_2 such that [state] = [state]xr_1 and [state] = [state]yr_2.
But then, with [state] = [state]yr_2, we have [state] = [state]xr_1, so [y;x].
As this holds for all [state], we can conclude that x;yy;x.
The equivalence holds by symmetry.



  (randtest)
Take [x;].
Then [x] and .
By definition, it means () ∈ where () is the 0-ary tuple so, =.
In particular, , which implies [;x].

The other direction is similar.




§ DERIVED AXIOMS



	
  (cupidemp)

    =       by (leqantisym)
        ()  ()    by (choicel)  and (choicer)
          by (leqrefl)



  (cupcomm)

    () ()    by (choicel)
        () ()    by FOL
          by (choicel)
          by (leqrefl)

The other case holds by symmetry.


  (cupassoc)
We write ().

    ()    ()    by (choicel)
        ()    by FOL
          by (choicel)
          by (leqrefl)



  (testand)

    ;   ;;   by  (seqidr)
          by  (sequence)
        ()    by  (test)
        ()  ()    by  (testbax)
          by FOL
    
    ;   ;;   by  (seqidl)
          by  (sequence)
        ()    by  (test)
        ()  ()    by  (testbax)
          by FOL


Then we can conclude by (leqantisym).


  (testor)

    ()  ()    by  (choicer)
        ()  ()    by  (test)
          by FOL
    
        ()  ()    by  (choicel)
        ()  ()    by  (test)
          by FOL

Then we can conclude by (leqantisym).


  (seqdistr) By (leqantisym), we prove both directions.

    ( ;)( ;) ( );    (; ( );)  (; ( );)    by  (choicel)
          by  (sequence)
          by  (leqrefl)
          by  (choicel)
          by  (leqrefl)



	();    ( ;)( ;)

	   (();;) (();;)    by  (choicer)

	   ( ) ( )    by  (sequence)

	   ( ) ( )    by  (leqrefl)

	        by  (choicel)

	      by  (leqrefl)




The reverse implication of (testdet) and (assigndet) is consequence of the general implication:

    ;;    ()    by  (sequence)
          by  (leqrefl)


As a consequence, we have the following derivation:

    [MPax];;   [Gax];;

and symmetrically we can derive:

    ;;


Associated with (leqtrans), this means we can use axioms to rewrite inside sequences. This will be done implicitly in the following derivations.



  (assignsub)

    x;y[]x;y[x]   xy[]y[x]   by  (assigndet)
       y[]y[]   by  (assignbax)
          by  (leqrefl)

The other direction is similar.

In fact, by using the same reasoning, we can show:

    [assigntestaux|:=_test_s]Substitution in test[eq]
    	  x;[]x;[x]



  (assigntest)

    x;[x]   x;[]   by  (assigntestaux)
       x;x = []   by  (testand)
       x;[] x =    by FOL
       x;[];x =    by  (testand)
       [];x;x =    by  (randtest)
       [];x   by  (update)



  (assignmerge)

    x;x[x]   x;x = ;x[x]   by  (update)
       x; y (y =  x = [y])   by  (randtestassignmerge)
       x;x = []   by FOL
       x[]   by  (update)



  (assignrandcomm)

    y;x   y;x;x =    by  (update)
       x;y;x =    by  (randcomm)
       x;x = ;y   by  (randtest)
       x;y   by  (update)



  (assigncomm)

    x;y[x]   x;y[]   by  (assignsub)
       x;x = ;y[]   by  (update)
       x;y[];x =    by  (assigntest)
       y[];x;x =    by  (assignrandcomm)
       y[];x   by  (update)


We also derive the example from sec:dRL-calculus: xf;x = x


    xf;x   x;x = f;x   by  (update)
       x;∃ y (y = f)   by  (randtestmerge)
       x;   by FOL
       x   by  (seqidr)


We can also obtain the following derivation:

    [MPax][Kax] ()   [Gax]

This derivation ensures that an implication, e.g. (testbax), can be used inside a box operator.


	
  (assignbeqax)

    ∀ x(x = f [x])    xx = f [x]   by  (randomb)
       xx = f[x]   by  (testbax)
       x;x = f[x]   by  (composebax)

Then we prove xf[x]x;x = f[x] by (boxleq) and (update).


  (iteratebax)

    ()    by FOL
          by  (testbax)
       ;   by  (composebax)
       ;   by  (choicebax)

Then we prove ; by (boxleq) and (unfold-l).


  (DEax)

    x=f(x)q(x)xx   x=f(x)q(x);xx   by  (composebax)

Then we prove x=f(x)q(x)x=f(x)q(x);xx by (boxleq) and (DEref).



  (diffweakenax)

    x=xq(x)(q(x) p(x))   x=xq(x)q(x)p(x)   by  (testbax)
       x=xq(x);q(x)p(x)   by  (composebax)

Then we prove x=xq(x)p(x)x=xq(x);q(x)p(x) by (boxleq).

Indeed, we can derive both refinements:

    x=xq(x);q(x)   x=x;q(x)   by  (test)
       x=xq(x)   by  (seqidr)

and

    x=xq(x)   q(x);x=xq(x);q(x)   by  (DWref)
       ;x=xq(x);q(x)   by  (test)
       x=xq(x);q(x)   by  (seqidl)



  (DCax)
We prove the implication by proving (x=xq(x))  (x=xq(x) r(x)) assuming x=xq(x)r(x).

	x=x   q(x) x=xq(x)r(x)

	   x=xq(x)(x=xq(x)r(x))    by  (ode)

	   x=xq(x)xx(x=xq(x)r(x))    by  (DEax)

	   x=xq(x)(x=xq(x)r(x))    by  (assignbax)

	   x=xq(x)(q(x)r(x))    by FOL

	   x=xq(x)(q(x)q(x)r(x))    by  (diffweakenax)

	   x=xq(x)r(x)    by FOL



	x=xq(x) r(x)    x=xq(x)

	   xxq(x)r(x)(x=xq(x))    by  (DX)

	   q(x)r(x)(x=xq(x))    by  (assignbax)

	   q(x)r(x) x=xq(x)    by  (testbax)

	      by FOL

We can then conclude by (boxleq).



§ PROOFS FOR SEC:DECIDABLE



	For any x ∉ctrl_a, we have ctrl_a xx;ctrl_a by (stutter).
	Thus, without loss of generality, we assume ctrl_a = ctrl_b.
	Then, for all variables x ∈ctrl_a = ctrl_b and fresh variables x^+, we have ctrl_a  ctrl_b iff x^+xctrl_a  ctrl_b by (assignbax), iff x^+x;ctrl_a x^+x;ctrl_b by (assigndet).
	In the following, we write x^+x for the sequence of assignments where x^+ corresponds to all fresh variables introduced and x corresponds to all bound variables.
	Axiom (sequence) will be used without explicit mention in the schematic form
	
    ;;


	We show that for any program  that is a sequence of tests and (possibly nondeterministic) assignments, (x^+x;)  (x^+x;x;(x^+,x)) for some first-order formula (x^+,x). 
	Using (seqassoc) if required, the left side of a sequence is assumed to always be an (possibly nondeterministic) assignment or a test.
	We prove by induction on the structure of  that for all x ∩⊆ y ⊆ x and first-order formula (x^+,y), the program x^+x;y;(x^+,y); is equivalent to one of the form x^+x;x;(x^+,x).
	
		
  * For (x), we have = ∅ so y = x.
		In that case, (x^+x;x;(x^+,x);(x^+,x))  (x^+x;x;(x^+,x) (x^+,x)) by (testand) and (sequence).
		
		
  * For zf(x) when z ∉ y, i.e. x = y ∪z, then 
		
			x^+x;y;   (x^+,y);zf(y,z) 

			   y^+y;y;z^+z;(x^+,y);zf(y,z)    (assignrandcomm)

			   y^+y;y;z^+z;zf(y,z);(x^+,y)    (assigntest)

			   y^+y;y;z^+z;zf(y,z^+);(x^+,y)    (assignsub)

			   x^+x;y;zf(y,z^+);(x^+,y)    (assignrandcomm)

			   x^+x;y;z;z = f(y,z^+);(x^+,y)     (update)

			   x^+x;x;z = f(y,z^+) (x^+,y)     (testand)
		
		
		
  * For zf(x) when y = y_2∪z, i.e. x = y, then
		
			x^+x   ;y;(x^+,y);zf(y) 

			   x^+x;y_2;z;(x^+,y_2,z);zf(y_2,z)     (randcomm)

			   x^+x;y_2;z;z_2(x^+,y_2,z_2) z = f(y_2,z_2)    (randtestassignmerge)
		

		
  * For z when z ∉ y, i.e. x = y∪z, then  we have by (randtest) 
    x^+x;y;(x^+,y);zx^+x;y;z;(x^+,y)

		
		
  * For z when y = y_2∪z, i.e. y = x, then 
		
			x^+x;y;(x^+,y)   ;z 

			   x^+x;y_2;z;(x^+,y);z    (randcomm)

			   x^+x;y_2;zz(x^+,y)     (randtestmerge)
		
		
		
  * For ;, using (seqassoc), x^+x;y;(x^+,y);; (x^+x;y;(x^+,y););. As we have that  is a test or an (possibly nondeterministic) assignment, we can apply a reasoning similar to the previous cases to . Then we can apply the induction hypothesis to .
	

	This result can be extended to programs with choice.
	By (seqdistl) and (seqdistr), we can rewrite x^+x; as ⋃_ix^+x;_i for some sequences of assignments and tests _i.
	By the proof above, this program is equivalent to ⋃_ix^+x;x;_i(x^+,x) for some formulas _i(x^+,x).
	By (seqdistl) and (testor), we finally obtain that
	x^+x;x^+x;x;⋁_i_i(x^+,x).


	As ctrl_a and ctrl_b are concrete, loop-free, discrete programs, they only contain (possibly nondeterministic) assignments, tests, sequences, and choices, so they correspond to the case above.
	Thus, we have that ctrl_a  ctrl_b iff x^+x;x;(x^+,x)x^+x;x;(x^+,x) for some formulas (x^+,x) and (x^+,x).
	By (sequence) and (Gax), proving (x^+,x) (x^+,x) entails x^+x;x;(x^+,x)x^+x;x;(x^+,x), but by looking at the semantics, we can see that the reasoning is complete.


The derivation of the rule is given in the canonical proof.
We focus on the converse and use  (resp. ) for ctrl_a;plant_a (resp. ctrl_b;plant_b). The proof is done in two steps.

First, we show that the following rule is derived.
 
    

This can be done by transitivity:

    ;   (seqidr)
       ;(;)    (leqrefl) and (choicer)
       ;   (unfold-l)
       ;   (leqrefl)  and  (choicer)
          (unfold-l)
          (hypothesis)

Then, we have to prove why the loop can be removed from .
For all [], [state] = (r) for some function , with a u̅-variation [state] such that we have [ctrl_a] and (0) a y̅-variation of [state].
This means that [] holds for all t∈[0,r] and (t) is a (y̅∪y̅)-variation of [state].
As , we have [] for all t∈[0,r].

Recall that the system has a global clock, which is written t_0 to prevent confusion.
As t_0 is only modified in the plant with the differential equation t_0 = 1, we have t_0 = t_0 and t_0 = t_0 + t.

As y̅ is unchanged in (0) and contains the strictly increasing time t_0, we know that the values of y̅ must remain constant throughout the execution of .
The only behavior for a differential equation with global time where the values of y̅ remain constant is the one described in the axiom (DX).
This can be rewritten as having ([state],(0))∈[(ctrl_b;y̅q(y̅,u̅);R)] where plant_b  (y̅=q(y̅,u̅)R) for some polynomial q.

This program refines by (ctrl_b;y̅q(y̅,u̅)), by (seqidr), (test) and (unloop).
By applying (unfold-r) before using the refinement above, i.e. removing the test R, we obtain ([state],(0))∈[(ctrl_b;y̅q(y̅,u̅));ctrl_b;y̅q(y̅,u̅);R].
Since ctrl_b is idempotent and does not depend on y̅, the first assignment to y̅ is irrelevant in ctrl_b;y̅q(y̅,u̅);ctrl_b;y̅q(y̅,u̅)
The program ctrl_b;y̅q(y̅,u̅);R is actually idempotent. 
This means that ctrl_b;y̅q(y̅,u̅) is also idempotent.
Thus, by using (loopl), we have that ((ctrl_b;y̅q(y̅,u̅));ctrl_b;y̅q(y̅,u̅))  (ctrl_b;y̅q(y̅,u̅)).
So ([state],(0))∈[ctrl_b;y̅q(y̅,u̅);R]⊆[].

Let us show that we can remove the left test.
As ctrl_a does not depend on y̅, take x∈y̅ and s ≠x we have ([state]xs, (0))∈[], so ([state]xs, (0))∈[] holds.
([state],(0))∈[] only holds if [state] = (0), meaning that as [state]≠[state]xs, we would have ([state]xs, (0))∈[].
The same reasoning as the one done for  can be done for , which entails ([state], (0))∈[].

For t > 0, the global time t_0 is modified so at least one iteration must have occurred: [;].
So for each t∈(0,r], there is [state] such that we have [;ctrl_b] and [y̅=q(y̅,u̅)R].
In particular, this entails y̅ = q(y̅,u̅) = q(y̅,u̅) for all t∈[0,r].
The same equality can also be said about the plant of :
y̅ = p(y̅,u̅) holds for all t∈[0,r] where plant_a  (y̅=p(y̅,u̅)Q).
As the two polynomials p(·, u̅) and q(·, u̅) are equal at infinitely many points, they must be equal everywhere, meaning plant_ap(y̅,u̅) = q(y̅,u̅) holds.
Checking that R follows from [] for t > 0, and for t = 0, it follows from ([state],(0))∈[].
In the end, we have plant_ap(y̅,u̅) = q(y̅,u̅)  R.
By the axiom (ode), we then have plant_a  plant_b, which implies [plant_b].
As ctrl_b does not affect differential variables and we have ([state],(0))∈[ctrl_b;plant_b], we have [ctrl_b] and we can conclude [].



Following lem:refineidemp, we are left to prove the decidability for one iteration of the loop: ctrl_a;y̅=p(y̅,u̅)Q ctrl_b;y̅=q(y̅,u̅)R.
In practice, we do not use axiom (sequence) immediately, as this would be incomplete if ctrl_a have an execution which violates the domain constraint Q and that ctrl_b does not have.

Using (DWref), we have (y̅=p(y̅,u̅)Q)  (Q;y̅=p(y̅,u̅)Q), and similarly for y̅=q(y̅,u̅)R.
By using (sequence), we are left with two formulas:

	
  * ctrl_a;Q ctrl_b;R
	
  * ctrl_a;Q(y̅=p(y̅,u̅)Qy̅=q(y̅,u̅)R)

By assumption and lem:decidiscret, both of them are decidable.

The use of the axiom (sequence) is complete for an argument similar to the one used in the proof of lem:refineidemp.
If ctrl_a;plant_a  ctrl_b;plant_b, and [ctrl_a], and [plant_a] and t_0 = t_0, then [ctrl_a;y̅p(y̅,u̅);Q] and [ctrl_b;y̅q(y̅,u̅);R].
As the continuous and discrete variables are distinct, this entails the first formula.
For the second one, we also need to consider the case where t_0 > t_0, in which case the proof of lem:refineidemp shows that [ctrl_b] and [plant_b].




