On the Fly Model-Checking of TPN: \(TPN-TCTL^{\varDelta }_{h}\)

  • Naima Jbeli
  • Zohra Sbai
  • Rahma Ben Ayed
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 746)


Temporal logic provides a fundamental framework for formally specifying systems and reasoning about them. Furthermore, model checking techniques lead to the automatic verification of some temporal logic specification that a finite state model of a system should satisfy.

In this paper, we adapt the extended logic \(TCTL^{\varDelta }_{h}\); presented in our previous work [9, 10]; to deal with GMECs (Generalized Mutual Exclusion Constraints: specification of Petri net markings) instead of atomic properties. This leads to an extension of TCTL (Timed Computational Tree Logic) on time Petri nets (TPN) called \(TPN-TCTL^{\varDelta }_{h}\). Then, we prove the PSPACE-completeness of this new logic on bounded TPNs. Finally, we propose symbolic verification algorithms which are based on the concept of on the fly verification and implement them using Romeo tool.


Time constraints Time Petri nets Model checking TPN-TCTL \(TCTL^{\varDelta }_{h}\) Decidability Complexity 


  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. (TCS) 126, 183–235 (1994)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time Petri nets. J. Logic Comput. 19, 1509–1540 (2009)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Gardey, G., Lime, D., Magnin, M., Roux, O.(H.): Romeo: a tool for analyzing time Petri nets. In: 17th International Conference on Computer Aided Verification (CAV 2005), vol. 3576, pp. 418–423 (2005)CrossRefGoogle Scholar
  5. 5.
    Gardey, G., Roux, O.H., Roux, O.F.: Using zone graph method for computing the state space of a time Petri net. In: vol. 2791 of LNCS, pp. 24–259. Springer, Heidelberg (2003)Google Scholar
  6. 6.
    Giua, A., DiCesare, F., Silva, M.: Generalized mutual exclusion constraints on nets with uncontrollable transitions. In: IEEE International Conference on SMC (1992)Google Scholar
  7. 7.
    Hadjidj, R., Boucheneb, H.: On the fly TCTL model checking for time Petri nets. Theoret. Comput. Sci. 410(42), 4241–4261 (2009)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)Google Scholar
  9. 9.
    Jbeli, N., Sbaï, Z., Ben Ayed. R.: \(TCTL^{\Delta }_{h}\) for quantitative verification of information systems. In: 4th International Workshop on Advanced Information Systems for Enterprises (IWAISE 2016) (2016)Google Scholar
  10. 10.
    Jbeli, N., Sbaï, Z., Ben Ayed, R.: On expressiveness of \(TCTL^{\Delta }_{h}\) for model checking distributed systems. In: 8th International Conference on Computational Collective Intelligence (ICCCI 2016), pp. 323–332 (2016)CrossRefGoogle Scholar
  11. 11.
    Laroussinie, F.: Model checking temporisé: algorithmes efficaces et complexité. Master’s thesis, ENSCachan, Décembre 2005Google Scholar
  12. 12.
    Lime, D., Roux, O.H.: Model checking of time Petri nets using the state class timed automaton. Discrete Events Dyn. Syst. (DEDS) 16(2), 179–205 (2006)MathSciNetCrossRefGoogle Scholar
  13. 13.
    LSV. Dossier scientifique. Ecole Normale Supérieure de Cachan (2004)Google Scholar
  14. 14.
    Mokadem, H.B., Bérard, B., Bouyer, P., Laroussinie, F.: Timed temporal logics for abstracting transient states. In: 4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006), vol. 4218, pp. 337–351 (2006)CrossRefGoogle Scholar
  15. 15.
    Sbaï, Z., Barkaoui, K., Boucheneb, H.: Compatibility analysis of time open workflow nets. In: Proceedings of the International Workshop on Petri Nets and Software Engineering, co-located with 35th International Conference on Application and Theory of Petri Nets and Concurrency (PetriNets 2014) and 14th International Conference on Application of Concurrency to System Design (ACSD 2014), Tunis, Tunisia, 23–24 June 2014, pp. 249–268 (2014)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.RISC, ENITTunis El Manar UniversityTunisTunisia
  2. 2.College of Computer Engineering and SciencePrince Sattam Bin Abdulaziz UniversityAl-KharjKingdom of Saudi Arabia

Personalised recommendations