Introduction

This page reports the open issues identified prior to the presentation of results or during the discussion following this presentation on June 25th, 2013 in Milano.

Organizational Matters

• Io1 - Live Event: this event, lately announced, had to be canceled, which is a pity. Its objective is to provide feedback on tools from a "usability" point of view (look and feel, quality of documentation and tutorials, etc). We will announce it earlier for the next edition in 2014.
• Io2 - People: so far, active people in the model checking contest are to few...
• Io3 - Global schedule: the submission deadline should be pushed earlier to allow more time for analysis of the tools.
• Io4 - "known" and "surprise" models: A strong suggestion is, after the call for model, to decide that all new models will be "surprise" and thus not submitted after the call for models. Models of previous years will then be the only "known" models. This should ease the management of the MCC and help to relax the agenda and have the call for tools submission out earlier.
• Io5 - Rules:
some people suggest to clean up the rules in order to make clear what is possible and what is not allowed. In particular, all precomputed aspects should be carefully investigated
• Io6 - Trophies:
we all agree on the fact that the formulas used this year are mainly temporary. This formula should be discussed and should introduce more aspects on the results like, time and memory consumption, how correct the outputs are (only for the state space examination this year), support of P/T and/or colored models, etc.

Technical issues

• It1 - Generation of formulas: this is an issue for the second year and it was not yet solved. The problem is to select a large number of formulas for which we can state their result: satisfied or unsatisfied. Considering the number of models and instances of these models (a total of 255 in 2013), these mush be generated automatically
  It seems that SPOT could provide a basis of solution for LTL formulas.
  During the discussion, several other possible solutions. One is the definition of formula patterns that could be repeated and arranged randomly and combined together with atomic propositions.
  Another possibility is to propose manually sort of "parameterized" formulas that are scaled up for each instances, however, if this requires less formulas, there are yet numerous formulas to provide.
  The participants agree on the fact that purely random formulas are not good but it is necessary to generate formulas automatically in "a good way". We can insert existing formulas when they are available (this was done for the surprise model "Vasy2003"). Another important point is that the output values of formula should be known in advance so that: 1) their veracity could be checked, and 2) there can be the same amount of satisfied and unsatisfied formulas to be processes (maybe separately).
  There is however a real problem due to issue Io2; manpower is quite low and must be extended to let time for these tasks.
• It2 - Grammar for formula: It could be made less ambiguous (e.g. fully braketed expressions). Some people reported difficulties of interpretation and then translation. The idea is to have a small task force that will bring out proposals, especially for the atomic propositions. Somebody suggested to use PNML identifiers of objects instead of their labels (but this may cause problems with the equivalences between colored nets and P/T ones).
• It3 - BenchKit: if this benchmarking tool appear to be operational (it was successfully used to operate the 54293 executions required this year), its usage remains difficult for the non-developers. A new version should appear, making its "individual use" easier, thus allowing the community to reuse outputs from this contest and later ones.
• It4 - High-level colored nets: a solution should be proposed to have high-level colored nets (the problem in 2012 and 2013 was how to produce their PNML representation). This would allow some tools using such models to be "more on their playground" than with lower level Petri nets.