Simulating Dynamic Systems Using Linear Time Calculus Theories

B. Bogaerts, J. Jansen, M. Bruynooghe, B. De Cat, J. Vennekens, M. Denecker

KU Leuven

Overview

  • Motivation & context
  • Linear time
  • Progression & the Markov property
  • Inference with LTC theories
  • Demo
  • Related Work

KBS Paradigm

Multiple forms of inference on the same KB
  • Reuse of knowledge
  • Separating knowledge from computation

KBS Paradigm

  • Theorem provers: deduction
  • Sat solvers, ASP solvers, CP solvers: model expansion
  • Database systems: querying
  • Prolog systems: definition evaluation
  • ...
KBS paradigm: represent knowledge once, apply multiple forms of inference

KBS Paradigm: Dynamic systems

  • Planning
  • Model checking
  • Execution/simulation
  • ...
  • Is the KBS paradigm applicable here?
    • Can we define several useful inference methods on the same specification?
    • Can we extend IDP (a KBS for the logic FO(ID)) with specific inference methods for a dynamic context

FO(ID)

Typed first-order logic
(Inductive) Definitions

Pacman

\[ \begin{array}{l} \left\{ \begin{array}{l} \forall a, p: Pos(a,0) = p\leftarrow StartPos(a)=p.\\ \forall a, t, p: Pos(a,t+1)=p \\\quad\leftarrow Pos(a,t)=p\land \lnot \exists d: Move(a,d,t).\\ \forall a, t, p: Pos(a,t+1)=p\\\quad\leftarrow \exists d: Move(a,d,t)\land Next(Pos(a,t),d,p).\\ \forall s: Pell(s,0).\\ \forall s, t: Pell(s,t+1)\leftarrow Pell(s,t) \land Pos(pacman,t)\neq s.\\ \end{array}\right\}\\ \forall a, t, d, d': Move(a,d,t) \land Move(a,d',t)\Rightarrow d=d'.\\ \dots \end{array} \]

Linear Time Vocabulary

  • typed FO vocabulary
  • with (linear) Time: type interpreted by $\mathbb{N}$
  • predicates and functions: at most one argument typed Time; for functions: not their output-type

LINEAR TIME VOCABULARY

  • Types: $\definecolor{myorange}{RGB}{255,153,0} \textcolor{myorange}{Time}, Agent, Square, Dir$
  • Static symbols:
    • $Pacman:Agent$
    • $Next(Square, Dir, Square)$
    • $StartPos(Agent):Square$
  • Dynamic symbols:
    • $Move(Agent, Dir, \textcolor{myorange}{Time})$
    • $Pell(Square, \textcolor{myorange}{Time})$
    • $GameOver(\textcolor{myorange}{Time})$
    • $Pos(Agent,\textcolor{myorange}{Time}):Square$

Derived Single-State Vocabulary

  • Types: $\definecolor{myorange}{RGB}{255,153,0} Agent, Square, Dir$
  • Static symbols:
    • $Pacman:Agent$
    • $Next(Square, Dir, Square)$
    • $StartPos(Agent):Square$
  • Projected dynamic symbols:
    • $Move_\textcolor{myorange}{curr}(Agent, Dir)$
    • $Pell_\textcolor{myorange}{curr}(Square)$
    • $GameOver_\textcolor{myorange}{curr}()$
    • $Pos_\textcolor{myorange}{curr}(Agent):Square$

Linear Time Structure

  • $\Sigma$-structure $J$: infinite run of a dynamic system
  • $\Sigma_{ss}$-structure: snapshot (single state)

Proposition 
$\Sigma$-structures $\cong$ sequences $(J_k)_{k=0}^\infty$ of $\Sigma_{ss}$-structures

(Weak) Markov Property

(Weak) Progression

(WEAK) PROGRESSION

  • Input
    • Theory $T$ over $\Sigma$ (Markov)
    • Structure $S$ over $\Sigma_{ss}$
  • Output
    • $T$-succesors of $S$

LTC Theories

  • Syntactical criterion
  • Satisfy the Markov property...
  • ... and the weak Markov property

Pacman

\[ \begin{array}{l} \left\{ \begin{array}{l} \forall a, p: Pos(a,0) = p\leftarrow StartPos(a)=p.\\ \forall a, t, p: Pos(a,t+1)=p \\\quad\leftarrow Pos(a,t)=p\land \lnot \exists d: Move(a,d,t).\\ \forall a, t, p: Pos(a,t+1)=p\\\quad\leftarrow \exists d: Move(a,d,t)\land Next(Pos(a,t),d,p).\\ \forall s: Pell(s,0).\\ \forall s, t: Pell(s,t+1)\leftarrow Pell(s,t) \land Pos(pacman,t)\neq s.\\ \end{array}\right\}\\ \forall a, t, d, d': Move(a,d,t) \land Move(a,d',t)\Rightarrow d=d'.\\ \dots \end{array} \]

LTC Theories

Derived theories $T_0$ and $T_t$


KBS Paradigm

Multiple forms of inference on the same KB
  • Reuse of knowledge
  • Separating knowledge from computation

Planning


Progression


Interactive Simulation (Execution)

Interactive Simulation (Execution)

Interactive Simulation (Execution)

Interactive Simulation (Execution)

Interactive Simulation (Execution)

Interactive Simulation (Execution)

Interactive Simulation (Execution)

Interactive Simulation (Execution)

Interactive Simulation (Execution)

Proving Invariants

  • Symbolic
  • Concrete


PROVING INVARIANTS

Induction, reusing $T_0$ and $T_t$


Model Checking

Model Checking

Implementation

Implemented in $\mathrm{IDP}^3$
All above inference methods except model checking

Demo

Related Work

\[\definecolor{myorange}{RGB}{255,153,0} \newcommand{\YES}{\color{myorange}{\bf\small \times}} \tiny \begin{array}{l|cccccccc} & IDP & Planners & Clingo &oClingo & NuSMV & LPS & ProB \\ \hline \text{Progression} & \YES & - & - &\YES & \YES & \YES & \YES \\ \text{Execution} & \YES & - & - &\YES & \YES & \YES & \YES \\ \text{Planning } & \YES & \YES & \YES & - & \YES & \YES & \YES \\ \text{Optimal Plan. } & \YES & \YES & \YES & - & - & - & \YES \\ \text{Prove Invar.} & \YES & - & - & - & - & - & - \\ \text{Model Checking} & - & - & - & - & \YES & - & \YES \end{array}\]

Conclusion

  • KBS paradigm works
    • Tested in the context of dynamic specifications
    • Identified many inference tasks
  • $IDP^3$ easily extensible with new inference methods

Thank you!

Questions?