@inproceedings{fff5e180d704435b91874b8c172272b0,
title = "On the fly model-checking of TPN: TCTLΔh",
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Δ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Δ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.",
keywords = "Complexity, Decidability, Model checking, TCTL, Time constraints, Time petri nets, TPN-TCTL",
author = "Naima Jbeli and Zohra Sbai and \{Ben Ayed\}, Rahma",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG, part of Springer Nature 2018.; 6th World Conference on Information Systems and Technologies, WorldCIST 2018 ; Conference date: 27-03-2018 Through 29-03-2018",
year = "2018",
doi = "10.1007/978-3-319-77712-2\_42",
language = "English",
isbn = "9783319777115",
series = "Advances in Intelligent Systems and Computing",
publisher = "Springer Verlag",
pages = "441--451",
editor = "Reis, \{Luis Paulo\} and Alvaro Rocha and Sandra Costanzo and Hojjat Adeli",
booktitle = "Trends and Advances in Information Systems and Technologies",
address = "Germany",
}