“Sometimes” and “not never” revisited
Journal of the ACMPublished 2 January 1986Open access
E. Allen Emerson, Joseph Y. Halpern
Citations996
SJR quartileQ1
SJR score2.25
SNIP3.16
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined and the expressive power of a number of sublanguages is compared.
Abstract
The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL * , in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.
Keywords
Computer Science
The temporal logic of programs
5,586 Citations1977Amir Pnueli
A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.
Journal of Computer and System SciencesPropositional dynamic logic of regular programs
1,191 Citations1979Michael J. Fischer, Richard E. Ladner
A formal syntax and semantics for the propositional dynamic logic of regular programs is defined and principal conclusions are that deciding satisfiability of length n formulas requires time d n /log n for some d > 1, and that satisfiability can be decided in nondeterministic time cn for some c.
Journal of the ACMThe complexity of propositional linear temporal logics
1,107 Citations1985A. Prasad Sistla, E. M. Clarke
The complexity of satisfiability and determination of truth in a particular finite structure are considered for different propositional linear temporal logics and it is shown that these problems are NP-complete for the logic with F and PSPACE- complete for the logics with F, X, with U, with S, X operators.
Lecture notes in computer scienceDESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC
1,075 Citations2008Edmund M. Clarke, E. Allen Emerson
A method of constructing concurrent programs in which the synchronization skeleton of the program is automatically synthesized from a high-level (branching time) Temporal Logic specification.
On the temporal analysis of fairness
726 Citations1980Dov M. Gabbay, Amir Pnueli +2 more
It is shown that with the addition of the 'until' operator -U the temporal language becomes expressively complete and two deductive systems DX and DUX are proved to be complete for the languages without and with the new operator respectively.
Theoretical Computer ScienceThe temporal semantics of concurrent programs
701 Citations1981Amir Pnueli
It is demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs.
Science of Computer ProgrammingUsing branching time temporal logic to synthesize synchronization skeletons
662 Citations1982E. Allen Emerson, Edmund M. Clarke
A method of constructing concurrent programs in which the synchronization skeleton of the program is automatically synthesized from a (branching time) temporal logic specification by using a decision procedure based on the finite model property of the logic.
ACM Transactions on Programming Languages and SystemsProving Liveness Properties of Concurrent Programs
583 Citations1982Susan Owicki, Leslie Lamport
A formal proof method, based on temporal logic, for deriving liveness properties is presented, which allows a rigorous formulation of simple informal arguments and how to reason with temporal logic and use safety (invariance) properties in proving liveness is shown.
ACM Transactions on Programming Languages and SystemsSynthesis of Communicating Processes from Temporal Logic Specifications
497 Citations1984Zohar Manna, Pierre Wolper
Propositional Temporal Logic is applied to the specification and synthesis of the synchronization part of communicating processes by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL.
Automatic verification of finite state concurrent system using temporal logic specifications
412 Citations1983E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.
Journal of Computer and System SciencesDecision procedures and expressiveness in the temporal logic of branching time
406 Citations1985E. Allen Emerson, Joseph Y. Halpern
Acta InformaticaThe temporal logic of branching time
371 Citations1983Mordechai Ben‐Ari, Amir Pnueli +1 more
The following metatheoretical results are proven: 1) an exponential decision procedure for satisfiability; 2) a finite model property; 3) the completeness of an axiomatization.
Lecture notes in computer scienceCharacterizing correctness properties of parallel programs using fixpoints
337 Citations1980E. Allen Emerson, Edmund M. Clarke
It is shown that correctness properties of parallel programs can be described using computation trees and that from these descriptions fixpoint characterizations can be generated, and conditions on the form of computation tree descriptions to ensure that a correctness property can be characterized using continuous fixpoints are given.
Information and ControlDeciding full branching time logic
191 Citations1984E. Allen Emerson, A. Prasad Sistla
It is shown that the problem of determining if a CTL* formula is satisfiable in a structure generated by a binary relation is decidable in triple exponential time.
Decision procedures and expressiveness in the temporal logic of branching time
177 Citations1982E. Allen Emerson, Joseph Y. Halpern
It is established that CTL has the small property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from a small -&-ldquo;pseudo-model-&-rdquo%; resulting from the Fischer Ladner quotient construction.
Improved upper and lower bounds for modal logics of programs
141 Citations1985Moshe Y. Vardi, Larry Stockmeyer
It is shown that the satisfiability problems for Streett's delta-PDL.
Modalities for model checking (extended abstract)
139 Citations1985E. Allen Emerson, Chin‐Laung Lei
Journal of Computer and System SciencesProcess logic: Expressiveness, decidability, completeness
138 Citations1982David Harel, Dexter Kozen +1 more
A deductive system for PL which includes the Segerberg axioms for PDL and it is proved that it is complete and that PL is decidable.
Information and ControlReasoning with time and chance
137 Citations1982Daniel Lehmann, Saharon Shelah
Three different axiomatic systems are proposed and shown complete for general models, finite models and models with bounded transition probabilities respectively, which are decidable, by the results of Rabin [Ra1].
Lecture notes in computer scienceYet another process logic
83 Citations1984Moshe Y. Vardi, Pierre Wolper
A process logic that differs from the one introduced by Harel, Kozen and Parikh in several ways is presented, which uses the extended temporal logic of Wolper for statements about paths and allows a “repeat” operator in the programs.
Theoretical Computer ScienceAlternative semantics for temporal logics
78 Citations1983E. Allen Emerson
This paper shows that each of the first three constraints on the allowable sets of computation paths can be independent of the others, and their conjunction is precisely equivalent to the fourth constraint.
Process logic
76 Citations1979Vaughan Pratt
It is indicated how such Gentzen-type axiomatizations lead to deterministic exponential time upper bounds on the complexity of decision procedures for these languages.
Lecture notes in computer scienceThe modal logic of programs
70 Citations1979Zohar Manna, Amir Pnueli
The Temporal interpretation of Modal Logic is adopted and the variety of program properties expressible within the modal formalism is demonstrated.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)Decidability and expressiveness of logics of processes
62 Citations1980Karl Abrahamson
It is shown that PDL is decidable only when processes are tree-like, in Parikh's sense, and that extending PDL by a concurrency operator, a global invariance operator and flowgraph programs, among others, adds no expressive power to PDL.
Specification and synthesis of communicating processes using an extended temporal logic
41 Citations1982Pierre Wolper
This work applies an Extended Propositional Temporal Logic (EPTL) to the specification and synthesis of the synchronization part of communicating processes and constructs a model of the given specifications using a tableau-like satisfiability algorithm for the extended temporal logic.
Information and ControlLooping vs. repeating in dynamic logic
33 Citations1982David Harel, R. W. Sherman
Two extensions of propositional dynamic logic for dealing with infinite computations, LPDL and RPDL, are compared in expressive power and it is shown here that the converse fails.
Foundations of Computer ScienceDeterministic process logic is elementary
7 Citations1982Joseph Y. Halpern