Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths
We compare the complexities of the following two model checking problems: checking whether a linear-time formula is satisfied by all paths (which we call universal model checking) and checking whether a formula is satisfied by almost all paths (which we c
- PDF / 521,924 Bytes
- 12 Pages / 430 x 660 pts Page_size
- 42 Downloads / 159 Views
2
ETH Zürich, Switzerland [email protected] IBM Zurich Research Laboratory, Switzerland [email protected] 3 PPS - CNRS & Univ. Paris 7, France [email protected]
Abstract. We compare the complexities of the following two model checking problems: checking whether a linear-time formula is satisfied by all paths (which we call universal model checking) and checking whether a formula is satisfied by almost all paths (which we call fair model checking here). For many interesting classes of linear-time formulas, both problems have the same complexity: for instance, they are PSPACE-complete for LTL. In this paper, we show that fair model checking can have lower complexity than universal model checking, viz., we prove that fair model checking for L(F∞ ) can be done in time linear in the size of the formula and of the system, while it is known that universal model checking for L(F∞ ) is co-NP-complete. L(F∞ ) denotes the class of LTL formulas in which F∞ is the only temporal operator. We also present other new results on the complexity of fair and universal model checking. In particular, we prove that fair model checking for RLTL is co-NP-complete.
1
Introduction
A reactive system satisfies a specification expressed by a formula of linear-time temporal logic if all its executions satisfy the formula. In this case, we say that a system is universally correct, and the problem of verifying universal correctness is called universal model checking. Sometimes a system does not satisfy a specification, but only because of a “small” set of executions that do not satisfy the formula. From a measuretheoretic point of view, “small” means having probability 0. From a topological point of view, it means being a meager set. The topological point of view corresponds to the notion of fairness [15], i.e., a set of executions Y of a system is meager if and only if there exists some fairness assumption F for the system such that each execution in Y is unfair w. r. t. F . Varacca and Völzer [12] have shown that, for LTL formulas and finite-state systems, the two notions of smallness coincide. More importantly, they coincide
Most of the work was done while the first two authors were affiliated with the University of Lübeck, Germany.
V. Arvind and S. Prasad (Eds.): FSTTCS 2007, LNCS 4855, pp. 532–543, 2007. c Springer-Verlag Berlin Heidelberg 2007
Model Checking Almost All Paths
533
independently of the probability measure chosen (provided it belongs to a very general class of measures). If the set of executions that do not satisfy the specification is small, we say that the system is almost correct or fairly correct. The problem of verifying fair correctness is called fair model checking in this paper.1 As indicated above, fair model checking is — for finite systems and LTL specifications — equivalent to qualitative probabilistic model checking (i.e., checking a specification for probability 1) (cf. [12]). Fair model checking is an interesting alternative to universal model checking even for non-probabilistic systems that are d
Data Loading...
