NDLI: "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report)

Please wait, while we are loading the content...

Five paradigm shifts in programming language design and their realization in Viron, a dataflow programming environment

Uncovering principles of novice programming

Code generation for silicon

Derivation of efficient DAG marking algorithms

Reasoning about nonatomic operations

Verifying reachability invariants of linked structures

Practical program verification: automatic program proving for real-time embedded software

Making variables abstract: an equational theory for Russell

Transformational programming: applications to algorithms and systems

Polymorphic type inference

Computer experiments with the REVE term rewriting system generator

Precise typing of abstract data type specifications

Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach

"Sometimes" and "not never" revisited: on branching versus linear time (preliminary report)

How to cook a temporal proof system for your pet language

Structural semantics for polymorphic data types (preliminary report)

Incremental data flow analysis

Conversion of control dependence to data dependence

Loops in combinator-based compilers

Compilation of data-driven programs for synchronous execution

Summarizing graphs by regular expressions

A program form based on data dependency in predicate regions

Practical use of a polymorphic applicative language

On the unification of data and program abstraction in Ada

Incremental polymorphic type checking in B

Mechanisms for compile-time enforcement of security

Abstraction mechanisms in the BETA programming language

Locality in software systems

"Sometimes" and "not never" revisited: on branching versus linear time (preliminary report)

Content Provider	ACM Digital Library
Author	Emerson, E. Allen Halpern, Joseph Y.
Abstract	Temporal logic ([PR57], [PR67]) provides a formalism fordescribing the occurrence of events in time which is suitable forreasoning about concurrent programs (cf. [PN77]). In definingtemporal logic, there are two possible views regarding theunderlying nature of time. One is that time is linear: at eachmoment there is only one possible future. The other is that timehas a branching, tree-like nature: at each moment, time may splitinto alternate courses representing different possible futures.Depending upon which view is chosen, we classify (cf. [RU71]) asystem of temporal logic as either a linear time logic in which thesemantics of the time structure is linear, or a system of branchingtime logic based on the semantics corresponding to a branching timestructure. The modalities of a temporal logic system usuallyreflect the semantics regarding the nature of time. Thus,in a logicof linear time, temporal operators are provided for describingevents along a single time path (cf. [GPSS80]). In contract, in alogic of branching time the operators reflect the branching natureof time by allowing quantification over possible futures cf.[AB80],[EC80]).Some controversy has arisen in the computer science communityregarding the differences between and appropriateness of branchingversus linear time temporal logic. In a landmark paper [LA80]intended to "clarify the logical foundations of the application oftemporal logic to concurrent programs," Lamport addresses theseissues. He defines a single language based on the temporaloperators "always" and "sometimes". Two distinct interpretationsfor the language are given. In the first interpretation formulaemake assertions about paths, whereas in the second interpretationthey make assertions about states. Lamport associates the formerwith linear time and the latter with branching time (although itshould be noted that in both cases the underlying time structuresare branching). He then compares the expressive power of lineartime and branching time logic. Based on his comparison and otherarguments, he concludes that, while branching time logic issuitable for reasoning about nondeterministic programs, linear timelogic is preferable for reasoning about concurrent programs.In this paper, we re-examine Lamport's arguments and reachsomewhat different conclusions. We first point out some technicaldifficulties with the formalism of [LA80]. For instance, thedefinition of expressive equivalence leads to paradoxicalsituations where satisfiable formulae are classified as equivalentto false. Moreover, the proofs of the results comparing expressivepower do not apply in the case of structures generated by a binaryrelation like those used in the logics of [FL79] and [BMP81]. Wegive a more refined basis for comparing expressive power thatavoids these technical difficulties. It does turn out thatexpressibility results corresponding to Lamport's still hold.However, it should be emphasized that these results apply only tothe two particular systems that he defines. Sweeping conclusionsregarding branching versus linear time logic in general are notjustified on this basis.We will argue that there are several different aspects to theproblem of designing and reasoning about concurrent programs. Whilethe specific modalities needed in a logic depend on the precisenature of the purpose for which it is intended, we can make somegeneral observations regarding the choice between a system ofbranching or linear time. We believe that linear time logics aregenerally adequate for verifying the correctness of pre-existingconcurrent programs. For verification purposes, we are typicallyinterested in properties that hold of all computation paths. It isthus satisfactory to pick an arbitrary path and reason about it.However, there are applications where we need the ability to assertthe existence of alternative computation paths as provided by abranching time logic. This arises from the nondeterminism - beyondthat used to model concurrency - present in many concurrentprograms. In order to give a complete specification of such aprogram, we must ensure that there are viable computation path acorresponding to the nondeterministic choices the program mightmake. (An example is given in section 6.) Neither of Lamport'ssystems is entirely adequate for such applications.In order to examine these issues more carefully, we define alanguage, CTL, in which a universal or existential path quantifiercan prefix an arbitrary linear time assertion. CTL is an extensionof the Computation Tree Logic, CTL, defined in [CE81] and studiedin [EH82]. This language subsumes both of Lamport's interpretationsand allows us to compare branching with linear time. Moreover, thesyntax of CTL* makes it clear which interpretation is intended.The paper is organized as follows: In section 2 we summarizeLamport's approach and discuss its limitation. In section 3 wepresent the syntax and semantics of CTL. We also define somenatural sublanguages of CTL and compare their expressive power inSection 4. In particular, we show that (cf. Theorem 4.1) a languagesubstantially less expressive than CTL* still subsumes both ofLamport's interpretations. Section 5 then shows how CTL* can beembedded in MPL [AB80] and PL [HKP80]. Finally, section 6 concludeswith a comparison of the utility of branching and linear timelogic.
Starting Page	127
Ending Page	140
Page Count	14
File Format	PDF
ISBN	0897910907
DOI	10.1145/567067.567081
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-01-24
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in