Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. (TCS) 126, 183–235 (1994)
Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time Petri nets. J. Logic Comput. 19, 1509–1540 (2009)
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)
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)
Giua, A., DiCesare, F., Silva, M.: Generalized mutual exclusion constraints on nets with uncontrollable transitions. In: IEEE International Conference on SMC (1992)
Hadjidj, R., Boucheneb, H.: On the fly TCTL model checking for time Petri nets. Theoret. Comput. Sci. 410(42), 4241–4261 (2009)
Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
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)
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)
Laroussinie, F.: Model checking temporisé: algorithmes efficaces et complexité. Master’s thesis, ENSCachan, Décembre 2005
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)
LSV. Dossier scientifique. Ecole Normale Supérieure de Cachan (2004)
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)
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)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Jbeli, N., Sbai, Z., Ben Ayed, R. (2018). On the Fly Model-Checking of TPN: \(TPN-TCTL^{\varDelta }_{h}\). In: Rocha, Á., Adeli, H., Reis, L., Costanzo, S. (eds) Trends and Advances in Information Systems and Technologies. WorldCIST'18 2018. Advances in Intelligent Systems and Computing, vol 746. Springer, Cham. https://doi.org/10.1007/978-3-319-77712-2_42
Download citation
DOI: https://doi.org/10.1007/978-3-319-77712-2_42
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-77711-5
Online ISBN: 978-3-319-77712-2
eBook Packages: EngineeringEngineering (R0)