computation-tree-logic v0.0.1

computation-tree-logic: CTL for JS

This library offers a way to verify CTL properties for given transition functions. The transition function and states are represented by binary decision diagrams. Fairness conditions can be imposed.

The satisfying states of the CTL property are computed via fixed-point computations.

The binary decision diagram is internally guaranteed to be reduced and ordered. The variable ordering is determined on instantiation.

Installation

yarn install computation-tree-logic

Example

const bdd = require('binary-decision-diagrams')
const ctl = require('computation-tree-logic')

const [a, _a] = ctl.variable()
const [b, _b] = ctl.variable()

const initial    = bdd.and(a,b)
const transition = bdd.orN([
  bdd.andN([a,          b,          _a,          bdd.not(_b)]),
  bdd.andN([a,          bdd.not(b), bdd.not(_a), bdd.not(_b)]),
  bdd.andN([bdd.not(a), bdd.not(b), _a,          _b]),
  bdd.andN([bdd.not(a), b,          _a,          _b]),
])

// Prints the reachable states from the initial state
console.warn(ctl.reachable(initial, transition))

Future plans

• Parse CTL property from string
• Witness and counterexample generation (Tree-like counterexample in model checking by Clarke et al)?
• Partial transitions?
• FORCE variable ordering?