EN | DE
Theoretische Informatik

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

ws18:ober [2019/02/12 17:54]
tadeusz
ws18:ober [2019/02/12 17:58] (current)
tadeusz
Line 14: Line 14:
 |< 100% 5em 15em >| |< 100% 5em 15em >|
 ^ Date ^ Speaker, Topic ^ Abstract^ ^ Date ^ Speaker, Topic ^ Abstract^
 +| 12-Feb | Matthias Zinner, // Integrating CTLf into NuSMV // [{{:ws18:ober:slidesHandout.pdf|slides}}] | The focus of the presentation is to give a short introduction to CTLf and explain its integration into NuSMV. In particular, the parsing process, model checking and trace generation implementation is discussed. Also, the relationship between existing fairness mechanics for CTL and CTLf is described. |
 | 12-Feb | Tadeusz Litak, // Be fair to CTL // [{{:ws18:ober:befairtoctl_feb2019.pdf|slides}}] | I present an ongoing work on expressive power and model-checking aspects of CTLf, an extension of CTL with a binary "fairness" connective, proposed recently for model-theoretic reasons by Ghilardi & van Gool (LiCS 2016).  I will recall fairness-capturing extensions of CTL proposed in 1980's (ECTL, FCTL, GFCTL, ECTL+... ) and sketch how CTLf relates to (at least some of) them. Apart from highlighting CTLf model-checking advantages,  I will also briefly discuss the possibility of using efficient parity-games for modal mu-calculi. This talk incorporates discussions with Christoph Rauch and Daniel Hausmann, and provides an introduction to the following presentation of Matthias Zinner's master project. | | 12-Feb | Tadeusz Litak, // Be fair to CTL // [{{:ws18:ober:befairtoctl_feb2019.pdf|slides}}] | I present an ongoing work on expressive power and model-checking aspects of CTLf, an extension of CTL with a binary "fairness" connective, proposed recently for model-theoretic reasons by Ghilardi & van Gool (LiCS 2016).  I will recall fairness-capturing extensions of CTL proposed in 1980's (ECTL, FCTL, GFCTL, ECTL+... ) and sketch how CTLf relates to (at least some of) them. Apart from highlighting CTLf model-checking advantages,  I will also briefly discuss the possibility of using efficient parity-games for modal mu-calculi. This talk incorporates discussions with Christoph Rauch and Daniel Hausmann, and provides an introduction to the following presentation of Matthias Zinner's master project. |
 | 5-Feb | Miriam Polzer, // Towards Weakest Precondition Calculus for Local Store // [{{:ws18:ober:polzer-slides.pdf|slides}}]  | Inspired by Hasuo's approach to weakest precondition semantics, I will show how to obtain a predicate transformer that may provide a weakest precondition calculus for local store monads. We will recapitulate the presheaf structures admitting a notion of being 'indifferent to privately allocated locations' and then, starting from a full local store monad T, we will construct a submonad R that provides propositions suitable for allocation of new memory cells. Ultimately, we will see how postconditions that depend on newly allocated locations are naturally transformed into preconditions that only depend on already existing store. Along the way, we will also encounter the connection required to unify work on local store by Plotkin/Power and Kammar et al. | | 5-Feb | Miriam Polzer, // Towards Weakest Precondition Calculus for Local Store // [{{:ws18:ober:polzer-slides.pdf|slides}}]  | Inspired by Hasuo's approach to weakest precondition semantics, I will show how to obtain a predicate transformer that may provide a weakest precondition calculus for local store monads. We will recapitulate the presheaf structures admitting a notion of being 'indifferent to privately allocated locations' and then, starting from a full local store monad T, we will construct a submonad R that provides propositions suitable for allocation of new memory cells. Ultimately, we will see how postconditions that depend on newly allocated locations are naturally transformed into preconditions that only depend on already existing store. Along the way, we will also encounter the connection required to unify work on local store by Plotkin/Power and Kammar et al. |