LIPN
Abstract: Biochemical networks - as metabolic networks, signal transduction networks, or gene regulatory networks - are by their very nature bipartite graphs with nodes representing biochemical entities or reactions. Thus, biochemically interpreted Petri nets are an intuitive approach in systems biology, allowing at the same time to reuse established Petri net analysis techniques for validation of bionetwork knowledge and model-based experiment design. Even more, the biochemical interpretation of Petri nets comes along with new challenges for Petri net theory. In the talk two (new) open problems are presented and motivated by biochemical network examples: time-dependent boundedness and time-dependent liveness. No prerequisite knowledge in systems biology is required.
Abstract: the automata theoretic approach to model checking linear-time temporal properties is a classical verification technique for concurrent systems. Both the system and the property to verify are expressed as automata on infinite words (omega-automata). Some operations on these automata establish whether the property holds in the system. We focus on a kind of omega-automata called Transition-based Generalized Büchi Automata (TGBA). We start by revisiting the main two steps of the approach: the translation of linear-time temporal logic formulae into TGBA, and the emptiness check of TGBA. For both steps we show the benefits of using TGBA. We then generalize the emptiness check to transition-based Streett automata; this enables the verification of properties under strong fairness assumptions.