Fundamenta Informaticae - Volume 50, issue 2

Authors: Janicki, Ryszard

Article Type: Other

Keywords:

Citation: Fundamenta Informaticae, vol. 50, no. 2, pp. i-ii, 2002

Authors: Baldamus, Michael | Schneider, Klaus

Article Type: Research Article

Abstract: The automated verification of concurrent systems by model checking is often confronted with the state space explosion problem. A widely adopted method to tackle this problem is to use binary decision diagrams (BDDs) for representing systems and state spaces implicitly. However, it may be that even the system …representation itself is prohibitively large. It is therefore interesting to study which factors influence the size of a BDD that represents the transition relation of a system. In this article, we consider the BDD representations of synchronous, asynchronous, and interleaved processes with communication via shared variables and present upper bounds for their sizes. To this end, we introduce a general representation strategy where catastrophic exponential growth of the BDD can only be due to the specifics of communication and/or write conflict resolution; it is neither due to the number of processes nor to the concurrency discipline. Moreover, conditions on communication and write conflict resolution are presented that are sufficient for polynomial sized BDD representations. Show more

Keywords: Binary Decision Diagrams, Concurrency, Shared Variables

Citation: Fundamenta Informaticae, vol. 50, no. 2, pp. 111-133, 2002

Authors: Carmona, Josep | Cortadella, Jordi | Pastor, Enric

Article Type: Research Article

Abstract: This paper presents a method for the automatic synthesis of asynchronous circuits from Petri net specifications. The method is based on a structural encoding of the system in such a way that a circuit implementation is always guaranteed. Moreover, a set of transformations is presented for the subclass of Free-Choice Petri nets that enables the exploration of different solutions. The set of transformations is derived from previous work on Petri net synthesis. Both the encoding technique …and the set of transformations preserve the property of free-choiceness, thus enabling the use of structural methods for the synthesis of asynchronous circuits. Preliminary experimental results indicate that the quality of the circuits is comparable to that obtained by methods that require an exhaustive enumeration of the state space. This novel synthesis method opens the door to the synthesis of large control specifications generated from hardware description languages. Show more

Keywords: Asynchronous circuits, Structural synthesis, Complete State Coding

Citation: Fundamenta Informaticae, vol. 50, no. 2, pp. 135-154, 2002

Authors: Garnic, O. | Lanchares, J. | Hermida, R.

Article Type: Research Article

Abstract: This paper is devoted to studying two key issues of the asynchronous pipelines: their performance, and the influence that the position of stages have on the latency of a pipelined asynchronous circuit as a whole. To attain the performance evaluation, we derive expressions of the latency and the cycle time of a linear pipeline as closed-form formulas. To attain the influence of the position, we present some experiments, using the previous closed-form formulas, on different pipelines.

Keywords: Asynchronous circuits, pipeline performance

Citation: Fundamenta Informaticae, vol. 50, no. 2, pp. 155-174, 2002

Authors: Pietkiewicz-Koutny, Marta

Article Type: Research Article

Abstract: We here consider transition systems of Elementary Net Systems with Inhibitor Arcs. There are basically two different types of non-interleaving semantics of such Petri nets, the a-posteriori and a-priori semantics. The synthesis problem for Elementary Net Systems with Inhibitor Arcs executed under the a-priori semantics (ENI) was solved in [18]. In this paper we completely characterise transition systems which can be generated by Elementary Net Systems with Inhibitor Arcs executed under the a-posteriori …semantics (ENI_apost). This is achieved by adapting the notion of a step transition system, i.e. one in which arcs are labelled by sets of events executed concurrently. In developing the model, we follow the standard approach in which the relationship between nets and their transition systems is established via the notion of a region. We define, and show consistency of, two behaviour preserving translations between nets and transition systems. We then compare transition systems which are generated by ENI_apost and ENI-systems (called respectively TSENI_apost and TSENI transition systems). Show more

Keywords: causality/partial order theory of concurrency, analysis and synthesis, structure and behaviour of nets, theory of regions, transition systems

Citation: Fundamenta Informaticae, vol. 50, no. 2, pp. 175-203, 2002

Authors: Xia, Fei | Clark, Ian

Article Type: Research Article

Abstract: This paper presents new algorithms for the Signal and Message asynchronous data communication mechanisms (ACMs) and their modelling and analysis using Petri net techniques. This work extends the general knowledge of ACMs, the confidence of designing systems around them and the scope of their potential applications by standard Petri net techniques to model and analyse important properties of the new algorithms. The new algorithms and their proof also demonstrate that implementations of all types of ACMs …can be found, and data communication within heterogeneously timed systems can span the full spectrum of asynchrony between processes. Show more

Keywords:

Citation: Fundamenta Informaticae, vol. 50, no. 2, pp. 205-222, 2002

Authors: Zuberek, W.M.

Article Type: Research Article

Abstract: The performance of modern multiprocessor systems is often limited by the delays of interconnections or long latencies of memory subsystems. Instruction-level multithreading is a technique to tolerate such long latencies by switching from one instruction thread to another and continuing instruction execution concurrently with the long-latency operations. Using timed Petri net models, the paper analyzes performance limitations introduced by different components of distributed-memory multithreaded multiprocessor systems. Simulation results are used to compare …performance improvements obtained by replicating critical components of the system to those obtained using components with better performance characteristics. Show more

Keywords: Instruction-level multithreading, distributed-memory multiprocessor systems, timed Petri nets, performance analysis, performance bottlenecks, event-driven simulation

Citation: Fundamenta Informaticae, vol. 50, no. 2, pp. 223-241, 2002