Symbolic model checking for mu-calculus requires exponential time

Authors
Rabinovich, A
Citation
A. Rabinovich, Symbolic model checking for mu-calculus requires exponential time, THEOR COMP, 243(1-2), 2000, pp. 467-475
Citations number
14
Categorie Soggetti
Computer Science & Engineering
Journal title
THEORETICAL COMPUTER SCIENCE
ISSN journal
03043975 → ACNP
Volume
243
Issue
1-2
Year of publication
2000
Pages
467 - 475
Database
ISI
SICI code
0304-3975(20000728)243:1-2<467:SMCFMR>2.0.ZU;2-E
Abstract
We investigate the complexity of symbolic model checking for mu-calculus. T he exponential time lower bound is proved. Moreover, this lower bound holds even for a fixed alternation-free formula. (C) 2000 Elsevier Science B.V. All rights reserved.