Skip to main content
WorldCist'18 - 6th World Conference on Information Systems and Technologies

Full Program »

On the fly model-checking of TPN: $TPN-TCTL^{\Delta}_{h}$

Temporal logic provides a fundamental framework for formally specifying systems and reasoning about them. Furthermore, model cheking 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^{\Delta}_{h}$; presented in our previous work; to deal with GMECs (specification of Petri net markings) instead of atomic properties. This leads to an extension of TCTL on TPNs called $TPN-TCTL^{\Delta}_{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.

Naima JBELI
ENIT
Tunisia

Zohra SBAI
ENIT
Tunisia

Rahma BEN AYED
ENIT
Tunisia

 

Powered by OpenConf®
Copyright ©2002-2017 Zakon Group LLC