CASINO - CAusal SemantIcs of Nets with inhibitOr arcs

Project Dates: From October 2004 to September 2007

Project Leader: Prof. Maciej Koutny

Sponsors: EPSRC

 

The overall aim of the proposed visits is to develop to complete the development of the fundamental part of the causality semantics for nets with inhibitor arcs which are used in the modelling and analysis of complex concurrent systems, and to investigate whether such a semantics can be used to develop efficient verification techniques. To achieve the first objective we will proceed by adopting (and, if necessary, modifying) those ideas which had proved effective for our prior work on finite causal nets generated by inhibitor nets. We expect that the existing framework is sufficiently developed to allow a relatively straightforward definition of the operational way in which such causal nets are generated. This, however, needs to be complemented by a suitable axiomatic definition which is much harder to formulate and then prove equivalent with the operational one.  The second objective brings into the framework the issue of conflict in the behaviour specified by inhibitor nets. We plan to conduct a comprehensive study of the relationship between (weak and strong) causality and action conflict in the context of inhibitor nets. The third objective is to investigate the ways in which a (typically infinite) unfolding could be truncated to a finite representative (its prefix) which would still have full information about the state space of the original inhibitor net, and we plan to re-evaluate the thinking behind the prefix-based approach to the verification of the standard Petri nets.