A really temporal logic

Rajeev Alur; T. A. Henzinger

doi:10.1109/sfcs.1989.63473

Abstract

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>

Keywords

Temporal logicUndecidable problemFormalism (music)Computer scienceProgramming languageLinear temporal logicNatural languageModel checkingTheoretical computer scienceArtificial intelligenceAlgorithmDecidability

Affiliated Institutions

Stanford University US

Related Publications

Explicit clock temporal logic

Eyal Harel , Orna Lichtenstein , Amir Pnueli

The authors present a single exponent decision procedure for the validity of XCTL formulas, and a double exponent decision procedure for the validity of XCTL formulas over finit...

2002 [1990] Proceedings. Fifth Annual IEEE... 136 citations

Model-checking for real-time systems

Rajeev Alur , Costas Courcoubetis , David L. Dill

This research extends CTL model-checking to the analysis of real-time systems, whose correctness depends on the magnitudes of the timing delays. For specifications, the syntax o...

2002 [1990] Proceedings. Fifth Annual IEEE... 890 citations

Using dynamic programming for solving variational problems in vision

Amir A. Amini , Terry E. Weymouth , Ramesh Jain

Dynamic programming is discussed as an approach to solving variational problems in vision. Dynamic programming ensures global optimality of the solution, is numerically stable, ...

1990 IEEE Transactions on Pattern Analysis... 1003 citations

Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models

Carl A. Sunshine , D.H. Thompson , Roddy W. Erickson +2 more

It is becoming increasingly important that communication protocols be formally specified and verified. This paper describes a particular approach–the state transition model–usin...

1982 IEEE Transactions on Software Enginee... 54 citations

Reception of multiple co-channel digital signals using antenna arrays with applications to PCS

Shilpa Talwar , A. Paulraj , Mats Viberg

Antenna arrays can be used to increase system capacity in PCS networks by supporting multiple co-channel users per cell in receive and in transmit. We propose a novel approach f...

2002 11 citations

Publication Info

Year: 1989
Type: article
Pages: 164-169
Citations: 162
Access: Closed

External Links

View on DOI.org

Social Impact

Altmetric

A really temporal logic

PlumX Metrics

Social media, news, blog, policy document mentions

Citation Metrics

162

OpenAlex

115

CrossRef

Cite This

APA Style

                            
                                    Rajeev Alur, 
                                
                                    T. A. Henzinger
                                
                            (1989). 
                            A really temporal logic. 
                            30th Annual Symposium on Foundations of Computer Science
                            
                            , 164-169.
                            https://doi.org/10.1109/sfcs.1989.63473

Identifiers

DOI: 10.1109/sfcs.1989.63473

Data Quality

Data completeness: 77%