Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Heuristics for Probabilistic Timed Automata with Abstraction Refinement
verfasst von : Luis María Ferrer Fioriti, Holger Hermanns
Erschienen in: Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Probabilistic Timed Automata provide a theory to model and verify real-time systems with non-deterministic and probabilistic behaviors. The main approach to model checking Probabilistic Timed Automata is based on encoding the time behavior either with abstractions based on a region graph or with digitalization of clocks. In this paper we present a sound method that combines digitalization to encode time behavior and predicate abstraction to reduce the state space, allowing the analysis of models with possibly infinite numbers of locations. Our method is compatible with abstraction refinement techniques previously used for Probabilistic Automata. Based on experimental results, we show that the underlying digital semantics of clocks is prone to produce an overhead in the abstraction process that can sometimes make the model checking infeasible. To cope with this problem we present some heuristics to handle clocks and show their impact on the verification.