Fundamenta Informaticae - Volume 108, issue 1-2

Authors: Edwards, Stephen A. | Janicki, Ryszard | Vogler, Walter

Article Type: Other

DOI: 10.3233/FI-2011-410

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. v-vii, 2011

Authors: Carmona, Josep | Júlvez, Jorge | Cortadella, Jordi | Kishinevsky, Michael

Article Type: Research Article

Abstract: With the scaling of process technologies, communication delays represent a bottleneck for the performance of circuits. One of the main issues that has to be handled is the variability of such delays. Latency-insensitive circuits offer a form of elasticity that tolerates variations in those delays. This flexibility usually requires the addition of a control layer that synchronizes the flow of information. This paper proposes a method for eliminating the complexity of the control layer, replacing it by a set of iterative schedulers that decide when to activate computations. Unlike previous approaches, this can be achieved with low complexity algorithms and …without extra circuitry. Show more

DOI: 10.3233/FI-2011-411

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. 1-21, 2011

Authors: Crafa, Silvia | Ranzato, Francesco | Tapparo, Francesco

Article Type: Research Article

Abstract: A number of algorithms for computing the simulation preorder on Kripke structures and on labelled transition systems are available. Among them, the algorithm by Ranzato and Tapparo [2007] has the best time complexity,while the algorithm by Gentilini et al. [2003] – successively corrected by van Glabbeek and Ploeger [2008] – has the best space complexity. Both space and time complexities are critical issues in a simulation algorithm, in particular memory requirements are crucial in the context of model checking when dealing with large state spaces. Here, we propose a new simulation algorithm that is obtained as a space saving modification …of the time efficient algorithm by Ranzato and Tapparo: a symbolic representation of sets is embedded in this algorithm so that any set of states manipulated by the algorithm can be efficiently stored as a set of blocks of a suitable state partition. It turns out that this novel simulation algorithm has a space complexity comparable with Gentilini et al.'s algorithm while improving on Gentilini et al.'s time bound. Show more

Keywords: Simulation preorder, simulation algorithm, coarsest partition problem

DOI: 10.3233/FI-2011-412

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. 23-42, 2011

Authors: Lohmann, Niels | Wolf, Karsten

Article Type: Research Article

Abstract: Operating guidelines characterize correct interaction (e. g., deadlock freedom) with a service. They can be stored in a service registry. They are typically represented as an annotated transition system where the annotations are Boolean formulae attached to the states. The core result of this article is to propose an alternative representation of operating guidelines where, instead of a Boolean formula, only a few bits need to be stored with a state. This way, we safe one order of magnitude in the space complexity of the representation. Moreover, we demonstrate that the new representation yields efficiency gains in several algorithms which …involve operating guidelines. Finally we show that the new representation permits the translation of the transition system representing the operating guidelines into a Petri net which typically yields further gains concerning the space for storing operating guidelines. Show more

DOI: 10.3233/FI-2011-413

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. 43-62, 2011

Authors: Mokhov, Andrey | Khomenko, Victor | Yakovlev, Alex

Article Type: Research Article

Abstract: A new way of constructing N-way arbiters is proposed. The main idea is to perform arbitrations between all pairs of requests, and then make decision on what grant to issue based on their outcomes. Crucially, all the mutual exclusion elements in such an arbiter work in parallel. This ‘flat’ arbitration is prone to new threats such as formation of cycles (leading to deadlocks), but at the same time opens up new opportunities for designing arbitration structures with different decision policies due to the availability of the global order relation between requests. To facilitate resolution of such cycles and further developments …in the context of flat arbitration, the paper presents new theoretical results, including a proof of correctness of a generic structure for the N-way arbiter decision logic. In particular, in some situations a request that lost some pairwise arbitrations has to be granted to avoid a deadlock. Show more

Keywords: Arbiters, Speed-independent circuits, Asynchronous circuits, Signal Transition Graph (STG)

DOI: 10.3233/FI-2011-414

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. 63-90, 2011

Authors: Potop-Butucaru, Dumitru | Sorel, Yves | de Simone, Robert | Talpin, Jean-Pierre

Article Type: Research Article

Abstract: We propose a general method to characterize and synthesize correctness-preserving asynchronous wrappers for synchronous processes on a globally asynchronous locally synchronous (GALS) architecture. While a synchronous process may rely on the absence of a signal to trigger a reaction, sensing absence in an asynchronous environment may be unfeasible due to uncontrolled communication latencies. A simple and common solution is to systematically encode and send absence notifications, but it is unduly expensive at run-time. Instead, our approach is based on the theory of weakly endochronous systems, which defines the largest sub-class of synchronous systems where (possibly concurrent) asynchronous evaluation is faithful …to the original (synchronous) specification. Our method considers synchronous processes or modules that are specified by synchronization constraints expressed in a high-level multi-clock synchronous reactive formalism. The algorithm uses a compact representation of the abstract synchronization configurations of the analyzed process and determines a minimal set of synchronization patterns generating by union all its possible reactions. A specification is weakly endochronous if and only if these generators do not need explicit absence information. In this case, the set of generators can directly be used to synthesize the concurrent asynchronous multi-rate wrapper of the process. Show more

Keywords: endochrony, synchrony, multi-clock, asynchronous implementation

DOI: 10.3233/FI-2011-415

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. 91-118, 2011

Authors: Raclet, Jean-Baptiste | Badouel, Eric | Benveniste, Albert | Caillaud, Benoît | Legay, Axel | Passerone, Roberto

Article Type: Research Article

Abstract: This paper presents the modal interface theory, a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows the designer to express assumptions on the environment and which uses an optimistic view of composition: two components can be composed if there is an environment where they can work together. Modal specifications are a language theoretic account of a fragment of the modal mu-calculus logic with a rich composition algebra which meets certain methodological requirements but which does not allow the environment and the component to be distinguished. The …present paper contributes a more thorough unification of the two theories by correcting a first attempt in this direction by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing the comparison between interface automata, modal automata and modal interfaces even further. The work reported here is based on earlier work presented in [41] and [42]. Show more

Keywords: Component-based System, Compositional Reasoning, Interface Theory, Interface Automata, Modal Specifications

DOI: 10.3233/FI-2011-416

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. 119-149, 2011

Authors: Wolf, Karsten | Stahl, Christian | Weinberg, Daniela | Ott, Janine | Danitz, Robert

Article Type: Research Article

Abstract: A big issue in the paradigm of Service Oriented Architectures (SOA) is service discovery. Organizations publish their services via the Internet. These published services can then be automatically found and accessed by other services, meaning, the services are composed. A fundamental property of a service composition is weak termination, which guarantees the absence of deadlocks and livelocks. In principle, weak termination can be verified by inspecting the state space of the composition of (public views of) the involved services. We propose a methodology to build that state space from precomputed fragments, which are computed upon publishing a service. That way, …we shift computation effort from the resource critical “find” phase to the less critical “publish” phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions. We further show the positive impact of our approach to the computational effort of service discovery. Show more

Keywords: deadlock- and livelock freedom, SOA, service discovery, state space reduction

DOI: 10.3233/FI-2011-417

Citation: Fundamenta Informaticae, vol. 108, no. 1-2, pp. 151-180, 2011