Abstract— Several techniques have been proposed for symbolic enumeration and analysis of the state space of reactive systems with non-deterministic temporal parameters taking values within a dense domain. In a large part of these techniques, the state space is covered by collecting states within equivalence classes each comprised of a discrete logical location and a dense variety of clock valuations encoded as a Difference Bounds Matrix (DBM). The reachability relation among such classes enables qualitative verification of properties pertaining the ordering of events along critical runs and the satisfaction of stimulus/response deadlines. However, up to now, no results have been proposed which extend state class enumeration so as to combine the veri- fication of the possibility of critical behaviors with a quantitative evaluation of their probability. In this paper, we extend the concept of equivalence classes based on DBM encoding with a density function which provides a measure for the probability associated with individual states collected in the class itself. To this end, we extend the formalism of Time Petri Nets by associating the static firing interval of each transition with a probability density function. We then expound how this probabilistic information determines a probability for the states collected within a class and how this probability evolves in the enumeration of the reachability relation among state classes. This opens the way to characterizing the possibility of critical behaviors with a quantitative measure of probability.

INTRODUCING PROBABILITY WITHIN STATE CLASS ANALYSIS OF DENSE-TIME-DEPENDENT SYSTEMS / G. BUCCI; E. VICARIO; R. PIOVOSI; L. SASSOLI. - STAMPA. - (2005), pp. 13-22. ((Intervento presentato al convegno QEST 2005 tenutosi a TORINO [10.1109/QEST.2005.17].

INTRODUCING PROBABILITY WITHIN STATE CLASS ANALYSIS OF DENSE-TIME-DEPENDENT SYSTEMS

BUCCI, GIACOMO;VICARIO, ENRICO;
2005

Abstract

Abstract— Several techniques have been proposed for symbolic enumeration and analysis of the state space of reactive systems with non-deterministic temporal parameters taking values within a dense domain. In a large part of these techniques, the state space is covered by collecting states within equivalence classes each comprised of a discrete logical location and a dense variety of clock valuations encoded as a Difference Bounds Matrix (DBM). The reachability relation among such classes enables qualitative verification of properties pertaining the ordering of events along critical runs and the satisfaction of stimulus/response deadlines. However, up to now, no results have been proposed which extend state class enumeration so as to combine the veri- fication of the possibility of critical behaviors with a quantitative evaluation of their probability. In this paper, we extend the concept of equivalence classes based on DBM encoding with a density function which provides a measure for the probability associated with individual states collected in the class itself. To this end, we extend the formalism of Time Petri Nets by associating the static firing interval of each transition with a probability density function. We then expound how this probabilistic information determines a probability for the states collected within a class and how this probability evolves in the enumeration of the reachability relation among state classes. This opens the way to characterizing the possibility of critical behaviors with a quantitative measure of probability.
QEST 2005
TORINO
G. BUCCI; E. VICARIO; R. PIOVOSI; L. SASSOLI
File in questo prodotto:
File Dimensione Formato  
Quest 2005.pdf

accesso aperto

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Open Access
Dimensione 596.64 kB
Formato Adobe PDF
596.64 kB Adobe PDF Visualizza/Apri

I documenti in FLORE 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: http://hdl.handle.net/2158/18240
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 4
social impact