Subject: Re: safety and liveness definitions
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Fri Sep 27 2002 - 01:01:40 PDT
I agree. I think this is appropriate in the context.
Anthony
skshukla@ics.uci.edu wrote:
> Again this path based definition of safety property just works for
> Linear Time Safety properties.
>
> Regards
>
> Sandeep
>
> -----Original Message-----
> From: owner-vfv@eda.org [mailto:owner-vfv@eda.org] On Behalf Of Anthony
> McIsaac
> Sent: Thursday, September 26, 2002 10:11 AM
> To: vfv@eda.org
> Subject: safety and liveness definitions
>
> I was asked to suggest alternative "more formal" definitions if I
> could improve on those in the text, with "any sequence" replaced by "any
> finite path",
> and "sequence" by "path".
>
> On reflection, the definition of safety properties seems to me nearly
> correct.
> I won't pursue the line I was taking at the meeting, but have got a
> different point.
>
> I believe that safety properties are commonly identified with closed,
> prefix-closed
> sets of paths. The definition as it stands covers the prefix-closed
> aspect, so the only
> gap concerns closure. This crops up with properties like "eventually!
> (always !a)"
> (there are only finitely many occurrences of a), which isn't violated on
> any finite
> path, so satisfies the definition as it stands, but isn't a safety
> property.
> If we want the definition to cover this, I suggest
> "A safety property is a property such that if any path violates the
> property, then
> it has a finite subpath such that every extension of the subpath
> violates the property."
>
> As for liveness properties, as far as I know there isn't a formal
> definition; it's
> more of an informal notion (perhaps the academics on the committee will
> correct me
> on this). So it probably doesn't matter if the "more formal" definition
> isn't
> quite accurate, and I'm not going to propose an alternative. I would
> just mention
> that, according to the definition given, "there are more occurrences of
> a than b"
> is a liveness property.
>
> Anthony
>
> --
> Anthony McIsaac
>
> STMicroelectronics Limited
> 1000 Aztec West
> Almondsbury
> Bristol BS32 4SQ
>
> Tel: ++44 (0)1454 462466
> Fax: ++44 (0)1454 617910
>
> Email: Anthony.McIsaac@st.com
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Fri Sep 27 2002 - 01:07:26 PDT