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.
Type | Description |
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:
|
|
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). |
Function or value | Description |
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. |
|
Full Usage:
ComputePath withTrans k startStates endStates
Parameters:
bool
k : KripkeStructureBdd
startStates : BddAdr
endStates : BddAdr
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).
|
Full Usage:
InitializeBddPackageWithAssociatedKripke auto
Parameters:
AutomatonSymb
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).
|
|
Compute the existential predecessor states of the states represented by Bdd phi in the Kripke structure k as a Bdd.
|
|
Compute the existential successor states of the states represented by Bdd phi in the Kripke structure k as a Bdd.
|
Full Usage:
Witness2DotFile (initPath, cyclePath) outStr
Parameters:
BddAdr[]
cyclePath : BddAdr[]
outStr : TextWriter
|
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).
|