Automata-Theoretic Techniques for Modal Logics of Programs

[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 problem can 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 exponential decision procedures for several variants of deterministic propositional dynamic logic.

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 :

1986

Journal title :

Journal of Computer and System Sciences

ISSN :

0022-0000

eISSN :

1090-2724

Publisher :

Elsevier

Volume :

Issue :

Pages :

183-221

Peer reviewed :

Peer Reviewed verified by ORBi

Available on ORBi :

since 22 June 2017

Statistics

Number of views

49 (1 by ULiège)

Number of downloads

0 (0 by ULiège)

More statistics

Scopus citations^®

333

Scopus citations^®
without self-citations

283

OpenCitations

255

OpenAlex citations

526

Bibliography

Ben-Ari, Halpern, Pnueli (1982) Deterministic propositional dynamic logic: finite models, complexity, and completeness. J. Comput. System Sci. 25:402-417.
Ben-Ari, Manna, Pnueli (1981) The temporal logic of branching time. Proc. 8th ACM Symp. on Principles of Programming Languages , Williamsburg; 164-176.
Büchi (1962) On a decision method in restricted second order arithmetic. Proc. Internat Congr. Logic, Method and Philos Sci. 1960 , Stanford University Press; 1-12.
Emerson, Halpern (1985) Decision procedures and expressiveness in the temporal logic of branching time. J. Computer and System Sciences 30:1-24.
Emerson, Sistla (1984) Deciding branching time logic. Proc. 16th ACM Symp. on Theory or Computing , Washington; 12-24.
Fisher, Ladner (1979) Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2):194-211.
Gabbay Investigation in Modal and Tense Logic, Reidel; 1976.
Habasinski (1983) Decidability Problems in Logics of Programs. Ph.D. Thesis, Dpt. of Mathematics, Technical University of Poznan; .
Hossley, Rackoff (1972) The emptiness problem for automata on infinite trees. Proc. 13th IEEE Symp. on Switching and Automata Theory 121-124.
Harel, Sherman (1982) Looping vs. repeating in dynamic logic. Information and Control 55:175-192.
Harel, Sherman (1983) Propositional dynamic logic of flowcharts. Proc. Int. Conf. on Foundations of Computational Theory , Lecture Notes in Computer Science, Springer-Verlag, Berlin; 158:195-206.
Jones, Laaser (1977) Complete problems in deterministic polynomial time. Theoretical Computer Science 3:105-117.
Kozen, Parikh (1981) An elementary proof of the completeness of PDL. Theoretical Computer Science 14(1):113-118.
Meyer (1975) Weak monadic second order theory of successor is not elementary recursive. Proc. Logic Colloquium , Lecture Notes in Mathematics, Springer-Verlag; 453:132-154.
Müller (1963) Infinite sequences and finite machines. Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical Design , New York; 3-16.
Parikh (1980) Propositional logics of programs: systems, models and complexity. Proc. 7th Symp. on Principles of Programming Languages , Las Vegas; 186-192.
Pnueli (1981) The temporal logic of concurrent programs. Theoretical Computer Science 13:45-60.
Pratt (1976) Semantical considerations on Floyd-Hoare logic. Proc. 17th IEEE Symp. on Foundations of Computer Science , Houston; 109-121.
Pratt (1979) Models of program logics. Proc. 20th IEEE Symp. on Foundations of Computer Science , San Juan; 115-122.
Pratt (1980) A near-optimal method for reasoning about action. J. Comput. System Sci. 20:231-254.
Pratt (1982) Using graphs to understand PDL. Proc. Workshop on Logics of Programs , D. Kozen, Lecture Notes in Computer Science, Springer-Verlag, Berlin, Yorktown-Heights; 131:387-396.
Pnueli, Sherman (1983) Propositional dynamic logic of looping flowcharts. Technical Report, Weizmann Institute, Rehovot, Israel; .
Rabin (1969) Decidibility of second order theories and automata on infinite trees. Trans AMS 141:1-35.
Rabin (1970) Weakly definable relations and special automata. Proc. Symp. Math. Logic and Foundations of Set Theory , Y. Bar-Hillel, North-Holland; 1-23.
Rabin (1972) Automata on infinite objects and church's problem. Proc. Regional AMS Conf. Series in Math. 13:1-22.
Sherman (1984) Variants of Propositional Dynamic Logic. Ph.D. Dissertation, The Weizmann Inst. of Science; .
Streett (1980) A Propositional Dynamic Logic for Reasoning about Program Divergence. M. Sc. Thesis, MIT; .
Streett (1982) Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control 54:121-141.
Thatcher, Wright (1968) Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical System Theory 2:57-81.
Vardi, Stockmeyer (1985) Improved upper and lower bounds for modal logics of programs. Proc. 17th ACM Symp. on Theory of Computing 240-251.
Vardi, Wolper (1984) Automata-theoretic techniques for modal logics of programs. Proc. 16th ACM Symp. on Theory of Computing , Washington; 446-456.