Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse




Conference Paper

Superposition-Based Analysis of First-Order Probabilistic Timed Automata


Fietzke,  Arnaud
Automation of Logic, MPI for Informatics, Max Planck Society;

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Fietzke, A., Hermanns, H., & Weidenbach, C. (2010). Superposition-Based Analysis of First-Order Probabilistic Timed Automata. In C. G. Fermüller, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 302-316). Berlin: Springer. doi:10.1007/978-3-642-16242-8.

Cite as:
This paper discusses the analysis of first-order probabilistic timed automata (FPTA) by a combination of hierarchic first-order superposition-based theorem proving and probabilistic model checking. We develop the overall semantics of FPTAs and prove soundness and completeness of our method for reachability properties. Basically, we decompose FPTAs into their time plus first-order logic aspects on the one hand, and their probabilistic aspects on the other hand. Then we exploit the time plus first-order behavior by hierarchic superposition over linear arithmetic. The result of this analysis is the basis for the construction of a reachability equivalent (to the original FPTA) probabilistic timed automaton to which probabilistic model checking is finally applied. The hierarchic superposition calculus required for the analysis is sound and complete on the first-order formulas generated from FPTAs. It even works well in practice. We illustrate the potential behind it with a real-life DHCP protocol example, which we analyze by means of tool chain support.