Reasoning about fair concurrent programs
Published 1 January 1986
Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper
Citations33
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
This paper investigates the use of branching time temporal logic to reason about fair programs and finds that the branching time logic of fair programs is the same as the branchingTime logic of probabilistic programs and as the logic of fusionand suffix-closed programs defined by Abrahamson.
Abstract
Article Reasoning about fair concurrent programs Share on Authors: C Courcoubetis AT&T Bell Laboratories, 600 Mountain ave., Murray Hill, NJ AT&T Bell Laboratories, 600 Mountain ave., Murray Hill, NJView Profile , M Y Vardi IBM Almaden Research Center, Department K55/801, 650 Harry Road, San Jose, CA IBM Almaden Research Center, Department K55/801, 650 Harry Road, San Jose, CAView Profile , P Wolper AT&T Bell Laboratories, 600 Mountain ave., Murray Hill, NJ AT&T Bell Laboratories, 600 Mountain ave., Murray Hill, NJView Profile Authors Info & Claims STOC '86: Proceedings of the eighteenth annual ACM symposium on Theory of computingNovember 1986 Pages 283–294https://doi.org/10.1145/12130.12159Online:01 November 1986Publication History 19citation247DownloadsMetricsTotal Citations19Total Downloads247Last 12 Months3Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access
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.
IBM Journal of Research and DevelopmentFinite Automata and Their Decision Problems
1,867 Citations1959M. O. Rabin, D. Scott
Finite automata are considered as instruments for classifying finite tapes as well as generalizations of the notion of an automaton are introduced and their relation to the classical automata is determined.
Graduate texts in mathematicsDenumerable Markov Chains
791 Citations1976John G. Kemeny, J. Laurie Snell +1 more
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.
Checking that finite state concurrent programs satisfy their linear specification
618 Citations1985Orna Lichtenstein, Amir Pnueli
An algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program and a formal proof in case the formula is valid over the program is presented.
Journal of Computer and System SciencesAutomata-theoretic techniques for modal logics of programs
523 Citations1986Moshe Y. Vardi, Pierre Wolper
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
Reasoning about infinite computation paths
309 Citations1983Pierre Wolper, Moshe Y. Vardi +1 more
This work investigates extensions of temporal logic by finite automata on infinite words by investigating the addition of alternation and shows that it does not increase the complexity of the decision problem.
Regional conference series in mathematicsAutomata on Infinite Objects and Church’s Problem
293 Citations1972Michael O. Rabin
Lecture notes in computer scienceImpartiality, justice and fairness: The ethics of concurrent termination
283 Citations1981Daniel Lehmann, Amir Pnueli +1 more
The method of well founded structures for proving termination of programs is extended to concurrent programs and different versions of fairness are introduced: Impartiality, Fairness and Justice.
Theoretical Computer ScienceComplete problems for deterministic polynomial time
279 Citations1976Neil D. Jones, William T. Laaser
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.
Studies in logic and the foundations of mathematicsWeakly Definable Relations and Special Automata
186 Citations1970
It is shown that the weak second-order theory of a unary function and theWeak second- order theory of linearly ordered sets are decidable.
Propositional Dynamic Logic of looping and converse
152 Citations1981Robert S. Streett
Propositional Dynamic Logic can be extended to include both an infinitary iteration construct delta and a backtracking construct converse, and the resulting logic does not satisfy the finite model property, but is nevertheless elementarily decidable.
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
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].
On the extremely fair treatment of probabilistic algorithms
94 Citations1983Amir Pnueli
The proof system proposed is shown to be relatively complete with respect to validity over all extremely fair computations and proven by proving correctness of a new probabilistic algorithm for solving the mutual exclusion problem.
"Sometimes" and "not never" revisited
93 Citations1983E. Allen Emerson, Joseph Y. Halpern
This paper re-examines Lamport's arguments, points out some technical difficulties with the formalism of [LA80], and concludes that, while branching time logic issuitable for reasoning about nondeterministic programs, linear timelogic is preferable for reasoningAbout concurrent programs.
Deciding branching time logic
90 Citations1984E. Allen Emerson, A. Prasad Sistla
The decision procedure exploits the special structure of the finite state ω-automata for linear temporal formulae which allows them to be determinized with only a single exponential blowup in size.
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.
Probabilistic temporal logics for finite and bounded models
78 Citations1984Sergiu Hart, Micha Sharir
Two (closely-related) propositional probabilistic temporal logics based on temporallogics of branching time as introduced by Ben-Ari, Pnueli and Manna and by Clarke and Emerson are presented.
Generalized fair termination
40 Citations1984Nissim Francez, Dexter Kozen
A generalization of the known fairness and equifairness notions, called @@@@-fairness, is presented, in three versions: unconditional, weak and strong, which are proved to be sound and semantically complete.
Decision procedures for time and chance
8 Citations1983Sarit Kraus, Daniel Lehmann
A deterministic exponential lower bound is proved for the three systems TCg, TCb and TCf, and all three systems are shown to be PSPACE-hard using results of [SC].