Process logic: preliminary report

ABSTRACT

We discuss problems arising in reasoning about on-going processes, using the modal constructs after, throughout, during, and preserves. Earlier work established decidability of the theory whose language included only the first two of these, along with program connectives | , ; and *. Here we give a complete Gentzen-type axiomatizations for useful combinations of the other modalities. We also indicate how such Gentzen-type axiomatizations lead to deterministic exponential time upper bounds on the complexity of decision procedures for these languages. It remains an open problem how to completely axiomatize the combination of modalities during and preserves.

REFERENCES

• 1: Banachowski, L., A. Kreczmar, G. Mirkowska H. Rasiowa, A. Salwicki. An Introduction to Algorithmic Logic; Metamathematical Investigations in the Theory of Programs . In Math. Found. of Comp. Sc. (eds. Mazurkiewicz and Pawlak), Banach Center Publications, Warsaw. 1977.
• 2: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 3: Michael J. Fischer , Richard E. Ladner, Propositional modal logic of programs, Proceedings of the ninth annual ACM symposium on Theory of computing, p.286-294, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803418]
• 4: Gentzen, G. Untersuchungen ueber das Logische Schliessen, Math. Zeitschr, 39, 176-210, 405-431. 1934-5. (English tr.: Investigations into Logical Deduction, in The Collected Papers of G. Gentzen, 69-131. 1969.)
• 5: David Harel , Vaughan R. Pratt, Nondeterminism in logics of programs, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.203-213, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512782]
• 6: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 7: Parikh, R. A Completeness Result for PDL. Symposium on Mathematical Foundations of Computer Science, Zakopane, Warsaw, Sept. 1978.
• 8: Parikh, R. Second Order Process Logic. Internal Report, MIT, April 1978.
• 9: Pnueli, A. The Temporal Logic of Programs. 18th IEEE Symposium on Foundations of Computer Science, 46-57. Oct. 1977.
• 10: Pnueli, A. Correctness of Concurrent Programs: The Temporal Logic Approach. Unpublished talk, NSF-CBMS Conference on the Logic of Computer Programming, Troy, NY. June 1978.
• 11: Pratt, V. R. Semantical Considerations on Floyd-Hoare Logic. Proc. 17th Ann. IEEE Symp. on Foundations of Comp. Sci., 109-121. 1976.
• 12: V. R. Pratt, A practical decision method for propositional dynamic logic (Preliminary Report), Proceedings of the tenth annual ACM symposium on Theory of computing, p.326-337, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804362]
• 13: Pratt, V. R. A Near Optimal Method for Reasoning About Action. MIT/LCS/TM-113, M.I.T., Oct. 1978.
• 14: Salwicki, A. Formalized Algorithmic Languages. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 18. No. 5. 1970.
• 15: Segerberg, K. A Completeness Theorem in the Modal Logic of Programs. Preliminary report. Notices of the AMS, 24, 6, A-552. Oct. 1977.