Equivalent Paths in State Spaces

In addition to checking the equivalence of the behaviour of the two models only by means of the above mentioned techniques, we have tried to compare paths in the state spaces of the two models. We have checked that, whenever one of the models can make a step (let a transition occur) then the other model must also be able to make a step. This was done by exploring paths through the state space. We considered the arcs on the path in the state space of the unfolded CPN model. For every binding of a transition on the path in this CPN model, we checked if the corresponding folded transition in the folded CPN model was enabled. This was indeed the case for the paths that we followed. In addition, we checked that for every node on the path, the same number of successor nodes existed in both CPN models. From this comparison we get even more confident in the equivalence of the two CPN models.

However, we plan to do this more consequently than what we have done so far. We will define a mapping M_{unf old} from states in the folded CPN model into states in the unfolded CPN model. This mapping should be based on the equivalence between markings in the folded and unfolded CPN models. A similar mapping BE_{unf old} should be defined for mapping binding elements in the folded CPN model into binding elements in the unfolded CPN model. Then the two mappingsM_{unf old} andBE_{unf old}should be applied to the state space of the folded CPN model to show that resulting state space is identical to the state space of the unfolded CPN model (modulo the extra initialisation marking and arc in the folded CPN model).

7.6 Conclusion and Future Work

When using CP-nets for creating models one have to be careful to choose the right level of folding. This paper shows that it is sometimes useful to have

7.6. Conclusion and Future Work 83

Place Best Upper Multi-set Bounds

Top’O 1‘(1,1,(ii (”56131”)))++ 1‘(1,1,(ii (”65095”))) ++

1‘(1,2,(ii (”56131”)))++ 1‘(1,2,(ii (”65035”))) ++

1‘(1,3,(ii (”65035”)))++

1‘(7,1,(ii (”196500”)))++ 1‘(7,2,(ii (”233750”)))++

1‘(8,1,(ii (”45673”))) ++ 1‘(8,2,(ii (”51935”)))++

1‘(8,3,(ii (”51935”))) ++

1‘(9,1,(ii (”294572”)))++ 1‘(9,1,(ii (”300891”)))++

1‘(9,2,(ii (”171766”)))++ 1‘(9,2,(ii (”294572”)))++

1‘(9,2,(ii (”300849”)))++ 1‘(9,3,(ii (”171766”)))++

1‘(9,3,(ii (”176807”)))++ 1‘(9,3,(ii (”300849”)))++

1‘(9,4,(ii (”171766”)))++ 1‘(9,4,(ii (”176807”)))++

1‘(9,4,(ii (”300849”)))++ 1‘(9,5,(ii (”176807”)))++

1‘(9,6,(ii (”176807”)))

Initial’Structure 1‘{NodeID = 2,PreSet = [],PostSet = [7]}++

1‘{NodeID = 3,PreSet = [],PostSet = [1]}++

1‘{NodeID = 4,PreSet = [],PostSet = [8]}++

1‘{NodeID = 5,PreSet = [],PostSet = [7]} Intermediate’Structure 1‘{NodeID = 1,PreSet = [3,7],PostSet = [9]}++

1‘{NodeID = 7,PreSet = [2,5],PostSet = [8,1]}++

1‘{NodeID = 8,PreSet = [7,4],PostSet = [9]} Terminal’Structure 1‘{NodeID = 9,PreSet = [1,8],PostSet = []}

Table 7.5: Folded CPN model: best upper multi-set bounds.

co-existing models with different degrees of folding.

One CPN model with a relatively extensive net structure to be used for understanding the model and for reference to the modelled system. This may require that the level of folding is kept so low that a new CPN model has to be created for each instance of the problem. However, if the model can be generated automatically as for the models presented in this paper, it may not be a problem.

The second model should focus on modelling the entire class of problems.

This model is typically a folded version of the other one, which implies that the one and only model can be used for any instance of the problem. That means that the general CPN model will typically have relatively little net structure compared to the specific models.

A method for validating the equivalence between the folded and unfolded models has successfully been applied to several different TINLs with different time delays. Therefore, we believe in that the behaviour of the models are equivalent. However, we have not proved or verified that they are equivalent.

Future work will first of all focus on verification of the equivalence of the behaviour of the models. In particular we want to get more confident that the structure of the state spaces from the different models are equivalent. We plan to establish a formal proof to prove the equivalence of the behaviour of the

models.

We will also experiment with alternative graphical interfaces for the simu-lators of the CPN models. The current web-based graphical interface is only useful for non-interactive simulations. By being able to interact with the sim-ulator during simulations it will be possible to access the current state of the TINL represented by the CPN model during a simulation. This may be useful if the simulator is integrated with the CAT-tool (using TCP/IP communication) which is used to create the TINL. That would make it possible to display the results in the CAT-tool during simulations.

Acknowledgements. This research was conducted at the C3I Center of George Mason University (GMU), VA, USA, with partial support provided by the U.S.

Air Force Office for Scientific Research under Grant No. F49620-98-1-0179.

The work in this paper proposing or-gates in influence nets for information assurance is based on work done by Insub Shin, GMU. Special thanks goes to Alexander H. Lewis and Lee W. Wagenhals, GMU, for valuable discussions and support during the project. Finally, we also want to thank Kurt Jensen and the anonymous referees for constructive critique and usefull suggestions on improving the paper.

Chapter 8

Operational Planning using Web-Based