سیستم های انتقال انتزاعی : برنامه ای برای ماشین آلات خودکار FIFO

Formal methods based on symbolic representations have been found to be very effective. In the case of infinite state systems, there has been a great deal of interest in accelerations—a technique for characterizing the result of iterating an execution sequence an arbitrary number of times, in a sound, but not necessarily complete, way. We propose the use of abstractions as a general framework to design accelerations. We investigate SemiLinear Regular Expressions (SLREs) as symbolic representations for FIFO automata. In particular, we show that: (a) SLREs are easy to manipulate, (b) SLREs form the core of known FIFO symbolic representations, and (c) SLREs are sufficient to represent the effect of arbitrary iterations of a loop for FIFO automata with one channel.

Formal methods are now routinely applied in design and implementation of finite state systems, such as those that occur in VLSI circuits. It has also been applied fairly regularly in the design and implementation of network protocols. Based on the success of formal methods in reasoning about finite state systems [9] there has been a great deal of interest in reasoning about infinite state systems. Given that programs, as well as network protocols, are infinite state in nature there is a need for automatic techniques to extend the reach of formal methods to a much larger class. Infinite state systems could, in general, be Turing-powerful. Consequently, in reasoning about any non-trivial property of such systems we will have to contend with incompleteness. At least two approaches have been considered in the literature: (a) semi-computation of the set of reachable states [1], [4], [5] and [26], and (b) computation of a superset of reachability set [14] and [32]. A requirement common to both approaches is that an infinite set of reachable states (from some given initial state) be finitely described. Clearly, the finite description should be such that it admits questions of membership and emptiness to be answered effectively. However, given that the reachability set is explored in an iterative fashion, an even more important question is “how does one infer the existence of an infinite set of states in the reachability set? And how does one calculate it?” Techniques called accelerations or meta-transitions have been discussed in the literature [1], [4], [5], [10], [12] and [20]. We focus in this paper on symbolic representations for the computation of the reachability set of FIFO automata—a finite control with multiple unbounded FIFO channels. To the best of our knowledge, Pachl uses for the first time regular expressions to represent infinite sets of channel contents [31]. In [17], linear regular expressions have been defined and used. Boigelot et al. chose a deterministic finite automata based representation, namely Queue-content Decision Diagrams[4] and afterwards Bouajjani et al. added Pressburger formulas, namely Constrained QDDs[5]. Simple regular expressions have been introduced for lossy FIFO automata [1]. We propose to address the issue “what are symbolic representations?” In this paper, we show how symbolic representations and accelerations can be couched in terms of abstract interpretation [14], a powerful semantics-based technique for explaining data flow analysis. We present a generic algorithm which, given an abstraction of a labelled transition system and an acceleration, computes a symbolic tree. We illustrate the usefulness of this approach by exploring Linear and SemiLinear Regular Expressions (LREs and SLREs) as symbolic representations for FIFO automata. In particular, we show the following about SLREs: • SLREs are easy to manipulate: indeed, SLREs are exactly regular languages of polynomial density[35]. This class enjoys good complexity properties. In particular, we prove that inclusion between two SLREs is in NP∩coNP. • SLREs form the core of known FIFO symbolic representations: more formally, a set of queue contents is SLRE representable iff it is both CQDD representable and QDD representable (SLREs=QDDs∩CQDDs), • SLREs are usually sufficient since for FIFO automata with one channel, an arbitrary iteration of a loop is SLRE representable. Moreover, several examples in the literature have a SLRE representable reachability set: the alternating bit protocol [31], the bounded retransmission protocol of Philips [1], the producer/consumer described in [4] and the connection/deconnection protocol [28]. We say that a labelled transition system is flat when its set of traces is included in a SLRE language. We give an algorithm which computes an exact symbolic reachability set of any flat labelled transition system whose abstraction has a sound and complete acceleration. The road map for the paper is as follows: in Section 2 we introduce labelled transition systems, in Section 3 we discuss FIFO automata and symbolic representations based on SLREs. In Section 4 we rephrase the notions of symbolic representations and accelerations in the framework of abstractions. In Section 5 we discuss accelerations based on SLREs. Finally, in Section 6 we compare QDDs, CQDDs, and SLREs.

The goal of this paper was to give a general setting for the fast computation of post* (and pre* by duality). The contributions of the paper are two fold: the investigation of SLREs as a symbolic representation, and the use of abstractions as a uniform mechanism for explaining symbolic representations and accelerations. In particular, we have been able to investigate the relation between SLREs and other formalisms such as QDDs and CQDDs. The two algorithms defined in Section 4 become implementable when the abstract inclusion ⊑ is decidable, and when the three total functions View the MathML source, ⊔ and ∇ are computable. This is the case for the View the MathML source based abstraction (and also for the View the MathML source and View the MathML source based abstractions), hence our abstraction View the MathML source and its two associated accelerations View the MathML source are effective. Pressburger formulas are usually used to symbolically represent counter values. Comon et al. showed in [12] that the effect of arbitrary iteration of a loop in a multiple counters automaton can be described by a Pressburger formula. Thus, an abstraction based on Pressburger formulas, along with a sound and complete acceleration can be defined for multiple counters automata. Our general abstraction and acceleration framework can also capture the notions of well structured transition systems [2], [15], [16] and [19]. In [15] and [16], an acceleration is defined by means of limits (or lubs) in order to compute a finite coverability tree. No acceleration is used in [2] and [19] since the abstract domain satisfies the ascending chain condition. We expect that these notions would carry over to accelerations of parametrized systems [6] and to combinations of symbolic representations—topics we propose to consider in the near future.