Advertisement
Published in:
2012 | OriginalPaper | Chapter
Heuristics for Probabilistic Timed Automata with Abstraction Refinement
Authors : Luis María Ferrer Fioriti, Holger Hermanns
Published in: Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.