# 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

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

• 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

• 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$ 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

## 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

• $IDP^3$ easily extensible with new inference methods