This module implements functions for global and local model checking of mu-calculus and CTL formulas of explicitly defined Kripke structures. It also provides functions for some Kripke structure examples like the NIM game.
Type | Description |
Function or value | Description |
Full Usage:
ComputePreStructure phi
Parameters:
SpecExpr
Returns: Map<int, cubeOfAtoms> * Set<int> * Set<int * int>
|
compute a transition system whose states and transitions contains all models of a given formula if that formula is satisfiable at all
|
Full Usage:
ComputeStates ostr prefix k phi
Parameters:
'a option
prefix : string
k : KripkeStructureExpl
phi : SpecExpr
Returns: Set<int>
|
This function implements a model checker for CTL and mu-calculus using an explicit representation of the Kripke structure as given in this module.
|
|
|
|
|
|
|
Full Usage:
FindInfinitePath k startSet
Parameters:
KripkeStructureExpl
startSet : Set<int>
Returns: int list
|
Find an infinite path through the Kripke structure k. The function can also be used to compute a witness for EG phi when k is restricted first to phi-states before calling the function.
|
Full Usage:
FindPath k startSet targetSet
Parameters:
KripkeStructureExpl
startSet : Set<int>
targetSet : Set<int>
Returns: int list
|
Find a path from startSet to targetSet (assuming that such a path exists). The function is used to compute witnesses or counterexamples.
|
|
|
|
Converting a given mu-calculus formula into guarded form so that local model checking will not run into infinite loops.
|
Full Usage:
LocalModelCheckTree2Dot ostr statePrefix pt
Parameters:
TextWriter
statePrefix : string
pt : Map<int, (int * int * SpecExpr * bool * int list)>
|
|
Full Usage:
LocalModelChecking allSubgoals k state phi
Parameters:
bool
k : KripkeStructureExpl
state : int
phi : SpecExpr
Returns: bool * int * Map<int, (int * int * SpecExpr * bool * int list)>
|
This function implements a local model checking procedure for CTL and mu-calculus using an explicit representation of the Kripke structure as given in this module. Given state s of a Kripke structure k, and formula phi, the function computes a triple (res,initNode,proofTree) where the boolean value res holds iff phi holds in s, initNode is the index of the root node (labelled with (s,phi)), and proofTree is a map where integers (used as identifiers for nodes of the proof tree) are mapped to tuples (kd,s,phi,res,sucL) with the following meaning: kd>0 for nodes with a conjunctive branching or proven leaf nodes, kd<0 for nodes with a disjunctive branching or disproven leaf nodes, and kd=0 when there is a unique successor node. (s,phi) are the state and the formula proven or disproven by the proof tree starting in this node, and res is the boolean value that tells us whether it is proven (res=true) or disproven (res=false). Finally, sucL is the list of successor nodes of this node.
|
compute a tree automaton for a given CTL* or mu-calculus formula: for a given CTL* formula, it computes (doneAbbrv,abbrvMap,phiTop) where doneAbbrv is a list of abbreviations x[i]=phi[i] where x[i] is a new (state) variable and phi[i] a modal logic formula over the state and input variables; abbrvMap is a map that maps x[i] to a CTL* formula which is abbreviated by it; and phiTop is a modal logic formula whose satisfying assignments are the initial states
|
|
|
This function is meant to be called from cgi; it expects a Kripke structure as value of name "KripkeStructureExpl" and a μ-calculus formula given as value of name "Property" in the qscoll argument. The values are parsed, and then the set of states where the μ-calculus formula holds are compute step by step.
|
|
The following function generates a Kripke structure for the mystic square puzzle, i.e., a NxN matrix with numbers 0,...,NxN-1, where the number 0 is considered to be a hole where its neighbors can be moved in. The task is to sort the matrix by such moves.
|
|
The following function generates a Kripke structure for the NIM game, i.e., an array of size N, which is used by two players. Each player can remove any number of tokens of an array element i.e., can reduce the number as much as (s)he likes. The player who has to take the last element loses the game.
|
Full Usage:
PreStructure2Dot ostr onlyProp statePrefix (indexMap, initialStates, transRel)
Parameters:
TextWriter
onlyProp : bool
statePrefix : string
indexMap : Map<int, cubeOfAtoms>
initialStates : Set<int>
transRel : seq<int * int>
|
|
Full Usage:
PreStructure2DotNew ostr statePrefix (indexMap, initialStates, transRel)
Parameters:
TextWriter
statePrefix : string
indexMap : Map<int, Set<SpecExpr>>
initialStates : Set<int>
transRel : seq<int * int>
|
|
Full Usage:
PreStructure2File filename onlyProp (indexMap, initialStates, transRel)
Parameters:
string
onlyProp : bool
indexMap : Map<int, cubeOfAtoms>
initialStates : Set<int>
transRel : seq<int * int>
|
|
Full Usage:
PreStructure2KripkeStructureExpl (indexMap, initialStates, transRel)
Parameters:
Map<'a, cubeOfAtoms>
initialStates : Set<int>
transRel : Set<int * int>
Returns: KripkeStructureExpl
|
|
|
|
|
|
|
|
|
|
|
|