Averest


KripkeStructures Module

This module implements functions for checking (bi)simulation relations of labeled transition systems (Kripke structures). It also computes quotients and products of Kripke structures.

Types

Type Description

KripkeStructureExpl

This denotes the type of a Kripke structure. States are unsigned integers, and the labels are then given by a simple array of sets of strings, and the transition relation is a list of pairs of states (integers). Finally,the initial states are given as a set of states.

Functions and values

Function or value Description

BisimulationQuotientsTool qscoll

Full Usage: BisimulationQuotientsTool qscoll

Parameters:

This function is meant to be called from cgi; it expects two Kripke structures given as name value pairs in the qscoll argument where the names are Kripke1 and Kripke2. The values are parsed by function ParseKripkeStructureExpl, and then the various simulation and bisimulation relations are computed in addition to the quotient structures to minimize the given Kripke structures.

qscoll : NameValueCollection

CheckBisimulation ostr prefix1 K1 prefix2 K2

Full Usage: CheckBisimulation ostr prefix1 K1 prefix2 K2

Parameters:
Returns: bool * Set<int * int>

check whether K1 and K2 are bisimilar

ostr : TextWriter
prefix1 : string
K1 : KripkeStructureExpl
prefix2 : string
K2 : KripkeStructureExpl
Returns: bool * Set<int * int>

CheckSimulation ostr prefix1 K1 prefix2 K2

Full Usage: CheckSimulation ostr prefix1 K1 prefix2 K2

Parameters:
Returns: bool * Set<int * int>

check whether K2 simulates K1

ostr : TextWriter
prefix1 : string
K1 : KripkeStructureExpl
prefix2 : string
K2 : KripkeStructureExpl
Returns: bool * Set<int * int>

CheckUniqueLabels k

Full Usage: CheckUniqueLabels k

Parameters:
Returns: bool

Check whether each state has a unique label (this is required for making a symbolic representation of the Kripke structure).

k : KripkeStructureExpl
Returns: bool

ComputeProduct k1 k2

Full Usage: ComputeProduct k1 k2

Parameters:
Returns: KripkeStructureExpl

compute a product structure of given Kripke structures

k1 : KripkeStructureExpl
k2 : KripkeStructureExpl
Returns: KripkeStructureExpl

ComputeQuotient k sigma

Full Usage: ComputeQuotient k sigma

Parameters:
Returns: KripkeStructureExpl

compute a quotient structure by a given equivalence relation; the states are those states of an equivalence class with minimal index

k : KripkeStructureExpl
sigma : Set<int * int>
Returns: KripkeStructureExpl

Kripke2Dot ostr statePrefix k

Full Usage: Kripke2Dot ostr statePrefix k

Parameters:

write Kripke structure to a dot file

ostr : TextWriter
statePrefix : string
k : KripkeStructureExpl

MkInitialRel k1 k2

Full Usage: MkInitialRel k1 k2

Parameters:
Returns: Set<int * int>

construct all pairs of states of the two structures having the same labels

k1 : KripkeStructureExpl
k2 : KripkeStructureExpl
Returns: Set<int * int>

ParseKripkeStructureExpl s

Full Usage: ParseKripkeStructureExpl s

Parameters:
    s : string

Returns: KripkeStructureExpl

parsing a Kripke structure from a string; the syntax is explained by the following example: vars a,b,c,d; init 0,1; labels 0:a,b; 1:b; 2:b,c; 3:c; 4:d; 5:c; transitions 0->1; 0->2; 1->3; 1->4; 2->5; 3->3; 4->4; 5->5;

s : string
Returns: KripkeStructureExpl

StateSet2String statePrefix s

Full Usage: StateSet2String statePrefix s

Parameters:
    statePrefix : string
    s : Set<int>

Returns: string
statePrefix : string
s : Set<int>
Returns: string

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

mkSymbolicRepresentation k

Full Usage: mkSymbolicRepresentation k

Parameters:
Returns: string

generate a symbolic description of the Kripke structure in DNF

k : KripkeStructureExpl
Returns: string

printSimDiagrams ostr prefix1 k1 prefix2 k2

Full Usage: printSimDiagrams ostr prefix1 k1 prefix2 k2

Parameters:

prints the diagrams for iterating the simulation relations

ostr : TextWriter
prefix1 : string
k1 : KripkeStructureExpl
prefix2 : string
k2 : KripkeStructureExpl