compute a transition system whose states and transitions contains all models of a given formula if that formula is satisfiable at all

This function implements a model checker for CTL and mu-calculus using an explicit representation of the Kripke structure as given in this module.

decompose a set of goals where each goal is split into blocks gA which contain only literals and finished E- and A-blocks and where each block is split into b = b = bA ∪ bB where formulas in bA are all X-formulas so that no rule applies anymore.

find some valid CTL formulas

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.

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.

write local model checking proof tree to a dot file

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 "KripkeStructure" 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.

draw a pre-structure to a dot file

draw a pre-structure to a dot file

convert a given pre-structure to a Kripke structure

prove a given CTL* or mu-calculus formula

generate a random CTL logic formula of a given size

check satisfiability of a given CTL* or mu-calculus formula

This is the cgi-function for the special model checking examples.

compute a prestructure for a given alternating tree automaton