Averest


ModelCheckingSymbolic Module

This module implements functions symbolic model checking of mu-calculus and temporal logics. The model checking algorithms are mainly implemented by means of BDDs. There is also a function for symbolic computation of predecessor and successor states using quantifier elimination.

Types

Type Description

KripkeStructureBdd

This data type implements a representation of a Kripke structure by Bdds which is the basis for symbolic model checking with Bdds. It has the following components:

  • nowAtoms : the list of atoms for the current state
  • nxtAtoms : the corresponding list of atoms for the next state; i.e., where operator BoolNext was applied to the nowAtoms
  • nowAtomsIdxBdd = BoolExpr2Bdd MkListConj nowAtoms
  • nxtAtomsIdxBdd = BoolExpr2Bdd MkListConj nxtAtoms
  • initCondBDD : Bdd index of the initial condition
  • transRelBDD : Bdd index of the transition relation
  • fairCnstBDDs : list of Bdd indices of the fairness constraints
  • fairStatesBDD : Bdd index of the fair states (if already computed)
Note that nowAtomsIdxBdd and nxtAtomsIdxBdd are to be used for computing symbolic predecessor and successor state sets by Bdd function ExistAnd.

KripkeStructureSymbolic

This data type implements a symbolic description of a Kripke structure: States are identified with the set of variables that hold in that state, and in addition to the formulas that encode the initial states and transitions, there is also a set of fairness constraints (of type GF) to define fair computations (these are the only ones that are considered).

Functions and values

Function or value Description

ComputeFairInitialPath k

Full Usage: ComputeFairInitialPath k

Parameters:
Returns: BddAdr[] * BddAdr[]

This function computes a fair initial path of the associated Kripke structure of a generalized Buechi automaton. The computed path is represented by a pair (initPath, cyclePath) of paths where initPath is a path from an initial state s0 to some state sK, and cyclePath is then a path from sK to sK that traverses all fairness constraints.

k : KripkeStructureBdd
Returns: BddAdr[] * BddAdr[]

ComputePath withTrans k startStates endStates

Full Usage: ComputePath withTrans k startStates endStates

Parameters:
Returns: BddAdr[] option

Given a structure k represented by BDDs and sets of states startStates and endStates (all are BDDs), function ComputePath computes an array of non-empty state sets [|S0;...;Sn|] such that each state in S[i] has a transition to a state in S[i+1], S[n] is contained in endStates, and S[0] is contained in startStates. Each S[i] is a cube, i.e., some variables are given concrete truth values, while others are don't cares. Thus, one can use arbitrary truth values for the remaining truth values to complete a single path through the transition system. If argument withTrans is given, then the path consists of at least one transition (otherwise, we would just get a state if startStates and endstates would have a nonempty intersection).

withTrans : bool
k : KripkeStructureBdd
startStates : BddAdr
endStates : BddAdr
Returns: BddAdr[] option

InitializeBddPackageWithAssociatedKripke auto

Full Usage: InitializeBddPackageWithAssociatedKripke auto

Parameters:
Returns: KripkeStructureBdd

This function expects a given existential generalized Buechi automaton auto of the form ExistsAuto(qVars,initCond,transRel,fairConstr,acpt) as generated by function LTL2GeneralBuechi. The function computes the associated Kripke structure of that automaton and will represent that structure by Bdds. To this end, the function also initializes the Bdd package accordingly. The fair states are all states of the associated Kripke structure that have path where all fairness constraints hold infinitely often. Having computed the fair states, the function also computes the conjunction of the initial states with these states and also computes the conjunction of the fair states with the transition relation. The computation of the fair states is based on a fixpoint definition of the fair states condition (see also EmLe85, EmLe86a, EmLe86b, EmLe87, CGMZ95, SoRB02, SeTV05).

auto : SpecExpr
Returns: KripkeStructureBdd

LTL2LO1 phi

Full Usage: LTL2LO1 phi

Parameters:
Returns: BoolExpr

Convert a given LTL formula to an equivalent LO1 formula. Note that the generated formula is not type-consistent with the Quartz semantics, since we are using boolean arrays as monadic predicates. Note further that the three variables (t0,t1,t2) are sufficient, where the formula is applied at time t0 whereas t1 and t2 are auxiliary variables.

phi : SpecExpr
Returns: BoolExpr

PreE k phi

Full Usage: PreE k phi

Parameters:
Returns: int

Compute the existential predecessor states of the states represented by Bdd phi in the Kripke structure k as a Bdd.

k : KripkeStructureBdd
phi : BddAdr
Returns: int

ProveLTL dotExe showCounterexample psi

Full Usage: ProveLTL dotExe showCounterexample psi

Parameters:
    dotExe : string
    showCounterexample : bool
    psi : SpecExpr

Returns: bool

prove validity of LTL formulas via emptiness checking of equivalent B├╝chi automata dotexe should be the path to graphviz, showCounterexample a flag which decides to print counterexamples as svg graphics, and psi is the formula

dotExe : string
showCounterexample : bool
psi : SpecExpr
Returns: bool

SucE k phi

Full Usage: SucE k phi

Parameters:
Returns: BddAdr

Compute the existential successor states of the states represented by Bdd phi in the Kripke structure k as a Bdd.

k : KripkeStructureBdd
phi : BddAdr
Returns: BddAdr

SymbolicPreSuccessorTool qscoll

Full Usage: SymbolicPreSuccessorTool qscoll

Parameters:

This cgi-function is used to compute predecessor and successor states in a symbolic way by simply expanding the boolean quantifier into the disjunction/conjunction of the cofactors.

qscoll : NameValueCollection

Temp2LO1 (t0, t1, t2) phi

Full Usage: Temp2LO1 (t0, t1, t2) phi

Parameters:
Returns: BoolExpr
t0 : NatExpr
t1 : NatExpr
t2 : NatExpr
phi : SpecExpr
Returns: BoolExpr

Temp2LO1Interval (t0, b0, t1, b1) t2 phi

Full Usage: Temp2LO1Interval (t0, b0, t1, b1) t2 phi

Parameters:
Returns: BoolExpr
t0 : NatExpr
b0 : bool
t1 : NatExpr
b1 : bool
t2 : NatExpr
phi : SpecExpr
Returns: BoolExpr

TemporalLogicProverTool qscoll

Full Usage: TemporalLogicProverTool qscoll

Parameters:

This function is called by the cgi-interface for the TemporalLogicProver.

qscoll : NameValueCollection

Witness2DotFile (initPath, cyclePath) outStr

Full Usage: Witness2DotFile (initPath, cyclePath) outStr

Parameters:

Printing a fair path which is given as two BddAdr arrays which each element denotes a state which is given as a cube. For printing, we better adapt to the state transition conventions, i.e., not mentioned variables are false, and don't cares have to be fixed to any value (choose false).

initPath : BddAdr[]
cyclePath : BddAdr[]
outStr : TextWriter