Synchronized product of linear bounded machines

  • Teodor Knapik
  • Ètienne Payet
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)


This paper introduces a class of graphs associated to linear bounded machines. It is shown that this class is closed, up to observational equivalence, under synchronized product. The first-order theory of these graphs is investegated and shown to be undecidable. The latter result extends to any logic in which the existence of sinks may be stated.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. Arnold. Finite Transition Systems. Prentice Hall Int., 1994.Google Scholar
  2. 2.
    A. Arnold and M. Nivat. Comportements de processus. In Colloque AFCET “Les mathèmatiques de l’Informatique”, pages 35–68, 1982.Google Scholar
  3. 3.
    G. Boudol. Notes of algebraic calculi of processes. In Logics and Models of Concurrent Systems, volume F-13 of NATO ASI series, pages 261–303. 1985.Google Scholar
  4. 4.
    R. Bryant. Binary decision diagrams and beyond: Enabling technologies for formal verification. In Proceedings of the International Conference on Computer Aided Design, ICCAD’95, 1995.Google Scholar
  5. 5.
    D. Caucal. On infinite transition graphs having a decidable monadic second-order theory. In F. M. auf der Heide and B. Monien, editors, 23th International Colloquium on Automata Languages and Programming, LNCS 1099, pages 194–205, 1996.Google Scholar
  6. 6.
    G. Chaitin. A Theory of Program Size Formally Identical to Information Theory. J. Assoc. Compt. Mach., (22):329–340, 1975.zbMATHMathSciNetGoogle Scholar
  7. 7.
    B. Courcelle. The monadic second-order logic of graphs, II: Infinite graphs of bounded width. Mathematical System Theory, 21:187–221, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 997–1072. Elsevier, 1990.Google Scholar
  9. 9.
    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32:137–162, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    T. Knapik. Domains of word-functions and Thue specifications. Technical Report INF/96/11/05/a, IREMIA, Universitè de La Rèunion, 1997.Google Scholar
  11. 11.
    D. Kozen and J. Tiuryn. Logics of programs. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 789–840. Elsevier, 1990.Google Scholar
  12. 12.
    R. P. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.Google Scholar
  13. 13.
    K. McMillan. Symbolic Model Checking. Kluwer, 1993.Google Scholar
  14. 14.
    R. Milner. Calculus of Communicating Systems. LNCS 82. Springer Verlag, 1980.zbMATHGoogle Scholar
  15. 15.
    D. E. Muller and P. E. Schupp. The theory of ends, pushdown automata and second-order logic. Theoretical Comput. Sci., 37:51–75, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    M. Nivat. Sur la synchronisation des processus. Revue technique Thomson-CSF, (11):899–919, 1979.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Teodor Knapik
    • 1
  • Ètienne Payet
    • 1
  1. 1.IREMIA, Universitè de La RèunionSaint Denis Messag. Cedex 9France

Personalised recommendations