Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
A. Arnold. Finite Transition Systems. Prentice Hall Int., 1994.
A. Arnold and M. Nivat. Comportements de processus. In Colloque AFCET “Les mathèmatiques de l’Informatique”, pages 35–68, 1982.
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.
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.
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.
G. Chaitin. A Theory of Program Size Formally Identical to Information Theory. J. Assoc. Compt. Mach., (22):329–340, 1975.
B. Courcelle. The monadic second-order logic of graphs, II: Infinite graphs of bounded width. Mathematical System Theory, 21:187–221, 1989.
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.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32:137–162, 1985.
T. Knapik. Domains of word-functions and Thue specifications. Technical Report INF/96/11/05/a, IREMIA, Universitè de La Rèunion, 1997.
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.
R. P. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.
K. McMillan. Symbolic Model Checking. Kluwer, 1993.
R. Milner. Calculus of Communicating Systems. LNCS 82. Springer Verlag, 1980.
D. E. Muller and P. E. Schupp. The theory of ends, pushdown automata and second-order logic. Theoretical Comput. Sci., 37:51–75, 1985.
M. Nivat. Sur la synchronisation des processus. Revue technique Thomson-CSF, (11):899–919, 1979.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Knapik, T., Payet, È. (1999). Synchronized product of linear bounded machines. In: Ciobanu, G., Păun, G. (eds) Fundamentals of Computation Theory. FCT 1999. Lecture Notes in Computer Science, vol 1684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48321-7_30
Download citation
DOI: https://doi.org/10.1007/3-540-48321-7_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66412-3
Online ISBN: 978-3-540-48321-2
eBook Packages: Springer Book Archive