Fortuna: Model Checking Priced Probabilistic Timed Automata

Abstract

Fortuna is the first tool for model checking priced probabilistic timed automata (PPTAs). PPTAs are an important model that can handle the combination of real-time, probabilistic and cost features. Only model checkers that incorporate all these features can address the key design trade-offs that arise in many practical applications such as: 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), by having cost-rates and discrete cost increments on states. Fortuna is able to compute the maximal probability by which a class of states can be reached under a certain cost-bound (and time bound.) Although the problem is undecidable in general, there exists a semi-algorithm that produces a non-decreasing sequence of maximal probabilities. This paper enhances that algorithm. We compared the performance of Fortuna with existing approaches for PTAs. Surprisingly, although PPTAs are more general, our techniques exhibit superior performance.