Backwards Reachability for Probabilistic Timed Automata: A Replication Report

TL;DR

This paper presents a new implementation of backwards reachability for probabilistic timed automata, supporting both minimum and maximum probabilities, thus offering a more general tool for model checking PTCTL properties.

Contribution

The authors introduce an enhanced backwards reachability implementation in the Modest Toolset that supports both minimum and maximum probabilities, surpassing previous limitations.

Findings

Supports both min and max probability calculations

Compared behavior with original backwards reachability results

Most general implementation available today

Abstract

Backwards reachability is an efficient zone-based approach for model checking probabilistic timed automata w.r.t. PTCTL properties. Current implementations, however, are restricted to maximum probabilities of reachability properties. In this paper, we report on our new implementation of backwards reachability as part of the Modest Toolset. Its support for minimum and maximum probabilities of until formulas makes it the most general implementation available today. We compare its behaviour to the experimental results reported in the original papers presenting the backwards reachability technique.