Journal of the ACM Bibliography

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 omega-automata or formulas in extended temporal logic. Copyright 1995 by ACM, Inc.

The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.

Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification; F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems -- complexity of proof procedures; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs -- mechanical verification; G.3 [Probability and Statistics] -- probabilistic algorithms

General Terms: Algorithms, Theory, Verification

Additional Key Words and Phrases: Automata, EXPTIME-complete, Markov chain, model checking, probabilistic algorithm, PSPACE-complete, temporal logic

Selected references

• Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114-133, January 1981.

• Edmund M. Clarke Jr., E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 117-126, Austin, Texas, January 1983.

• E. Allen Emerson and Joseph Y. Halpern. ``sometimes'' and ``not never'' revisited: On branching versus linear time. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 127-140, Austin, Texas, January 1983.

• E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time strikes back. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 84-96, New Orleans, Louisiana, January 1985.

• Nissim Francez and Michael Rodeh. A distributed abstract data type implemented by a probabilistic communication scheme. In 21st Annual Symposium on Foundations of Computer Science, pages 373-379, Syracuse, New York, 13-15 October 1980. IEEE.

• Dov M. Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal basis of fairness. In Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, pages 163-173, Las Vegas, Nevada, January 1980.

• Sergiu Hart and Micha Sharir. Probabilistic temporal logics for finite and bounded models. In Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing, pages 1-13, Washington, D.C., 1984.

• Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent program. ACM Transactions on Programming Languages and Systems, 5(3):356-380, July 1983.

• Daniel J. Lehmann and Michael O. Rabin. On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, pages 133-138, Williamsburg, Virginia, January 1981.

• Daniel Lehmann and Saharon Shelah. Reasoning with time and chance. Information and Control, 53(3):165-198, June 1982.

• Orna Lichtenstein and Amir Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97-107, New Orleans, Louisiana, January 1985.

• Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, October 1966.

• Amir Pnueli. On the extremely fair treatment of probabilistic algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, pages 278-290, Boston, Massachusetts, 25-27 April 1983.

• Amir Pnueli and Lenore Zuck. Probabilistic verification by tableaux. In Proceedings, Symposium on Logic in Computer Science, pages 322-331, Cambridge, Massachusetts, 16-18 June 1986. IEEE Computer Society.

• Shmuel Safra. On the complexity of omega-automata. In 29th Annual Symposium on Foundations of Computer Science, pages 319-327, White Plains, New York, 24-26 October 1988. IEEE.

• A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, July 1985.

• Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In 26th Annual Symposium on Foundations of Computer Science, pages 327-338, Portland, Oregon, 21-23 October 1985. IEEE.

• Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings, Symposium on Logic in Computer Science, pages 332-344, Cambridge, Massachusetts, 16-18 June 1986. IEEE Computer Society.

• Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56(1/2):72-99, January/February 1983.

• Pierre Wolper, Moshe Y. Vardi, and A. Prasad Sistla. Reasoning about infinite computation paths (extended abstract). In 24th Annual Symposium on Foundations of Computer Science, pages 185-194, Tucson, Arizona, 7-9 November 1983. IEEE.

Shortcuts: