Concurrency, Specification & Programming. 24th International Workshop, CS&P 2015. Rzeszow, Poland, September 28-30, 2015. Proceedings
We present an efficient equivalence-checking algorithm for a propositional model of programs with semantics based on (what we call) progressive monoids on the finite set of statements generated by relations of a specific form. We consider arbitrary set of relations for commutativity (relations of the form ab=ba for statements a, b) and left absorption (relations of the form ab=b for statements a, b) properties. The main results are a polynomial-time decidability for the equivalence problem in the considered case, and an explicit description of an equivalence-checking algorithm which terminates in time polynomial in size of programs.
In this paper we study how it is possible to control Petri net behavior using time constrains. Controlling here means forcing a process to behave in a stable way by associating time intervals to transitions and hence transforming a classic Petri net into a Time Petri net. For Petri net models stability is often ensured by liveness and boundedness. These properties are crucial in many application areas, e.g. workflow modeling, embedded systems design, and bioinformatics. This paper deals with the problem of transforming a given live, but unbounded Petri net into a live and bounded one by adding time constraints. We specify necessary conditions for the solvability of this problem and present an algorithm for adding time intervals to net transitions in such a way that the resulting net becomes bounded while staying live.