# Combinatorial Criteria Over Graphs of Specification to Decide Synthesis by Sequential Circuits

• Y. P. Tison
• P. Simonnet
Chapter

## Abstract

Here we present some algorithms which decide, for a given functional specification, whether the function is continuous and whether the function is sequential. When the specification is synchronous (i.e the graph of the function is realized by a synchronous automata) then these two notions coincide with asynchronous sequential functions with bounded delay. We give an example where Büchi’s synthesis by a synchronous sequential function is not possible, but synthesis by an asynchronous sequential function with bounded delay is possible. When the specification is asynchronous, we present an example of a continuous but not sequential function, and we give a sufficient criterion to prove that a function is not sequential.

## Keywords

Finite Automaton Winning Strategy Sequential Circuit Computation Tree Logic Finite Alphabet
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

1. [1]
Arnold, A., “Rational languages are unambiguous”, Theor. Comp. Sci. 26, 1983 pp. 221–223.Google Scholar
2. [2]
Berstel, J., “Transductions and Context-Free Languages”, Stuttgart, Teubner, 1979.
3. [3]
Büchi, J.R., “On a decision method in restricted second order arithmetic”, in Proc. Int. Congr. Logic, Method. and Philos. of Science ( E. Nagel et al., eds.), Stanford Univ. Press, Stanford, 1962, pp. 1–11.Google Scholar
4. [4]
Büchi, J.R., Landweber, L.H., “Solving sequential conditions by finite-state strategies”, Trans. Amer. Math. Soc. 138, 1969, pp. 295–311.Google Scholar
5. [5]
Burch, J.R., Clarke, E.M., Mc Millan, K.L., Dill, D.L., Hwang, L.J., “Symbolic model checking: 1020 states and beyond”, Informations and Computation 98 (2), 1992, pp. 142–170.
6. [6]
Büttner, W., Winkelmann, K., “Equation solving over 2-adic integers and applications to the specification, verification and synthesis of finite state machines”, 1995, to be published.Google Scholar
7. [7]
Choffrut, C., “Une caractérisation des fonctions séquentielles et des fonctions sous-séquentielles en tant que relations rationnelles”, Theoretical Computer Science 5, 1977, pp. 325–338.
8. [8]
Church, A., “Logic, arithmetic and automata”, Proc. Intern. Congr. Math. 1962, Almquist and Wiksells, Uppsala, 1963, pp. 21–35.Google Scholar
9. [9]
Clarke, E., Grumberg, O., Long, D., “Verification tools for finite-state concurrent systems”, A Decade of Concurrency (J.W. de Bakker et al., eds), Lecture Notes in Computer Science 803, Springer-Verlag, Berlin, 1994, pp. 124–175.Google Scholar
10. [10]
Eilenberg, S., “Automata, Languages and Machines”, vol A, Academic Press, New York, 1974.
11. [11]
Frougny, C., Sakarovitch, J., “Rational relations with bounded delay”, Rapport d’activité Laboratoire Informatique Théorique et Programmation 90.83, Institut Blaise Pascal, 1990.Google Scholar
12. [12]
Ginsburg, S., Rose, G.F., “A Characterization of machine mappings”, Canadian Journal of Mathematics 18, 1966, pp. 381–388.
13. [13]
Landweber, L.H., “Decision problems for w-automata”, Math. Syst. Theory 3, 1969, pp. 376–384.Google Scholar
14. [14]
Latteux, M., Timmerman, E., “Rational w-transductions”, Laboratoire d’Informatique fondamentale de Lille, Publication n IT 176 90, 1990.Google Scholar
15. [15]
Mc Naughton, R., “Testing and generating infinite sequences by a finite automaton”, Inform. and Control 9, 1966, pp. 521–530.
16. [16]
Moschovakis, Y.N., “Descriptive set theory”, North-Holland, 1980.Google Scholar
17. [17]
Nivat, M., Perrin, D., “Automata on infinite words”, Ecole de Printemps LNCS 192, 1984.Google Scholar
18. [18]
Nökel, K., Winkelmann, K., “Controller synthesis and verification: a case study”, C. Lewerentz, Th. Linder, Formal Development of Reactive Systems, Case Study Production Cell, Springer Lecture Notes in Computer Science, 891, Berlin, Heidelberg, 1995.Google Scholar
19. [19]
Perrin, D., Pin, J.E., “Mots infinis”, Laboratoire Informatique Théorique et Programmation, LITP 93. 40, 1993.Google Scholar
20. [20]
Staiger, L., “Sequential mappings of w-languages”, Math. Syst. Theory 3, 1987, pp. 376–384.Google Scholar
21. [21]
Thomas, W., 1990, “Automata on infinite objects”, Handbook of Theoretical Computer Science, Vol B, North-Holland, Amsterdam.Google Scholar
22. [22]
Thomas, W., 1994, “On the synthesis of strategies in infinite games”, Institut für Informatik und Praktische Matematik, Christian-AlbrechtsUniversität Kiel.Google Scholar
23. [23]
Trakhtenbrot, B.A., Barzdin, Y.M., “Finite automata”, North-Holland, Amsterdam, 1973.
24. [24]
Vuillemin, J., “On circuits and numbers”, IEEE Trans. on Computers 43:8: 868–27, 79, 1994.
25. [25]
Wagner, K., “On ω-regular sets, Information and control 43, 1979, pp. 123–177.Google Scholar