Skip to main content
SpringerLink
Log in

A product version of dynamic linear time temporal logic

  • Invited Talks
  • Conference paper
  • First Online:
Book cover CONCUR '97: Concurrency Theory (CONCUR 1997)

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

Included in the following conference series:

Abstract

We present here a linear time temporal logic which simultaneously extends LTL, the propositional temporal logic of linear time, along two dimensions. Firstly, the until operator is strengthened by indexing it with the regular programs of propositional dynamic logic (PDL). Secondly, the core formulas of the logic are decorated with names of sequential agents drawn from fixed finite set. The resulting logic has a natural semantics in terms of the runs of a distributed program consisting of a finite set of sequential programs that communicate by performing common actions together. We show that our logic, denoted DLTL⊗, admits an exponential time decision procedure. We also show that DLTL⊗ is expressively equivalent to the so called regular product languages. Roughly speaking, this class of languages is obtained by starting with synchronized products of (ω-)regular languages and closing under boolean operations. We also sketch how the behaviours captured by our temporal logic fit into the framework of labelled partial orders known as Mazurkiewicz traces.

Part of this work was done while visiting BRICS. Part of this work has been supported by IFCPAR Project 1502-1.

Basic Research in Computer Science, Centre of the Danish National Research Foundation.

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. Fischer, M. J., Ladner, R. E.: Prepositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2) (1979) 194–211

    Article  Google Scholar 

  2. Gabbay, A., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. Proceedings of the 7th Annual Symposium on Principles of Programming Languages, ACM (1980) 163–173

    Google Scholar 

  3. Godefroid, P.: Partial-order Methods for the Verification of Concurrent Systems. Lecture Notes in Computer Science 1032, Springer-Verlag (1996)

    Google Scholar 

  4. Harel, D.: Dynamic logic. In Gabbay, D., Guenthner, F., eds.: Handbook of Philosophical Logic, Vol. II, Reidel, Dordrecht (1984) 497–604

    Google Scholar 

  5. Henriksen, J. G., Thiagarajan, P. S.: Dynamic linear time temporal logic. BRICS technical report RS-97-8, Department of Computer Science, University of Aarhus, Denmark (1997)

    Google Scholar 

  6. Hromkovič, J., Seibert, S., Wilke, T.: Translating regular expressions into small ε-free nondeterministic automata. Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 1200, Springer-Verlag (1997) 55–66

    Google Scholar 

  7. Kamp, H. R.: Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California (1968)

    Google Scholar 

  8. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems (Specification), Springer-Verlag (1992)

    Google Scholar 

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

    Google Scholar 

  10. McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9 (1966) 521–530

    Google Scholar 

  11. Mukund, M., Thiagarajan, P. S.: Linear time temporal logics over Mazurkiewicz traces. Proceedings of the 21st Intl. Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) pp. 62–92

    Google Scholar 

  12. Peled, D.: Partial order reduction: model checking using representatives. Proceedings of the 21st Intl. Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) 93–112

    Google Scholar 

  13. Pnueli, A.: The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE (1977) 46–57

    Google Scholar 

  14. Thiagarajan, P. S.: A trace based extension of linear time temporal logic. Proceedings of the 9th Annual Symposium on Logic in Computer Science, IEEE (1994) 438–447

    Google Scholar 

  15. Thiagarajan, P. S.: PTL over product state spaces. Technical report TCS-95-4, School of Mathematics, SPIC Science Foundation, Madras (1995)

    Google Scholar 

  16. Thiagarajan, P. S.: A trace consistent subset of PTL. Proceedings of the 6th Annual Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag (1995) 438–452

    Google Scholar 

  17. Thomas, W.: Automata over infinite objects. In van Leeuwen, J., ed., Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, Elsevier/MIT Press (1990) 133–191

    Google Scholar 

  18. Valmari, A.: A stubborn attack on state explosion. Formal Methods in Systems Design 1 (1992) 285–313

    Google Scholar 

  19. Vardi, M. Y., Wolper, P.: An automata-theoretic approach to automatic program verification. Proceedings of the 1st Annual Symposium on Logic in Computer Science, IEEE (1986) 332–345

    Google Scholar 

  20. Wolper, P.: Temporal logic can be more expressive. Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, IEEE (1981) 340–348

    Google Scholar 

  21. Wolper, P., Vardi, M. Y., Sistla, A. P.: Reasoning about infinite computation paths. Proceedings of the 24nd Annual Symposium on Foundations of Computer Science, IEEE (1983) 185–194

    Google Scholar 

  22. Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. Informatique Théorique et Applications 21 (1987) 99–135

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Jesper G. Henriksen

  2. SPIC Mathematical Institute, Madras, India

    P. S. Thiagarajan

Authors
  1. Jesper G. Henriksen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. S. Thiagarajan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Antoni Mazurkiewicz Józef Winkowski

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Henriksen, J.G., Thiagarajan, P.S. (1997). A product version of dynamic linear time temporal logic. In: Mazurkiewicz, A., Winkowski, J. (eds) CONCUR '97: Concurrency Theory. CONCUR 1997. Lecture Notes in Computer Science, vol 1243. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63141-0_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-63141-0_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-69188-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation