文章基本信息

标题：Probabilistic abstraction for model checking: An approach based on property testing
本地全文：下载
作者：Sophie Laplante ; Richard Lassaigne ; Frederic Magniez 等
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2001
卷号：2001
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：In model checking, program correctness on all inputs is verified by considering the transition system underlying a given program. In practice, the system can be intractably large. In property testing, a property of a single input is verified by looking at a small subset of that input. We join the strengths of both approaches by introducing to model checking the notion of probabilistic abstraction. We put forth the notion of \eps -reducibility which is implicit in many property testers. Our probabilistic abstraction associates a set of small random transition systems to a program. Under some conditions, these transition systems are sufficient to guarantee that a program approximately decides on all its inputs a property like bipartiteness, k -colorability, or any first order graph properties of type . We give a concrete example of an abstraction for a program which decides bipartiteness. Finally, we show that abstraction is necessary by proving an exponential lower bound on OBDDs for approximate bipartiteness.
关键词：abstraction , Communication complexity , model checking , Property Testing