markov

Documentation

Index

• func ChenBound(counts [][]int, source int, epsilon, delta float64) float64
• func HorizonReachabilityProbability(model *Model, start int, targets map[int]struct{}, steps int) (float64, error)
• func HorizonReachabilityProbabilityByState(model *Model, startState string, targetStates []string, steps int) (float64, error)
• func ReachabilityProbability(model *Model, start int, targets map[int]struct{}, options ReachabilityOptions) (float64, error)
• func ReachabilityProbabilityByState(model *Model, startState string, targetStates []string, ...) (float64, error)
• func WriteModelJSON(w io.Writer, model *Model) error
• type BuildOptions
• type Model
  • func BuildModel[O any](logs [][]O, abs abstraction.Interface[O], options BuildOptions) (*Model, error)
  • func ReadModelJSON(r io.Reader) (*Model, error)
  • func (m Model) IndexForState(state string) (int, bool)
  • func (m Model) SortedStateIndexes() []int
  • func (m Model) StateForIndex(index int) (string, bool)
  • func (m Model) Validate() error
• type ReachabilityOptions

Functions

func ChenBound

func ChenBound(counts [][]int, source int, epsilon, delta float64) float64

ChenBound returns a sample-bound right-hand side for one source state.

func HorizonReachabilityProbability

func HorizonReachabilityProbability(model *Model, start int, targets map[int]struct{}, steps int) (float64, error)

HorizonReachabilityProbability computes P_start(F<=steps target).

Unlike ReachabilityProbability, this is a finite-session risk estimate. It is the probability of reaching a target state within the next steps transitions.

func HorizonReachabilityProbabilityByState

func HorizonReachabilityProbabilityByState(model *Model, startState string, targetStates []string, steps int) (float64, error)

HorizonReachabilityProbabilityByState computes finite-horizon reachability using symbolic state labels.

func ReachabilityProbability

func ReachabilityProbability(model *Model, start int, targets map[int]struct{}, options ReachabilityOptions) (float64, error)

ReachabilityProbability computes P_start(F target) for the Markov-chain model.

func ReachabilityProbabilityByState

func ReachabilityProbabilityByState(model *Model, startState string, targetStates []string, options ReachabilityOptions) (float64, error)

ReachabilityProbabilityByState computes P_start(F target) using symbolic state labels.

func WriteModelJSON

func WriteModelJSON(w io.Writer, model *Model) error

WriteModelJSON writes a learned model as JSON.

Types

type BuildOptions

type BuildOptions struct {
	// Alpha is the validity-aware Laplace smoothing amount.
	Alpha float64
}

BuildOptions controls Markov-chain model learning.

type Model

type Model struct {
	States              []string                   `json:"states"`
	StateIndex          map[string]int             `json:"state_index"`
	StateInterpretation map[string]map[string]bool `json:"state_interpret,omitempty"`
	StateCounts         map[int]int                `json:"state_counts,omitempty"`
	TransitionCounts    map[int]map[int]int        `json:"transition_counts,omitempty"`
	TransitionProbs     map[int]map[int]float64    `json:"transition_probs"`
	Metadata            map[string]json.RawMessage `json:"metadata,omitempty"`
}

Model is a learned Markov-chain model over integer-indexed symbolic states.

func BuildModel

func BuildModel[O any](logs [][]O, abs abstraction.Interface[O], options BuildOptions) (*Model, error)

BuildModel learns a Markov-chain model from observation traces.

func ReadModelJSON

func ReadModelJSON(r io.Reader) (*Model, error)

ReadModelJSON reads a learned model from JSON.

func (Model) IndexForState

func (m Model) IndexForState(state string) (int, bool)

IndexForState returns the integer index for a symbolic state.

func (Model) SortedStateIndexes

func (m Model) SortedStateIndexes() []int

SortedStateIndexes returns all model indexes in ascending order.

func (Model) StateForIndex

func (m Model) StateForIndex(index int) (string, bool)

StateForIndex returns the symbolic state for an index.

func (Model) Validate

func (m Model) Validate() error

Validate checks basic Markov-chain model invariants.

type ReachabilityOptions

type ReachabilityOptions struct {
	Tolerance     float64
	MaxIterations int
}

ReachabilityOptions controls iterative probability solving.