Advertisement

On Expressiveness of TCTL\(^{\varDelta }_{h}\) for Model Checking Distributed Systems

  • Naima JbeliEmail author
  • Zohra Sbaï
  • Rahma Ben Ayed
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9875)

Abstract

Systems analysis is becoming more and more important in different fields such as network applications, communication protocols and client server applications. This importance is seen from the fact that these systems are faced to specific errors like deadlocks and livelocks which may in the major cases cause disasters. In this context, model checking is a promising formal method which permits systems analysis at early stage, thus ensuring prevention from errors occurring. In this paper, we propose an extension of timed temporal logic TCTL with more powerful modalities called \(TCTL^{\varDelta }_{h}\). This logic permits to combine in the same property clocks quantifiers as well as features for transient states. We formally define the syntax and the semantics of the proposed quantitative logic and we show via examples its expressive power.

Keywords

Distributed systems Model checking \(TCTL^{\varDelta }_{h}\) Quantitative verification 

References

  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time, 2–34 (1993). BerlinGoogle Scholar
  2. 2.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Comput. Sci. (TCS) 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–203 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Alur, R., Henzinger, T.A.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22, 181–201 (1996)CrossRefGoogle Scholar
  5. 5.
    Mokadem, H.B., Bérard, B., Bouyer, P., Laroussinie, F.: A new modality for almost everywhere properties in timed automata. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 110–124. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Bérard, B.: Model checking temporisé. In: Roux, O.H., Jard, C. (eds.) Approches formelles des systemes embarqués communicants. Hermes/Lavoisier (2008)Google Scholar
  7. 7.
    Bruyère, V., Raskin, J.F.: Real-time model-checking: parameters everywhere. Log. Methods Comput. Sci. 3(1:7) (2007)Google Scholar
  8. 8.
    Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. In: Automatic Verifiation Methods for Finite State Systems, Grenoble, France (1992)Google Scholar
  9. 9.
    Emerson, E.A., Trefler, J.R.: Parametric Quantitative Temporal Reasoning. University of Texas, USA (1999)CrossRefGoogle Scholar
  10. 10.
    Hadjidj, R., Boucheneb, H.: On-the-fly TCTL model-checking for time Petri nets. Theor. Comput. Sci. 410(42), 4241–4261 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Henzinger, T., Manna, Z., Pnueli, A.: Timed transition systems (1992)Google Scholar
  12. 12.
    Jansen, D.N., Wieringa, R.: Reducing the extensions of CTL with actions, real time. Technical report, Universiteit Twente: CTIT, Enschede, December 2000Google Scholar
  13. 13.
    Laroussinie, F.: Model checking temporisé: Algorithmes efficaces et complexité. Master’s thesis, ENSCachan, Décembre (2005)Google Scholar
  14. 14.
    Laroussinie, F., Turuani, M., Schnoebelen, P.: On the expressivity and complexity of quantitative branching-time temporal logics. Theor. Comput. Sci. 297, 297–315 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    LSV. Dossier scientifique. Ecole Normale Supérieure de Cachan (2004)Google Scholar
  16. 16.
    Mathieu, S.: Méthodes qualitatives et quantitatives pour la détection d’information cachée. Ph.D. thesis, Université Pierre et Marie Curie (2011)Google Scholar
  17. 17.
    Bel Mokadem, H.: Verification des proprietes temporisees des automates programmables industriels. Ph.D. thesis, ECOLE NORMALE SUPERIEURE DE CACHAN (2007)Google Scholar
  18. 18.
    Mokadem, H.B., Bérard, B., Bouyer, P., Laroussinie, F.: Timed temporal logics for abstracting transient states. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 337–351. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.École Nationale d’Ingénieurs de TunisUniversité de Tunis El ManarTunisTunisia

Personalised recommendations