Prof. Stefan Haar visited HSE PAIS Lab
Seminar I (Monday, Sep 15, 18:00-19:30, auditorium 420)
What Occurrence Nets Reveal
Occurrence nets are a well known partial order model for the concurrentbehavior of Petri nets, and provide a useful tool to tackle state-spaceexplosion in verification and related tasks. Moreover, their structureallows to access directly the relations of causal precedence,concurrency, and conflict between events. By exploring the datastructure further, one finds that event a may reveal event b in thesense that occurrence of a implies that b inevitably occurs, too, be itbefore, after, or concurrently with a. Knowledge of reveals facilitatesin particular the analysis of partially observable systems, in thecontext of diagnosis, testing, or verification; it can also be used togenerate more concise representations of behaviours via abstractions.This binary reveals relation has been shown decidable: for a given paira,b in the unfolding U of a safe Petri net N, a finite prefix P of U issufficient to decide whether or not a reveals b.Beyond these binary structural relations,we generalize the revealsrelation to express more general dependencies, involving more than twoevents, and indicate some applications, including diagnosisto be treated in the second seminar.
Seminar II (Monday, Sep 22, 18:00-19:30, auditorium 420)
Reveal your faults!
From a partial observation of the behaviour of a labeled Discrete EventSystem, fault diagnosis is the task of detecting whether or not thegiven sequence of observed labels indicates that some unobservable faulthas occurred. Diagnosability is an associated system property, statingthat in any possible execution an occurrence of a fault can eventuallybe diagnosed.
We will show some facets of diagnosis and diagnosability from recent work:1) Active diagnosis aims at controlling the system in order to make itdiagnosable. With a dedicatedautomata construction, we can solve the active diagnosability decisionproblem and the active diagnoser synthesis problem in a way thatimproves over previous solution, in that (a) our procedures are optimalw.r.t. to computational complexity, and (b) the memory required for theactive diagnoser produced by the synthesis is minimal. If time allows,stochastic extensions and ideas for future work can also be discussed.2) When diagnosis is considered in the context of concurrent systems,partial order semantics adds to the difficulty of the problem, but alsoprovides a richer and more complex picture of observation and diagnosis.In *weak* diagnosis, one asks whether a concurrent chronicle of observedeventsallows to determine that a non-observable fault willinevitably occur, sooner or later, on any maximal system run compatiblewith the observation. Under the assumption that the system is modeledby a safe Petri net, it suffices to compute suitable finite unfoldingprefixes of bounded size, to obtain sufficient information for thediagnosis algorithm.Our work extends and generalizes the unfolding-based diagnosis approaches byBenveniste et al (2003 etc). as well as Esparza and Kern (2012).
Colloquium (Thursday, Sep 18, 16:40 - 18:00, Dekart lecture hall)
True concurrency - from C.A. Petri to Telecom and Systems Biology
Some circles, squares and arrows, plus some black dots moving along:that is all it takes to build a Petri net. These nets are a mathematicaltool and model for dynamical systems generally considered to be ?"athome" in computer science. However, a great deal of the theory of Petrinets and of the concurrency (describing asynchronous parallel processes)which they involve, had been developed for and inspired by theunderstanding of physical processes, building upon principles fromchemical reactions, and both relativisticand quantum physics. It is fair to say that Petri nets are not only intuitive, but alsofertile for many fields; in this talk, I will illustrate this in thecontexts of physics, engineering, and biology,reflecting in some sort the evolution that the field has taken over thepast 50 years.
Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!
To be used only for spelling or punctuation mistakes.