[Club2] Einladung: Certifying Probabilistic Model Checking: Syntactic Co-saf... - Mi 14. Apr. 2021 14:00 - 14:30 (MESZ) (club2 at mailbroy.informatik.tu-muenchen.de)

[piller at in.tum.de]

Sie wurden zum folgenden Termin eingeladen.

Titel: Certifying Probabilistic Model Checking: Syntactic Co-safe Linear  
Temporal Logic Properties
Speaker: Florian Märkl

Type: IDP Vortrag


Abstract:
We develop an executable certificate checker that verifies probabilistic  
model checking results. We are given a Markov decision process K and a  
formula φ in linear temporal logic. The goal is to give a lower bound for  
the probability that φ is satisfied by a trace on K, starting in a given  
state s0. For this, the MoChiBA model checker, which is implemented as  
untrusted Java code, produces a certificate containing a Markov chain K'  
and claims this to be a concrete scheduler on K, as well as a probability P  
for φ on K'. Instead of trying to formally verify the MoChiBA Java code to  
only yield correct certificates, we formalize checks to determine the  
validity of a given certificate in Isabelle/HOL and generate executable  
code from it. This approach significantly reduces the amount of code to  
verify. We prove that if this code determines the certificate to be valid,  
then P is also a lower bound of the probability for φ on K, which is our  
final model checking result.
Wann: Mi 14. Apr. 2021 14:00 – 14:30 Mitteleuropäische Zeit - Berlin
Wo: https://bbb.rbg.tum.de/sim-h4f-emd
Kalender: club2 at mailbroy.informatik.tu-muenchen.de
Wer
     * piller at in.tum.de- Veranstalter
     * esparza at in.tum.de
     * s.sickert at tum.de
     * club2 at mailbroy.informatik.tu-muenchen.de
     * nipkow at in.tum.de
     * f.maerkl at tum.de

Termininformationen:  
https://calendar.google.com/calendar/event?action=VIEW&eid=MHBvbGFmY2llc2dmcGNnbmRmbWUyMG0wazkgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM5NWVkNDhjYzFlMjU2YWI2YWRmNDgzOTA4OTA5ZDE1NjgyOGRjZGY&ctz=Europe%2FBerlin&hl=de&es=0

Einladung von Google Kalender: https://calendar.google.com/calendar/

Sie erhalten diese E-Mail unter club2 at mailbroy.informatik.tu-muenchen.de,  
da Sie ein Gast bei diesem Termin sind.

Lehnen Sie diesen Termin ab, um keine weiteren Informationen zu diesem  
Termin zu erhalten. Sie können auch unter  
https://calendar.google.com/calendar/ ein Google-Konto erstellen und Ihre  
Benachrichtigungseinstellungen für Ihren gesamten Kalender steuern.

Wenn Sie diese Einladung weiterleiten, kann jeder Empfänger eine Antwort an  
den Organisator senden und zur Gästeliste hinzugefügt werden. Außerdem  
könnte er weitere Nutzer einladen und Ihre Antwort ändern. Weitere  
Informationen: https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210408/58a29ae1/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 3079 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210408/58a29ae1/attachment-0001.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 3135 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210408/58a29ae1/attachment-0001.bin>