Abstract
In this paper we analyze a particular sequence of points in the poset of nonnegative lattice points in n-dimensions. For this sequence, in 2-dimensions, we obtain optimal upper bounds on the number of points to be selected in order to ensure desired chain lengths among selected points; for higher dimensions, the upper bounds obtained are not optimal [6]. We use these bounds to decide full weak safety for a simple resource-oriented model for concurrent systems ([5, 12]). In this model, processes execute a sequence of operations (a program) which are controlled by a finite state device called the synchronizer. Concurrency among processes is modeled as an interleaving of their operations. A concurrent system consisting of a synchronizer and infinitely many identical processes is full weak safe if and only if all valid interleavings (of any finite number of processes) are accepted by the synchronizer. To decide full weak safety, we use our chain length result to give an effective procedure to obtain a threshold τ, such that the model is full weak safe if and only if all interleavings of operations length τ or less are accepted by the synchronizer.
Preview
Unable to display preview. Download preview PDF.
References
A. Valmari. A Stubborn Attack On State Explosion. Computer Aided Verification, 1990.
E. M. Clarke, Emerson, and Sistla. Automatic Verification Of Finite-state Concurrent Systems Using Temporal Logic Specifications. 10th ACM Symposium on Principles of Programming Languages, 1983.
E. M. Clarke, O. Grumberg, and M. C. Browne. Reasoning About Networks With Many Identical Finite State Processes. Proc. 5th ACM Symposium on Principles of Distributed Computing, August 1986.
Gischer Jay. Shuffle Languages, Petri Nets, And Context-Sensitive Languages. Communications of the ACM, September 1981.
K. Ramamritham. Synthesizing Code For Resource Controllers. IEEE Transactions on Software Engg, August 1985.
Mahesh Girkar and Robert Moll. Bounds On Chain Lengths For Collections Of Non-negative Points In n-space. CS Technical Report 92-31, Dept. of Computer Science, Univ. of Massachussetts, April 1992.
Mahesh Girkar and Robert Moll. Stability Analysis of Concurrent Systems with an Indefinite Number of Processes. CS Technical Report 92-72, Dept. of Computer Science, Univ. of Massachussetts, November 1992.
R. P. Kurshan. Modelling Concurrent Programs. Symp. on Applied Mathematics, 1985.
S. German and A. P. Sistla. Reasoning With Many Processes. Proc. Symp. on Logic in Computer Science, June 1987.
S. German and A. P. Sistla. Reasoning About Systems With Many Processes. JACM, July 1992.
S. Rao. Kosaraju. Decidability Of Reachability In Vector Addition Systems. Proceedings of the 16th ACM Symposium on Theory of Computing, May 1982.
Ugo Buy and Robert Moll. Analysis And Synthesis Of Inter-process Communication Code. To appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Girkar, M., Moll, R. (1993). Vector sequence analysis and full weak safety for concurrent systems. In: Ésik, Z. (eds) Fundamentals of Computation Theory. FCT 1993. Lecture Notes in Computer Science, vol 710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57163-9_21
Download citation
DOI: https://doi.org/10.1007/3-540-57163-9_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57163-6
Online ISBN: 978-3-540-47923-9
eBook Packages: Springer Book Archive