Resumen de Structural methods for the synthesis of well-formed concurrent specificantions
The specification of a concurrent system describes a set of components that operate in a parallel environment and eventually interact. When modeling such concurrent behavior, the set of states that the system can reach are typically very large or even infinite. This phenomenon is known as the state space explosion problem. Consequently, algorithms that work on the state space of such type of systems suffer from the state space explosion problem, thus having high complexity. In this work we tackle the problem of synthesis of concurrent systems.
Asynchronous circuits are the simplest class of concurrent systems. Despite of their simplicity, problems like the state space explosion problem already exist. Therefore, state-based algorithms for the automatic synthesis of asynchronous circuits can only synthesize small size specifications. This work provides structural methods for the synthesis of large specifications.
The methods developed perform as a state-based method would do if there was enough memory or machine-power. By using graph algorithms or linear algebra, the design flow presented avoids the computation of the whole state space. Experimental results show the significant improvement with respect to existing approaches.
The most important problem in the synthesis of asynchronous circuits is the problem of the encoding. Informally, a specification is correctly encoded if the system knows what to do just by looking at the value of the signals.
If a specification is not correctly encoded, it can not be correctly implemented.
In our work we tackle this problem and provide structural methods, based in the transformation of an interpreted Petri net, that guarantee a correct encoding. Also structural methods based on Linear Algebra are developed to semidecide the encoding problem. The methods introduced provide a speed-up of several orders of magnitude with respect to existing approaches.
The contributions presented in this work are:
