Temporal Logic Can Be More Expressive

[en] We first review Temporal Logic and prove that there are some properties of sequences that it cannot express, though these are expressible using for instance regular expressions. Then, we show how Temporal Logic can be extended to express any property definable by a right-linear grammar and hence a regular expression. Finally, we give a complete axiomatization and a decision procedure for the extended Temporal Logic and examine its complexity.

Disciplines :

Computer science

Author, co-author :

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 :

Temporal Logic Can Be More Expressive

Publication date :

1983

Journal title :

Information and Control

ISSN :

0019-9958

Publisher :

Academic Press, New York, United States - New York

Volume :

Issue :

1--2

Pages :

72-99

Peer reviewed :

Peer Reviewed verified by ORBi

Available on ORBi :

since 09 July 2011

Statistics

Number of views

149 (17 by ULiège)

Number of downloads

6 (3 by ULiège)

More statistics

Scopus citations^®

464

Scopus citations^®
without self-citations

453

OpenCitations

389

OpenAlex citations

673

Bibliography

Ben-Ari, Manna, Pnueli (1981) The temporal logic of branching time. Eighth ACM Symposium on Principles of Programming Languages , Williamburg, Va.; 164-176.
Cohen, Gold (1977) Theory of ω-languages 1. Characterization of ω-context-free languages. J. Comput. System Sci. 15:169-184.
Emerson, Clarke (1980) Characterizing correctness properties of parallel programs as fixpoints. Proceeding, 7th Int. Colloquium on Automata, Languages and Programming , Lecture notes in Computer Science, Springer-Verlag, New York; 85:169-181.
Fisher, Ladner (1979) Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18:194-211.
Gabbay, Pnueli, Shelah, Stavi (1980) The temporal analysis of fairness. Seventh ACM Symposium on Principles of Programming Languages , Las Vegas, Nev.; 163-173.
Habermann (1975) Path Expressions. Computer Science Report, Carnegie-Mellon University, Berlin; .
Harel (1979) First Order Dynamic Logic. Lecture Notes in Computer Science, Springer-Verlag, Pittsburgh, Pa, No. 68; .
Harel, Kozen, Parikh (1980) Process logic: Expressiveness, decidability, completeness. Proceedings of the 21st Symposium on Foundations of Computer Science , Syracuse, N. Y.; 129-142.
Harel, Pnueli, Stavi (1981) Propositional dynamic logic of context-free programs. Proceedings of the Twenty-Second Symposium on Foundations of Computer Science , Nashville, Tenn.; 310-321.
Halpern, Reif (1981) The propositional dynamic logic of determinisitc, well-structured programs. Proceedings of the Twenty-Second Symposium on Foundations of Computer Science , Nashville, Tenn.; 322-334.
Kamp (1968) Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Berlin; .
Kozen, Parikh (1981) An elementary proof of the completeness of PDL. Theoret. Comput. Sci. 14:113-118.
Manna (1981) Verification of sequential programs: Temporal axiomatization. Theoretical Foundations of Programming Methodology, NATO Scientific Series, F.L. Bauer, E.W. Dijkstra, C.A.R. Hoare, Reidel, Los Angeles; .
Meyer (1975) Weak monadic second order theory of successor is not elementary recursive. Proceedings Logic Colloquium, Lecture Notes in Mathematics , Springer-Verlag, Holland; 453:132-154.
Manna, Pnueli (1981) Verification of concurrent programs: The temporal framework. The Correctness Problem in Computer Science , R.S. Boyer, J.S. Moore, International Lecture Series in Computer Science, Academic Press, Berlin; 215-273.
Pnueli (1977) The temporal logic of programs. Proceedings of the Eighteenth Symposium on Foundations of Computer Science , Providence, RI; 46-57.
Pratt (1981) Using graphs to understand PDL. Proceedings of the Workshop on Logics of Programs , Yorktown-Heights, N.Y., Lecture Notes in Computer Science, Springer-Verlag, London; 131 Vo.:387-396.
Rescher, Urquart Temporal Logic, Springer-Verlag, Berlin; 1971.
Savitch (1970) Relationship between nondeterministic and deterministic tape complexities. J. Comput. System Sci. 4:177-192.
Sistla, Clarke (1982) The complexity of propositional linear temporal logic. Proceedings of the 14th ACM Symposium on Theory of Computing, San Francisco, Calif; .
Shaw (1979) Software Specification Languages Based on Regular Expressions. Technical Report, ETH Zurich, Berlin; .
Smullyan First Order Logic, Springer-Verlag; 1968.
Streett (1981) Propositional dynamic logic of looping and converse. Proceedings of the 13th Symposium on Theory of Computing , Milwaukee, Wisc.; 375-383.
Wolper (1982) Specification and synthesis of communicating processes using and extended temporal logic. Ninth Symposium on Principles of Programming Languages , Albuquerque, N. Mex.; 20-33.
Wolper (1982) Synthesis of Communicating Processes from Temporal Logic Specifications. PhD thesis, Stanford University, Berlin; .