Pmin = -infinity

[zakopc...@gmail.com]

Hi,

I have two questions concerning model checking of imported explicit model when trying to ensure fairness.

I ran the model checking of imported explicit model and I chose the property to be verified such that only fair runs would be considered. However the obtained result of Pmin was "-Infinity", so I would like to ask you why did it happen or what it means and in which cases I can get such result.
(I've attached the states and the transitions file, as well as the output of prism).

I also tried to run the verification of the same model with -fair switch implemented in PRISM. It seemed to give me the correct result, however I cannot see why it should work as I provide PRISM only with transitions and states, but I don't give it any information about my processes.
I tried fo find out more information about the -fair switch, how it works etc. but unsuccessfully. So I was wondering if you could comment on or provide some materials describing the possibility of using it with imported explicit model and why it seems to work and in case it actually works, on what basis.

I will be very grateful for any information.

Kind regards,

Kristina Zakopcanova

[Dave Parker]

Hi Kristina,

> I ran the model checking of imported explicit model and I chose the
> property to be verified such that only fair runs would be considered.
> However the obtained result of Pmin was "-Infinity", so I would like to
> ask you why did it happen or what it means and in which cases I can get
> such result.
> (I've attached the states and the transitions file, as well as the
> output of prism).

If the result is -Infinity, this must be a bug of some kind. I'll look
into it.

> I also tried to run the verification of the same model with -fair switch
> implemented in PRISM. It seemed to give me the correct result, however I
> cannot see why it should work as I provide PRISM only with transitions
> and states, but I don't give it any information about my processes.
> I tried fo find out more information about the -fair switch, how it
> works etc. but unsuccessfully. So I was wondering if you could comment
> on or provide some materials describing the possibility of using it with
> imported explicit model and why it seems to work and in case it actually
> works, on what basis.

The notion of fairness that is enabled in PRISM when using the -fair
switch is the one from this paper:

C. Baier and M. Kwiatkowska.
Model checking for a probabilistic branching time logic with fairness.
Distributed Computing, 11(3):125-155, 1998.

It does not depend on processes being scheduled. Instead, a path of the
MDP is considered to be fair if, for states s occurring infinitely often
in the path, each possible nondeterministic choice available in state s
is taken infinitely often.

This is fairness can be checked on an imported model, even without any
information about processes.

Best wishes,

Dave.