Entry Kuperman:2000:ATA from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Kuperman:2000:ATA,
  author =       "Orna Kuperman and Moshe Y. Vardi",
  title =        "An automata-theoretic approach to modular model
                 checking",
  journal =      j-TOPLAS,
  volume =       "22",
  number =       "1",
  pages =        "87--128",
  month =        jan,
  year =         "2000",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Tue Sep 26 10:12:58 MDT 2000",
  bibsource =    "http://www.acm.org/pubs/contents/journals/toplas/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org/pubs/citations/journals/toplas/2000-22-1/p87-kuperman/",
  abstract =     "In {\em modular verification\/} the specification of a
                 module consists of two part. One part describes the
                 guaranteed behavior of the module. The other part
                 describes the assumed behavior of the system in which
                 the module is interacting. This is called the {\em
                 assume-guarantee\/} paradigm. In this paper we consider
                 assume-guarantee specifications in which the guarantee
                 is specified by branching temporal formulas. We
                 distinguish between two approaches. In the first
                 approach, the assumption is specified by branching
                 temporal formulas too. In the second approach, the
                 assumption is specified by linear temporal logic. We
                 consider guarantees in CTL, and CTL*. We develop two
                 fundamental techniques: building maximal models for CTL
                 and CTL* formulas and using alternating automata to
                 obtain space-efficient algorithms for fair model
                 checking. Using these techniques we classify the
                 complexity of satisfiability, validity, implication,
                 and modular verification for CTL and CTL*. We show that
                 modular verification is PSPACE-complete for CTL and is
                 EXSPACE-complete for CTL*. We prove that when the
                 assumption is linear, these bounds hold also for
                 guarantees in CTL and CTL*. On the other hand, the
                 problem remains EXSPACE-hard even when we restrict the
                 assumptions to LTL and take the guarantees as a fixed
                 CTL formula.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "automata; modular verification; temporal logic",
  subject =      "Software --- Software Engineering --- Software/Program
                 Verification (D.2.4)",
}

Related entries