How to abstract a set?

Hi,

this happens to me all the time when trying to abstract software - I
need to verify properties like 'only if a customer has been logged in,
he may retrieve something'. Because I want to do model checking, I
require a finite abstraction, so maintaining a set of customers logged
in is not feasible. A naive approach would be to distinguish the
abstract states 'the customer a is logged in' and '... not logged in',
and only talk about customer a. But then I need to make sure that the
abstract state 'a is logged in' is not reached by an action other than
a logging in etc., so to make this short: any literature on that
topic?

Thanks!

.

Relevant Pages

  • Re: How to abstract a set?
    ... abstract states 'the customer a is logged in' and '... ... have a class of state machines, where the unique identifier ...
    (comp.theory)
  • Re: How to abstract a set?
    ... abstract states 'the customer a is logged in' and '... ... You appear to be thinking of Petri nets or something much like it. ... customers (and other relevant objects) across their possible states. ...
    (comp.theory)