Fortuna: Model Checking Priced Probabilistic Timed Automata

We introduce Fortuna, the first tool for model checking priced probabilistic timed automata (PPTAs). Fortuna can handle the combination of real-time, probabilistic and cost features, which is required for addressing key design trade-offs that arise in many practical applications. For example the Zeroconf, Bluetooth, IEEE802.11 and Firewire protocols, protocols for sensor networks, and scheduling problems with failures. PPTAs are an extension of probabilistic timed automata (PTAs) with cost-rates and discrete cost increments on states. Fortuna is able to compute the maximal probability by which a state can be reached under a certain cost-bound (and time-bound). Although this problem is undecidable in general, there exists a semi-algorithm that produces a non-decreasing sequence of probabilities converging to the maximum. This paper presents a number of crucial optimizations of that algorithm. Since PPTAs are PTAs with trivial cost parameters, we were able to compare the performance of F...

• Type: Journal
• Year: 2010
• Where: QEST
• Authors: Jasper Berendsen, David N. Jansen, Frits W. Vaandrager
• Keywords: Fortuna, Key Design Trade-offs, Modeling And Simulation, Probabilistic, QEST 2010