Abstract
Given a distributed computation and a predicate, detection of the predicate in \(\mathit{Definitely}\) modality means checking whether in every path from the least state to the greatest state in the state space generated from the computation, there exists a state satisfying the predicate. It is well known that the state space is a lattice. The regular predicate is a class of predicates. All the states satisfying a regular predicate form a sublattice of the lattice. In this paper, we prove that detection of a regular predicate in \(\mathit{Definitely}\) modality is coNP-complete.
Supported by the National Natural Science Foundation of China under Grant Nos. 60721061, 60833001 and 60603049, and the National High Technology Research and Development Program (”863”Program) of China under Grant No. 2007AA01Z112.
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
Chase, C., Garg, V.K.: Efficient detection of restricted classes of global predicates. In: Helary, J.-M., Raynal, M. (eds.) WDAG 1995. LNCS, vol. 972, pp. 303–317. Springer, Heidelberg (1995)
Cooper, R., Marzullo, K.: Consistent detection of global predicates. In: Proceedings of ACM/ONR workshop on Parallel and Distributed Debugging, pp. 163–173 (1991)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
Garg, V.K., Mittal, N.: On slicing a distributed computation. In: Proceedings of IEEE International Conference on Distributed Computing Systems, pp. 322–329 (2001)
Garg, V.K., Waldecker, B.: Detection of weak unstable predicates in distributed programs. IEEE Transactions on Parallel and Distributed Systems 5(3), 299–307 (1994)
Garg, V.K., Waldecker, B.: Detection of strong unstable predicates in distributed programs. IEEE Transactions on Parallel and Distributed Systems 7(12), 1323–1333 (1996)
Hurfin, M., Mizuno, M., Raynal, M., Singhal, M.: Efficient detection of conjunctions of local predicates. IEEE Transactions on Software Engineering 24(8), 664–677 (1998)
Lamport, L.: Time, clocks and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–564 (1978)
Mattern, F.: Virtual time and global states of distributed systems. In: Proceedings of the International Workshop on Parallel and Distributed Algorithms, pp. 120–131 (1989)
Mittal, N., Garg, V.K.: Techniques and applications of computation slicing. Distributed Computing 17(3), 251–277 (2005)
Sen, A., Garg, V.K.: Detecting temporal logic predicates on the happened before model. In: Proceedings of the 16th International Symposium on Parallel and Distributed Processing, pp. 76–83 (2002)
Sen, A., Garg, V.K.: On checking whether a predicate definitely holds. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 15–29. Springer, Heidelberg (2004)
Tarafdar, A., Garg, V.K.: Predicate control for active debugging of distributed programs. In: Proceedings of IEEE 9th Symposium on Parallel and Distributed Processing(SPDP), pp. 763–769 (1998)
Venkatesan, S., Dathan, B.: Test and debugging distributed programs using global predicates. IEEE Transactions on Software Engineering 21(2), 163–177 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huang, H. (2009). On Detecting Regular Predicates in Distributed Systems. In: Liu, Z., Ravn, A.P. (eds) Automated Technology for Verification and Analysis. ATVA 2009. Lecture Notes in Computer Science, vol 5799. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04761-9_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-04761-9_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04760-2
Online ISBN: 978-3-642-04761-9
eBook Packages: Computer ScienceComputer Science (R0)