RT Journal Article
T1 Implementation relations for stochastic finite state machines
A1 García Merayo, María De Las Mercedes
A1 Núñez García, Manuel
A1 Rodríguez Laguna, Ismael
AB We present a timed extension of the classical finite state machines model where time is introduced in two ways. On the one hand, timeouts can be specified, that is, we can express that if an input action is not received before a fix amount of time then the machine will change its state. On the other hand, we can associate time with the performance of actions. In this case, time will be given by means of random variables. Intuitively, we will not have conditions such as "the action a takes t time units to be performed" but conditions such as "the action a will be completed before time t with probability p." In addition to introducing the new language, we present several conformance relations to relate implementations and specifications that are defined in terms of our new notion of stochastic finite state machine.
PB Springer Verlag
SN 0302-9743
YR 2006
FD 2006
LK https://hdl.handle.net/20.500.14352/50035
UL https://hdl.handle.net/20.500.14352/50035
LA eng
NO Formal methods and stochastic models for performance evaluation. 3rd European Performance Engineering Workshop. JUN 21-22, 2006. Budapest, HUNGARY.
NO MCYT
NO Junta de Castilla-La Mancha
NO Marie Curie
DS Docta Complutense
RD 8 abr 2025