Intuitionistic LTL and a New Characterization of Safety and Liveness

1. Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)

   Article  Google Scholar 

2. Abadi, M., Merz, S.: An abstract account of composition. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 499–508. Springer, Heidelberg (1995)

   Chapter  Google Scholar 

3. Abadi, M., Plotkin, G.D.: A logical view of composition. Theoretical Computer Science 114, 3–30 (1993)

   Article  MathSciNet  Google Scholar 

4. Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)

   Article  MathSciNet  Google Scholar 

5. Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Computing 2(3), 117–126 (1987)

   Article  Google Scholar 

6. Davies, R.: A temporal-logic approach to binding-time analysis. In: Proceedings of the 11th IEEE Symposium on Logic in Computer Science (LICS), pp. 184–195. IEEE Computer Society Press, Los Alamitos (1996)

   Chapter  Google Scholar 

7. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)

   Chapter  Google Scholar 

8. Allen Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)

   Google Scholar 

9. Peter Gumm, H.: Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. Information Processing Letters 47(6), 291–294 (1993)

   Article  MathSciNet  Google Scholar 

10. Jonsson, B., Tsay, Y.-K.: Assumption/guarantee specifications in lineartime temporal logic. Theoretical Computer Science 167, 47–72 (1996)

    Article  MathSciNet  Google Scholar 

11. Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)

    Article  MathSciNet  Google Scholar 

12. Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

13. Maier, P.: A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning. PhD thesis, Universität des Saarlandes, Saarbrücken (July 2003)

    Google Scholar 

14. Maier, P.: Intuitionistic LTL and a new characterization of safety and liveness. Technical Report MPI-I-2004-2-002, Max-Planck-Institut für Informatik (2004)

    Google Scholar 

15. Manolios, P., Trefler, R.: Safety and liveness in branching time. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS), pp. 366–374. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

16. Manolios, P., Trefler, R.: A lattice-theoretic characterization of safety and liveness. In: Proceedings of the 22nd ACM Symposium on Principles of Distributed Computing (PODC), pp. 325–333. ACM Press, New York (2003)

    MATH  Google Scholar 

17. Plotkin, G., Stirling, C.: A framework for intuitionistic modal logics. In: Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pp. 399–406. Morgan Kaufmann, San Francisco (1986)

    Chapter  Google Scholar 

18. Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)

    Article  MathSciNet  Google Scholar 

19. Prasad Sistla, A.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing 6, 495–511 (1994)

    Article  Google Scholar 

Download references