[PPL-devel] PPL: Problem with Checked-Ints

[Didier Lime]

>> Good idea but, in Romeo, I actually need those non-strict  
>> inequalities so this is not an option.
>
> Do you mean that you need those _strict_ inequalities?

Yes strict, I must have been distracted when typing!

> If so, this may be one application of strict inequalities we do not  
> know.
> Can you give us some intuition or point us to a paper that explains
> the role played by strict inequalities in the verification of Time  
> Petri Nets?

Well, first you may want to say that your process takes (strictly)  
less than, say, 3 time units to execute. The theory of time Petri  
nets is compatible with attaching open intervals to the transitions.  
But it is not always very natural to model using strict inequalities.

Second, when you do some model-checking you may want to ensure that  
from some state, whatever you do, some property P (e.g. the  
occurrence of some marking of the net) will be true at some date t  
belonging to some closed interval [a,b].

To do so we regroup the states of the net in symbolic states  
consisting of a marking and a polyhedron describing the possible  
dates associated to the marking (one variable per enabled transition).

Then, in the algorithm checking the property if you find P within the  
interval [c,d] with c < a and, say, d in [a,b] then you want to  
continue looking for P from all the states in [c, a[. It is mandatory  
to have this strictness in a because you have already satisfied your  
property at date a and maybe no matter how you extend the path  
starting from the state where t=a, you will not find P again and the  
algorithm would (possibly wrongly) answer "false".

I am not sure this is very clear. Unfortunately I do not have a paper  
explaining this particular problem to point you to at the moment. On  
the computation of the state-space of time Petri nets with polyhedra  
you may want to have a look to the paper roux-ICATPN-04 whose bibtex  
you will find below. It only deals with non-strict inequalities but  
if you allow open intervals on transitions then you get NNC polyhedra.

Finally, you may be interested in knowing that we had the PPL compile  
on Windows XP without using Cygwin (I do not have all the details  
however since I have not done it myself but I can ask for them).

Best wishes,

Didier

@inproceedings{roux-ICATPN-04,
	Address = {Bologna, Italy},
	Author = {O.H. Roux and D. Lime},
	Booktitle = {The 25th International Conference on Application and  
Theory of {Petri} Nets, (ICATPN 2004)},
	Editor = {Jordi Cortadella and Wolfgang Reisig},
	Month = JUN,
	Pages = {371--390},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Time {Petri} Nets with Inhibitor Hyperarcs. {Formal}  
Semantics and State Space Computation},
	Volume = {3099},
	Year = 2004}



--
Dr. Didier Lime
Maître de Conférences
IRCCyN / École Centrale de Nantes
Nantes, France

http://www.irccyn.ec-nantes.fr/~lime