Skip to main content
SpringerLink
Log in
Book cover

Colloquium on Trees in Algebra and Programming

CAAP 1994: Trees in Algebra and Programming — CAAP'94 pp 291–307Cite as

On projective and separable properties

  • Contributed Papers
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 787))

Abstract

A language L over the Cartesian product of component alphabets is called projective if it is closed under projections. That is, together with each word α ε L, it contains all the words that have the same projections up to stuttering as α. We prove that in each of the behavior classes: ω-regular, regular and star-free ω-regular (i.e., definable by linear temporal logic) languages, the projective languages are precisely the Boolean combinations of stuttering-closed component languages from the corresponding class. Languages of these behavior classes can also be seen as properties of various temporal logics; some uses of projective properties for specification and verification of programs are studied.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, L. Lamport, P. Wolper, Realizable and Unrealizable Concurrent Program Specifications, ICALP 1989, LNCS 372, Springer-Verlag, 1–17.

    Google Scholar 

  2. Y. Afek, G. M. Brown, M. Merritt, Lazy Caching, ACM Transactions on Programming Languages and Systems 15 (1993), 182–205.

    Article  Google Scholar 

  3. K. Apt, N. Francez, S. Katz, Appraising fairness in languages for distributed programming, Distributed Computing, Vol 2 (1988), 226–241.

    Article  Google Scholar 

  4. A. Arnold, A Syntactic congruence for Rational ω-languages, Theoretical Computer Science 39 (1985), 333–335.

    Article  Google Scholar 

  5. V. Diekert, Combinatorics on Traces, LNCS 454, Springer-Verlag, 1990.

    Google Scholar 

  6. S. Eilenberg, Automata, Languages and Machines, Vol. A, Academic Press, New York, 1974.

    Google Scholar 

  7. D. Gabbay, A. Pnueli, S. Shelah, J. Stavi, On the Temporal Analysis of Fairness, ACM Symposium on Principles of Programming Languages, 1980, 163–173.

    Google Scholar 

  8. J. E. Hopcroft, J. D. Ullman, Introduction to Automata Theory, Languages and Computation, Addison Wesley, 1979.

    Google Scholar 

  9. N. D. Jones, L.H. Landweber, Y. E. Lien, Complexity of some problems in Petri Nets, Theoretical Computer Science 4, 277–299.

    Google Scholar 

  10. S. Katz, D. Peled, Interleaving Set Temporal Logic, Theoretical Computer Science, Vol. 75, Number 3, 21–43.

    Google Scholar 

  11. S. Katz, D. Peled, Verification of Distributed Programs using Representative Interleaving Sequences, Distributed Computing (1992) 6, 107–120.

    Google Scholar 

  12. M. Z. Kwiatkowska, Fairness for Non-interleaving Concurrency, Phd. Thesis, Faculty of Science, University of Leicester, 1989.

    Google Scholar 

  13. L. Lamport, Time, clocks and the ordering of events in a distributed system, Communications of the ACM 21 (1978), 558–565.

    Google Scholar 

  14. L. Lamport, How to make a multiprocess computer that correctly executes multiprocess programs, IEEE Transactions on Computers, Vol. c-28, No. 9, 690–691.

    Google Scholar 

  15. L. Lamport, What good is temporal logic, in R.E.A. Mason (Ed.), Information Processing 83, Elsevier Science Publishers, 1983, 657–668.

    Google Scholar 

  16. O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, Proceedings of the 11th ACM Annual Symposium on Principles of Programming Languages, 1984, 97–107.

    Google Scholar 

  17. R. McNaughton, S. Papert, Counter-Free Automata, The MIT Press, 1971.

    Google Scholar 

  18. A. Nerode, Linear Automaton Transformations, Proceedings AMS 9, 541–544.

    Google Scholar 

  19. C. Papadimitiou, The Theory of Database Concurrency Control, Computer Science Press, 1986.

    Google Scholar 

  20. D. Peled, All from One, One for All: on Model Checking using Representatives, Proceedings of Computer Aided Verification 93, Elounda, Greece, LNCS 697, 609–623.

    Google Scholar 

  21. D. Peled, S. Katz, A. Pnueli, Specifying and Proving Serializability in Temporal Logic, 6th IEEE annual symposium on Logic in Computer Science, Amsterdam, The Netherlands, July 1991, 232–245.

    Google Scholar 

  22. D. Perrin, Recent Results on Automata and Infinite Words, Mathematical Foundations of Computer Science, LNCS 176, Springer Verlag 1984, 134–148.

    Google Scholar 

  23. M. P. Schützenberger, Sur les relations rationnelles functionnelles, in M. Nivat (ed.), Automata, Languages and Programming, North Holland, 103–114.

    Google Scholar 

  24. A.P. Sistla, E.M. Clarke, The Complexity of Propositional Temporal Logics, Journal of the ACM 32 (1985), 733–749.

    Article  Google Scholar 

  25. W. Thomas, Automata on Infinite Objects, in J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B, Elsvier, 133–191.

    Google Scholar 

  26. T. Wilke, An algebraic theory for regular languages of finite and infinite words, Technical report 9202, 1992, Christian-Albrechts university, Kiel, Germany.

    Google Scholar 

  27. P. Wolper, Temporal Logic Can be More Expressive, Information and Control 56 (1983), 72–99.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AT&T Bell Laboratories, 600 Mountain Avenue, 07974, Murray Hill, NJ, USA

    Doron Peled

Authors
  1. Doron Peled
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Sophie Tison

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Peled, D. (1994). On projective and separable properties. In: Tison, S. (eds) Trees in Algebra and Programming — CAAP'94. CAAP 1994. Lecture Notes in Computer Science, vol 787. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017489

Download citation

  • DOI: https://doi.org/10.1007/BFb0017489

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57879-6

  • Online ISBN: 978-3-540-48373-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation