Costas Courcoubetis
Abstract
We determine the complexity of testing whether a finite state, sequential or concurrent probabilistic program satisfies its specification expressed in linear-time temporal logic. For sequential programs, we present an algorithm that runs in time linear in the program and exponential in the specification, and also show that the problem is in PSPACE, matching the known lower bound. For concurrent programs, we show that the problem can be solved in time polynomial in the program and doubly exponential in the specification, and prove that it is complete for double exponential time. We also address these questions for specifications described by ω-automata or formulas in extended temporal logic.
- ~AHO, A. V., HOPCROFT, J., AND ULLMAN, J. D. t974. The Design and Analysis of Computer ~Algorithms. Addison-Wesley, Reading, Mass. Google Scholar
- ~BREIMAN, L. 1968. Probabih_ty, Addison-Wesley, Reading, Mass.Google Scholar
- ~BUCHi, J. R. 1962. On a decision method in restricted second order arithmetic. In Procee&ngs of ~the Intemattonal Congress on Logic. Method and Phdosophzcal Science. pp. 1 12.Google Scholar
- ~BUCHi, J. R. 1973. The monadic second-order theory of ro1. In Decidable Theories If. Lecture ~Notes in Mathematics, vol. 328. Springer-Verlag, New York, pp. 1-128.Google Scholar
- ~CHANDRA, A. m., KOZEN, D. C., AND STOCKMEYER, L. J. 1981. Alternation. J. ACM 28, 1 (Jan.) ~pp. 114-133. Google Scholar
- ~CHOUEkA, Y. 1974. Theories of automata on w-tapes: A simplified approach. J. Comput. Syst. ~Scl. 8, 117-141.Google Scholar
- ~LARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1983. Automatic verification of finite-state ~concurrent systems using temporal logic specifications: A practical approach. In Proceedings of ~the lOth Annual ACM Symposium on Pnnciples of Programming Languages (Austin, Tex., Jan. ~24-26). ACM, New York, pp. 117 126. Google Scholar
- ~COURCOUBETIS~ C., AND YANNAKAKIS, M. 1990. Markov decision processes and regular events. ~In Proc. of the 17th Intl. Colloquzum on Automata, Languages and Programming. pp. 336-349. Google Scholar
- ~EMERSON, E. A., AND HALPERN, J. Y. 1983. "Sometimes" and "Not Never" revisited: On ~branching vs. linear time. In Proceedings of lOth Annual ACM Symposium on Principles of ~Programming Languages (Austin, Tex., Jan. 24-26). ACM, New York, pp. 127-140. Google Scholar
- ~EMERSON, E. m., AND LEI, C. L. 1985. Modalities for model checking: Branching time strikes ~back. In Proceedings of the 12th Annual ACM S3,mposzum on Principles of Programming Lan- ~guages (New Orleans, La., Jan. 14-16). ACM. New York, pp. 84 96. Google Scholar
- ~EMERSON, E. A. AND SISTLA, m. P. 1983. A triple exponential decision procedure for CTL*. In ~CMU Workshop on Logic oJ Programs. Carnegie-Mellon Univ., Pittsburgh, Pa. Google Scholar
- ~FRANCEZ, N., AND RODEH, M. 1980. A distributed data type implemented by a probabilistic ~communication scheme. In Proceedings of 21st IEEE Symposium on Foundattons of Computer ~Science. IEEE, New York, pp. 373-379.Google Scholar
- ~GABBY, D., PNUELI, A., SHELAH, S., AND STAVI, J. 1980. On the temporal analysis of fairness. In ~Proceedings of 7th Annual ACM Sympostum on Principles of Programming Languages (Las Vegas, ~Nev., Jan. 28 30). ACM, New York, pp. 163-173. Google Scholar
- ~HART, S., AND SHARIR, M. 1984. Probabilistic temporal logic for finite and bounded models. In ~Proceedings of the lOth Annual ACM Symposium on Theory of Computing (Washington, D.C., ~Apr. 30-May 2). ACM, New York, pp. 1-13. Google Scholar
- ~HART, S., SHARIR, M., AND PNUELI, A. 1983. Termination of probabilistie concurrent programs. ~ACM Trans. Prog. Lang. Syst. 5, 3 (July), 356-380. Google Scholar
- ~KEMENY, J. G., SNELL, J. L., AND KNAPP, A. W. 1976. Denumerable Markov Chains. Springer- ~Verlag, New York.Google Scholar
- ~LEHMAN, D., AND RABIN, M. O. t981. On the advantage of free choice: A symmetric and fully ~distributed solution to the dining philosophers problem. In Proceedings of the 8th AnnualACM ~Symposium on Principles of Programming Languages (Williamsburg, Va., Jan. 26 28). ACM, New ~York, pp. 133-138. Google Scholar
- ~LEHMAN, D., AND SHELAH, S. 1982. Reasoning with time and chance. Inf. Control 53, 165-198.Google Scholar
- ~LICHTENSTEIN, O, AND PNUELI, A. i985. Checking that finite-state concurrent programs samfy ~their linear specification. In Proceedings of the 12th Annual ACM Symposium on Princzples of ~ProgrammmgLanguages (New Orleans, La., Jan. 14 16). ACM, New York, pp. 97-107. Google Scholar
- ~MCNAUGHTON, R. 1966. Testing and generating infinite sequences by a finite automaton. Inf. ~Contr. 9, 521-530.Google Scholar
- PNUELI, A. 1981. The temporal logic of concurrent programs. Theoret. Comput. Scl. 73, 45 60.Google Scholar
- PNUELI, A. 1983. On the extremely fair treatment of probabilistic algorithms. In Proceedings of ~&e 15& Annual ACM Symposium on Theory of Computmg (Boston, Mass., Apr. 25-27). ACM, ~New York, pp. 278-290. Google Scholar
- ~PNUELI, A., AND ZUCK, L. 1986. Probabilistic verification by tableaux. In Proceedings of the l~t ~Symposium on Logm in Computer Science. IEEE, New York.Google Scholar
- ~QUEILLE, J. P., AND SIFAKIS, J. 1982. Fairness and related properties in transition systems. ~Research Report #292. IMAG, Grenoble, Switzerland.Google Scholar
- ~RABtN, M. O. 1072. Automata on infinite objects and Church's problem. In Proceedings of the ~RegtonalAMS Conference Series m Mathematm~, vol. 13. AMS, Providence, R.I., pp. 1-22. Google Scholar
- ~SAFRA, S. 1988. On the complexity of w-automata. In Proceedings of tile 29th IEEE Symposium ~on Foundations of Computer Science. IEEE, New York, pp. 319-327.Google Scholar
- ~SISTLA, A. P.~ AND CLARKE, E. M. 1985. The complexity of propositional linear temporal logics. ~J. ACM 32, 3 (July), 733-749. Google Scholar
- ~SISTLA, A. P., VARDI, M. Y., AND WOLPER, P. 1987. The complimentation problem for Buchi ~automata with application to temporal logic. Theoret. Comput. Sci. 49, 217-237. Google Scholar
- ~VARm, M. 1985. Automatic verification of probabilistic concurrent finite-state programs. In ~Proceedings of 26th 1EEE Symposium on Foundations of Computer Sctence. IEEE, New York, ~pp. 327-338.Google Scholar
- ~VARDI, m., AND WOLPER, P. 1986. An automata-theoretic approach to automatic program ~verification. In Proceedings of the 1st Symposium on Logic in Computer Sctence. IEEE, New ~York.Google Scholar
- ~WOLPER, P., VARDI, M. Y., AND SISTLA, A. P. 1983. Reasoning about infinite computation paths. ~In Proceeding,' of tile 24th IEEE Symposium on Foundations of Computer Science. IEEE, New ~York, pp. 185-194.Google Scholar
- ~WOLPER, P. 1983. Temporal logic can be more expressive. Inf. Control 56, 72-99.Google Scholar
Index Terms
- The complexity of probabilistic verification
Recommendations
Regular model checking for LTL(MSO)
Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...
Alternating interval based temporal logics
ICFEM'10: Proceedings of the 12th international conference on Formal engineering methods and software engineeringTo specify properties of open systems with interval based temporal logics, alternating interval based temporal logics are proposed by introducing Concurrent Game Structures (CGS) to Propositional Projection Temporal Logic (PPTL) and Propositional ...
Back to the future: towards a theory of timed regular languages
SFCS '92: Proceedings of the 33rd Annual Symposium on Foundations of Computer ScienceThe authors introduce two-way timed automata-timed automata that can move back and forth while reading a timed word. Two-wayness in its unrestricted form leads, like nondeterminism, to the undecidability of language inclusion. However, if they restrict ...
Reviews
Moshe Vardi
Program verification has always been a desirable task, but never an easy one. The advent of concurrent programming has made it significantly more necessary and difficult. Indeed, the conceptual complexity of concurrency increases the likelihood of a program containing errors. In the traditional approach to concurrent program verification, the correctness of the program is expressed as a formula in first-order temporal logic. To prove that the program is correct, one has to prove that the correctness formula is a theorem of a certain deductive system. This proof is constructed manually and is usually quite difficult to construct. It often requires an intimate understanding of the program. Furthermore, there is no hope of constructing the proof completely algorithmically. The only extent of automation that one can hope for is to have the proof checked by a machine and, possibly, to have some limited heuristic help in finding the proof. A different approach was introduced in the early 1980s [1] for finite-state programs, that is, programs in which the variables range over finite domains. The significance of this class follows from the fact that a significant number of the communication and synchronization protocols studied in the literature are, in essence, finite-state programs. Thus, to verify the correctness of the program, one has only to check algorithmically that the program, viewed as a finite-state transition system, satisfies (is a model of) a propositional temporal logic specification. This approach, called “verification by model checking,” was described by Apt and Kozen as “one of the most exciting developments in the theory of program correctness.” An extension of the model-checking approach to probabilistic programs was proposed in my paper [2]. Here, the program is modeled as a finite sequential Markov chain or finite concurrent Markov chain. Instead of attempting to verify that all computations of the program satisfy the specification (given by a linear temporal formula), one attempts to verify that the specification holds with probability 1, that is, that the set of computations that satisfy the specification has probability 1. This can be called probabilistic verification. The probability is relative to the probabilistic steps of the program and the worst possible scheduling of the various processes. This definitive paper continues the investigation by studying the complexity of probabilistic verification. It provides tight upper and lower bound. For sequential programs, the problem is shown to be PSPACE-complete, and for concurrent programs, the problem is 2EXPTIME-complete. (2EXPTIME denotes the class of problems that can be solved in doubly exponential time.) In either case, the source of the high complexity is the linear temporal specification; the algorithms run in time that is linear in the size of the program. The fundamental idea is to reduce model checking to the checking of certain graph-theoretic properties of the underlying Markov chain. It turns out that the precise numeric value of the probabilities is irrelevant.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments