Rules for trace consistent reasoning

  • R. Ramanujam
Session I
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


Formulas of temporal logic which cannot distinguish between different interleavings of the same run are said to be trace consistent. So called partial-order methods can be applied for verification of such formulas, since checking such a property over an equivalence class of runs reduces to checking it for one representative.

In this paper, we present inference rules that typify this kind of reasoning. The rules lead us to a complete axiomatization of a linear time temporal logic, all formulas of which are trace consistent. The axiomatization is presented in a layered manner so that we can attempt to isolate the global reasoning required.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [DGP95]
    Diekert, V., Gastin, P. and Petit, A., “Rational and recognizable complex trace languages”, Information and Computation, vol 116, #1, 1995, 134–153.CrossRefGoogle Scholar
  2. [GW94]
    Godefroid, P. and Wolper, P., “A partial approach to model checking”, Information and Computation, vol 110, 1994, 305–326.CrossRefGoogle Scholar
  3. [KP92]
    Katz, S. and Peled, D., “Interleaving set temporal logic”, TCS, vol. 73, #3, 1992, 21–43.Google Scholar
  4. [P93]
    Peled, D., “All from one and one from all: on model checking using representatives”, Proc. CAV, LNCS 697, 1993, 409–423.Google Scholar
  5. [PWW96]
    Peled, D., Wilke, T. and Wolper, P., “An algorithmic approach to proving closure properties of ω-regular language”, Proc. CONCUR, LNCS 1119, 1996.Google Scholar
  6. [R96a]
    Ramanujam, R., “Locally linear time temporal logic”, Proc. IEEE LICS, 1996, 118–127.Google Scholar
  7. [R96b]
    Ramanujam, R., “Axiomatization of a partial order based temporal logic”, Bericht Nr 9605, Christian-Albrechts Universität Kiel, June 1996.Google Scholar
  8. [R96c]
    Ramanujam, R., “Trace consistency and inevitability”, Proc. FST and TCS, LNCS 1180, 1996, 250–261.Google Scholar
  9. [Ru96]
    Rushby, J., “Mechanized formal methods: progress and prospects”, Proc. FST and TCS, LNCS 1180, 1996, 43–51.Google Scholar
  10. [T94]
    Thiagarajan, P.S., “A trace based extension of propositional linear time temporal logic”, Proc. IEEE LICS, 1994, 438–447.Google Scholar
  11. [T95]
    Thiagarajan, P.S., “A trace consistent subset of PTL”, Proc. CONCUR, LNCS 962, 1995, 438–452.Google Scholar
  12. [TW97]
    Thiagarajan, P.S. and Walukiewicz, I., “An expressively complete linear time temporal logic for Mazurkiewicz traces”, Proc. IEEE LICS, 1997.Google Scholar
  13. [V90]
    Valmari, A., “A stubborn attack on state explosion”, Proc. CAV, LNCS 531, 1990, 156–165.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • R. Ramanujam
    • 1
  1. 1.The Institute of Mathematical SciencesMadrasIndia

Personalised recommendations