English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 DetailsSummary
  Superposition-Based Analysis of First-Order Probabilistic Timed Automata

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.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-14C1-A Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BB3F-E
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Fietzke, Arnaud1, Author           
Hermanns, Holger2, Author
Weidenbach, Christoph1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2External Organizations, ou_persistent22              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2011-01-1920102010
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 536347
DOI: 10.1007/978-3-642-16242-8
URI: http://dx.doi.org/10.1007/978-3-642-16242-8_22
Other: Local-ID: C125716C0050FB51-A58766A53216A228C12577EE0045E1FE-FietzkeWeidenbach2010
 Degree: -

Event

show
hide
Title: 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Place of Event: Yogyakarta, Indonesia
Start-/End Date: 2010-10-10 - 2010-10-15

Legal Case

show

Project information

show

Source 1

show
hide
Title: Logic for Programming, Artificial Intelligence, and Reasoning
  Subtitle : 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings
  Abbreviation : LPAR 2010
Source Genre: Proceedings
 Creator(s):
Fermüller, Christian G.1, Editor
Voronkov, Andrei2, Editor           
Affiliations:
1 External Organizations, ou_persistent22            
2 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 302 - 316 Identifier: ISBN: 978-3-642-16241-1

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 6397 Sequence Number: - Start / End Page: - Identifier: -