Approximate parameter synthesis for probabilistic time-bounded reachability

Han, T. and Katoen, J.P. and Mereacre, A. (2008) Approximate parameter synthesis for probabilistic time-bounded reachability. In: Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008), 1-3 Dec 2008, Barcelona, Spain.

PDF
Restricted to UT campus only: Request a copy
237Kb

Abstract:	This paper proposes a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity ofbounded reachability properties. This algorithm is based ondiscretizing parameter ranges together with a refinement technique. This paper describes the algorithm, analyzes its time complexity, and shows its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/62645
Official URL:	http://dx.doi.org/10.1109/RTSS.2008.19
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 255051