Semi-Markov Stochastic Petri Nets (SM-SPNs) are a high-level formalism for defining semi-Markov processes. We present an extended Continuous Stochastic Logic (eCSL) which provides an expressive way to articulate performance queries at the SM-SPN model level. eCSL supports queries involving steady-state, transient and passage time measures. We demonstrate this by formulating and answering eCSL queries on an SM-SPN model of a distributed voting system with up to 107 states.
Citation:
Jeremy T. Bradley, Nicholas J. Dingle, Peter G. Harrison, William J. Knottenbelt, "Performance Queries on Semi-Markov Stochastic Petri Nets with an Extended Continuous Stochastic Logic," pnpm, pp.62, 10th International Workshop on Petri Nets and Performance Models (PNPM '03), 2003