Formal specification of symbolic-probabilistic systems

We consider the formal specification and validation of systems where probabilistic information is not given by means of fixed values but as sets of probabilities. These sets will be intervals contained in (0, 1] indicating the possible value of the real probability. In order to specify this kind of systems we will introduce a suitable extension of the notion of finite state machine. Essentially, choices between transitions outgoing from a state and having the same input action axe probabilistically resolved. We will also present some implementation relations to assess the conformance of an implementation to a specification. The first implementation relation will clearly present the probabilistic constraints of the specification, but it will be unfeasible from the practical point of view. The other relations will overcome the problems of the first one by introducing a notion of conformance up to a given level of confidence. These relations will assess the validity of an implementation with respect to a specification by considering a finite sample of executions of the implementation and comparing it with the probabilistic constraints imposed by the specification.