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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arnold, A., “Rational languages are unambiguous”, Theor. Comp. Sci. 26, 1983 pp. 221–223.
Berstel, J., “Transductions and Context-Free Languages”, Stuttgart, Teubner, 1979.
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.
Büchi, J.R., Landweber, L.H., “Solving sequential conditions by finite-state strategies”, Trans. Amer. Math. Soc. 138, 1969, pp. 295–311.
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.
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.
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.
Church, A., “Logic, arithmetic and automata”, Proc. Intern. Congr. Math. 1962, Almquist and Wiksells, Uppsala, 1963, pp. 21–35.
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.
Eilenberg, S., “Automata, Languages and Machines”, vol A, Academic Press, New York, 1974.
Frougny, C., Sakarovitch, J., “Rational relations with bounded delay”, Rapport d’activité Laboratoire Informatique Théorique et Programmation 90.83, Institut Blaise Pascal, 1990.
Ginsburg, S., Rose, G.F., “A Characterization of machine mappings”, Canadian Journal of Mathematics 18, 1966, pp. 381–388.
Landweber, L.H., “Decision problems for w-automata”, Math. Syst. Theory 3, 1969, pp. 376–384.
Latteux, M., Timmerman, E., “Rational w-transductions”, Laboratoire d’Informatique fondamentale de Lille, Publication n IT 176 90, 1990.
Mc Naughton, R., “Testing and generating infinite sequences by a finite automaton”, Inform. and Control 9, 1966, pp. 521–530.
Moschovakis, Y.N., “Descriptive set theory”, North-Holland, 1980.
Nivat, M., Perrin, D., “Automata on infinite words”, Ecole de Printemps LNCS 192, 1984.
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.
Perrin, D., Pin, J.E., “Mots infinis”, Laboratoire Informatique Théorique et Programmation, LITP 93. 40, 1993.
Staiger, L., “Sequential mappings of w-languages”, Math. Syst. Theory 3, 1987, pp. 376–384.
Thomas, W., 1990, “Automata on infinite objects”, Handbook of Theoretical Computer Science, Vol B, North-Holland, Amsterdam.
Thomas, W., 1994, “On the synthesis of strategies in infinite games”, Institut für Informatik und Praktische Matematik, Christian-AlbrechtsUniversität Kiel.
Trakhtenbrot, B.A., Barzdin, Y.M., “Finite automata”, North-Holland, Amsterdam, 1973.
Vuillemin, J., “On circuits and numbers”, IEEE Trans. on Computers 43:8: 868–27, 79, 1994.
Wagner, K., “On ω-regular sets, Information and control 43, 1979, pp. 123–177.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Tison, Y.P., Simonnet, P. (1997). Combinatorial Criteria Over Graphs of Specification to Decide Synthesis by Sequential Circuits. In: Baron, C., Geffroy, JC., Motet, G. (eds) Embedded System Applications. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-2574-2_8
Download citation
DOI: https://doi.org/10.1007/978-1-4757-2574-2_8
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-5179-3
Online ISBN: 978-1-4757-2574-2
eBook Packages: Springer Book Archive