Computation tree logic library for JS
npm install computation-tree-logicThis 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.
Binary decision diagrams (BDD)
In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. Unlike other compressed representations, operations are performed directly on the compressed representation, i.e. without decompression. Other data structures used to represent Boolean functions include negation normal form (NNF), Zhegalkin polynomials, and propositional directed acyclic graphs (PDAG).
~ Wikipedia, 09/10/2020
Computation tree logic (CTL)
Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied (e.g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e.g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic is in a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL.
~ Wikipedia, 09/10/2020
Fair computation tree logic
Fair computational tree logic is conventional computational tree logic studied with explicit fairness constraints.
~ Wikipedia, 09/10/2020
yarn install computation-tree-logic
Example
javascript
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))
``