Checking that finite state concurrent programs satisfy their linear specification
Published 1 January 1985Open access
Orna Lichtenstein, Amir Pnueli
Citations618
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
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.
Abstract
We present an algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program. The running time of the algorithm is exponential in the size of the formula but linear in the size of the checked program. The algorithm yields also a formal proof in case the formula is valid over the program. The algorithm has four versions that check satisfiability by unrestricted, impartial, just and fair computations of the given program.
Keywords
Computer Science
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. 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.
Lecture notes in computer scienceDesign and synthesis of synchronization skeletons using branching time temporal logic
2,137 Citations2005Edmund M. Clarke, E. Allen Emerson
It is shown that it is possible to automatically synthesize the synchronization skeleton of a concurrent program from a Temporal Logic specification and it is believed that this approach may in the long run turn out to be quite practical.
Lecture notes in computer scienceSpecification and verification of concurrent systems in CESAR
1,277 Citations1982J. P. Queille, Joseph Sifakis
By an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications, is illustrated.
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.
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.
Verification of Concurrent Programs. Part I. The Temporal Framework,
323 Citations1981Zohar Manna, Amir Pnueli
The temporal formalism is introduced as a tool for reasoning about sequences of states and the set of interesting properties is classified into invariance (safety), eventuality (liveness, and precedence) properties.
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.
IRE Transactions on Communications SystemsTowards Analyzing and Synthesizing Protocols
239 Citations1980P. Zafiropulo, Colin H. West +3 more
How to cook a temporal proof system for your pet language
219 Citations1983Zohar Manna, Amir Pnueli
An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied, and is shown to be relatively complete with respect to pure first-order temporal logic.
Verification of concurrent programs: a temporal proof system
140 Citations1983Zohar Manna, Amir Pnueli
A proof system based on temporal logic is presented for proving properties of concurrent programs based on the shared-variables computation model and derived proof principles for these classes of properties obtained and lead to a compact representation of proofs.
Real-time programming and asynchronous message passing
117 Citations1983Ron Koymans, Jan Vytopil +1 more
This paper indicates a method of describing real-time processes and their asynchronous communication by means of message exchanges based upon an extension of linear time temporal logic to a special temporal logic in which real- time and asynchronous message passing properties can be expressed.
"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.
Lecture notes in computer scienceVerification of concurrent programs: Temporal proof principles
90 Citations2005Zohar Manna, Amir Pnueli
This paper presents proof methods for establishing invariance (safety) and eventuality (liveness) properties of temporal logic in concurrent programs.
The complexity of propositional linear temporal logics
56 Citations1982A. Prasad Sistla, Edmund Clarke
This work considers the complexity of satisfiability and determination of truth in a particular finite structure for different propositional linear temporal logics and shows that both the above problems are NP-complete for the logic with F operator and PSPACE- complete for the logics with F,X, with U, with S, with X, and Wolper's extended logic with regular operators.
Lecture notes in computer scienceProving precedence properties: The temporal way
41 Citations2006Zohar Manna, Amir Pnueli
The first methodological approach to the precedence properties is presented, while providing a review of the invariance and liveness properties, based on the ''unless'' operator, which is a weak version of the ''until'' operator.