LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Laurent Doyen and Stefan Göller.

The seminar is open to public and does not require any form of registration.

Next Seminar

A Model Checking Approach to Dynamical Systems Analysis

Visit website for this news | Export event in iCalendar format

 David  Safranek
Date
Tuesday, January 24 2017 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
David Safranek (Masaryk University, Brno)

We will describe our novel high-performance algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems based on coloured model checking. The method employs a symbolic representation of sets of parameter valuations in terms of first-order theory of the reals. Moreover, we will discuss an interesting extension of the algorithm that allows to address the problem of bifurcation analysis of parameterised high-dimensional dynamical systems.

To this end, we introduce the hybrid CTL logic augmented with direction formulae. This allows us to describe various behaviour patterns and phase portraits. Finally, we will describe applications of the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour involving multi-stability or limit cycles.


Upcoming Seminars

Asynchronous Distributed Automata: A Characterization of the Modal Mu-Fragment

Visit website for this news | Export event in iCalendar format

Date
Tuesday, February 21 2017 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Fabian Reiter (IRIF, Université Paris Diderot)

I will present the equivalence between a class of asynchronous distributed automata and a small fragment of least fixpoint logic, when restricted to finite directed graphs. More specifically, the considered logic is (a variant of) the fragment of modal μ-calculus that allows least fixpoints but forbids greatest fixpoints. The corresponding automaton model uses a network of identical finite-state machines that communicate in an asynchronous manner and whose state diagram must be acyclic except for self-loops. As a by-product, the connection with logic also entails that the expressive power of those machines is independent of whether or not messages can be lost.


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Jan 24
Tue, Feb 21

Past seminars