Zohar Manna
Amir Pnueli
ABSTRACT
An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied. Given a new language, it is sufficient to deline the interface notions of atomic transitions, justice, and fairness in order to obtain a full temporal proof system for this language. This construction is particularly useful for the analysis of concurrent systems. We illustrate the construction on the shared-variable model and on CSP. The generic proof system is shown to be relatively complete with respect to pure first-order temporal logic.
- {B} Ben-Ari, M., "Temporal Logic Proofs of Concurrent Programs," Technical Report, Tel Aviv University (1981).Google Scholar
- {H} Hoare, C. A. R., "Communicating Sequential Processes," CACM 21 (1978), pp. 666-677. Google ScholarDigital Library
- {KR} Kuiper, R. and de Roever, W. P., "Fairness Assumptions for CSP in a Temporal Logic Framework," TC2 Working Conference on the Formal Description of Programming Concepts, Garmisch (June 1982).Google Scholar
- {M} Manna, Z., "Verification of Sequential Programs: Temporal Axiomatization," Theoretical Foundations of Programming Methodology (M. Broy and G. Schmidt, eds.), NATO Scientific Series, D. Reidel Pub. Co., Holland (1982), pp. 53-102.Google Scholar
- {MP1} Manna, Z. and Pnueli, A., "Verification of Concurrent Programs: The Temporal Framework," in The Correctness Problem in Computer Science (R. S. Boyer and J S. Moore, eds.), International Lecture Series in Computer Science, Academic Press, London, 1982, pp. 215273.Google Scholar
- {MP2} Manna, Z. and Pnueli, A., "Verification of Concur rent Programs: a Temporal Proof System," Proc. 4th School on Advanced Programming, Amsterdam, Holland (June 1982).Google Scholar
- {MP3} Manna, Z. and Pnueli, A., "Verification of Concurrent Programs: Temporal Proof Principles," Proc. of the Workshop on Logic of Programs (D. Kozen, ed.), Yorktown-Heights, N.Y. (1981). Springer-Verlag Lecture Notes in Computer Science 131, pp. 200-252. Google ScholarDigital Library
- {OL} Owicki, S. and Lamport, L., "Proving Liveness Properties of Concurrent Programs," ACM Transactions on Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455-495. Google ScholarDigital Library
- {P} Pnueli, A., "The Temporal Semantics of Concurrent Programs," Theoretical Computer Science 13 (1981), pp. 45-60.Google ScholarCross Ref
- {PR} Pnueli, A. and de Roever, W. P., "Rendezvous with ADA --- A Proof Theoretical View," Proc. of the AdaTEC Conference, Crystal City (1982).Google Scholar
- {SM} Schwartz, R. L. and Melliar-Smith, P. M., "Temporal Logic Specifications of Distributed Systems," Proc. of the 2nd International Conference on Distributed Computing Systems, Paris, France (1981).Google Scholar
Recommendations
A complete proof system for propositional projection temporal logic
The paper presents a proof system for Propositional Projection Temporal Logic (PPTL) with projection-plus. The syntax, semantics, and logical laws of PPTL are introduced together with an axiom system consisting of axioms and inference rules. To ...
A proof system for temporal reasoning with sequential information
SBIA'10: Proceedings of the 20th Brazilian conference on Advances in artificial intelligenceA new logic, sequence-indexed linear-time temporal logic (SLTL), is obtained semantically from the standard linear-time temporal logic LTL by adding a sequence modal operator which represents a sequence of symbols. By the sequence modal operator of SLTL,...
A Proof System for a Unified Temporal Logic
Computing and CombinatoricsAbstractTheorem proving is a widely used approach to the verification of computer systems, and its theoretical basis is generally a proof system for formal derivation of logic formulas. In this paper, we propose a proof system for Propositional Projection ...
Comments