Fundamenta Informaticae - Volume 88, issue 4

Article Type: Other

Citation: Fundamenta Informaticae, vol. 88, no. 4, pp. i-iii, 2008

Authors: Béal, Frédéric | Yoneda, Tomohiro | Myers, Chris J.

Article Type: Research Article

Abstract: This paper proposes a new approach for the hazard checking of timed asynchronous circuits. Previous papers proposed either exact algorithms, which suffer from state-space explosion, or efficient algorithms which use (conservative) approximations to avoid state-space explosion, but have the drawback of a rather conservative definition of failure states, which results in the rejection of designs which are valid. Algorithms based on [1], extending it to the timed case [7], while being very efficient, are unable to …handle circuits with internal loops, which prevents their use in some cases. We propose a new approach to the problem in order to overcome the mentioned limitations, without sacrificing efficiency. To do so, we first introduce a general framework targeted at the conservative checking of safety failures. This framework is not restricted to the checking of timed asynchronous circuits. Then, we propose a new (conservative) semantics to timed circuits, in order to use the proposed framework for hazard checking of such circuits. Using this framework with the proposed semantics yields an efficient algorithm that solves the limitations of the previous approaches. Show more

Citation: Fundamenta Informaticae, vol. 88, no. 4, pp. 411-435, 2008

Authors: Bergenthum, Robin | Desel, Jörg | Lorenz, Robert | Mauser, Sebastian

Article Type: Research Article

Abstract: In this paper we present two algorithms that effectively synthesize a finite place/transition Petri net (p/t-net) froma finite set of labeled partial orders (a finite partial language). The synthesized p/t-net either has exactly the non-sequential behavior specified by the partial language, or there is no such p/t-net. The first algorithm is based on the theory of token flow regions for partial languages developed by Lorenz and Juhás. Thus, this paper shows the applicability of this …concept. The second algorithm uses the classical theory of regions applied to the set of step sequences generated by the given partial language. We finally develop an algorithm to test whether the net synthesized by either of the two algorithms has exactly the non-sequential behavior specified by the partial language. We implemented all algorithms in our framework VipTool. In this paper, the implementations of the first two algorithms are used to compare the algorithms by means of experimental results. Show more

Citation: Fundamenta Informaticae, vol. 88, no. 4, pp. 437-468, 2008

Authors: Boucheneb, Hanifa | Rakkay, Hind

Article Type: Research Article

Abstract: We consider here time Petri nets (TPN model). We first propose an abstraction to its generally infinite state space which preserves linear properties of the TPN model. Comparing with TPN abstractions proposed in the literature, our abstraction produces graphs which are both smaller and faster to compute. In addition, our characterization of agglomerated states allows a significant gain in space. Afterwards, we show how to apply Yoneda's partial order reduction technique to construct directly …reduced graphs useful to verify LTL_{-X} properties of the model. Using our approach, both time and space complexities are reduced. Finally, we propose a time extension for Büchi automata which is useful to model checking timed linear properties of the model, using the abstraction proposed here. Show more

Keywords: Time Petri nets, state class graph, state explosion problem, partial order techniques, independent transitions, timed linear properties, Interval timed Büchi automata

Citation: Fundamenta Informaticae, vol. 88, no. 4, pp. 469-495, 2008

Authors: Cassez, Franck | Tripakis, Stavros

Article Type: Research Article

Abstract: We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of fixed static observers, where the set of observable events is fixed and does not change during execution of the system. In this paper, we consider static observers where the set …of observable events is not fixed, but needs to be optimized (e.g., minimized in size). We also consider dynamic observers, where the observer can "switch" sensors on or off, thus dynamically changing the set of events it wishes to observe. It is known that checking diagnosability (i.e., whether a given observer is capable of identifying faults) can be solved in polynomial time for static observers, and we show that the same is true for dynamic ones. On the other hand, minimizing the number of (static) observable events required to achieve diagnosability is NP-complete. We show that this is true also in the case of mask-based observation, where some events are observable but not distinguishable. For dynamic observers' synthesis, we prove that amost permissive finite-state observer can be computed in doubly exponential time, using a game-theoretic approach. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer. We show how to compute an optimal observer using results on mean-payoff games by Zwick and Paterson. Show more

Citation: Fundamenta Informaticae, vol. 88, no. 4, pp. 497-540, 2008

Authors: Khomenko, Victor | Schaefer, Mark | Vogler, Walter

Article Type: Research Article

Abstract: Signal Transition Graphs (STG) are a formalism for the description of asynchronous circuit behaviour. In this paper we propose (and justify) a formal semantics of non-deterministic STGs with dummies and OR-causality. For this, we introduce the concept of output-determinacy, which is a relaxation of determinism, and argue that it is reasonable and useful in the speed-independent context. We apply the developed theory to improve an STG decomposition algorithm used to tackle the state explosion problem …during circuit synthesis, and present some experimental data for this improved algorithm and some benchmark examples. Show more

Keywords: output-determinacy, decomposition, STG, asynchronous circuits, OR-causality

Citation: Fundamenta Informaticae, vol. 88, no. 4, pp. 541-579, 2008

Authors: Sokolov, Danil | Poliakov, Ivan | Yakovlev, Alex

Article Type: Research Article

Abstract: A token-based model for asynchronous data path, called static data flow structures (SDFS), is formally defined. Three token game semantics are introduced for this model, namely atomic token, spread token and counterflow. The SDFS semantics are analysed using a simple benchmark example; their advantages and drawbacks are highlighted. A combination of spread token and counterflow models, which employs the advantages of both, is presented. A technique is described for mapping the high-level SDFS token game semantics …into the low level of underlying Petri nets (PNs). The PNs are employed as a back-end for verification of SDFS models. For analysis and comparison of SDFS semantics a software tool has been developed, which integrates all SDFS semantics into a consistent framework, implements their conversion into PNs and provides an interface to existing model checking tools. Show more

Citation: Fundamenta Informaticae, vol. 88, no. 4, pp. 581-610, 2008