Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 DetailsÜbersicht
  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

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-14C1-A Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BB3F-E
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Fietzke, Arnaud1, Autor           
Hermanns, Holger2, Autor
Weidenbach, Christoph1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2External Organizations, ou_persistent22              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2011-01-1920102010
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 536347
DOI: 10.1007/978-3-642-16242-8
URI: http://dx.doi.org/10.1007/978-3-642-16242-8_22
Anderer: Local-ID: C125716C0050FB51-A58766A53216A228C12577EE0045E1FE-FietzkeWeidenbach2010
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Veranstaltungsort: Yogyakarta, Indonesia
Start-/Enddatum: 2010-10-10 - 2010-10-15

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Logic for Programming, Artificial Intelligence, and Reasoning
  Untertitel : 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings
  Kurztitel : LPAR 2010
Genre der Quelle: Konferenzband
 Urheber:
Fermüller, Christian G.1, Herausgeber
Voronkov, Andrei2, Herausgeber           
Affiliations:
1 External Organizations, ou_persistent22            
2 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 302 - 316 Identifikator: ISBN: 978-3-642-16241-1

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
  Kurztitel : LNCS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 6397 Artikelnummer: - Start- / Endseite: - Identifikator: -