Nasal Pathway Melodrama

    computation-tree-logic

    0.0.1 • Public • Published

    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

    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?

    Keywords

    none

    Install

    npm i computation-tree-logic

    DownloadsWeekly Downloads

    1

    Version

    0.0.1

    License

    MIT

    Unpacked Size

    27.7 kB

    Total Files

    24

    Last publish

    Collaborators

    • knaapje