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.

A TOOL SET FOR MODELING AND SIMULATION OF ROBOTIC WORKCELLS / G. BUCCI; E. VICARIO; F. BALDINI. - STAMPA. - (2005), pp. 106-114. ((Intervento presentato al convegno FIRB-PERF WORKSHOP TECHNIQUES, METHODOLOGIES AND TOOLS FOR PERFORMANCE EVALUATION OF COMPLEX SYSTEMS tenutosi a TORINO.

A TOOL SET FOR MODELING AND SIMULATION OF ROBOTIC WORKCELLS

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.
FIRB-PERF WORKSHOP TECHNIQUES, METHODOLOGIES AND TOOLS FOR PERFORMANCE EVALUATION OF COMPLEX SYSTEMS
TORINO
G. BUCCI; E. VICARIO; F. BALDINI
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/18241
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact