Petri net synthesis from labelled transition systems and from languages
Eric Badouel, SUMO, IRISA Rennes
Abstract: Net synthesis can be understood as an algorithmic procedure aimed at constructing a Petri net structure from a specification of its intended or desired behaviour, given typically in the form of a transition system or a formal language. The procedure has to decide whether such a specification can be realised and, if the answer is positive, deliver as efficiently as possible a Petri net with the specified behaviour. Such a Petri net is then correct-by-construction, making net synthesis an attractive alternative to the design-and-verify approach to building concurrent and distributed system. If, however, the specification cannot be realised in full, the synthesis procedure is expected to deliver a Petri net approximating the specified behaviour in an optimal way. In this talk we survey the techniques of Petri net synthesis from labelled transitions or from languages and discuss some of their applications to process mining and the supervisory control of discrete event systems.

Exact and Approximate Diagnosis of Probabilistic Systems
Serge Haddad, LSV, ENS Cachan
Abstract: Diagnosis of partially observable stochastic systems prone to faults was introduced in the late nineties. Diagnosability, i.e. the existence of a diagnoser, may be specifi ed in di fferent ways: (1) exact diagnosability (called A-diagnosability) requires that almost surely a fault is detected and that no fault is erroneously claimed while (2) approximate diagnosability (called epsilon-diagnosability) allows a small probability of error when claiming a fault and (3) accurate approximate diagnosability (called AA-diagnosability) requires that this error threshold may be chosen arbitrarily small. In this talk, I will cover three aspects of diagnosis. First, I solve semantical issues like the (non) equivalence of different notions. Then I study algorithmic issues establishing in most of the cases, the decidability status and the complexity class of the diagnosability problem. Finally, I explain how to synthetize a diagnoser when the system is diagnosable.