Subject: RE: efficiency claims
From: Armoni, Roy (roy.armoni@intel.com)
Date: Sat Nov 17 2001 - 23:57:27 PST
Hi Sandeep,
As far as I understand, it should be NSPACE(n) for formula size n,
and by Savitch, NSPACE(n) \subseteq DSPACE(n^2),
which keeps you in PSPACE.
Roy
-----Original Message-----
From: SANDEEP SHUKLA [mailto:skshukla@ics.uci.edu]
Sent: Tuesday, December 18, 2001 12:11 AM
To: Moshe Vardi
Cc: havlicek@adttx.sps.mot.com; vfv@eda.org
Subject: Re: efficiency claims
Hi Moshe,
You said in point (2) that translating the Forspec formula into Buchi
automaton is linear, and then modeling checking is linear in the size of the
automaton. However, from your earlier results model checking LTL is PSPACE
complete withrespect to the formula size, which tells me that in point (2) I
should not expect linear time. Do you mean linear space in both the steps?
So do we have an model checking algorithm for LTL in DPSACE(n) with respect
to formula size n?
REgards
Sandeep
Moshe Vardi wrote:
> >
> > It will help me to understand the way in which this paper substantiates
> > the efficiency claims if you, or anyone else, would explicitly state
> > the complexities that are being claimed as efficient for compilation,
> > and complementation of ForSpec formulas and how these complexities
> > relate to the complexities of static and dynamic verification of
> > ForSpec formulas.
>
> 1. Complementaing ForSpec is trivial: the complement of a formula f is
> the formula !f.
>
> 2. The compilation of a ForSpec formula into a symbolic representation
> of a Buchi automaton (which is what is needed for model checking or
> simulation checking) is linear in the size of the formula.
>
> 3. Model checking ForSpec is linear in the size of the transition system
> representing the design and the property automaton. This transition
> system can be exponential in the size of the symbolic representation.
>
> What can you tell us about the complexity of CBV? I have not so far
> seen any formal claims regarding CBV.
>
> Thanks,
> Moshe
This archive was generated by hypermail 2b28 : Sat Nov 17 2001 - 23:58:40 PST