Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

QEST

2010

IEEE

2010

IEEE

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...

Related Content

Added |
14 Feb 2011 |

Updated |
14 Feb 2011 |

Type |
Journal |

Year |
2010 |

Where |
QEST |

Authors |
Jasper Berendsen, David N. Jansen, Frits W. Vaandrager |

Comments (0)