TTL: A formalism to describe local and global properties of distributed systems. (English) Zbl 0766.68035

Summary: We develop a logic formalism to describe and prove properties of finite- state districuted systems. This formalism is based on a branching time approach and is called typed temporal logic (TTL). For a distributed system \(D\), we give two TTL theories, LTT\(_ D\) and LGTT\(_ D\) (local time theory and local and global time theory of \(D\), respectively). The theory LTT\(_ D\) allows specifying distributed systems by local axioms, namely by properties that hold with respect to local observations of system parts. The theory LGTT\(_ D\) has a mechanism to infer global properties of the system \(D\) from local properties. For both theories we show that theorem proving is reducible to model checking.


68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
03B45 Modal logic (including the logic of norms)
Full Text: DOI EuDML


[1] 1. J. VAN BENTHEM, Modal Logic and Classical Logic, Bibliopolis, Napoli, 1985. Zbl0639.03014 MR832432 · Zbl 0639.03014
[2] 2. M. BEN-ARI, A. PNUELI and Z. MANNA, The Temporal Logic of Branching Time, Acta Inform., 1983, 20, pp. 207-226. Zbl0533.68036 MR733676 · Zbl 0533.68036 · doi:10.1007/BF01257083
[3] 3. E. M. CLARKE, E. A. EMERSON and A. P. SISTLA, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, A.C.M. Trans. Prog. Lang. Syst., 1986, 8, pp. 244-263. Zbl0591.68027 · Zbl 0591.68027 · doi:10.1145/5397.5399
[4] 4. E. M. CLARKE, O. GRUMBERG and R. P. KURSHAN, A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems, ”Logic at Botik ’89”, Lect. Notes in Comput. Sci., 1989, 363, Springer, Berlin, pp. 81-90. Zbl0688.68019 MR1030568 · Zbl 0688.68019
[5] 5. E. M. CLARKE, D. E. LONG and K. L. MCMILLAN, Compositional Model Checking, ”Fourth Annual Symposium on Logic in Computer Science”, I.E.E.E. Computer Society Press, Washington, D.C., 1989, pp. 353-362. Zbl0716.68035 · Zbl 0716.68035
[6] 6. M. DANELUTTO and A. MASINI, A Temporal Logic Approach to Specify and to Prove Properties of Finite State Concurrent Systems, ”CSL’88”, Lecture Notes in Comput. Sci, 1989, 385, Springer, Berlin, pp. 63-79. Zbl0746.68030 MR1035562 · Zbl 0746.68030
[7] 7. P. DEGANO, R. DE NICOLA and U. MONTANARI, A Distributed Operational Semantics for CCS Based on Condition/Event Systems, Acta Inform., 1987, 26, pp. 59-91. Zbl0656.68061 MR969870 · Zbl 0656.68061 · doi:10.1007/BF02915446
[8] 8. E. A. EMERSON, Alternative Semantics for Temporal Logics, Theoret. Comput. Sci., 1983, 26, pp. 121-130. Zbl0559.68050 MR726915 · Zbl 0559.68050 · doi:10.1016/0304-3975(83)90082-8
[9] 9. E. A. EMERSON and E. M. CLARKE, Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Sci. Comput. Programming, 1982, 2, pp. 241-266. Zbl0514.68032 · Zbl 0514.68032 · doi:10.1016/0167-6423(83)90017-5
[10] 10. E. A. EMERSON and J. Y. HALPERN, Décision Procedures and Expressiveness in the Temporal Logic of Branching Time, J. Comput. System Sci., 1985, 30, pp. 1-24. Zbl0559.68051 MR788828 · Zbl 0559.68051 · doi:10.1016/0022-0000(85)90001-7
[11] 11. E. A. EMERSON and J. Y. HALPERN, ”Sometimes” and ”Not Never” Revisited: On Branching Versus Linear Time Temporal Logic, J. A.C.M., 1986, 33, pp. 151-178. Zbl0629.68020 MR820103 · Zbl 0629.68020 · doi:10.1145/4904.4999
[12] 12. E. A. EMERSON and C. L. LEI, Modalities for Model Checking: Branching Time Strikes Back, 12th A.C.M. Symposium on Principles of Programming Languages, 1985, pp. 84-96. · Zbl 0615.68019
[13] 13. E. A. EMERSON and A. P. SISTLA, Deciding Full Branching Time Logic, Inform. and Control, 1984, 61, pp. 175-201. Zbl0593.03007 MR773404 · Zbl 0593.03007 · doi:10.1016/S0019-9958(84)80047-9
[14] 14. P. ENJALBERT and M. MICHEL, Many-Sorted Temporal Logic for Multi-Process Systems, ”Mathematical Foundations of Computer Science, 1984”, Lecture Notes in Comput. Sci., 176, Springer, Berlin, 1984, pp. 273-281. Zbl0558.68026 MR783456 · Zbl 0558.68026
[15] 15. F. KRÖGER, Temporal Logic of Programs, Springer, Berlin, 1987. Zbl0609.03007 MR889458 · Zbl 0609.03007
[16] 16. L. LAMPORT, ”Sometimes” is Sometimes ”Not Never”: On the Temporal Logic of Programs, 7th A.C.M. Symposium on Principles of Programming Languages, 1980, pp. 174-185.
[17] 17. K. LODAYA and P. S. THIAGARAJAN, A Modal Logic for a Subclass of Event Structures, Automata Languages and Programming ’87, Lecture Notes in Comput. Sci., 1987. 267, Springer, Berlin, pp. 290-303. Zbl0643.68026 MR912717 · Zbl 0643.68026
[18] 18. Z. MANNA and P. WOLPER, Synthesis of Communicating Process from Temporal Logic Specifications, A.C.M. Trans. Prog. Lang. Syst., 1984, 6, pp. 68-93. Zbl0522.68030 · Zbl 0522.68030 · doi:10.1145/357233.357237
[19] 19. A. MASINI, I Sistemi di Interazione: una proposta di formalizzazione logico-temporale e di realizzazione semanticamente corretta, Tesi di Laurea in Scienze dell’Informazione,Università di Pisa, 1986.
[20] 20. V. NGUYEN, A. DEMERS, D. GRIES and S. OWICKI, A Model and Temporal Proof System for Networks of Processes, Distributed Computing, 1986, 1, pp. 7-25. Zbl0598.68025 · Zbl 0598.68025 · doi:10.1007/BF01843567
[21] 21. H. F. WEDDE, An Iterative and Starvation-Free Solution for a General Class of Distributed Control Problems Based on Interaction Primitives, Theoret. Comput. Sci., 1983, 24, pp. 1-20. Zbl0511.68013 MR707645 · Zbl 0511.68013 · doi:10.1016/0304-3975(83)90127-5
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.