Alternative semantics for temporal logics

DOI10.1016/0304-3975(83)90082-8MaRDI QIDQ2265815zbMATH OpenOpenAlexFDO

Authors E. Allen Emerson

Publication date 1983

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(83)90082-8

zbMATH Keywords

allowed sets of computation pathsfusion closurelimit closureR-generable pathssuffix closuretemporal logics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

The paper studies relationships between alternative semantics for temporal logics. Three common constraints on the allowed sets of computation paths, the suffix closure [\textit{D. Harel}, \textit{D. Kozen} and \textit{R. Parikh}, J. Comput. Syst. Sci. 25, 144-170 (1982; Zbl 0494.03016)], the fusion closure [\textit{V. R. Pratt}, Process logic, in: Proc. 6th ACM Symp. on Principles of Programming Languages (1979)] and the limit closure [\textit{K. Abrahamson}, Expressiveness and decidability of logics of processes, Ph. D. thesis, Univ. of Washington, Seattle (1980)], are shown to be independent and their conjunction to be equivalent to the R-generable paths [\textit{Z. Manna} and \textit{A. Pnueli}, Lect. Notes Comput. Sci. 71, 385-409 (1979; Zbl 0404.68011)].

Recommendations

• Alternating-time temporal logic
• A temporal semantics for basic logic
• scientific article; zbMATH DE number 7723711
• Temporal Logics
• Timed Alternating-Time Temporal Logic
• Alternating-time temporal logics with linear past
• Alternating-time temporal logic in the calculus of (co)inductive constructions
• Alternating-time temporal logic with strong and weak exceptions
• Comparing semantics for temporal STIT logic

Cites work

• Formalization of Properties of Functional Programs
• scientific article; zbMATH DE number 3675301 (Why is no real title available?)
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• Process logic: Expressiveness, decidability, completeness
• The temporal semantics of concurrent programs

Cited in

(24)

• The complexity of reasoning about knowledge and time. I: Lower bounds
• R-generability, and definability in branching time logics
• Verification of distributed programs using representative interleaving sequences
• Time-extraction for temporal logic -- logic programming and local process time
• Safety, liveness and fairness in temporal logic
• Axiomatising extended computation tree logic
• Spanning the spectrum from safety to liveness
• Decision procedures and expressiveness in the temporal logic of branching time
• Infinite unfair shuffles and associativity
• Interleaving set temporal logic
• scientific article; zbMATH DE number 3878351 (Why is no real title available?)
• Alternating-time temporal logic
• A Labeled Natural Deduction System for a Fragment of CTL *
• TTL : a formalism to describe local and global properties of distributed systems
• A tableau-based decision procedure for CTL^*
• Expressiveness and succinctness of a logic of robustness
• Reasoning about programs by exploiting the environment
• Game-Theoretic Semantics for Alternating-Time Temporal Logic
• Axiomatising extended computation tree logic
• scientific article; zbMATH DE number 7723711 (Why is no real title available?)
• Automated temporal reasoning about reactive systems
• A coalgebraic approach to infinite games
• ConcurrentHOL
• Branching versus linear logics yet again

This page was built for publication: Alternative semantics for temporal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2265815)