Symbolic Diagnosis of Partially Observable Concurrent Systems
Monitoring large distributed concurrent systems is a challenging task. In this paper we formulate (model-based) diagnosis by means of hidden state history reconstruction, from event (e.g. alarm) observations. We follow a so-called true concurrency approach: the model defines explicitly the causal and concurrency relations between the observable events, produced by the system under supervision on different points of observation. The problem is to compute on-the-fly the different partial order histories, which are the possible explanations of the observable events. In this paper we extend our first method based on Petri nets unfolding to high-level parameterized Petri nets. This allows the designer to model data aspects (even on infinite domains) and non deterministic actions. The observation of such an action gives only partial information and the supervisor has to introduce parameters to represent the hidden aspects of the reached state. This supposes that the possible values for the parameters are symbolically computed and refined during supervision. In practice, non deterministic actions can also be used as an approximation to deal with incomplete information about the system. In this case the refinement of the parameters during supervision improves the knowledge of the model.
KeywordsDiscrete Event System Symbolic Execution Input Place Deterministic Action Presburger Arithmetic
- 7.Fabre, E.: Monitoring distributed systems with distributed algorithms. In: Proc. of the 2002 IEEE Conf. on Decision and Control, pp. 411–416 (2002)Google Scholar
- 11.Kozura, V.E.: Unfolding of coloured Petri nets. Technical Report 80, A.P. Ershov Institute of Informatics Systems (2000)Google Scholar
- 16.Vernier, I.: Symbolic executions of symmetrical parallel programs. In: Proc. of 4th Euromicro Workshop on Parallel and Distributed Processing, Braga, Portugal, pp. 327–334 (1996)Google Scholar