storm::utility::parameterlifting Namespace Reference

Functions
template<typename ValueType >
static bool	validateParameterLiftingSound (storm::models::sparse::Model< ValueType > const &model, storm::logic::Formula const &formula)
	Checks whether the parameter lifting approach is sound on the given model with respect to the provided property.

Function Documentation

validateParameterLiftingSound()

template<typename ValueType >

static bool storm::utility::parameterlifting::validateParameterLiftingSound ( storm::models::sparse::Model< ValueType > const &  model, storm::logic::Formula const &  formula  )

static

Checks whether the parameter lifting approach is sound on the given model with respect to the provided property.

This method is taylored to an efficient but incomplete check, i.e., if false is returned, parameter lifting might still be applicable.

More precisely, we only check if the occurring functions are multilinear polynomials. However, Parameter Lifting also works for fractions of multilinear polynomials where for every state s, every probability and reward occurring at s have the same denominator.

Parameters

model
formula

Returns

true iff it was successfully validated that parameter lifting is sound on the provided model.

Definition at line 33 of file parameterlifting.h.