Skip to main content
SpringerLink
Log in

A hierarchy of partial order temporal properties

  • Conference paper
  • First Online:
Temporal Logic (ICTL 1994)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 827))

Included in the following conference series:

Abstract

We propose a classification of partial order temporal properties into a hierarchy, which is a generalization of the safety-progress hierarchy of Chang, Manna and Pnueli. The classes of the hierarchy are characterized through three views: language-theoretic, topological and temporal. Instead of the domain of strings, we take the domain of Mazurkiewicz traces as a basis for our considerations. For the language-theoretic view, we propose operations on trace languages which define the four main classes of properties: safety, guarantee, persistence and response. These four classes are shown to correspond precisely to the two lower levels of the Borel hierarchy of the Scott topology of the domain of traces relativized to the infinite traces. In addition, a syntactic characterization of the classes is provided in terms of a sublogic of the Generalized Interleaving Set Temporal Logic GISTL (an extension of ISTL).

Supported in part by CEC grant CIPA3510PL927369. Visiting Academic at the Department of Computing, Imperial College, for the duration of the Nuffield Science Foundation Fellowship SCI/124/528/G.

On leave from Institute of Computer Science, PAS, Warsaw, Poland. Supported in part by CEC grant CIPA3510PL927370 and by the Polish grant No. 2 2047 9203.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181–185, 1985.

    Article  Google Scholar 

  2. E. Chang, Z. Manna, and A. Pnueli A Hierarchy of Temporal Properties. Stanford University, Technical Report.

    Google Scholar 

  3. V. Diekert. On the concatenation of infinite traces. In Choffrut C. et al., editors, Proceedings of the 8th Annual Symposium on Theoretical Aspects of Computer Science (STACS'91), Hamburg 1991, number 480 in Lecture Notes in Computer Science, pages 105–117, Berlin-Heidelberg-New York, 1991. Springer. To appear 1993 in Theoret. Comput. Sci.

    Google Scholar 

  4. V. Diekert and A. Muscholl. Deterministic asynchronous automata for infinite traces. In P. Enjalbert, A. Finkel, and K. W. Wagner, editors, Proceedings of the 10th Annual Symposium on Theoretical Aspects of Computer Science (STACS'93), Würzburg 1993, number 665 in Lecture Notes in Computer Science, pages 617–628, Berlin-Heidelberg-New York, 1993. Springer.

    Google Scholar 

  5. P. Gastin and A. Petit. Asynchronous automata for infinite traces. In W. Kuich, editor, Proceedings of the 19th International Colloquium on Automata Languages and Programming (ICALP'92), Vienna (Austria) 1992, number 623 in Lecture Notes in Computer Science, pages 583–594, Berlin-Heidelberg-New York, 1992. Springer.

    Google Scholar 

  6. G. Gierz, K. Hofmann, K. Keimel, J. Lawson, M. Mislove, and D. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980.

    Google Scholar 

  7. M. Kwiatkowska. A metric for traces. Information Processing Letters, 35:129–135, 1990.

    Article  Google Scholar 

  8. M. Kwiatkowska. On the domain of traces and sequential composition. In S. Abramsky and T.S.E.. Maibaum, editors, Proceedings 16th Coll. on Trees in Algebra and Programming (CAAP'91), Brighton (UK), number 493 in Lecture Notes in Computer Science, pages 42–56, Berlin-Heidelberg-New York, 1991. Springer.

    Google Scholar 

  9. M. Z. Kwiatkowska. On topological characterization of behavioural properties. In G. Reed, A. Roscoe, and R. Wachter, editors, Topology and Category Theory in Computer Science, pages 153–177. Oxford University Press, 1991.

    Google Scholar 

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

    Google Scholar 

  11. S. Katz, D. Peled. Interleaving Set Temporal Logic. Theoretical Computer Science, Vol. 75, Number 3, 21–43, also appeared in proceedings of the 6 Annual ACM Symposium on Principles of Distributed Computing, Vancouver, Canada, 178–190, 1987.

    Google Scholar 

  12. A. Mazurkiewicz. Basic notions of trace theory. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 25–34. Springer-Verlag, 1989.

    Google Scholar 

  13. Z. Manna and A. Pnueli. The anchored version of the temporal framework. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 112 of Lecture Notes in Computer Science, pages 201–284. Springer-Verlag, 1989.

    Google Scholar 

  14. Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proceedings, 9th ACM Symposium on Principles of Distributed Computing, pages 377–408. ACM Press, 1990.

    Google Scholar 

  15. Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83(1):97–139, 1991.

    Article  Google Scholar 

  16. D. Peled and A. Pnueli. Proving partial order liveness properties. Theoretical Computer Science, 1993. A preliminary version appeared in the proceedings of the 17th International Colloquium on Automata, Languages and Programming, Warwick University, England, July 1990, Lecture Notes in Computer Science 443, Springer Verlag, 553–571.

    Google Scholar 

  17. W. Penczek. Temporal logics for trace systems: On automated verification. International Journal of Foundations of Computer Science, Vol. 4 No. 1, pp. 31:67, 1993.

    Article  Google Scholar 

  18. A.P. Sistla and E. Clarke. The complexity of propositional temporal logic. In 14th ACM Symposium on Theory of Computing, pages 159–167, 1982.

    Google Scholar 

  19. A. Szalas. A complete axiomatic characterization of first-order temporal logic of linear time. Theoretical Computer Science, 54:199–214, 1987.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Math. and Comp. Science, University of Leicester, LE1 7RH, Leicester, UK

    Marta Kwiatkowska

  2. AT & T Bell Laboratories, 600 Mountain Avenue, POB 636, 07974-0636, Murray Hill, NJ, USA

    Doron Peled

  3. Department of Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB Eindhoven, The Netherlands

    Wojciech Penczek

Authors
  1. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Doron Peled
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wojciech Penczek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Dov M. Gabbay Hans Jürgen Ohlbach

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kwiatkowska, M., Peled, D., Penczek, W. (1994). A hierarchy of partial order temporal properties. In: Gabbay, D.M., Ohlbach, H.J. (eds) Temporal Logic. ICTL 1994. Lecture Notes in Computer Science, vol 827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014001

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58241-0

  • Online ISBN: 978-3-540-48585-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation