Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




Author, Editor

Author(s):

Fietzke, Arnaud
Hermanns, Holger
Weidenbach, Christoph

dblp
dblp
dblp

Not MPG Author(s):

Hermanns, Holger

Editor(s):

Fermüller, Christian G.
Voronkov, Andrei

dblp
dblp

Not MPII Editor(s):

Fermüller, Christian G.
Voronkov, Andrei

BibTeX cite key*:

FietzkeWeidenbach2010

Title, Booktitle

Title*:

Superposition-based Analysis of First-Order Probabilistic Timed Automata

Booktitle*:

Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17

Event, URLs

URL of the conference:

http://www.computational-logic.org/lpar-17/Home.html

URL for downloading the paper:

http://dx.doi.org/10.1007/978-3-642-16242-8_22

Event Address*:

Yogyakarta, Indonesia

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

10 October 2010

Event End Date:

15 October 2010

Publisher

Name*:

Springer

URL:

http://www.springer.com

Address*:

Berlin

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

6397

Number:


Month:

October

Pages:

302-316

Year*:

2010

VG Wort Pages:

14

ISBN/ISSN:

978-3-642-16241-1

Sequence Number:


DOI:

10.1007/978-3-642-16242-8



Note, Abstract, ©


(LaTeX) 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.

Keywords:

first-order logic, theorem proving, probabilistic timed automata



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{FietzkeWeidenbach2010,
AUTHOR = {Fietzke, Arnaud and Hermanns, Holger and Weidenbach, Christoph},
EDITOR = {Ferm{\"u}ller, Christian G. and Voronkov, Andrei},
TITLE = {Superposition-based Analysis of First-Order Probabilistic Timed Automata},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17},
PUBLISHER = {Springer},
YEAR = {2010},
VOLUME = {6397},
PAGES = {302--316},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Yogyakarta, Indonesia},
MONTH = {October},
ISBN = {978-3-642-16241-1},
ISBN = {0302-9743},
DOI = {10.1007/978-3-642-16242-8},
}


Entry last modified by Anja Becker, 03/03/2011
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
12/03/2010 01:43:18 PM
Revisions
2.
1.
0.

Editor(s)
Anja Becker
Anja Becker
Arnaud Luc Fietzke

Edit Dates
03.03.2011 15:23:35
19.01.2011 14:35:24
12/03/2010 01:43:18 PM

Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section