Superposition-Based Analysis of First-Order Probabilistic Timed Automata

Fietzke, Arnaud; Hermanns, Holger; Weidenbach, Christoph

doi:10.1007/978-3-642-16242-8

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Superposition-Based Analysis of First-Order Probabilistic Timed Automata

MPS-Authors

/persons/resource/persons44415

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

/persons/resource/persons45719

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

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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: https://hdl.handle.net/11858/00-001M-0000-000F-14C1-A

Abstract

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.