Automata-Theoretic Techniques for Modal Logics of Programs

Vardi, Moshe Y; Wolper, Pierre

doi:10.1145/800057.808711

Request a copy

Paper published in a book (Scientific congresses and symposiums)

Automata-Theoretic Techniques for Modal Logics of Programs

Vardi, Moshe Y; Wolper, Pierre

1984 • In Proc. 16th ACM Symposium on Theory of Computing

Peer reviewed

Permalink
https://hdl.handle.net/2268/212084

DOI
10.1145/800057.808711

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

VW STOC 84.pdf

Publisher postprint (728.93 kB)

Request a copy

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Dynalmic logic; tree automata; mu-calculus

Abstract :

[en] We present a new technique for obtaining decision procedures for modal logics of programs. The technique centers around a new class of finite automata on infinite trees for which the emptiness problemcan be solved in polynomial time.The decision procedures then consist of constructing an automaton Af for a given formula f, such that Af accepts some tree if and only if f is satisfiable. We illustrate our technique by giving an exponential decision procedure for deterministic propositional dynamic logic and a variant of the mu-calculus of Kozen.

Disciplines :

Computer science

Author, co-author :

Vardi, Moshe Y

Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)

Language :

English

Title :

Automata-Theoretic Techniques for Modal Logics of Programs

Publication date :

1984

Event name :

STOC '84: sixteenth annual ACM symposium on Theory of computing

Event organizer :

ACM

Event place :

Washington DC, United States

Event date :

April 30th - May 2nd 1984

Audience :

International

Main work title :

Proc. 16th ACM Symposium on Theory of Computing

Publisher :

ACM, New York, United States

ISBN/EAN :

0-89791-133-4

Pages :

446-456

Peer reviewed :

Peer reviewed

Available on ORBi :

since 22 June 2017

Statistics

Number of views

45 (1 by ULiège)

Number of downloads

