Graf, Susanne On Lamport’s comparison between linear and branching time temporal logic. (English) Zbl 0551.68033 RAIRO, Inf. Théor. 18, 345-353 (1984). Comparison between a temporal logic of linear time \(TL_ L\) and a temporal logic of branching time \(TL_ B\) is given for a restricted class of models. Incomparability of these two logics is proved and it is shown that there is no linear time logic that is more expressive than the branching time logic \(TL_ B\). Reviewer: J.Zlatuska MSC: 68Q65 Abstract data types; algebraic specification 68Q60 Specification and verification (program logics, model checking, etc.) 03B45 Modal logic (including the logic of norms) 68N25 Theory of operating systems Keywords:expressive power; temporal logic; linear time; branching time Software:CESAR × Cite Format Result Cite Review PDF Full Text: EuDML References: [1] 1. E. M. CLARKE and E. A. EMERSON, Design and synthesis of synchronization skeletons using branching time logic, Harvard University TR-12-81. · Zbl 0546.68014 [2] 2. E. A. EMERSON, Alternative semantics for temporal logics, University of Texas at Austin, TR-182. · Zbl 0559.68050 [3] 3. E. A. EMERSON and J. Y HALPERN, Decision procedure and expressiveness in temporal logic of branching time, 14th Annual ACM Symp. on Theory of Computing, 1982. · Zbl 0559.68051 [4] 4. E. A. EMERSON and J. Y. HALPERN, ”Sometimes” and ”Not Never” revisited: on branching versus linear time, ACM Symp. on Principals of Programming Languages. · Zbl 0629.68020 [5] 5. L. LAMPORT, ”Sometimes” is sometimes ”Not Never”, 7th Annual ACM Symp. on Principals of Programming Languages, 1980. [6] 6. A. PNUELI, The temporal logic of concurrent Programs, 19th Annual Symp. on Foundations on Computer Science, 1971. [7] 7. J. P. QUEILLE and J. SIFAKIS, Specification and verification of concurrent Systems in CESAR, 5th International Symp. on Programming, 1982. Zbl0482.68028 MR807187 · Zbl 0482.68028 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.