On the expressive power of Dynamic Logic (Preliminary Report)

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

On the expressive power of Dynamic Logic (Preliminary Report)

Full text

Pdf (648 KB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the eleventh annual ACM symposium on Theory of computing table of contents

Atlanta, Georgia, United States

Pages: 167 - 175

Year of Publication: 1979

Authors

Albert R. Meyer
Karl Winklmann

Sponsors

ACM: Association for Computing Machinery
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 8, Citation Count: 4

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/800135.804410 What is a DOI?

ABSTRACT

We show that “looping” of while-programs can be expressed in Regular First-Order Dynamic Logic, disproving a conjecture made in [Harel-Pratt 1978]. In addition we show that the expressive power of quantifier-free Dynamic Logic increases when nondeterminism is introduced in the programs that are part of formulae of Dynamic Logic. Allowing assignments of random values to variables increases the expressive power even further.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	R. Hossley and C. Rackoff. The emptiness problem for automata on infinite trees. 13th Annual Symposium on Switching and Automata Theory, October 1972.
	2	D. Harel. Logics of Programs: Axiomatics and Descriptive Power. PhD Thesis, Massachusetts Institute of Technology, May 1978.
	3	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]
	4	M. Rabin. Automata on infinite trees and the synthesis problem. Tech. Report No. 37, Hebrew University, Jerusalem, January 1970.
	5	V. R. Pratt. Semantical Considerations on Floyd-Hoare Logic. 17th Annual Symposium on Principles of Programming Languages, January 1976.

CITED BY 4

	Robert S. Streett, Propositional Dynamic Logic of looping and converse, Proceedings of the thirteenth annual ACM symposium on Theory of computing, p.375-383, May 11-13, 1981, Milwaukee, Wisconsin, United States
	Albert R. Meyer , Rohit Parikh, Definability in Dynamic Logic, Proceedings of the twelfth annual ACM symposium on Theory of computing, p.1-7, April 28-30, 1980, Los Angeles, California, United States
	Albert R. Meyer , Joseph Y. Halpern, Axiomatic Definitions of Programming Languages: A Theoretical Assessment, Journal of the ACM (JACM), v.29 n.2, p.555-576, April 1982
	Joseph Y. Halpern , Albert R. Meyer, Axiomatic definitions of programming languages, II, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.139-148, January 26-28, 1981, Williamsburg, Virginia