Skip to main content
SpringerLink
Log in
Book cover

Annual Asian Computing Science Conference

ASIAN 1999: Advances in Computing Science — ASIAN’99 pp 126–138Cite as

An Expressive Extension of TLC

Extended Abstract

  • Conference paper
  • First Online:

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

Abstract

A temporal logic of causality (TLC) was introduced by Alur, Penczek and Peled in [1]. It is basically a linear time temporal logic interpreted over Mazurkiewicz traces which allows quantification over causal chains. Through this device one can directly formulate causality properties of distributed systems. In this paper we consider an extension of TLC by strengthening the chain quantification operators. We show that our logic TLC* adds to the expressive power of TLC. We do so by defining an Ehrenfeucht-Fraïssé game to capture the expressive power of TLC. We then exhibit a property and by means of this game prove that the chosen property is not definable in TLC. We then show that the same property is definable in TLC*. We prove in fact the stronger result that TLC* is expressively stronger than TLC exactly when the dependency relation associated with the underlying trace alphabet is not transitive.

Part of this work was done at Lehrstuhl für Informatik VII, RWTH Aachen, Germany

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Peled, D., Penczek, W.: Model checking of causality properties. Proceedings of LICS’95, IEEE Computer Society Press (1995) 90–100

    Google Scholar 

  2. Clarke, E. M., Emerson, E. A., Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2) (1986) 244–263

    Article  MATH  Google Scholar 

  3. Diekert, V., Gastin, P.: An expressively complete temporal logic without past tense operators for Mazurkiewicz traces. Proceedings of CSL’99, LNCS 1683, Springer-Verlag (1999)

    Google Scholar 

  4. Diekert, V., Rozenberg, G. (eds.): The book of traces. World Scientific (1995)

    Google Scholar 

  5. Etessami, K., Wilke, Th.: An until hierarchy for temporal logic. Proceedings of LICS’96, IEEE Computer Society Press (1996) 108–117

    Google Scholar 

  6. Godefroid, P.: Partial-order methods for the verification of concurrent systems. LNCS 1032, Springer-Verlag (1996)

    Google Scholar 

  7. Henriksen, J. G.: An Expressive Extension of TLC. Technical report RS-99-26, BRICS, Department of Computer Science, University of Aarhus (1999)

    Google Scholar 

  8. Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Report PB-78, Department of Computer Science, University of Aarhus, Denmark (1977)

    Google Scholar 

  9. Niebert, P.: A temporal logic for the specification and validation of distributed behaviour. Ph.D. thesis, University of Hildesheim (1997)

    Google Scholar 

  10. Peled, D.: Partial order reduction: model checking using representatives. Proceedings of MFCS’96, LNCS 1113, Springer-Verlag (1996) 93–112

    Google Scholar 

  11. Pnueli, A.: The temporal logic of programs. Proceedings of FOCS’77, IEEE Computer Society Press (1977) 46–57

    Google Scholar 

  12. Ramanujam, R.: Locally linear time temporal logic. Proceedings of LICS’96, IEEE Computer Society Press (1996) 118–127

    Google Scholar 

  13. Thiagarajan, P. S.: A trace based extension of linear time temporal logic. Proceedings of LICS’94, IEEE Computer Society Press (1994) 438–447

    Google Scholar 

  14. Thiagarajan, P. S., Henriksen, J. G.: Distributed versions of linear time temporal logic: A trace perspective. In Reisig and Rozenberg (Eds.), Lectures on Petri Nets I: Basic Models, LNCS 1491, Springer-Verlag (1998) 643–681

    Google Scholar 

  15. Thiagarajan, P. S., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces. Proceedings of LICS’97, IEEE Computer Society Press (1997) 183–194

    Google Scholar 

  16. Walukiewicz, I.: on the complexity of LTrL (extended abstract). Proceedings of ICALP’98, LNCS 1443, Springer-Verlag (1998) 140–151

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Aarhus, Denmark

    Jesper Gulmann Henriksen

Authors
  1. Jesper Gulmann Henriksen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Chennai Mathematical Institute, 92 G.N. Chetty Road, T. Nagar, Chennai, 600 017, India

    P. S. Thiagarajan

  2. School of Computing, National University of Singapore, Lower Kent Ridge Road, Singapore, 119260

    Roland Yap

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Henriksen, J.G. (1999). An Expressive Extension of TLC. In: Thiagarajan, P.S., Yap, R. (eds) Advances in Computing Science — ASIAN’99. ASIAN 1999. Lecture Notes in Computer Science, vol 1742. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46674-6_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-46674-6_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66856-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation