HOME       UP       PREV       NEXT (ABD - PSL Assertion, General Structure)  

ABD - State versus Path, Concrete Versus Symbolic.

Many assertions are over concrete state. For instance `Never is light A off when light B is on' .

Other assertions need to refer to symbolic values. For instance `The value in register X is always less than the value in register Y' .

State properties describe the current state only. For instance `Light A is off and light B is on'.

Path properties relate successive state properties to each other. For instance `light A always goes off before light B comes on '. We shall see PSL requires the symbolic values be embedded in the bottommost 'modelling layer' and that its temporal layer cannot deal with symbolic values. For instance, we cannot write `{ A(x);B(y) } |=> { C(x,y) }'.

Also note that the internal representation used by a checker tool for a concrete property could use a symbolic encoding (such as a BDD) to handle an exponentially-large state space using reasonable memory.

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.