# computation-tree-logic
> Computation tree logic library for JS
Latest version **0.0.1** (published 2020-10-12) · MIT license · 0 weekly downloads
## Install
```sh
npm install computation-tree-logic
pnpm add computation-tree-logic
yarn add computation-tree-logic
bun add computation-tree-logic
```
## Health
**Score 20/100 (F)** — status: abandoned.
Positive: esm support; no vulnerabilities.
Warnings: low downloads; no types; pre 1.0.
Negative: abandoned; low maintenance score.
## Facts
| | |
|---|---|
| Version | 0.0.1 |
| Published | 2020-10-12 |
| First published | 2020-10-12 |
| Weekly downloads | 0 |
| License | MIT |
| TypeScript types | none |
| Module format | ESM |
| Dependencies | 0 |
| Unpacked size | 27.1 KB |
| Known vulnerabilities | 0 |
| Install scripts | no |
| GitHub stars | 0 |
| Author | Ties Westendorp |
| Maintainers | knaapje |
## Links
- npm: https://www.npmjs.com/package/computation-tree-logic
- Repository: https://github.com/TiesWestendorp/CTL
- Homepage: https://github.com/TiesWestendorp/CTL#readme
- Issues: https://github.com/TiesWestendorp/CTL/issues
- npm.io page: https://npm.io/package/computation-tree-logic
## Recent versions
- 0.0.1 (latest) — 2020-10-12
- 1.0.0 — 2020-10-12
## README
# 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.
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
## Installation
```
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))
```
## 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?
---
_Source: https://npm.io/package/computation-tree-logic · Machine-readable twin of the npm.io package page. Health data is recomputed on every publish._