0 (0 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

Ben-Ari, M., Halpem, J., Pnueli, A., Deterministic prepositional dynamic logic: Finite models, complexity, and completeness (1982) Journal of Computer and System Science, 25, pp. 402-417. , BHP82
Ben-Ari, M., Manna, Z., Pnueli, A., The temporal logic of branching time (1981) Proc. 8th ACM Symposium on Principles of Programming Languages, pp. 164-176. , BMP81 Williamsburg, January
Buchi, J.R., On a decision method in restricted second order arithmetic (1960) Proc. Internat. Congr. Logic, Method and Philos. Sci., pp. 1-12. , Bu62 Stanford University Press, 1962
Clarke, E.M., Program invariants as fix- points (1977) Proc. 18th IEEE Symposium on Foundations of Computer Science, pp. 18-28. , Q77 Providence
Emerson, E.A., Halpem, J.Y., Decision procedures and expressiveness in the temporal logic of branching time (1982) Proc. 14th ACM Symposium on Theory of Computing, pp. 169-180. , EH82 San Francisco, May
Emerson, E.A., Sistla, A.P., An elementary decision procedure for the u-calculus Proc. 11th Int. Colloq. on Automata, Languages and Programming, , ES84 Lecture Notes in Computer Science, Springer-Verlag, Berlin, to appear
Fisher, M., Ladner, R., Propositional dynamic logic of regular programs (1979) J. of Computer and System Sciences, 18 (2), pp. 194-211. , FL79
Flon, L., Suzuki, M., The total correctness of parallel programs (1981) SIAM Journal of Computing, 10, pp. 227-245. , FS81
Hitchcock, P., Park, D., Induction rules and termination proofs (1973) Proc. 1st Int. Colloq. on Automata, Languages and Programming, pp. 225-251. , HP73 Lecture Notes in Computer Science, Springer- Verlag, Berlin
Hossley, R., Rackoff, C.W., The emptiness problem for automata on infinite trees (1972) Proc. 13th IEEE Symp. on Switching and Automata Theory, pp. 121-124. , HR72]
Harel, D., Sherman, R., Looping vs. Repeating in dynamic logic (1983) Technical Report CS83-02, , HS83a Weizmann Institute, Rehovot, Israel
Harel, D., Sherman, R., Propositional dynamic logic of flowcharts (1983) Proc. Int. Conf. on Foundations of Computation Theory, , HS83b Lecture Notes in Computer Science, Springer-Verlag, Berlin
Kozen, D., Results on the propositional u- calculus (1983) Theoretical Computer Science, 27, pp. 333-354. , Ko82
Kozen, D., Parikh, R., An elementary proof of the completeness of PDL (1981) Theoretical Computer Science, 14 (1), pp. 113-118. , KP81
Kozen, D., Parikh, R., A decision procedure for the propositional u-calculus (1984) Proc. of the Workshop on Logics of Programs, 164. , KP83 Springer- Verlag Lecture Notes in Computer Science -, (to appear), also IBM Research Report RC9987
Jones, N.D., Laaser, W.T., Complete problems in deterministic polynomial time (1977) Theoretical Computer Science, 3, pp. 105-117. , JL77
Meyer, A.R., Weak monadic second order theory of successor is not elementary recursive (1975) Proc. Logic Colloquium, 453, pp. 132-154. , Me75 Lecture Notes in Mathematics -, Springer- Verlag
Park, D., Fixpoint induction and proof of program semantics (1970) Machine Intelligence, 5, pp. 59-78. , Pa70 (Metlzer, Mitchie, eds.), Edinburgh University Press
Park, D., Finiteness is mu-ineffable (1976) Theoretical Computer Science, 3, pp. 173-181. , Pa76]
Parikh, R., Propositional game logic (1983) Proc. 24th IEEE Symp. on Foundations of Computer Science, pp. 195-200. , Par83 Tucson
Pnueli, A., The temporal logic of programs (1977) Proc. 8th IEEE Symp. on Foundations of Computer Science, pp. 46-57. , Pn77 Providence
Pratt, V.R., Semantical considerations on floyd-hoare logic (1976) Proc. 17th IEEE Symp. on Foundations of Computer Science, pp. 109-121. , Pr76 Houston, October
Pratt, V.R., Models of program logics (1979) Proc. 20th IEEE Symp. on Foundation of Computer Science, pp. 115-122. , Pr79 San Juan
Pratt, V.R., A near-optimal method for reasoning about action (1980) J. Computer and Systems Sciences, 20, pp. 231-254. , Pr80
Pratt, V.R., A decidable u-calculus (1981) Proc. 22nd IEEE Symp. on Foundations of Computer Science, pp. 421-427. , Pr81 Nashville, TN, October
Pnueli, A., Sherman, R., (1983) Propositional Dynamic Logic of Looping Flowcharts, , PS83 Technical Report, Weizmann Institute, Rehovot, Israel
Rabin, M.O., Decidability of second order theories and automata on infinite trees (1969) Transactions of American Mathematical Society, 141, pp. 1-35. , Ra69
Reif, J., Data row analysis of communicating processes (1979) Proc. 6th ACM Symp. on Principles of Programming Languages, , Re79 San Antonio, January
Scott, D., Lattice of flow diagrams (1971) Proc. Symp. on Semantics of Algorithmic Languages, 188, pp. 311-366. , Sc71 (E. Engeler, Ed.), Lecture Notes in Mathematics -, Springer-Verlag, Berlin
Scott, D., De Bakker, J., (1969) A Theory of Programs, , SdB69 unpublished lecture notes, Vienna
Streett, R., Propositional dynamic logic of looping and converse (1981) Proc. 13th ACM Symp. on Theory of Computing, pp. 375-383. , StSl Milwaukee
Tarski, A., A lattice-theoretical fixpoint theorem and its applications (1955) Pacific Journal of Mathematics, 5, pp. 285-309. , Ta55]
Thatcher, J.W., Wright, J.B., Generalized finite automata theory with an application to a decision problem of second-order logic (1968) Mathematical System Theory, 2, pp. 57-81. , TW68