Advertisement

Safety and Liveness Properties for Real Traces and a Direct Translation from LTL to Monoids

  • Volker Diekert
  • Paul Gastin
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2300)

Abstract

For infinite words there are well-known characterizations of safety and liveness properties. We extend these results to real Mazurkiewicz traces. This is possible due to a result, which has been established recently: Every first-order definable real trace language is definable in linear temporal logic using future tense operators, only. We show that the canonical choice for a topological characterization of safety and liveness properties is given by the Scott topology. In this paper we use an algebraic approach where we work with aperiodic monoids. Therefore we also give a direct translation from temporal logic to aperiodic monoids which is of independent interest.

Keywords

Mazurkiewicz traces temporal logics safety and liveness properties concurrency aperiodic monoids 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    IJ. J. Aalbersberg and G. Rozenberg. Theory of Traces. Theoretical Computer Science, 60:1–82, 1988.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    B. Alpern and F.B. Schneider. Defining Liveness. Information Processing Letters, 21:181–185, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    B. Alpern and F.B. Schneider. Recognizing Safety and Liveness. Distributed Computing, 2:117–126, 1987.zbMATHCrossRefGoogle Scholar
  4. 4.
    R. Alur, D. Peled, and W. Penczek. Model-Checking of Causality Properties. In Proceedings of LICS’95, pages 90–100, 1995.Google Scholar
  5. 5.
    E. Chang, Z. Manna, and A. Pnueli. Characterization of Temporal Property Classes. In W. Kuich, Editor, Proceedings of the 19th International Colloquium on Automata, Languages and Programming (ICALP’92), Vienna, volume 623 of Lecture Notes in Computer Science, pages 474–486, Berlin-Heidelberg-New York, 1992. Springer.Google Scholar
  6. 6.
    C. Choffrut. Combinatorics in Trace Monoids I. In V. Diekert and G. Rozenberg, Editors, The Book of Traces, chapter 3, pages 71–82. World Scientific, Singapore, 1995.Google Scholar
  7. 7.
    V. Diekert and P. Gastin. LTL Is Expressively Complete for Mazurkiewicz Traces. In U. M. et al., Editor, Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP’00), Geneva, number 1853 in Lecture Notes in Computer Science, pages 211–222. Springer, 2000.Google Scholar
  8. 8.
    V. Diekert and G. Rozenberg, Editors. The Book of Traces. World Scientific, Singapore, 1995.Google Scholar
  9. 9.
    W. Ebinger. Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. Dissertation, Institut für Informatik, Universität Stuttgart, 1994.Google Scholar
  10. 10.
    W. Ebinger and A. Muscholl. Logical Definability on Infinite Traces. Theoretical Computer Science, 154:67–84, 1996. A preliminary version appeared in Proceedings of the 20th International Colloquium on Automata, Languages and Programming (ICALP’93), Lund (Sweden) 1993, Lecture Notes in Computer Science 700, 1993.Google Scholar
  11. 11.
    A. Ehrenfeucht, H.J. Hoogeboom, and G. Rozenberg. Combinatorial Properties of Dependence Graphs. Information and Computation, 114(2):315–328, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    A. Ehrenfeucht and G. Rozenberg. On the Structure of Dependence Graphs. In K. Voss, H.J. Genrich, and G. Rozenberg, Editors, Concurrency and Nets, pages 141–170, Berlin-Heidelberg-New York, 1987. Springer.Google Scholar
  13. 13.
    D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the Temporal Analysis of Fairness. In Conference Record of the 12th ACM Symposium on Principles of Programming Languages, pages 163–173, Las Vegas, Nev., 1980.Google Scholar
  14. 14.
    P. Gastin and A. Petit. Infinite Traces. In V. Diekert and G. Rozenberg, Editors, The Book of Traces, chapter 11, pages 393–486. World Scientific, Singapore, 1995.Google Scholar
  15. 15.
    P. Gastin, A. Petit, and W. Zielonka. An Extension of Kleene’s and Ochmański’s Theorems to Infinite Traces. Theoretical Computer Science, 125:167–204, 1994. A preliminary version was presented at ICALP’91, Lecture Notes in Computer Science 510 (1991).Google Scholar
  16. 16.
    G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer, Berlin-Heidelberg-New York, 1980.zbMATHGoogle Scholar
  17. 17.
    G. Guaiana, A. Restivo, and S. Salemi. Star-Free Trace Languages. Theoretical Computer Science, 97:301–311, 1992. A preliminary version was presented at STACS’91, Lecture Notes in Computer Science 480 (1991).Google Scholar
  18. 18.
    H.J. Hoogeboom and G. Rozenberg. Dependence Graphs. In V. Diekert and G. Rozenberg, Editors, The Book of Traces, chapter 2, pages 43–67. World Scientific, Singapore, 1995.Google Scholar
  19. 19.
    R.M. Keller. Parallel Program Schemata and Maximal Parallelism I. Fundamental Results. Journal of the Association for Computing Machinery, 20(3):514–537, 1973.zbMATHMathSciNetGoogle Scholar
  20. 20.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, 1991.Google Scholar
  21. 21.
    A. Mazurkiewicz. Concurrent Program Schemes and Their Interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.Google Scholar
  22. 22.
    M. Mukund and P.S. Thiagarajan. Linear Time Temporal Logics over Mazurkiewicz Traces. In Proceedings of the 21th MFCS, 1996, number 1113 in Lecture Notes in Computer Science, pages 62–92. Springer, 1996.Google Scholar
  23. 23.
    P. Niebert. A v-calculus with Local Views for Sequential Agents. In Proceedings of the 20th MFCS, 1995, number 969 in Lecture Notes in Computer Science, pages 563–573. Springer, 1995.Google Scholar
  24. 24.
    W. Penczek. Temporal Logics for Trace Systems: On Automated Verification. International Journal of Foundations of Computer Science, 4:31–67, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    R. Ramanujam. Locally Linear Time Temporal Logic. In Proceedings of LICS’96, Lecture Notes in Computer Science, pages 118–128, 1996.Google Scholar
  26. 26.
    G. Rozenberg. Behaviour of Elementary Net Systems. In W. Brauer, Editor, Petri Nets: Central Models and Their Properties; Advances in Petri Nets; Proceedings of an Advanced Course, Bad Honnef, 8.–19. Sept. 1986, Vol. 1, number 254 in Lecture Notes in Computer Science, pages 60–94, Berlin-Heidelberg-New York, 1986. Springer.Google Scholar
  27. 27.
    G. Rozenberg and P.S. Thiagarajan. Petri Nets: Basic Notions, Structure and Behaviour. Number 224 in Lecture Notes in Computer Science, pages 585–668, Berlin-Heidelberg-New York, 1986. Springer.Google Scholar
  28. 28.
    P.S. Thiagarajan. A Trace Based Extension of Linear Time Temporal Logic. In Proceedings of LICS’94, pages 438–447, 1994.Google Scholar
  29. 29.
    P.S. Thiagarajan. A Trace Consistent Subset of PTL. In Proceedings of CONCUR’95, number 962 in Lecture Notes in Computer Science, pages 438–452, 1995.Google Scholar
  30. 30.
    P.S. Thiagarajan and I. Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. In Proceedings of LICS’97, 1997.Google Scholar
  31. 31.
    I. Walukiewicz. Difficult Configurations — on the Complexity of LTrL. In K. G. Larsen et al., Editors, Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP’98), Aalborg, number 1443 in Lecture Notes in Computer Science, pages 140–151, Berlin-Heidelberg-New York, 1998. Springer.Google Scholar
  32. 32.
    I. Walukiewicz. Local Logics for Traces. Journal of Automata, Languages and Combinatorics, 2001. To appear.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Volker Diekert
    • 1
  • Paul Gastin
    • 2
  1. 1.Inst. für InformatikUniversität StuttgartStuttgart
  2. 2.LIAFAUniversité ParisParis Cedex 05

Personalised recommendations