object SwitchedSystems
Provides support for generating switched system models under various switching mechanisms.
Also provides proof automation for stability proofs
- Alphabetic
- By Inheritance
- SwitchedSystems
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
Controlled(initopt: Option[Program], modes: List[(String, ODESystem, List[(String, Program)])], u: Variable) extends SwitchedSystem with Product with Serializable
Controlled switching models
Controlled switching models
- initopt
optional initialization program
- modes
list of modes, each mode consisting of: name: String (representing constant function name()) ode: ODESystem (continuous dynamics) transitions : List[(String,Program)] (transitions p->q where program a is executed along the transition, e.g., a guard and/or reset map)
- u
the mode control variable u
- case class Guarded(modes: List[(String, ODESystem, List[(String, Formula)])], u: Variable) extends SwitchedSystem with Product with Serializable
-
case class
StateDependent(odes: List[ODESystem]) extends SwitchedSystem with Product with Serializable
State dependent switching Switching between a list of ODEs (with domains)
- sealed trait SwitchedSystem extends AnyRef
- case class Timed(modes: List[(String, DifferentialProgram, Option[Term], List[(String, Option[Term])])], u: Variable, timer: Variable) extends SwitchedSystem with Product with Serializable
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
- def attractivitySpec(ss: SwitchedSystem): Formula
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
- def controlledFromProgram(p: Program, topt: Option[Variable]): Controlled
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def guardedFromProgram(p: Program, topt: Option[Variable]): Guarded
-
def
guardedTransitionMap(ss: SwitchedSystem): List[(Int, Int, Formula)]
Extract an underlying indexed transition map suitable for MLF generation
Extract an underlying indexed transition map suitable for MLF generation
- ss
the switched system under consideration
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
odeActive(sys: ODESystem, dom: Formula): Option[(String, Map[NamedSymbol, Expression])]
Check that ODE's domain includes points that are about to locally exit or enter it under the dynamics of the ODE
Check that ODE's domain includes points that are about to locally exit or enter it under the dynamics of the ODE
- sys
the ODE under consideration
- dom
the "global" domain of points to be considered
- Note
for closed domains, this is automatically true
,returns an option with string and counterexample if it manages to find one
- def proveAttractivityCLF(V: Term): DependentPositionTactic
-
def
proveAttractivityCLF(V: Option[Term]): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( x$13 , x$14 , x$15 , x$16 , x$17 , x$19 , x$20 , x$18 , x$21 , x$22 , x$23 , x$24 )
-
def
proveAttractivityStateMLF(Vp: List[Term]): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( x$37 , x$38 , x$39 , x$40 , x$41 , x$43 , x$44 , x$42 , x$45 , x$46 , x$47 , x$48 )
-
def
proveAttractivityTimeMLF(Vp: List[Term], Lp: List[Formula], rate: Term): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( "attractivityTimeMLF" , "attractivityTimeMLF" , ... , "Γ |- Vp' <= Lp*Vp, rate > 0" , ... , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
- def proveStabilityCLF(V: Term): DependentPositionTactic
-
def
proveStabilityCLF(V: Option[Term]): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( x$1 , x$2 , x$3 , x$4 , x$5 , x$7 , x$8 , x$6 , x$9 , x$10 , x$11 , x$12 )
-
def
proveStabilityStateMLF(Vp: List[Term]): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( x$25 , x$26 , x$27 , x$28 , x$29 , x$31 , x$32 , x$30 , x$33 , x$34 , x$35 , x$36 )
-
def
proveStabilityTimeMLF(Vp: List[Term], Lp: List[Formula]): DependentPositionWithAppliedInputTactic
MLF tactic for time-dependent
MLF tactic for time-dependent
- Vp
list of Lyapunov functions V_p
- Lp
list of lambdas such that V_p' <= -lambda V_p note: lambdas is provided as a list of Formulas expected to have shape lambda_p <= 0 or lambda_p > 0 This is to support parametric lambda (where the sign is not necessarily known)
- returns
Tactic proving stability for the Timed switched system at a given position
- Annotations
- @Tactic( "stabilityTimeMLF" , "stabilityTimeMLF" , ... , "Γ |- Vp' <= Lp*Vp" , ... , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
-
def
proveStable(lyap: Term, prog: Program, varsopt: Option[List[Variable]] = None, restr: Option[Formula] = None): DependentPositionTactic
Prove stability specification at the given top-level position using the given Lyapunov function V V must satisfy the "basic" properties: V(0) = 0, V > 0 away from the origin
Prove stability specification at the given top-level position using the given Lyapunov function V V must satisfy the "basic" properties: V(0) = 0, V > 0 away from the origin
Additionally, V must be a "throughout" invariant of the hybrid program
- lyap
the (common) Lyapunov function
- prog
?
- varsopt
?
- restr
?
- returns
stability tactic
-
def
slowSwitch(odes: List[ODESystem], dwell: Term, s: Variable = "s_".asVariable, u: Variable = "u_".asVariable, topt: Option[BaseVariable] = None): Program
Standard slow switching model Each ODE is indexed 0,...,n-1
Standard slow switching model Each ODE is indexed 0,...,n-1
- odes
ODEs in the family
- dwell
the (global) minimum dwell time
- returns
a hybrid program modeling slow switching between the ODEs
- def stabilitySpec(ss: SwitchedSystem): Formula
-
def
stableOrigin(prog: Program, varsopt: Option[List[(Variable, Term)]] = None, restr: Option[Formula] = None): Formula
Stability of the origin for a given hybrid program \forall eps > 0 \exists del > 0 \forall x ( ||x|| < del -> [ a ] ||x|| < eps )
Stability of the origin for a given hybrid program \forall eps > 0 \exists del > 0 \forall x ( ||x|| < del -> [ a ] ||x|| < eps )
- prog
the hybrid program a to specify stability
- varsopt
Optional list of variables to quantify and perturb. By default None will pick non-differential freeVars(a) \cap boundVars(a)
- restr
an optional additional restriction on the initial perturbation With the additional options, we can write down slightly more nuanced specifications \forall eps > 0 \exists del > 0 \forall x ( ||x|| < del -> [ a ] ||x|| < eps )
- def stateDependentFromProgram(p: Program, topt: Option[Variable]): StateDependent
-
def
stateSwitchActive(odes: List[ODESystem], dom: Formula = True): Option[(String, Map[NamedSymbol, Expression])]
Check that all states can locally evolve under at least one ODE
Check that all states can locally evolve under at least one ODE
- odes
ODEs in the family
- dom
the expected domain of the overall system (defaults: the entire state space)
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
timeSwitch(odes: List[(ODESystem, Option[Term])], transitions: List[List[(Int, Term)]], s: Variable = "s_".asVariable, u: Variable = "u_".asVariable, topt: Option[BaseVariable] = None): Program
General time dependent switching model Each ODE is indexed 0,...,n-1 Each index i can be associated with an (optional) positive time bound t <= T_i for the maximum dwell time Each pair (i,j) can be associated with a positive time tau_{ij} <= t for minimum dwell time before transition
General time dependent switching model Each ODE is indexed 0,...,n-1 Each index i can be associated with an (optional) positive time bound t <= T_i for the maximum dwell time Each pair (i,j) can be associated with a positive time tau_{ij} <= t for minimum dwell time before transition
- odes
ODEs in the family with their time bounds
- transitions
for each ODE i, an associated list of pairs (j,tau_{ij})
- returns
a hybrid program modeling time-dependent switching between the ODEs
- def timedFromProgram(p: Program, topt: Option[Variable]): Timed
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core
- KeYmaera X kernel, proof certificates, main data structuresExpression
- Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (one-pass) uniform substitutions and renaming.StaticSemantics
- Static semantics with free and bound variable analysisKeYmaeraXParser
.edu.cmu.cs.ls.keymaerax.parser
- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter
- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser
- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser
- Parser reading KeYmaera X model and proof archive.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.cmu.cs.ls.keymaerax.infrastruct
- Prover infrastructure outside the kernelUnificationMatch
- Unification algorithmRenUSubst
- Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context
- Representation for contexts of formulas in which they occur.Augmentors
- Augmenting formula and expression data structures with additional functionalityExpressionTraversal
- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon
- Bellerophon tactic language and tactic interpreterBelleExpr
- Tactic language expressionsSequentialInterpreter
- Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics
- Bellerophon tactic library for conducting proofs.TactixLibrary
- Main KeYmaera X tactic library including many proof tactics.HilbertCalculus
- Hilbert Calculus for differential dynamic logicSequentCalculus
- Sequent Calculus for propositional and first-order logicHybridProgramCalculus
- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
- Unification-based uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]
- Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma
- Lemma mechanismLemma
- Lemmas are Provables stored under a name, e.g., in files.LemmaDB
- Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe
- Real arithmetic back-end solversMathematicaQETool
- Mathematica interface for real arithmetic.Z3QETool
- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
- Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica
- Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3
- Z3 interface for real arithmetic including simplifiers.Entry Points
Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX
- Command-line launcher for KeYmaera X supports command-line argument-help
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.AxIndex
- Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex
- Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax
- Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos