Packages

o

edu.cmu.cs.ls.keymaerax.btactics

ODEInvariance

object ODEInvariance

Implements ODE tactics based on the differential equation axiomatization.

Created by yongkiat on 05/14/18.

See also

Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ODEInvariance
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class Conj(left: Instruction, right: Instruction) extends Instruction with Product with Serializable
  2. case class ConjFml(left: Inst, right: Inst) extends Inst with Product with Serializable
  3. case class Darboux(is_eq: Boolean, cofactor: Term, pr: ProvableSig) extends Instruction with Product with Serializable
  4. case class Disj(left: Instruction, right: Instruction) extends Instruction with Product with Serializable
  5. case class DisjFml(left: Inst, right: Inst) extends Inst with Product with Serializable
  6. case class EqFml(rank: Int, groebner: List[Term], cofactors: List[List[Term]]) extends Inst with Product with Serializable
  7. case class GeqFml(rank: Int, groebner: List[Term], cofactors: List[List[Term]]) extends Inst with Product with Serializable
  8. case class GtFml(rank: Int) extends Inst with Product with Serializable
  9. sealed trait Inst extends AnyRef
  10. sealed trait Instruction extends AnyRef
  11. case class Strict(bound: Int) extends Instruction with Product with Serializable
  12. case class Triv() extends Instruction with Product with Serializable

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def affine_norm_bound(n: Int): ProvableSig
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def cauchy_schwartz_bound(n: Int): ProvableSig

    Pre-prove the symbolic lemmas for n-dimensional Cauchy Schwartz Note: this lemma proves pretty quickly e.g.

    Pre-prove the symbolic lemmas for n-dimensional Cauchy Schwartz Note: this lemma proves pretty quickly e.g. for n=10

    n

    the dimension to use

    returns

    the symbolic bound (u.v)2 <= (||u||||v||)2

  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. lazy val dCClosure: DependentPositionTactic
  9. val dFP: DependentPositionTactic

    Implements differential fixed point

    Implements differential fixed point

    G, x=x0 |- [x'=f(x)& Q & x=x0]P G|-f(x)=0 --- (dFP) G |- [x'=f(x)&Q]P

  10. val dRI: DependentPositionTactic

    Implements (conjunctive) differential radical invariants

    Implements (conjunctive) differential radical invariants

    G,Q |- /\_i p_i*=0 --- (dRI) G |- [x'=f(x)&Q]/\_i p_i=0

    This proof rule is complete for open semialgebraic domain constraints Q This requires a top-level postcondition which rearranges to be a conjunction of equalities

    See also

    Khalil Ghorbal, Andrew Sogokon, and André Platzer. Invariance of conjunctions of polynomial equalities for algebraic differential equations.

  11. def dgVdbx(Gco: List[List[Term]], ps: List[Term], negate: Boolean = false): DependentPositionTactic
  12. val dgVdbxAuto: DependentPositionTactic
  13. def diffDivConquer(p: Term, cofactor: Option[Term] = None): DependentPositionTactic
  14. def domainStuck: DependentPositionTactic
    Annotations
    @Tactic( x$28 , x$29 , x$30 , x$25 , x$26 , x$31 , x$32 , x$27 , x$33 , x$34 , x$35 , x$36 )
  15. def dot_prod(v1: List[Term], v2: List[Term]): Term
  16. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  18. def fStar(ode: ODESystem, f: Formula): (Formula, Inst)

    Given a formula f in normal form (conjunction/disjunction of >=0, >0 or =0), generates the formula f* This is accompanied by an extra data structure that caches additional information at each step

    Given a formula f in normal form (conjunction/disjunction of >=0, >0 or =0), generates the formula f* This is accompanied by an extra data structure that caches additional information at each step

    ode

    : the ODE system

    f

    : the formula in semialgebraic normal form

    returns

    : (f*, i)

  19. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  20. def frobenius_subord_bound(n: Int): (ProvableSig, ProvableSig)

    Pre-prove the following double-sided bound: -(||G||2+1) ||p||2 <= 2*((Gp).p) <= (||G||2+1) ||p||2

    Pre-prove the following double-sided bound: -(||G||2+1) ||p||2 <= 2*((Gp).p) <= (||G||2+1) ||p||2

    The arithmetic is guided as follows: For each row (G_i.p)2 <= ||G_i||2 ||p||2 (Cauchy Schwartz) Which implies ||Gp||2 = sum_i (G_i.p)2 <= sum_i ||G_i||2 ||p||^2

    Then since ((Gp).p)2 <= ||Gp||2 ||p||2 (Cauchy Schwartz) This yields ((Gp).p)2 <= (sum_i ||G_i||2) ||p||2 ||p||^2

    Then use a usubst lemma to get: 2((Gp).p) <= (1+sum_i ||G_i||2) ||p||2 and also: 2((Gp).p) >= -(1+sum_i ||G_i||2) ||p||2

    n

    the dimension to use

    returns

    the symbolic bounds (||G||2 + 1) ||p||2 <= 2*((Gp).p) <= (||G||2 + 1) ||p||2

  21. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  22. def getDiffAdjInst(odels: List[AtomicODE]): ProvableSig

    Get the correct instantiation of diff adjoints from a list of atomic ODEs

    Get the correct instantiation of diff adjoints from a list of atomic ODEs

    odels

    the list of atomic ODEs

    returns

    the instantiated axiom

  23. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  24. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  25. def linFormODE(p: DifferentialProgram): Option[(List[List[Term]], List[Term], List[BaseVariable])]
  26. def localProgressFml(ode: ODESystem, f: Formula, bound: Option[Int] = None): Formula

    Computes the local progress formula f* f* is assumed to consist of atomic comparisons normalized to have 0 on RHS (<=0,>=0,<0,>0,=0,!=0), And, Or Sub-formulas outside this grammar are ignored if strict = false

    Computes the local progress formula f* f* is assumed to consist of atomic comparisons normalized to have 0 on RHS (<=0,>=0,<0,>0,=0,!=0), And, Or Sub-formulas outside this grammar are ignored if strict = false

    ode

    : the ODEs under consideration

    f

    : the formula f to compute f* for

    bound

    : optionally bounds the number of higher Lie derivatives that are considered

  27. def lpgen(inst: Inst): BelleExpr
  28. def lpstep: DependentPositionTactic
  29. def matvec_prod(m: List[List[Term]], v: List[Term]): List[Term]
  30. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  31. def nilpotentSolve(solveEnd: Boolean): DependentPositionTactic
  32. val nilpotentSolveTimeVar: Variable

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P with x'=f(x) a linear, nilpotent ODE

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P with x'=f(x) a linear, nilpotent ODE

    Adds the (polynomial) solution x=Phi(x_0,t) of that ODE to the domain constraint

    --- QE Q(Phi(x_0,t)), t>=0 |- P(Phi(x_0,t)) --- (only continues if solveEnd = true) G,x=x_0, t=0 |- [x'=f(x),t'=1& Q&t>=0& x=Phi(x_0,t)]P --------------- (nilpotent solve) G |- [x'=f(x)&Q]P

    returns

    See the rule rendition above Special failure cases: 1) Linearity heuristic checks fail e.g.: x'=1+x2-x2 will be treated as non-linear even though it is really linear

  33. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  34. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  35. def pStar(ode: ODESystem, p: Term, bound: Option[Int], geq: Boolean = true): Formula

    Given a bound i, generate the local progress formula up to that bound i.e.

    Given a bound i, generate the local progress formula up to that bound i.e. the i-th Lie derivative is strict: p>=0 & (p=0 -> (p'>=0 & (p'=0 -> ...) & (p=0&... -> p'^i >0) Computes up to the rank if bound = None

    ode

    : the ODEs under consideration

    p

    : the polynomial p to generate p*>0

    bound

    : number of higher Lie derivatives to generate

    geq

    : generate for >= (or <= if false)

    returns

    ( p*>0 )

  36. def pStarGeq(ode: ODESystem, p: Term): (Formula, (Int, List[Term], List[List[Term]]))

    Given a polynomial p, and an ODE system, generates the formula p*>0 along with additional information for p*=0 (as provided by rank(ode,p)) -- this avoids recomputation of the cofactors The rank r is reduced according to equalities already present in the domain constraint In other words, the generated p* satisfies: <x'=f(x)&Q>O & p*>=0 -> <x'=f(x)& p>=0 >O

    Given a polynomial p, and an ODE system, generates the formula p*>0 along with additional information for p*=0 (as provided by rank(ode,p)) -- this avoids recomputation of the cofactors The rank r is reduced according to equalities already present in the domain constraint In other words, the generated p* satisfies: <x'=f(x)&Q>O & p*>=0 -> <x'=f(x)& p>=0 >O

    ode

    : the ODE system

    p

    : the polynomial p

    returns

    : (p*>0, p*=0, rank)

  37. def pStarHom(ode: DifferentialProgram, p: Term, bound: Int): Formula

    Homomorphically extend pStar to max and min terms

    Homomorphically extend pStar to max and min terms

    ode

    : the ODEs under consideration

    p

    : the term p>=0 (including max/min terms)

    bound

    : number of higher Lie derivatives to generate

    returns

    p*>0

  38. def rank(ode: ODESystem, polys: List[Term]): (Int, List[Term], List[List[Term]])

    Explicitly calculate the conjunctive rank of a list of polynomials (uses conjunctive optimization from SAS'14)

    Explicitly calculate the conjunctive rank of a list of polynomials (uses conjunctive optimization from SAS'14)

    ode

    the ODESystem to use

    polys

    the polynomials to compute rank for

    returns

    the (conjunctive) rank, the Groebner basis closed under Lie derivation, and its cofactors (in that order)

  39. def rankOneFml(ode: DifferentialProgram, dom: Formula, f: Formula): Option[Formula]
  40. def rewriteODEAt(ode2: DifferentialProgram): DependentPositionTactic
  41. def sAI: DependentPositionTactic

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P

    G|-P Q,Q*,P |- P* Q,Q-*, !P |- (!P)-* --------------- (sAI) G |- [x'=f(x)&Q]P

    returns

    closes the subgoal if P is indeed invariant,

    See also

    Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.

  42. def sAIRankOne(doReorder: Boolean = true, skipClosed: Boolean = true): DependentPositionTactic

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a semialgebraic invariant, i.e.

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a semialgebraic invariant, i.e. G|- [x'=f(x)&Q]P P is assumed to be formed from conjunctions, disjunctions and inequalities This does not go via (closed) real induction, and so also applies for strict inequalities However, all of the sub formulas need to be "recursively" rank 1, i.e. they are provable either: 1) with darboux inequalities p'>=qp (for p>=0 , p>0) 2) with a barrier certificate

    This tactic reorders conjunctions internally to try and find an order that works

    doReorder

    whether to reorder conjunctions

    skipClosed

    whether to skip over closed invariants (this should be used if the outer tactic already tried sAIclosedPlus, which is much faster than this one anyway) The option only applies if doReorder = true

    See also

    Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.

  43. def sAIclosed: DependentPositionTactic

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e.

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e. G|- [x'=f(x)&Q]P

    G|-P Q,P |- P* --------------- (sAIc) G |- [x'=f(x)&Q]P

    P is assumed to be formed from conjunctions, disjunction, p<=q, p>=q, p=q which are collectively normalized to f>=0 (f possibly involving max,min and abs)

    TODO: Add Q* to the antecedents in the second premise

    returns

    closes the subgoal if P is indeed invariant, This should only fail if either: 1) P fails to normalize to f>=0 form (it isn't closed) 2) it is not invariant

    See also

    Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.

  44. def sAIclosedPlus(bound: Int = 1): DependentPositionTactic

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e.

    Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e. G|- [x'=f(x)&Q]P P is assumed to be formed from conjunctions, disjunction, p<=q, p>=q, p=q which are collectively normalized to f>=0 (f possibly involving max,min and abs)

    Current tactic limitations: 1) Assumes that P is already in the antecedents, otherwise leaves that subgoal open 2) It does not characterize local progress for domain constraint Q 3) For polynomials p>=0 in the normalized form that are NOT rank 1, this tactic currently requires checks the progress formula (p*>0) up to a given bound, rather than p*>=0

    bound

    (default 1): the bound on higher Lie derivatives to check for strict inequality, i.e. for p>=0, this is generated p>=0 & (p=0 -> (p'>=0 & (p'=0 -> ...p'^bound > 0 ...)) (i.e. the bound-th Lie derivative is required to be strict)

    returns

    closes the subgoal if P is indeed invariant, fails if P fails to normalize to f>=0 form, or if one of tactic limitations is met

    See also

    Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.

  45. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  46. def timeBound: DependentPositionTactic

    Given a top-level succedent of the form [{t'=c,x'=f(x)& Q & t=d}]P proves P invariant because the domain constraint prevents progress This tactic is relatively flexible: t'=c can be any time-like ODE (except c cannot be 0) t=d requires d to be a constant number, which forces the whole ODE to be frozen (of course, P should be true initially)

  47. def toString(): String
    Definition Classes
    AnyRef → Any
  48. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  49. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  50. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped