Paris Automata and Concurrency Theory Seminar

This talk explores the relationship between fairness and promptness in fragments of Linear Temporal Logic (LTL). We begin by contrasting two perspectives on LTL model checking: the universal problem, where all system runs must satisfy a given formula, and the fair problem, where almost all runs do. Although these problems share the same theoretical complexity (PSPACE-complete), interesting differences emerge when we restrict attention to certain fragments. In particular, the Muller fragment of LTL was previously identified as one where these two notions diverge in complexity. Extending this line of inquiry, we investigate the prompt version of LTL (pLTL), which enriches LTL with a prompt eventually operator ensuring liveness within bounded time. We show that the Muller fragment of pLTL behaves differently from its classical counterpart, and we identify a new expressive fragment where fair model checking can be performed more efficiently than universal model checking.

Discrete models of complex systems (boolean networks, Petri nets) are often used for over-approximating the set of reachable states, for example in biological networks, and to provide predictions of (at least) all possible behaviours. Of particular interest are the long-time stable subspaces, aka attractors, which give, in the context of cell regulation, exactly the phenotypes that a cell can develop. Knowing the state space sufficiently well to find attractors is thus fundamentally important.
It has turned out that in our particular case, the desired over-approximation could not be obtained using boolean networks with classical update modes; a novel discrete semantics, giving most permissive Boolean networks (MPBN)s, finds reachable states previously unforeseen. The link with discrete Petri nets (and their associated analysis techniques) that existed in the classical case could not be established for MPBNs. Recent research has shown, however, that continuous Petri nets allow a faithful translation of MPBNs, and enjoy very nice dynamical properties supporting representing and analysing their behaviour with discrete means. Some open questions will be presented, to stimulate discussions.