Probabilistic State Automata

Description Definition Examples References

Description: This is clearly an abuse of the notation and needs a better name. Probabilistic State Automata here are defined as STA such that all transitions are actually deterministic, i.e. all transition probabilities p(s’; s, e’) are either 0 or 1. The only probabilistic feature remaining is the stochastic clock structure (which is clumsily reflected in the name). Formal Definition: A Probabilistic Timed Automaton (STA) is a six-tuple (E, X, Γ, f, X0, G) where E – is a finite set of events (here we mean event types) X – is a countable set of states Γ(x) – is a set of enabled events defined for all x, x’ ∈X, with Γ(x) a subset of E, f – is a state transition function, defined for all x, x’ ∈X, e’∈E. X0 – is initial state. G={Gi : i∈E} – is a stochastic clock structure – a set of distribution functions. Examples: See Stochastic Timed Automata (STA). References: