Symbolic model checking is a powerful technique for checking temporal logic properties over finite operational models. Recently, symbolic model checking has been extended to timed models to check temporal properties of real-time system. Real-time extensions of symbolic model checking require the description of the state space of the system to be analyzed in specific forms of timed graphs. This paper presents a symbolic model checking algorithm for analyzing specifications of real-time systems expressed in an intuitive and popular model, namely timed Petri nets. The algorithm proposed in this paper checks the validity of properties expressed in TCTL on the time reachability graph of timed Petri nets. A realistic example illustrates how the algorithm proposed in this paper can be successfully used in practical applications despite the worst case computational complexity

Symbolic Model Checking for Timed Petri Nets

1997

Abstract

Symbolic model checking is a powerful technique for checking temporal logic properties over finite operational models. Recently, symbolic model checking has been extended to timed models to check temporal properties of real-time system. Real-time extensions of symbolic model checking require the description of the state space of the system to be analyzed in specific forms of timed graphs. This paper presents a symbolic model checking algorithm for analyzing specifications of real-time systems expressed in an intuitive and popular model, namely timed Petri nets. The algorithm proposed in this paper checks the validity of properties expressed in TCTL on the time reachability graph of timed Petri nets. A realistic example illustrates how the algorithm proposed in this paper can be successfully used in practical applications despite the worst case computational complexity
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/1459
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact