۱- Introduction

۲- Basic notions

۳- Structural classification of minimal unsolvable words

۴- Generative nature of minimal unsolvable binary words

۵- Generation-based classification of minimal unsolvable words

۶- Experimental results

۷- Conclusion

References

Abstract

Sets of finite words, as well as some infinite ones, can be described using finite systems, e.g. automata. On the other hand, some automata may be constructed with the use of even more compact systems, like Petri nets. We call such automata Petri net solvable. In this paper we consider the solvability of singleton languages over a binary alphabet (i.e. binary words). An unsolvable (i.e. not solvable) word w is called minimal if each proper factor of w is solvable. We present a complete language-theoretical characterisation of the set of all minimal unsolvable binary words. The characterisation utilises morphic-based transformations which expose the combinatorial structure of those words, and allows to introduce a pattern matching condition for unsolvability.

Introduction

To deal with infinite sets of words we need to specify them in a finite way. Finite automata which are known as a classical model for describing regular languages, are equivalent to finite labelled transition systems [8]. Some sets may be expressed with the use of even more compact system models. In this paper we investigate the synthesis problem with a specification given in the form of labelled transition systems. The sought system model is a place/transition Petri net [11], with its reachability graph as a natural bridge between specification and implementation. Namely, we are concerned with finding a net, whose reachability graph is isomorphic to a given labelled transition system. To address this issue one may use the general approach for net-synthesis suggested by the theory of regions [1]. For a given labelled transition system, the solution of a number of linear inequations systems provided by the theory of regions exists if and only if there exists an implementation in the form of a net. Moreover, solutions of such linear inequations systems are usually utilised during the synthesis of the resulting system (see Synet [4] and APT [12]). Our aim is to initiate a combinatorial approach and to provide a complete characterisation of a generative nature for a special kind of labelled transition systems — non-branching and acyclic transition systems having at most two labels (i.e. binary words) [2]. More precisely, we characterise all minimal unsolvable binary words. The paper is organised as follows. First we give some basic notions and notations concerning labelled transition systems, Petri nets and theory of regions.